blob: 75204b9c51de6372ddcac1b89d8cf3662ed00b2f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
# encode lambda terms as numbers
# from https://hbr.github.io/Lambda-Calculus/computability/text.html
# see also std/Meta for unary variant
:import std/Combinator .
:import std/Logic .
:import std/Math .
# compute pairing function [n,m]
compress [[--((pow (+2) 1) ⋅ ++((+2) ⋅ 0))]] ⧗ Number → Number → Number
:test ((compress (+0) (+0)) =? (+0)) (true)
:test ((compress (+1) (+0)) =? (+1)) (true)
:test ((compress (+0) (+1)) =? (+2)) (true)
:test ((compress (+2) (+1)) =? (+11)) (true)
idx compress (+0) ⧗ Number → Number
app (compress (+1)) ∘∘ compress ⧗ Number → Number → Number
abs (compress (+2)) ∘∘ compress ⧗ Number → Number → Number
enc_zero abs (+1) (abs (+0) (idx (+0))) ⧗ Number
enc_inc abs (+2) (abs (+1) (abs (+0) enc)) ⧗ Number
enc app (idx (+1)) (app (app (idx (+2)) (idx (+1))) (idx (+0)))
wrap [0 (app enc_inc) enc_zero] ⧗ Number → Number
main [[0]]
|
