blob: e9e539c5bed0d929e8f7fc61d08f823578c4b49e (
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
# ==================
# Lennart
# From Lambda-n-ways
# ==================
true [[0]]
false [[1]]
if [[[2 0 1]]]
zero [[1]]
succ [[[0 2]]]
one succ zero
two succ one
three succ two
const [[1]]
pair [[[0 2 1]]]
fst [[1 0 [[1]]]]
snd [[1 0 [[0]]]]
fix [[1 (0 0)] [1 (0 0)]]
add fix [[[1 0 [succ (3 0 1)]]]]
mul fix [[[1 zero [add 1 (3 0 1)]]]]
fac fix [[0 one [mul 1 (2 0)]]]
eqnat fix [[[1 (0 true (const false)) [1 false [4 1 0]]]]]
sumto fix [[0 zero [add 1 (2 0)]]]
n5 add two three
n6 add three three
n17 add n6 (add n6 n5)
n37 succ (mul n6 n6)
n703 sumto n37
n720 fac n6
# this can take some time..
# - should return true
:print eqnat n720 (add n703 n17)
# =========
# Ackermann
# From AIT
# =========
two [[1 (1 0)]]
omega [0 0]
ackify [[0 1 0]]
ackerlike [0 ackify omega 0]
# this can take a VERY long while
# maybe even too long for benchmarking
# - should return exponential tower with 256 levels
# :print ackerlike two
main [0]
|
