Skip to content

Commit 3d19dee

Browse files
xieyuhengxieyuheng
committed
ackermann-wrap.lisp
1 parent d47e238 commit 3d19dee

File tree

4 files changed

+196
-48
lines changed

4 files changed

+196
-48
lines changed

‎examples/ackermann-wrap.lisp‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(import zero add1 sub1 zero? "nat-church.lisp")
2+
(import one two three four five "nat-church.lisp")
3+
(import if "bool.lisp")
4+
(import Y "fixpoint.lisp")
5+
(import ackermann "ackermann.lisp")
6+
7+
(define ackermann-wrap
8+
(lambda (ackermann)
9+
(lambda (m n)
10+
(if (zero? m)
11+
(add1 n)
12+
(if (zero? n)
13+
(ackermann (sub1 m) one)
14+
(ackermann (sub1 m) (ackermann m (sub1 n))))))))
15+
16+
(assert-equal ((Y ackermann-wrap) zero zero) one)
17+
(assert-equal ((Y ackermann-wrap) one zero) two)
18+
(assert-equal ((Y ackermann-wrap) zero one) two)
19+
(assert-equal ((Y ackermann-wrap) one one) three)
20+
(assert-equal ((Y ackermann-wrap) one two) four)
21+
(assert-equal ((Y ackermann-wrap) two one) five)
22+
23+
(assert-equal ackermann (ackermann-wrap ackermann))
24+
(assert-equal ackermann (ackermann-wrap (ackermann-wrap ackermann)))
25+
26+
(define (ackermann-1 m n)
27+
((ackermann-wrap ackermann-1)
28+
m n))
29+
30+
(assert-equal (ackermann-1 zero zero) one)
31+
(assert-equal (ackermann-1 one zero) two)
32+
(assert-equal (ackermann-1 zero one) two)
33+
(assert-equal (ackermann-1 one one) three)
34+
(assert-equal (ackermann-1 one two) four)
35+
(assert-equal (ackermann-1 two one) five)
36+
37+
(define (ackermann-2 m n)
38+
((ackermann-wrap
39+
(ackermann-wrap ackermann-2))
40+
m n))
41+
42+
(assert-equal (ackermann-2 zero zero) one)
43+
(assert-equal (ackermann-2 one zero) two)
44+
(assert-equal (ackermann-2 zero one) two)
45+
(assert-equal (ackermann-2 one one) three)
46+
(assert-equal (ackermann-2 one two) four)
47+
(assert-equal (ackermann-2 two one) five)
48+
49+
(define (ackermann-3 m n)
50+
((ackermann-wrap
51+
(ackermann-wrap
52+
(ackermann-wrap ackermann-3)))
53+
m n))
54+
55+
(assert-equal (ackermann-3 zero zero) one)
56+
(assert-equal (ackermann-3 one zero) two)
57+
(assert-equal (ackermann-3 zero one) two)
58+
(assert-equal (ackermann-3 one one) three)
59+
(assert-equal (ackermann-3 one two) four)
60+
(assert-equal (ackermann-3 two one) five)
61+
62+
;; TODO fail:
63+
64+
;; (assert-equal ackermann-1 ackermann-2)
65+
;; (assert-equal ackermann-1 ackermann-3)
66+
;; (assert-equal ackermann-2 ackermann-3)

‎examples/ackermann.lisp‎

Lines changed: 130 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
(import zero add1 sub1 zero? "nat-church.lisp")
2-
(import one two "nat-church.lisp")
2+
(import one two three four five "nat-church.lisp")
33
(import if "bool.lisp")
44

