added targeted rotation simproc

Author: akissinger

simprocs/basic_simp.ML

@@ -1,3 +1,5 @@
+(* normalises w.r.t. to the terminating/confluent fragment of the ZX-calculus,
+ * see e.g. http://www.cs.ox.ac.uk/people/bob.coecke/Aleks.pdf *)
 open RG_SimpUtil
 
 
@@ -22,3 +24,5 @@ register_simproc ("basic_simp", REDUCE_ALL simps);
 
 
 
+
+

simprocs/rotate_simp.ML

@@ -1,3 +1,5 @@
+(* naive simproc using the "rotate" rule to reduce to pseudo-normal form
+ * for phase-free graphs *)
 open RG_SimpUtil
 
 val rotate = load_rule "theorems/rotate";
@@ -33,3 +35,4 @@ register_simproc ("rotate_simp", simproc);
 
 
 
+

simprocs/rotate_targeted.ML

@@ -0,0 +1,40 @@
+(* improved simproc using the rotate rule to reduce to pseudo-normal form
+ * for phase-free graphs *)
+open RG_SimpUtil
+
+val rotate = load_rule "theorems/rotate_targeted";
+val green_ids = load_rule "theorems/green_id_on_red";
+val green_elim = load_rule "theorems/green_elim";
+val green_scalar = load_rule "axioms/green_scalar";
+val simps = load_ruleset [
+  "axioms/red_copy", "axioms/red_sp", "axioms/green_sp", "axioms/hopf",
+  "axioms/red_scalar", "axioms/green_scalar", "axioms/green_id",
+  "axioms/red_id", "axioms/red_loop", "axioms/green_loop"];
+
+val targetf = min_arity_vertex_where is_interior_green
+fun target_arity g = case targetf g of SOME v => arity g v | NONE => 0
+fun target_with_arity a = vertex_where (fn g => fn v =>
+  is_interior_green g v andalso arity g v = a)
+
+val simproc = (
+  REDUCE_ALL simps ++
+  REDUCE_METRIC_TO 0 num_boundary_red green_ids ++
+  LOOP (
+    LOOP_WHILE (fn g => target_arity g >= 2)
+      (REWRITE_TARGETED { PATTERN = const_vertex "v10", 
+                          TARGET  = targetf } rotate) ++
+    LOOP (
+      REWRITE_TARGETED { PATTERN = const_vertex "v10", 
+                         TARGET  = target_with_arity 1 } green_elim ++
+      REDUCE green_scalar)
+  ) ++
+  REDUCE_ALL simps
+);
+
+register_simproc ("rotate_targeted", simproc);
+
+
+
+
+
+

theorems/green_elim.qrule

@@ -1 +1 @@
-{"lhs":{"bang_boxes":{"bx0":{"contents":["b0","v0"]},"bx1":{"contents":["b0"],"parent":"bx0"}},"wire_vertices":{"b0":{"annotation":{"boundary":true,"coord":[0.0,-2.0]}}},"node_vertices":{"v0":{"annotation":{"coord":[0.0,-0.5]}},"v1":{"annotation":{"coord":[0.0,3.0]}},"v2":{"data":{"type":"X","value":""},"annotation":{"coord":[0.0,1.5]}}},"undir_edges":{"e0":{"src":"v1","tgt":"v2"},"e1":{"src":"v2","tgt":"v0"},"e2":{"src":"v0","tgt":"b0"}}},"rhs":{"bang_boxes":{"bx0":{"contents":["b0","v4"]},"bx1":{"contents":["b0"],"parent":"bx0"}},"wire_vertices":{"b0":{"annotation":{"boundary":true,"coord":[0.0,-2.0]}}},"node_vertices":{"v4":{"annotation":{"coord":[-0.0030441242608455848,-0.8107430454299842]}}},"undir_edges":{"e4":{"src":"v4","tgt":"b0"}}},"derivation":"derivations/green_elim"}
+{"lhs":{"bang_boxes":{"bx0":{"contents":["b0","v0"]},"bx1":{"contents":["b0"],"parent":"bx0"}},"wire_vertices":{"b0":{"annotation":{"boundary":true,"coord":[-0.02,-1.69]}}},"node_vertices":{"v10":{"annotation":{"coord":[0.0,3.25]}},"v0":{"annotation":{"coord":[0.0,-0.57]}},"v2":{"data":{"type":"X","value":""},"annotation":{"coord":[0.02,1.41]}}},"undir_edges":{"e1":{"src":"v2","tgt":"v0"},"e2":{"src":"v0","tgt":"b0"},"e3":{"src":"v2","tgt":"v10"}}},"rhs":{"bang_boxes":{"bx0":{"contents":["b0","v0"]},"bx1":{"contents":["b0"],"parent":"bx0"}},"wire_vertices":{"b0":{"annotation":{"boundary":true,"coord":[0.02,-1.81]}}},"node_vertices":{"v0":{"annotation":{"coord":[0.0,-0.71]}}},"undir_edges":{"e0":{"src":"v0","tgt":"b0"}}}}

theorems/rotate_targeted.qrule

@@ -0,0 +1 @@
+{"lhs":{"bang_boxes":{"bx5":{"contents":["b2"],"parent":"bx2"},"bx0":{"contents":["b0","v0"]},"bx6":{"contents":["b3"]},"bx4":{"contents":["b1"],"parent":"bx1"},"bx3":{"contents":["b0"],"parent":"bx0"},"bx1":{"contents":["b1","v1"]},"bx2":{"contents":["b2","v2"]}},"wire_vertices":{"b1":{"annotation":{"boundary":true,"coord":[-2.25,-3.0]}},"b0":{"annotation":{"boundary":true,"coord":[0.0,4.25]}},"b2":{"annotation":{"boundary":true,"coord":[2.25,-2.75]}},"b3":{"annotation":{"boundary":true,"coord":[-2.5,4.25]}}},"node_vertices":{"v2":{"annotation":{"coord":[2.0,-1.75]}},"v5":{"data":{"type":"X","value":""},"annotation":{"coord":[1.0,0.25]}},"v1":{"annotation":{"coord":[-1.75,-1.5]}},"v4":{"data":{"type":"X","value":""},"annotation":{"coord":[-1.0,0.25]}},"v0":{"annotation":{"coord":[0.0,2.5]}},"v10":{"annotation":{"coord":[-2.5,2.5]}}},"undir_edges":{"e6":{"src":"v1","tgt":"b1"},"e1":{"src":"v0","tgt":"v4"},"e5":{"src":"v2","tgt":"b2"},"e7":{"src":"v4","tgt":"v10"},"e0":{"src":"b0","tgt":"v0"},"e4":{"src":"v5","tgt":"v2"},"e8":{"src":"v5","tgt":"v10"},"e3":{"src":"v0","tgt":"v5"},"e9":{"src":"v10","tgt":"b3"},"e2":{"src":"v4","tgt":"v1"}}},"rhs":{"bang_boxes":{"bx5":{"contents":["b2"],"parent":"bx2"},"bx0":{"contents":["b0","v1"]},"bx6":{"contents":["b3"]},"bx4":{"contents":["b1"],"parent":"bx1"},"bx3":{"contents":["b0"],"parent":"bx0"},"bx1":{"contents":["b1","v0"]},"bx2":{"contents":["b2","v2"]}},"wire_vertices":{"b1":{"annotation":{"boundary":true,"coord":[-1.75,-2.75]}},"b0":{"annotation":{"boundary":true,"coord":[0.0,3.0]}},"b2":{"annotation":{"boundary":true,"coord":[1.5,-2.5]}},"b3":{"annotation":{"boundary":true,"coord":[-2.0,3.25]}}},"node_vertices":{"v2":{"annotation":{"coord":[1.25,-1.0]}},"v1":{"annotation":{"coord":[-0.0,1.75]}},"v4":{"data":{"type":"X","value":""},"annotation":{"coord":[0.75,0.25]}},"v0":{"annotation":{"coord":[-1.5,-1.0]}},"v3":{"data":{"type":"X","value":""},"annotation":{"coord":[-0.25,-1.0]}},"v10":{"annotation":{"coord":[-2.0,1.75]}}},"undir_edges":{"e6":{"src":"v3","tgt":"v2"},"e1":{"src":"v1","tgt":"v4"},"e5":{"src":"v0","tgt":"v3"},"e7":{"src":"v4","tgt":"v10"},"e0":{"src":"b0","tgt":"v1"},"e4":{"src":"v0","tgt":"b1"},"e8":{"src":"v10","tgt":"b3"},"e3":{"src":"v2","tgt":"b2"},"e2":{"src":"v4","tgt":"v2"}}}}