forked from tromp/AIT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
goodstein.lam
83 lines (71 loc) · 2.62 KB
/
goodstein.lam
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
let -- Direct translation from Haskell source, but with permuted arguments
-- nats
succ = \n\s\z. n s (s z);
1 = \f. f;
-- ordinal type: O = forall r. r -> (r -> r) -> ((N -> r) -> r) -> r
Z = \z\s\l. z;
S = \n.\z\s\l. s (n z s l);
L = \f.\z\s\l. l (\n. (f n) z s l);
-- arithmetic
add = \n\m. m n S L;
mul = \n\m. m Z (\x. add x n) L;
w = L (\n. n S Z);
expw = \n. n (S Z) (\x. mul x w) L;
goodstein = \o. o (\x. x) (\n\m. n (succ m)) (\f\m. f (succ (succ m)) m) 1
in
let -- Prepare optimization: Fold to values with z, s, l pre-applied
-- Caveat: This step is technically unsound; we are promising that the
-- discarded arguments inside the folds are equal to the pre-applied
-- ones from outside. There's probably a cleaner way of doing this.
add = \n\m.\z\s\l. m (n z s l) (\n. S (\_\_\_. n) z s l) (\f. L (\n\_\_\_. f n) z s l);
mul = \n\m.\z\s\l. m (Z z s l) (\x. add (\_\_\_. x) n z s l) (\f. L (\n\_\_\_. f n) z s l);
w = L (\n.\z\s\l. n (\n. S (\_\_\_. n) z s l) (Z z s l));
expw = \n.\z\s\l. n (\z. S Z z s l) (\x\z. mul (\z\_\_. x z) w z s l) (\f\z. L (\n\z\_\_. f n z) z s l) z
in
let -- Inline away
add = \n\m.\z\s\l. m (n z s l) s l;
mul = \n\m.\z\s\l. m z (\x. add (\_\_\_. x) n z s l) l;
w = \z\s\l. l (\n. n s z);
expw = \n.\z\s\l. n s (\x\z. mul (\z\_\_. x z) w z s l) (\f\z. l (\n. f n z)) z;
id = \x.x
in
let -- More inlining
expw = \n.\z\s\l. n s (\x\z. l (\n. n x z)) (\f\z. l (\n. f n z)) z
in
let -- Complete code
-- nats
succ = \n.\f\x. n f (f x);
1 = \f. f;
-- ordinal type: O = forall r. r -> (r -> r) -> ((N -> r) -> r) -> r
Z = \z\s\l. z;
-- arithmetic
add = \n\m.\z\s\l. m (n z s l) s l;
expw = \n.\z\s\l. n s (\x\z. l (\n. n x z)) (\f\z. l (\n. f n z)) z;
-- foldr lists
nil = \c\n. n;
cons = \x\xs.\c\n. c x (xs c n);
hd = \xs. xs (\x\xs.x) (\x.x);
tl = \xs\c\n. xs (\x\xs\f. f x (xs c)) (\_. n) (\x\y. y);
map = \f\xs\c. xs (\x. c (f x));
app = \xs\ys.\c\n. xs c (ys c n);
-- binary to ordinal conversion
go = \n.\lf\xs. n (\xs. lf (tl xs)) (app xs (map (add (expw (lf xs))) xs));
base2 = \n. n go (\x.x) hd (cons Z nil);
-- goodstein function
goodstein = \o. o
(\x. x)
(\n\m. n (succ m))
(\f\m. f (succ (succ m)) m)
1;
-- hardy o = goodstein o + 2
hardy = \o. o
(\x. x)
(\n\m. n (succ m))
(\f\m. f m m)
(\f\x. f (f (f x)));
-- programs
main = \n. goodstein (base2 n);
g16 = goodstein (expw (expw (expw (expw Z))));
h16 = hardy (expw (expw (expw (expw Z))))
in
main