test.bruijn


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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

atom0 [[[[[4]]]]]
atom1 [[[[[3]]]]]
atom2 [[[[[2]]]]]
atom3 [[[[[1]]]]]
atom4 [[[[[0]]]]]

# =========
# Reduction
# =========

:test [0] atom0 = atom0
:test [[0 1 0]] atom0 atom1 = atom1 atom0 atom1
:test [[[[3 2 1 0]]]] atom0 atom1 atom2 atom3 = atom0 atom1 atom2 atom3

# ===============
# Random examples
# ===============

set-of-three [[[[0 1 2 3]]]]
number-set set-of-three +1 +2 +3
access-first [0 [[[0]]]]
:test access-first number-set = +1

# ===========
# Combinators
# ===========

S [[[2 0 (1 0)]]]
K [[1]]
I [0]

i [0 S K]

:test I = i i
:test K = i (i (i i))
:test S = i (i (i (i i)))

# ===============
# Church numerals
# ===============

church-n0 [[0]]
church-n1 [[1 0]]
church-n2 [[1 (1 0)]]
church-n3 [[1 (1 (1 0))]]
church-n4 [[1 (1 (1 (1 0)))]]
church-n5 [[1 (1 (1 (1 (1 0))))]]
church-n6 [[1 (1 (1 (1 (1 (1 0)))))]]
church-n7 [[1 (1 (1 (1 (1 (1 (1 0))))))]]
church-n8 [[1 (1 (1 (1 (1 (1 (1 (1 0)))))))]]
church-n9 [[1 (1 (1 (1 (1 (1 (1 (1 (1 0))))))))]]
church-add [[[[3 1 (2 1 0)]]]]
church-mul [[[2 (1 0)]]]
church-pow [[0 1]]

:test church-add church-n2 church-n3 = church-n5
:test church-mul church-n2 church-n3 = church-n6
:test church-pow church-n2 church-n3 = church-n8

# ==================
# Lennart
# From Lambda-n-ways
# ==================

lnnrt-true [[0]]
lnnrt-false [[1]]
lnnrt-if [[[2 0 1]]]
lnnrt-zero [[1]]
lnnrt-succ [[[0 2]]]
lnnrt-one lnnrt-succ lnnrt-zero
lnnrt-two lnnrt-succ lnnrt-one
lnnrt-three lnnrt-succ lnnrt-two
lnnrt-const [[1]]
lnnrt-pair [[[0 2 1]]]
lnnrt-fst [[1 0 [[1]]]]
lnnrt-snd [[1 0 [[0]]]]
lnnrt-fix [[1 (0 0)] [1 (0 0)]]
lnnrt-add lnnrt-fix [[[1 0 [lnnrt-succ (3 0 1)]]]]
lnnrt-mul lnnrt-fix [[[1 lnnrt-zero [lnnrt-add 1 (3 0 1)]]]]
lnnrt-fac lnnrt-fix [[0 lnnrt-one [lnnrt-mul 1 (2 0)]]]
lnnrt-eqnat lnnrt-fix [[[1 (0 lnnrt-true (lnnrt-const lnnrt-false)) [1 lnnrt-false [4 1 0]]]]]
lnnrt-sumto lnnrt-fix [[0 lnnrt-zero [lnnrt-add 1 (2 0)]]]
lnnrt-n5 lnnrt-add lnnrt-two lnnrt-three
lnnrt-n6 lnnrt-add lnnrt-three lnnrt-three
lnnrt-n17 lnnrt-add lnnrt-n6 (lnnrt-add lnnrt-n6 lnnrt-n5)
lnnrt-n37 lnnrt-succ (lnnrt-mul lnnrt-n6 lnnrt-n6)
lnnrt-n703 lnnrt-sumto lnnrt-n37
lnnrt-n720 lnnrt-fac lnnrt-n6

# this test can take a minute, comment it if you're in a hurry
:test lnnrt-eqnat lnnrt-n720 (lnnrt-add lnnrt-n703 lnnrt-n17) = lnnrt-true

main [[1]]