[docs] 反应网编程 -- 加入到 演算场 的连接

TODO.md

@@ -1,19 +1,10 @@
 # articles
 
-[docs] 反应网编程 -- 加入到 演算场 的连接
 [docs] 反应网编程 -- 完成 `mul` 的讲解
 [docs] 反应网编程 -- 完成 `List` 的讲解
 [docs] 反应网编程 -- 完成 `DiffList` 的讲解
 [docs] 反应网编程 -- 翻译为 programming-with-interaction-nets
 
-# propaganda
-
-post on v2ex
-
-post on reddit
-
-post on hackernews
-
 # learn
 
 phase space and monoid -- understand the model theory of linear logic

docs/articles/反应网编程.md

@@ -171,7 +171,7 @@ year: 2023
 (add)-return   // 输出接口
 ```
 
-节点和节点之间可以通过接口相连。
+节点和节点之间可以通过接口相连，并且输入接口只能与输出接口相连。
 
 比如代表数字 2 的图：
 
@@ -252,16 +252,24 @@ end
 
 - 以 `type` 作为语句的开头，后面跟着类型的名字，`end` 做结尾。
 - 用一条分割线区分输入参数与输出参数。
-  - 分割线前面的是输入参数类型，只能是 `Type`。
-  - 分割线后面的是输出参数类型，只能是一个 `Type`。
+  - 分割线前面的是输入类型参数，只能是 `Type`。
+  - 分割线后面的是输出类型参数，只能是一个 `Type`。
   - 分割线写多长都可以，最短要求两个字符 `--`。
 
-比如，代表自然数的类型 `Nat` 没有输入参数，其定义是：
+比如，代表自然数的类型 `Nat` 没有输入类型参数，其定义是：
 
 ```
 type Nat -- Type end
 ```
 
+又比如链表 `List` 有一个输入类型参数，
+代表链表元素的类型，
+其定义是：
+
+```
+type List Type -- Type end
+```
+
 # 6
 
 针对指定的两个节点，可以定义反应规则。
@@ -295,8 +303,9 @@ prev            target   addend
 - 用 `port-(node)` 这个词组，
   同样引用因拆而暴露出来的接口，
   并且将这个接口与栈顶的接口相连。
-- 通过节点的名字引用节点，
-  并且将此节点的输入接口按顺序取栈顶的接口相连，
+- 用 `(node)` 这个词组，通过节点的名字引用节点，
+  并且按顺序取此节点的输入接口与栈顶的接口相连，
+  每一个输入接口会用掉栈中的一个接口，
   然后将此节点的输出接口按顺序放回栈中。
 
 以 `(add1)` 与 `(add)` 之间的规则为例：
@@ -311,10 +320,10 @@ end
 
 下面逐步分析在上面的定义中，
 每一个词作用之后栈的情况，
-以及调用节点时新产生的节点与连接。
+以及调用节点时新产生的节点与新产生的连接。
 
-- 由于调用节点名字而引入的新节点，加脚标以示是区分。
-- 注意不带角标的 `(add)-addend`
+- 由调用节点名字而引入的新节点，加脚标以示是区分。
+- 注意，不带角标的 `(add)-addend`
   并非代表 `(add)` 的接口 `addend`，
   而是代表由于在原图中拆掉 `(add)` 的接口 `addend`
   而暴露出来的对应接口。
@@ -367,6 +376,72 @@ end
 
 # 7
 
+综合上面所设计的语法关键词，完整的一段代码如下。
+
+在其中，我们还用了 `define` 来定义新词。
+在使用 `define` 做定义之前，必须先用 `claim` 来声明一个词的类型。
+
+我们还有一个线上的演算场，可以用来方便地分享代码。
+
+[去关于 Nat 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLS0tCiAgTmF0IDp2YWx1ZSEKZW5kCgpub2RlIGFkZAogIE5hdCA6dGFyZ2V0IQogIE5hdCA6YWRkZW5kCiAgLS0tLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gYWRkCiAgKGFkZCktYWRkZW5kCiAgcmV0dXJuLShhZGQpCmVuZAoKcnVsZSBhZGQxIGFkZAogIChhZGQpLWFkZGVuZAogIChhZGQxKS1wcmV2IGFkZAogIGFkZDEgcmV0dXJuLShhZGQpCmVuZAoKY2xhaW0gb25lIC0tIE5hdCBlbmQKCmRlZmluZSBvbmUKICB6ZXJvIGFkZDEKZW5kCgpjbGFpbSB0d28gLS0gTmF0IGVuZAoKZGVmaW5lIHR3bwogIG9uZSBvbmUgYWRkCmVuZAoKY2xhaW0gYWRkX3R3byBOYXQgLS0gTmF0IGVuZAoKZGVmaW5lIGFkZF90d28KICB0d28gYWRkCmVuZAoKb25lIGFkZF90d28Kb25lIGFkZF90d28KYWRk)
+
+```
+type Nat -- Type end
+
+node zero
+  ------------
+  Nat :value!
+end
+
+node add1
+  Nat :prev
+  ------------
+  Nat :value!
+end
+
+node add
+  Nat :target!
+  Nat :addend
+  ------------
+  Nat :return
+end
+
+rule zero add
+  (add)-addend
+  return-(add)
+end
+
+rule add1 add
+  (add)-addend
+  (add1)-prev add
+  add1 return-(add)
+end
+
+claim one -- Nat end
+
+define one
+  zero add1
+end
+
+claim two -- Nat end
+
+define two
+  one one add
+end
+
+claim add_two Nat -- Nat end
+
+define add_two
+  two add
+end
+
+one add_two
+one add_two
+add
+```
+
+# 8
+
 我们强调一下反应网的限制，
 以及由于这些限制而得到的，
 反应网作为计算模型的属性。
@@ -417,7 +492,7 @@ end
 同时进行图中不同位置的反应，
 这些线程之间也不会相互干扰。
 
-# 8
+# 9
 
 每个节点有且仅有一个主接口，
 这条限制，给计算模型带来了优越的属性，