ambr maxAux maxAdd1

cicada-lang · Jan 7, 2025 · 29ccf37 · 29ccf37
1 parent 0fbecc2
commit 29ccf37
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 36 deletions.
diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md
@@ -505,20 +505,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(
   first: Nat,
   second!: Nat
   --------
@@ -532,7 +532,7 @@ the rule between `(max)` and `(add1)`:
 ```
      result            result
        |                 |
-     (max)      =>    (maxAux)
+     (max)      =>    (maxAdd1)
      /    \            /   \
 (add1)   second     prev   second
    |
@@ -543,34 +543,34 @@ Rule definition:
 
 ```
 rule max(first!, second, result) add1(prev, value!) {
-  maxAux(prev, second, result)
+  maxAdd1(prev, second, result)
 }
 ```
 
-The rule between `(maxAux)` and `(zero)`:
+The rule between `(maxAdd1)` and `(zero)`:
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (zero)        first
 ```
 
 Rule definition:
 
 ```
-rule maxAux(first, second!, result) zero(value!) {
+rule maxAdd1(first, second!, result) zero(value!) {
   add1(first, result)
 }
 ```
 
-The rule between `(maxAux)` and `(add1)`:
+The rule between `(maxAdd1)` and `(add1)`:
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (add1)        (max)
            |           /   \
@@ -580,7 +580,7 @@ The rule between `(maxAux)` and `(add1)`:
 Rule definition:
 
 ```
-rule maxAux(first, second!, result) add1(prev, value!) {
+rule maxAdd1(first, second!, result) add1(prev, value!) {
   add1(max(first, prev), result)
 }
 ```
@@ -601,7 +601,7 @@ node add1(
   value!: Nat
 )
 
-node maxAux(
+node maxAdd1(
   first: Nat,
   second!: Nat
   --------
@@ -620,14 +620,14 @@ rule max(first!, second, result) zero(value!) {
 }
 
 rule max(first!, second, result) add1(prev, value!) {
-  maxAux(prev, second, result)
+  maxAdd1(prev, second, result)
 }
 
-rule maxAux(first, second!, result) zero(value!) {
+rule maxAdd1(first, second!, result) zero(value!) {
   add1(first, result)
 }
 
-rule maxAux(first, second!, result) add1(prev, value!) {
+rule maxAdd1(first, second!, result) add1(prev, value!) {
   add1(max(first, prev), result)
 }
 

diff --git a/docs/articles/反应网编程.md b/docs/articles/反应网编程.md
@@ -482,21 +482,20 @@ rule max(first!, second, result) zero(value!) {
 我们不得不增加一个辅助节点以及相关的规则，
 来明显地在两个可反应的边中做出选择。
 
-我们称辅助节点为 `(maxAux)`，
-其中 `aux` 是 auxiliary 的所写。
+我们称辅助节点为 `(maxAdd1)`。
 
 ```
      result
        |
-    (maxAux)
+    (maxAdd1)
      /    \
 first    second!
 ```
 
 定义如下：
 
 ```
-node maxAux(
+node maxAdd1(
   first: Nat,
   second!: Nat
   --------
@@ -509,7 +508,7 @@ node maxAux(
 ```
      result            result
        |                 |
-     (max)      =>    (maxAux)
+     (max)      =>    (maxAdd1)
      /    \            /   \
 (add1)   second     prev   second
    |
@@ -520,34 +519,34 @@ node maxAux(
 
 ```
 rule max(first!, second, result) add1(prev, value!) {
-  maxAux(prev, second, result)
+  maxAdd1(prev, second, result)
 }
 ```
 
-`(maxAux)` 与 `(zero)` 之间的规则：
+`(maxAdd1)` 与 `(zero)` 之间的规则：
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (zero)        first
 ```
 
 定义如下：
 
 ```
-rule maxAux(first, second!, result) zero(value!) {
+rule maxAdd1(first, second!, result) zero(value!) {
   add1(first, result)
 }
 ```
 
-`(maxAux)` 与 `(add1)` 之间的规则：
+`(maxAdd1)` 与 `(add1)` 之间的规则：
 
 ```
      result            result
        |                 |
-    (maxAux)     =>    (add1)
+    (maxAdd1)     =>   (add1)
      /    \              |
  first   (add1)        (max)
            |           /   \
@@ -557,7 +556,7 @@ rule maxAux(first, second!, result) zero(value!) {
 定义如下：
 
 ```
-rule maxAux(first, second!, result) add1(prev, value!) {
+rule maxAdd1(first, second!, result) add1(prev, value!) {
   add1(max(first, prev), result)
 }
 ```
@@ -578,7 +577,7 @@ node add1(
   value!: Nat
 )
 
-node maxAux(
+node maxAdd1(
   first: Nat,
   second!: Nat
   --------
@@ -597,14 +596,14 @@ rule max(first!, second, result) zero(value!) {
 }
 
 rule max(first!, second, result) add1(prev, value!) {
-  maxAux(prev, second, result)
+  maxAdd1(prev, second, result)
 }
 
-rule maxAux(first, second!, result) zero(value!) {
+rule maxAdd1(first, second!, result) zero(value!) {
   add1(first, result)
 }
 
-rule maxAux(first, second!, result) add1(prev, value!) {
+rule maxAdd1(first, second!, result) add1(prev, value!) {
   add1(max(first, prev), result)
 }
 

diff --git a/examples/datatypes/Nat.i b/examples/datatypes/Nat.i
@@ -90,9 +90,9 @@ rule mul(target!, mulend, result) add1(prev, value!) {
   add(second, mul(first, prev), result)
 }
 
-// To define `max`, we need `maxAux`.
+// To define `max`, we need `maxAdd1`.
 
-node maxAux(
+node maxAdd1(
   first: Nat,
   second!: Nat
   --------
@@ -111,13 +111,13 @@ rule max(first!, second, result) zero(value!) {
 }
 
 rule max(first!, second, result) add1(prev, value!) {
-  maxAux(prev, second, result)
+  maxAdd1(prev, second, result)
 }
 
-rule maxAux(first, second!, result) zero(value!) {
+rule maxAdd1(first, second!, result) zero(value!) {
   add1(first, result)
 }
 
-rule maxAux(first, second!, result) add1(prev, value!) {
+rule maxAdd1(first, second!, result) add1(prev, value!) {
   add1(max(first, prev), result)
 }