Add natural numbers

nbe-test.rkt

@@ -19,7 +19,7 @@
 
 (define tm-pair `(λ (λ (λ ,(tm-app '(var 0) '(var 2) '(var 1))))))
 
-(define tm-y
+(define tm-fix
   (let ([g (tm-abs (tm-app (tm-var 1) (tm-app (tm-var 0) (tm-var 0))))])
     (tm-abs (tm-app g g))))
 
@@ -41,6 +41,25 @@
       (tm-suc (tm-nat (- n 1)))
       tm-zero))
 
+(define (tm-pnat n)
+  (if (positive? n)
+      `(succ ,(tm-pnat (- n 1)))
+      'zero))
+
+(define (tm-ifz a b c)
+  `(if-zero ,a ,b ,c))
+
+(define (tm-psuc a)
+  `(succ ,a))
+
+(define (tm-double m)
+  (tm-app tm-fix
+          (tm-abs (tm-abs (tm-ifz (tm-var 0) 'zero 'zero))) m ))
+
+(define (tm-padd m n)
+  (tm-app tm-fix
+          (tm-abs (tm-abs (tm-abs (tm-ifz (tm-var 1) (tm-var 0) (tm-psuc (tm-app (tm-var 3) (tm-var 0) (tm-var 1))))))) m n))
+
 (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id)
@@ -49,5 +68,5 @@
 (check-equal? (normalize (tm-mult (tm-nat 3) (tm-nat 2))) (normalize (tm-nat 6)))
 (check-equal? (normalize (tm-mult (tm-nat 11) (tm-nat 116))) (normalize (tm-nat 1276)))
 (check η-eq? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
-(check βη-eq? (tm-mult (tm-nat 888) (tm-nat 999)) (tm-nat 887112))
+(check βη-eq? (tm-mult (tm-nat 6) (tm-nat 7)) (tm-nat 42))
-(check β-eq? (tm-mult (tm-nat 888) (tm-nat 999)) (tm-nat 887112))
+(check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3))

nbe.rkt

@@ -6,15 +6,31 @@
 ;; D := neu D_ne | fun [(var -> var) -> D → D]
 ;; D_ne := var i | app D_ne D
 
+(define (tm? a)
+  (match a
+    ['zero true]
+    [`(succ ,a) (tm? a)]
+    [`(if-zero ,a ,b ,c) (and (tm? a) (tm? b) (tm? c))]
+    [`(λ ,a) (tm? a)]
+    [`(app ,a ,b) (and (tm? a) (tm? b))]
+    [`(var ,i) (exact-nonnegative-integer? i)]
+    [_ false]))
 
-(define (ap a b)
+(define-syntax-rule (ap a b)
   (match a
     [`(fun ,f) (f identity b)]
-    [`(neu ,u) `(neu (app ,u ,b))]))
+    [`(neu ,u) `(neu (app ,u ,b))]
+    [_ (error "ap: type error")]))
+
+(define-syntax-rule (ifz a b c)
+  (match a
+    ['zero b]
+    [`(succ ,u) (ap c u)]
+    [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
 
 (define compose-ren compose)
 (define (compose-ren-sub ξ ρ) (compose (curry ren-dom ξ) ρ))
-(define (ext ρ a)
+(define-syntax-rule (ext ρ a)
   (lambda (i)
     (if (zero? i)
         a
@@ -23,26 +39,43 @@
 (define (ren-ne-dom ξ a)
   (match a
     [`(var ,i) `(var ,(ξ i))]
-    [`(app ,a ,b) `(app ,(ren-ne-dom ξ a) ,(ren-dom ξ b))]))
+    [`(app ,a ,b) `(app ,(ren-ne-dom ξ a) ,(ren-dom ξ b))]
+    [`(if-zero ,a ,b ,c) `(if-zero ,(ren-ne-dom ξ a) ,(ren-dom ξ b) ,(ren-dom ξ c))]))
 
 (define (ren-dom ξ a)
   (match a
+    ['zero 'zero]
+    [`(succ ,a) `(succ ,(ren-dom ξ a))]
     [`(neu ,a) `(neu ,(ren-ne-dom ξ a))]
     [`(fun ,f) `(fun ,(λ (ξ0 α) (f (compose-ren ξ0 ξ) α)))]))
 
+(define-syntax-rule (interp-fun a ρ)
+  (list 'fun (λ (ξ x) (interp a (ext (compose-ren-sub ξ ρ) x)))))
+
 (define (interp a ρ)
   (match a
     [`(var ,i) (ρ i)]
-    [`(λ ,a)  (list 'fun (λ (ξ x) (interp a (ext (compose-ren-sub ξ ρ) x))))]
+    ['zero 'zero]
+    [`(succ ,a) `(succ ,(interp a ρ))]
+    [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
+    [`(λ ,a) (interp-fun a ρ)]
     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
 
 (define (reify a)
   (match a
+    ['zero 'zero]
+    [`(succ ,a) `(succ ,(reify a))]
     [`(fun ,f) (list 'λ (reify (f  (curry + 1) '(neu (var 0)))))]
     [`(neu ,a) (reify-neu a)]))
 
+(define (extract-body a)
+  (match a
+    [`(λ ,a) a]
+    [_ (error "reify-neu: not reifiable")]))
+
 (define (reify-neu a)
   (match a
+    [`(if-zero ,a ,b ,c) (list 'if (reify-neu a) (reify b) (extract-body (reify c)))]
     [`(app ,u ,v) (list 'app (reify-neu u) (reify v))]
     [`(var ,i) a]))
 
@@ -51,7 +84,6 @@
 (define (normalize a)
   (reify (interp a idsub)))
 
-
 (define (subst ρ a)
   (match a
     [`(var ,i) (ρ i)]
@@ -84,6 +116,10 @@
 ;; Coquand's algorithm but for β-normal forms
 (define (η-eq? a b)
   (match (list a b)
+    ['(zero zero) true]
+    [`((succ ,a) (succ ,b)) (η-eq? a b)]
+    [`((if-zero ,a ,b ,c) (if-zero ,a0 ,b0 ,c0))
+     (and (η-eq? a a0) (η-eq? b b0) (η-eq? c c0))]
     [`((λ ,a) (λ ,b)) (η-eq? a b)]
     [`((λ ,a) ,u) (η-eq? a `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)))]
     [`(,u (λ ,a)) (η-eq? `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)) a)]
@@ -98,11 +134,4 @@
 (define (β-eq? a b)
   (equal? (normalize a) (normalize b)))
 
-(define (tm? a)
-  (match a
-    [`(λ ,a) (tm? a)]
-    [`(app ,a ,b) (and (tm? a) (tm? b))]
-    [`(var ,i) (exact-nonnegative-integer? i)]
-    [_ false]))
-
 (provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)