55
(define (ackermann m n)
@@ -13,36 +13,135 @@
1313

1414
;; ackermann
1515

16-
(define ackermann-wrap
17-
(lambda (ackermann)
18-
(lambda (m n)
19-
(if (zero? m)
20-
(add1 n)
21-
(if (zero? n)
22-
(ackermann (sub1 m) one)
23-
(ackermann (sub1 m) (ackermann m (sub1 n))))))))
24-
25-
(assert-equal ackermann ackermann)
26-
(assert-equal ackermann (ackermann-wrap ackermann))
27-
(assert-equal ackermann (ackermann-wrap (ackermann-wrap ackermann)))
28-
29-
(define (ackermann-1 m n)
30-
((ackermann-wrap ackermann-1)
31-
m n))
32-
33-
(define (ackermann-2 m n)
34-
((ackermann-wrap
35-
(ackermann-wrap ackermann-2))
36-
m n))
37-
38-
(define (ackermann-3 m n)
39-
((ackermann-wrap
40-
(ackermann-wrap
41-
(ackermann-wrap ackermann-3)))
42-
m n))
16+
(assert-equal (ackermann zero zero) one)
17+
(assert-equal (ackermann one zero) two)
18+
(assert-equal (ackermann zero one) two)
19+
(assert-equal (ackermann one one) three)
20+
(assert-equal (ackermann one two) four)
21+
(assert-equal (ackermann two one) five)
22+
23+
(assert-equal
24+
ackermann
25+
(lambda (m n)
26+
(if (zero? m)
27+
(add1 n)
28+
(if (zero? n)
29+
(ackermann (sub1 m) one)
30+
(ackermann (sub1 m) (ackermann m (sub1 n)))))))
31+
32+
(assert-equal
33+
ackermann
34+
(lambda (m n)
35+
(if (zero? m)
36+
(add1 n)
37+
(if (zero? n)
38+
(ackermann (sub1 m) one)
39+
((lambda (m n)
40+
(if (zero? m)
41+
(add1 n)
42+
(if (zero? n)
43+
(ackermann (sub1 m) one)
44+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
45+
(sub1 m)
46+
(ackermann m (sub1 n)))))))
47+
48+
(define (ackermann/1 m n)
49+
(if (zero? m)
50+
(add1 n)
51+
(if (zero? n)
52+
(ackermann/1 (sub1 m) one)
53+
((lambda (m n)
54+
(if (zero? m)
55+
(add1 n)
56+
(if (zero? n)
57+
(ackermann/1 (sub1 m) one)
58+
(ackermann/1 (sub1 m) (ackermann/1 m (sub1 n))))))
59+
(sub1 m)
60+
(ackermann/1 m (sub1 n))))))
61+
62+
63+
(assert-equal (ackermann/1 zero zero) one)
64+
(assert-equal (ackermann/1 one zero) two)
65+
(assert-equal (ackermann/1 zero one) two)
66+
(assert-equal (ackermann/1 one one) three)
67+
(assert-equal (ackermann/1 one two) four)
68+
(assert-equal (ackermann/1 two one) five)
4369

4470
;; TODO fail:
4571

46-
;; (assert-equal ackermann-1 ackermann-2)
47-
;; (assert-equal ackermann-1 ackermann-3)
48-
;; (assert-equal ackermann-2 ackermann-3)
72+
;; (assert-equal ackermann ackermann/1)
73+
74+
(assert-equal
75+
(lambda (m n)
76+
(if (zero? m)
77+
(add1 n)
78+
(if (zero? n)
79+
(ackermann (sub1 m) one)
80+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
81+
(lambda (m n)
82+
(if (zero? m)
83+
(add1 n)
84+
(if (zero? n)
85+
(ackermann (sub1 m) one)
86+
((lambda (m n)
87+
(if (zero? m)
88+
(add1 n)
89+
(if (zero? n)
90+
(ackermann (sub1 m) one)
91+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
92+
(sub1 m)
93+
(ackermann m (sub1 n)))))))
94+
95+
(assert-equal
96+
ackermann
97+
(lambda (m n)
98+
(if (zero? m)
99+
(add1 n)
100+
(if (zero? n)
101+
((lambda (m n)
102+
(if (zero? m)
103+
(add1 n)
104+
(if (zero? n)
105+
(ackermann (sub1 m) one)
106+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
107+
(sub1 m) one)
108+
((lambda (m n)
109+
(if (zero? m)
110+
(add1 n)
111+
(if (zero? n)
112+
(ackermann (sub1 m) one)
113+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
114+
(sub1 m)
115+
((lambda (m n)
116+
(if (zero? m)
117+
(add1 n)
118+
(if (zero? n)
119+
(ackermann (sub1 m) one)
120+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
121+
m (sub1 n)))))))
122+
123+
(assert-equal
124+
ackermann
125+
(lambda (m n)
126+
(if (zero? m)
127+
(add1 n)
128+
(if (zero? n)
129+
(if (zero? (sub1 m))
130+
(add1 one)
131+
(if (zero? one)
132+
(ackermann (sub1 (sub1 m)) one)
133+
(ackermann (sub1 (sub1 m)) (ackermann (sub1 m) (sub1 one)))))
134+
((lambda (m n)
135+
(if (zero? m)
136+
(add1 n)
137+
(if (zero? n)
138+
(ackermann (sub1 m) one)
139+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
140+
(sub1 m)
141+
((lambda (m n)
142+
(if (zero? m)
143+
(add1 n)
144+
(if (zero? n)
145+
(ackermann (sub1 m) one)
146+
(ackermann (sub1 m) (ackermann m (sub1 n))))))
147+
m (sub1 n)))))))

‎examples/ackermann.test.lisp‎

Lines changed: 0 additions & 16 deletions
This file was deleted.

‎examples/ackermann.test.lisp.out‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

0 commit comments

Comments
 (0)