Comment by archibaldJ
1 year ago
hmm I'm just a bit confused; Can I make sense of it like this?
```
S = ∀z r.result[res=adder(z,r)]
adder = ∀n m.result[case(m,n,result) = plus]
plus = ∀n m. if(m=0) then result[n] else result[s=plus(n, pred(m)), res=S(s)]
```
And so when we add 2 (S(S(0))) and 3 (S(S(S(0)))), we start with:
```
Z
|
S -> S -> S -> Z
|
S -> S -> Z
```
and then we would reduce it to:
```
Z
|
S -> S -> S -> S -> S -> Z
```
or am I missing something?
Thanks for your reply.
I think you are right about the rules, just expressing them in a different way, not by local interaction between neighboring nodes, but by first-order logic!
When we add 2 (S(S(0))) and 3 (S(S(S(0)))).
I think we start with:
```
Add
| -- S -- S -- Z
| -- S -- S -- S -- Z
```
and then we would reduce it to:
```
S -- S -- S -- S -- S -- Z
```
At the top right corner of the homepage, there is a link to "Docs" -- https://readonly.link/articles/https://cdn.inet.cic.run/docs...
Maybe this article can help.
aw thanks for the link! what’s very nice to read !
I was on mobile and I think I accidentally clicked the gh link for the doc, and thought the readme was the doc
btw for me the readonly link took a while (like 4 sec) to load, probably due to parsing & cuz I’m on vpn.
would be cool to have a server-rendered page