From 29ccf374ae9c9a0da4d13ab18636a504a0afd8db Mon Sep 17 00:00:00 2001 From: Xie Yuheng Date: Tue, 7 Jan 2025 20:37:23 +0800 Subject: [PATCH] ambr maxAux maxAdd1 --- .../programming-with-interaction-nets.md | 30 +++++++++--------- ...24\347\275\221\347\274\226\347\250\213.md" | 31 +++++++++---------- examples/datatypes/Nat.i | 10 +++--- 3 files changed, 35 insertions(+), 36 deletions(-) diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md index 18d5eda6..8544bf3b 100644 --- a/docs/articles/programming-with-interaction-nets.md +++ b/docs/articles/programming-with-interaction-nets.md @@ -505,12 +505,12 @@ 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! ``` @@ -518,7 +518,7 @@ 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,16 +543,16 @@ 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 ``` @@ -560,17 +560,17 @@ The rule between `(maxAux)` and `(zero)`: 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/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" index 52302569..05e2f8bf 100644 --- "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" +++ "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" @@ -482,13 +482,12 @@ rule max(first!, second, result) zero(value!) { 我们不得不增加一个辅助节点以及相关的规则， 来明显地在两个可反应的边中做出选择。 -我们称辅助节点为 `(maxAux)`， -其中 `aux` 是 auxiliary 的所写。 +我们称辅助节点为 `(maxAdd1)`。 ``` result | - (maxAux) + (maxAdd1) / \ first second! ``` @@ -496,7 +495,7 @@ 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,16 +519,16 @@ 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 ``` @@ -537,17 +536,17 @@ rule max(first!, second, result) add1(prev, value!) { 定义如下： ``` -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 index bf9cccd8..9f837dc2 100644 --- 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) }