prepare to remove lazy

Author: xieyuheng

TODO.md

@@ -1,4 +1,3 @@
-prepare to remove lazy
 remove lazy for now
 
 `readback` handle recursive function

examples/factorial-half.lisp

@@ -1,21 +1,21 @@
-(import zero? add mul sub1 "nat-church.lisp")
-(import zero one two three four "nat-church.lisp")
-(import if true false "bool.lisp")
+;; (import zero? add mul sub1 "nat-church.lisp")
+;; (import zero one two three four "nat-church.lisp")
+;; (import if true false "bool.lisp")
 
-;; (claim factorial-half
-;;   (fix (lambda (X) (-> X Nat Nat))))
+;; ;; (claim factorial-half
+;; ;;   (fix (lambda (X) (-> X Nat Nat))))
 
-(define (factorial-half self n)
-  (if (zero? n)
-    one
-    (mul n (self self (sub1 n)))))
+;; (define (factorial-half self n)
+;;   (if (zero? n)
+;;     one
+;;     (mul n (self self (sub1 n)))))
 
-factorial-half
+;; factorial-half
 
-(define factorial (factorial-half factorial-half))
+;; (define factorial (factorial-half factorial-half))
 
-(assert-equal (factorial zero) one)
-(assert-equal (factorial one) one)
-(assert-equal (factorial two) two)
-(assert-equal (factorial three) (mul three two))
-(assert-equal (factorial four) (mul four (mul three two)))
+;; (assert-equal (factorial zero) one)
+;; (assert-equal (factorial one) one)
+;; (assert-equal (factorial two) two)
+;; (assert-equal (factorial three) (mul three two))
+;; (assert-equal (factorial four) (mul four (mul three two)))

examples/factorial-half.lisp.out

@@ -1,7 +1,7 @@
 (import zero? add mul sub1 "nat-church.lisp")
 (import zero one two three four "nat-church.lisp")
 (import if true false "bool.lisp")
-(import Y turing "fix.lisp")
+(import Y "fix.lisp")
 
 ;; (claim factorial-wrap (-> (-> Nat Nat) (-> Nat Nat)))
 ;; (claim (Y factorial-wrap) (-> Nat Nat))
@@ -49,12 +49,6 @@ factorial-wrap
 (assert-equal ((Y factorial-wrap) three) (mul three two))
 (assert-equal ((Y factorial-wrap) four) (mul four (mul three two)))
 
-(assert-equal ((turing factorial-wrap) zero) one)
-(assert-equal ((turing factorial-wrap) one) one)
-(assert-equal ((turing factorial-wrap) two) two)
-(assert-equal ((turing factorial-wrap) three) (mul three two))
-(assert-equal ((turing factorial-wrap) four) (mul four (mul three two)))
-
 (define factorial (Y factorial-wrap))
 
 (assert-equal (factorial zero) one)

examples/factorial-wrap.lisp

@@ -21,6 +21,14 @@
 
 ;; (assert-equal factorial factorial)
 
+;; (assert-not-same
+;;   factorial
+;;   (lambda (x) (factorial x)))
+
+;; (assert-equal
+;;   factorial
+;;   (lambda (x) (factorial x)))
+
 ;; (assert-equal
 ;;   factorial
 ;;   (lambda (x) (factorial x))

examples/factorial.lisp

@@ -23,9 +23,14 @@
 
 ;; The following `Y` is one way of defining `Y`.
 
-(define (Y f)
-  ((lambda (x) (f (x x)))
-   (lambda (x) (f (x x)))))
+(define Y
+  (lambda (f)
+    ((lambda (u) (u u))
+     (lambda (x) (f (lambda (t) ((x x) t)))))))
+
+;; (define (Y f)
+;;   ((lambda (x) (f (x x)))
+;;    (lambda (x) (f (x x)))))
 
 ;; We will have
 
@@ -38,8 +43,8 @@
 
 ;; Another function to find fixpoint is `turing`.
 
-(define (turing-half x y) (y (x x y)))
-(define turing (turing-half turing-half))
+;; (define (turing-half x y) (y (x x y)))
+;; (define turing (turing-half turing-half))
 
 ;; We will have
 

examples/fix.lisp

@@ -1,7 +1,6 @@
 (import true false if and or not "bool.lisp")
 (import zero add1 sub1 zero? "nat-church.lisp")
 (import one two three four "nat-church.lisp")
-(import Y "fix.lisp")
 
 (define (even? n)
   (if (zero? n) true