lambda-calculus-interpreter/test_cases.txt at master · jimouris/lambda-calculus-interpreter · GitHub

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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
reduce (myparse "(\\x.zx)w")
"zw"

reduce (myparse "(\\x.\\y.zxy)w")
"zw"

reduce (myparse "(\\y.zy(\\x.xy))w")
"zw(\\x.xw)"

reduce (myparse "(\\x.\\y.zxy)(wy)")
"z(wy)"

reduce (myparse "xyz")
"xyz"

reduce (myparse "\\x.zx")
"z"

reduce (myparse "\\y.zxy")
"zx"

reduce (myparse "\\x.zxx")
"\\x.zxx"

reduce (myparse "\\z.(\\f.\\x.fzx)(\\y.y)")
"\\y.y"

// succ c0
reduce (myparse "(\\n.\\f.\\x.nf(fx))(\\f.\\x.x)")
"\\b.b"

// succ c1
reduce (myparse "(\\n.\\f.\\x.nf(fx))(\\f.\\x.fx)")
"\\b.\\c.b(bc)"

// not true
reduce (myparse "(\\z.z(\\x.\\y.y)(\\x.\\y.x))(\\x.\\y.x)")
"\\b.\\c.c"

// fst (true, false)
reduce (myparse "(\\z.z(\\x.\\y.x))((\\x.\\y.\\z.zxy)(\\x.\\y.x)(\\x.\\y.y))")
"\\b.\\c.b"

// snd (true, false)
reduce (myparse "(\\z.z(\\x.\\y.y))((\\x.\\y.\\z.zxy)(\\x.\\y.x)(\\x.\\y.y))")
"\\x.\\y.y"

// if true then e else r
reduce (myparse "(\\z.\\x.\\y.zxy)(\\x.\\y.x)er")
"e"

// if false then e else r
reduce (myparse "(\\z.\\x.\\y.zxy)(\\x.\\y.y)er")
"r"

// fst (e, r)
reduce (myparse "(\\z.z(\\x.\\y.x))((\\x.\\y.\\z.zxy)er)")
"e"

// snd (e, r)
reduce (myparse "(\\z.z(\\x.\\y.y))((\\x.\\y.\\z.zxy)er)")
"r"

// omega
reduce (myparse "(\\x.xx)(\\x.xx)")
"(\\x.xx)(\\x.xx)"

prettyprint chTrue
"\\x.\\y.x"

prettyprint (church 2)
"\\f.\\x.f(fx)"

prettyprint (chSucc (church 2))
"\\f.\\x.f(f(fx))"

prettyprint (chIsZero (church 0))
"\\x.\\y.x"

prettyprint (chIsZero (church 2))
"\\x.\\y.y"

prettyprint (chPlus (chSucc (church 2)) (church 3))
"\\f.\\x.f(f(f(f(f(fx)))))"

prettyprint (chMult (church 2) (church 3))
"\\f.\\b.f(f(f(f(f(fb)))))"

prettyprint (chExp (church 2) (church 3))
"\\b.\\c.b(b(b(b(b(b(b(bc)))))))"

prettyprint (chNot chFalse)
"\\x.\\y.x"

prettyprint (chCond chTrue (church 2) (church 10))
"\\b.\\c.b(bc)"

prettyprint (chFst (chPair (church 2) (church 1)))
"\\b.\\c.b(bc)"

prettyprint (chSnd (chPair (church 2) (church 3)))
"\\f.\\x.f(f(fx))"

prettyprint (chAnd chTrue chTrue)
"\\b.\\c.b"

prettyprint (chAnd chFalse chTrue)
"\\x.\\y.y"

prettyprint (chOr chFalse  chTrue)
"\\x.\\y.x"