blob: e870b29c8d455aa6c243ccc6937d904e3e44cf04 (
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
# ==================
# Lennart
# From Lambda-n-ways
# ==================
fix [[1 (0 0)] [1 (0 0)]]
zero [[1]]
succ [[[0 2]]]
add fix [[[1 0 [succ (3 0 1)]]]]
sumto fix [[0 zero [add 1 (2 0)]]]
mul fix [[[1 zero [add 1 (3 0 1)]]]]
one succ zero
two succ one
three succ two
n6 add three three
n703 sumto n37
n37 succ (mul n6 n6)
n17 add n6 (add n6 n5)
n5 add two three
true [[0]]
false [[1]]
const [[1]]
eqnat fix [[[1 (0 true (const false)) [1 false [4 1 0]]]]]
n720 fac n6
if [[[2 0 1]]]
pair [[[0 2 1]]]
fst [[1 0 [[1]]]]
snd [[1 0 [[0]]]]
fac fix [[0 one [mul 1 (2 0)]]]
# this can take some time..
# - should return true
:print eqnat n720 (add n703 n17)
# =========
# Ackermann
# From AIT
# =========
# ackerlike [0 ackify omega 0]
# two [[1 (1 0)]]
# omega [0 0]
# ackify [[0 1 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]
|
