-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathlambda_vars.txt
More file actions
29 lines (29 loc) · 2.78 KB
/
lambda_vars.txt
File metadata and controls
29 lines (29 loc) · 2.78 KB
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
id = Abs(x, Bound(x, 0))
tru = Abs(t, Abs(f, Bound(t, 1)))
fls = Abs(t, Abs(f, Bound(f, 0)))
and = Abs(b, Abs(c, App(App(Bound(b, 1), Bound(c, 0)), Free(fls))))
or = Abs(b, Abs(c, App(App(Bound(b, 1), Free(tru)), Bound(c, 0))))
not = Abs(b, App(App(Bound(b, 0), Free(fls)), Free(tru)))
c0 = Abs(s, Abs(z, Bound(z, 0)))
scc = Abs(n, Abs(s, Abs(z, App(Bound(s, 1), App(App(Bound(n, 2), Bound(s, 1)), Bound(z, 0))))))
plus = Abs(m, Abs(n, Abs(s, Abs(z, App(App(Bound(m, 3), Bound(s, 1)), App(App(Bound(n, 2), Bound(s, 1)), Bound(z, 0)))))))
times = Abs(m, Abs(n, Abs(s, App(Bound(m, 2), App(Bound(n, 1), Bound(s, 0))))))
pow = Abs(m, Abs(n, App(Bound(n, 0), Bound(m, 1))))
iszro = Abs(m, App(App(Bound(m, 0), Abs(x, Free(fls))), Free(tru)))
pair = Abs(f, Abs(s, Abs(b, App(App(Bound(b, 0), Bound(f, 2)), Bound(s, 1)))))
fst = Abs(p, App(Bound(p, 0), Free(tru)))
snd = Abs(p, App(Bound(p, 0), Free(fls)))
prd = Abs(m, App(Free(fst), App(App(Bound(m, 0), Abs(p, App(App(Free(pair), App(Free(snd), Bound(p, 0))), App(Free(scc), App(Free(snd), Bound(p, 0)))))), App(App(Free(pair), Free(c0)), Free(c0)))))
minus = Abs(m, Abs(n, App(App(Bound(n, 0), Free(prd)), Bound(m, 1))))
equal = Abs(m, Abs(n, App(App(Free(and), App(Free(iszro), App(App(Free(minus), Bound(m, 1)), Bound(n, 0)))), App(Free(iszro), App(App(Free(minus), Bound(n, 0)), Bound(m, 1))))))
cons = Abs(h, Abs(t, Abs(c, Abs(n, App(App(Bound(h, 3), Bound(c, 1)), App(App(Bound(t, 2), Bound(c, 1)), Bound(n, 0)))))))
isnil = Abs(l, App(App(Bound(l, 0), Abs(x, Abs(y, Free(fls)))), Free(tru)))
head = Abs(l, App(App(Bound(l, 0), Free(tru)), Abs(x, Bound(x, 0))))
tail = Abs(l, App(Free(fst), App(App(Bound(l, 0), Abs(h, Abs(t, App(App(Free(pair), App(Free(snd), Bound(t, 0))), App(App(Free(cons), Abs(c, Abs(n, App(App(Bound(c, 1), Bound(h, 3)), Bound(n, 0))))), App(Free(snd), Bound(t, 0))))))), App(App(Free(pair), Abs(c, Abs(n, Bound(n, 0)))), Abs(c, Abs(n, Bound(n, 0)))))))
fix = Abs(f, App(Abs(x, App(Bound(f, 1), Abs(y, App(App(Bound(x, 1), Bound(x, 1)), Bound(y, 0))))), Abs(x, App(Bound(f, 1), Abs(y, App(App(Bound(x, 1), Bound(x, 1)), Bound(y, 0)))))))
realnat = Abs(n, App(App(Bound(n, 0), Abs(x, PrimApp(succ, Bound(x, 0)))), PrimVal(0)))
realbool = Abs(b, App(App(Bound(b, 0), PrimVal(true)), PrimVal(false)))
realeq = Abs(m, Abs(n, App(App(App(App(Free(equal), Bound(m, 1)), Bound(n, 0)), PrimVal(true)), PrimVal(false))))
churchnat = App(Free(fix), Abs(f, Abs(n, Cond(PrimApp(iszero, Bound(n, 0)), Free(c0), App(Free(scc), App(Bound(f, 1), PrimApp(pred, Bound(n, 0))))))))
churchbool = Abs(b, Cond(Bound(b, 0), Abs(t, Abs(f, Bound(t, 1))), Abs(t, Abs(f, Bound(f, 0)))))
factorial = App(Free(fix), Abs(f, Abs(n, Cond(App(Free(realbool), App(Free(iszro), Bound(n, 0))), App(Free(scc), Free(c0)), App(App(Free(times), Bound(n, 0)), App(Bound(f, 1), App(Free(prd), Bound(n, 0))))))))