ambr maxAux maxAdd1

cicada-lang · Jan 7, 2025 · d4c4abd · d4c4abd
1 parent cad7cf9
commit d4c4abd
Show file tree

Hide file tree

Showing 4 changed files with 175 additions and 163 deletions.
diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md
@@ -577,20 +577,20 @@ But because of single-principal-port constraint,
 we have to introduce an auxiliary node and some auxiliary rules,
 to explicitly choose between two interactable edges.
 
-We call the auxiliary node `(maxAux)`.
+We call the auxiliary node `(maxAdd1)`.
 
 ```
      result
        |
-    (maxAux)
+    (maxAdd1)
      /    \
 first    second!
 ```
 
 Node definition:
 
 ```
-node maxAux
+node maxAdd1
   Nat :first
   Nat :second!
   --------
@@ -604,7 +604,7 @@ the rule between `(add1)` and `(max)`:
 ```
      result            result
        |                 |
-     (max)      =>    (maxAux)
+     (max)      =>    (maxAdd1)
      /    \            /   \
 (add1)   second     prev   second
    |
@@ -616,36 +616,36 @@ Rule definition:
 ```
 rule add1 max
   (max)-second
-  (add1)-prev maxAux
+  (add1)-prev maxAdd1
   result-(max)
 end
 ```
 
-The rule between `(zero)` and `(maxAux)`:
+The rule between `(zero)` and `(maxAdd1)`:
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (zero)        first
 ```
 
 Rule definition:
 
 ```
-rule zero maxAux
-  (maxAux)-first add1
-  result-(maxAux)
+rule zero maxAdd1
+  (maxAdd1)-first add1
+  result-(maxAdd1)
 end
 ```
 
-The rule between `(add1)` and `(maxAux)`:
+The rule between `(add1)` and `(maxAdd1)`:
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (add1)        (max)
            |           /   \
@@ -655,10 +655,10 @@ The rule between `(add1)` and `(maxAux)`:
 Rule definition:
 
 ```
-rule add1 maxAux
+rule add1 maxAdd1
   (add1)-prev
-  (maxAux)-first max
-  add1 result-(maxAux)
+  (maxAdd1)-first max
+  add1 result-(maxAdd1)
 end
 ```
 
@@ -676,7 +676,7 @@ node add1
   Nat :value!
 end
 
-node maxAux
+node maxAdd1
   Nat :first
   Nat :second!
   --------
@@ -695,18 +695,18 @@ rule zero max
 end
 
 rule add1 max
-  (max)-second (add1)-prev maxAux
+  (max)-second (add1)-prev maxAdd1
   result-(max)
 end
 
-rule zero maxAux
-  (maxAux)-first add1
-  result-(maxAux)
+rule zero maxAdd1
+  (maxAdd1)-first add1
+  result-(maxAdd1)
 end
 
-rule add1 maxAux
-  (add1)-prev (maxAux)-first max
-  add1 result-(maxAux)
+rule add1 maxAdd1
+  (add1)-prev (maxAdd1)-first max
+  add1 result-(maxAdd1)
 end
 
 claim one -- Nat end

diff --git a/docs/articles/反应网编程.md b/docs/articles/反应网编程.md
@@ -556,21 +556,20 @@ end
 我们不得不增加一个辅助节点以及相关的规则，
 来明显地在两个可反应的边中做出选择。
 
-我们称辅助节点为 `(maxAux)`，
-其中 `aux` 是 auxiliary 的所写。
+我们称辅助节点为 `(maxAdd1)`。
 
 ```
      result
        |
-    (maxAux)
+    (maxAdd1)
      /    \
 first    second!
 ```
 
 定义如下：
 
 ```
-node maxAux
+node maxAdd1
   Nat :first
   Nat :second!
   --------
@@ -583,7 +582,7 @@ end
 ```
      result            result
        |                 |
-     (max)      =>    (maxAux)
+     (max)      =>    (maxAdd1)
      /    \            /   \
 (add1)   second     prev   second
    |
@@ -595,36 +594,36 @@ end
 ```
 rule add1 max
   (max)-second
-  (add1)-prev maxAux
+  (add1)-prev maxAdd1
   result-(max)
 end
 ```
 
-`(zero)` 与 `(maxAux)` 之间的规则：
+`(zero)` 与 `(maxAdd1)` 之间的规则：
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (zero)        first
 ```
 
 定义如下：
 
 ```
-rule zero maxAux
-  (maxAux)-first add1
-  result-(maxAux)
+rule zero maxAdd1
+  (maxAdd1)-first add1
+  result-(maxAdd1)
 end
 ```
 
-`(add1)` 与 `(maxAux)` 之间的规则：
+`(add1)` 与 `(maxAdd1)` 之间的规则：
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (add1)        (max)
            |           /   \
@@ -634,10 +633,10 @@ end
 定义如下：
 
 ```
-rule add1 maxAux
+rule add1 maxAdd1
   (add1)-prev
-  (maxAux)-first max
-  add1 result-(maxAux)
+  (maxAdd1)-first max
+  add1 result-(maxAdd1)
 end
 ```
 
@@ -655,7 +654,7 @@ node add1
   Nat :value!
 end
 
-node maxAux
+node maxAdd1
   Nat :first
   Nat :second!
   --------
@@ -674,18 +673,18 @@ rule zero max
 end
 
 rule add1 max
-  (max)-second (add1)-prev maxAux
+  (max)-second (add1)-prev maxAdd1
   result-(max)
 end
 
-rule zero maxAux
-  (maxAux)-first add1
-  result-(maxAux)
+rule zero maxAdd1
+  (maxAdd1)-first add1
+  result-(maxAdd1)
 end
 
-rule add1 maxAux
-  (add1)-prev (maxAux)-first max
-  add1 result-(maxAux)
+rule add1 maxAdd1
+  (add1)-prev (maxAdd1)-first max
+  add1 result-(maxAdd1)
 end
 
 claim one -- Nat end

diff --git a/examples/datatypes/Nat.i b/examples/datatypes/Nat.i
@@ -91,9 +91,9 @@ rule add1 mul
   result-(mul)
 end
 
-// To define `max`, we need `maxAux`.
+// To define `max`, we need `maxAdd1`.
 
-node maxAux
+node maxAdd1
   Nat :first
   Nat :second!
   --------
@@ -112,16 +112,16 @@ rule zero max
 end
 
 rule add1 max
-  (max)-second (add1)-prev maxAux
+  (max)-second (add1)-prev maxAdd1
   result-(max)
 end
 
-rule zero maxAux
-  (maxAux)-first add1
-  result-(maxAux)
+rule zero maxAdd1
+  (maxAdd1)-first add1
+  result-(maxAdd1)
 end
 
-rule add1 maxAux
-  (add1)-prev (maxAux)-first max
-  add1 result-(maxAux)
+rule add1 maxAdd1
+  (add1)-prev (maxAdd1)-first max
+  add1 result-(maxAdd1)
 end