From 92e79a54d3779eaf1ca3c8cf8adc73b08047cab0 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 4 May 2025 23:53:17 -0400
Subject: [PATCH 1/7] Finish nbe based on de bruijn levels

---
 nbe.rkt | 50 ++++++++++++++++++++++----------------------------
 1 file changed, 22 insertions(+), 28 deletions(-)

diff --git a/nbe.rkt b/nbe.rkt
index f1afe9d..1e18965 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -18,7 +18,7 @@
 
 (define-syntax-rule (ap a b)
   (match (force a)
-    [`(fun ,f) (force (f identity b))]
+    [`(fun ,f) (force (f b))]
     [`(neu ,u) `(neu (app ,u ,b))]
     [_ (error "ap: type error")]))
 
@@ -28,30 +28,14 @@
     [`(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-syntax-rule (ext ρ a)
   (lambda (i)
     (if (zero? i)
         a
         (ρ (- i 1)))))
 
-(define (ren-ne-dom ξ a)
-  (match a
-    [`(var ,i) `(var ,(ξ i))]
-    [`(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)
-  (delay (match (force 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)))))
+  (list 'fun (λ (x) (interp a (ext ρ x)))))
 
 (define (interp a ρ)
   (delay (match a
@@ -62,28 +46,38 @@
     [`(λ ,a) (interp-fun a ρ)]
     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])))
 
-(define (reify a)
+(define (reify n a)
   (match (force a)
     ['zero 'zero]
-    [`(succ ,a) `(succ ,(reify a))]
-    [`(fun ,f) (list 'λ (reify (f  (curry + 1) '(neu (var 0)))))]
-    [`(neu ,a) (reify-neu a)]))
+    [`(succ ,a) `(succ ,(reify n a))]
+    [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
+    [`(neu ,a) (reify-neu n a)]))
 
 (define (extract-body a)
   (match a
     [`(λ ,a) a]
     [_ (error "reify-neu: not reifiable")]))
 
-(define (reify-neu a)
+(define (reify-neu n 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]))
+    [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+    [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
+    [`(var ,i) (list 'var (- n (+ i 1)))]))
 
-(define (idsub i) `(neu (var ,i)))
+(define (idsub s i) `(neu (var ,(- s (+ i 1)))))
+
+(define (scope a)
+  (match a
+    ['zero 0]
+    [`(succ ,a) (scope a)]
+    [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
+    [`(λ ,a) (max 0 (- (scope a) 1))]
+    [`(app ,a ,b) (max (scope a) (scope b))]
+    [`(var ,i) (+ i 1)]))
 
 (define (normalize a)
-  (reify (interp a idsub)))
+  (let ([sa (scope a)])
+    (reify sa (interp a (curry idsub sa)))))
 
 (define (subst ρ a)
   (match a

From 7bf8bdde485d5e0cfb8448b230f955220105c18f Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sat, 10 May 2025 00:32:57 -0400
Subject: [PATCH 2/7] Start porting to typed racket

---
 nbe.rkt | 247 ++++++++++++++++++++++++++++++++------------------------
 1 file changed, 142 insertions(+), 105 deletions(-)

diff --git a/nbe.rkt b/nbe.rkt
index 1e18965..a300468 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -1,132 +1,169 @@
-#lang racket
+#lang typed/racket
 ;; Grammar (Λ)
 ;; t := λ t | app t t | i
 
+(define-type V Nonnegative-Integer)
+
+(define-type Term (∪ Var Abs App))
+(struct Var ([get : V]))
+(struct Abs ([body : Term]))
+(struct App ([fun : Term] [arg : Term]))
+
+(define-type D (∪ D-ne Clos))
+(struct Idx ([get : V]))
+(struct D-ne ([get : (∪ Idx DApp)]))
+(struct Clos ([get : (-> (Promise D) (Promise D))] ))
+(struct DApp ([fun : D-ne] [arg : (Promise D)]))
+
+
+
+(: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
+(define (ext ρ a)
+    (lambda (i)
+    (if (zero? i)
+        a
+        (ρ (- i 1)))))
+
+(: ap (-> (Promise D) (Promise D) D))
+(define (ap a b)
+  (match (force a)
+    [(Clos f) (force (f b))]
+    [(D-ne u) (D-ne (DApp (D-ne u) b))]))
+
+;; (define-syntax-rule (ap a b)
+;;   (match (force a)
+;;     [`(fun ,f) (force (f b))]
+;;     [`(neu ,u) `(neu (app ,u ,b))]
+;;     [_ (error "ap: type error")]))
+
+
 ;; Domain
 ;; 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 (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-syntax-rule (ap a b)
-  (match (force a)
-    [`(fun ,f) (force (f b))]
-    [`(neu ,u) `(neu (app ,u ,b))]
-    [_ (error "ap: type error")]))
+;; (define-syntax-rule (ap a b)
+;;   (match (force a)
+;;     [`(fun ,f) (force (f b))]
+;;     [`(neu ,u) `(neu (app ,u ,b))]
+;;     [_ (error "ap: type error")]))
 
-(define-syntax-rule (ifz a b c)
-  (match (force a)
-    ['zero (force b)]
-    [`(succ ,u) (ap c u)]
-    [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
+;; (define-syntax-rule (ifz a b c)
+;;   (match (force a)
+;;     ['zero (force b)]
+;;     [`(succ ,u) (ap c u)]
+;;     [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
 
-(define-syntax-rule (ext ρ a)
-  (lambda (i)
-    (if (zero? i)
-        a
-        (ρ (- i 1)))))
+;; (define-syntax-rule (ext ρ a)
+;;   (lambda (i)
+;;     (if (zero? i)
+;;         a
+;;         (ρ (- i 1)))))
 
-(define-syntax-rule (interp-fun a ρ)
-  (list 'fun (λ (x) (interp a (ext ρ x)))))
+;; (define-syntax-rule (interp-fun a ρ)
+;;   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
-(define (interp a ρ)
-  (delay (match a
-    [`(var ,i) (force (ρ i))]
-    ['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 ρ))])))
+;; (: interp (-> Term (-> Term)))
 
-(define (reify n a)
-  (match (force a)
-    ['zero 'zero]
-    [`(succ ,a) `(succ ,(reify n a))]
-    [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
-    [`(neu ,a) (reify-neu n a)]))
+;; (define (interp a ρ)
+;;   (delay (match a
+;;     [`(var ,i) (force (ρ i))]
+;;     ['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 (extract-body a)
-  (match a
-    [`(λ ,a) a]
-    [_ (error "reify-neu: not reifiable")]))
+;; (define (reify n a)
+;;   (match (force a)
+;;     ['zero 'zero]
+;;     [`(succ ,a) `(succ ,(reify n a))]
+;;     [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
+;;     [`(neu ,a) (reify-neu n a)]))
 
-(define (reify-neu n a)
-  (match a
-    [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
-    [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
-    [`(var ,i) (list 'var (- n (+ i 1)))]))
+;; (define (extract-body a)
+;;   (match a
+;;     [`(λ ,a) a]
+;;     [_ (error "reify-neu: not reifiable")]))
 
-(define (idsub s i) `(neu (var ,(- s (+ i 1)))))
+;; (define (reify-neu n a)
+;;   (match a
+;;     [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+;;     [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
+;;     [`(var ,i) (list 'var (- n (+ i 1)))]))
 
-(define (scope a)
-  (match a
-    ['zero 0]
-    [`(succ ,a) (scope a)]
-    [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
-    [`(λ ,a) (max 0 (- (scope a) 1))]
-    [`(app ,a ,b) (max (scope a) (scope b))]
-    [`(var ,i) (+ i 1)]))
+;; (define (idsub s i) `(neu (var ,(- s (+ i 1)))))
 
-(define (normalize a)
-  (let ([sa (scope a)])
-    (reify sa (interp a (curry idsub sa)))))
+;; (define (scope a)
+;;   (match a
+;;     ['zero 0]
+;;     [`(succ ,a) (scope a)]
+;;     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
+;;     [`(λ ,a) (max 0 (- (scope a) 1))]
+;;     [`(app ,a ,b) (max (scope a) (scope b))]
+;;     [`(var ,i) (+ i 1)]))
 
-(define (subst ρ a)
-  (match a
-    [`(var ,i) (ρ i)]
-    [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
-    [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
-                              '(var 0)) a))]))
+;; (define (normalize a)
+;;   (let ([sa (scope a)])
+;;     (reify sa (interp a (curry idsub sa)))))
 
-(define (idsub-tm i) `(var ,i))
-(define (subst1 b a)
-  (subst (ext idsub-tm b) a))
+;; (define (subst ρ a)
+;;   (match a
+;;     [`(var ,i) (ρ i)]
+;;     [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
+;;     [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
+;;                               '(var 0)) a))]))
 
-(define (eval-tm a)
-  (match a
-    [(list 'var _) a]
-    [(list 'λ a) `(λ ,(eval-tm a))]
-    [(list 'app a b)
-     (match (eval-tm a)
-       [(list 'λ a) (eval-tm (subst1 b a))]
-       [v `(app ,v ,(eval-tm b))])]))
+;; (define (idsub-tm i) `(var ,i))
+;; (define (subst1 b a)
+;;   (subst (ext idsub-tm b) a))
 
-(define (eval-tm-strict a)
-  (match a
-    [(list 'var _) a]
-    [(list 'λ a) `(λ ,(eval-tm-strict a))]
-    [(list 'app a b)
-     (match (eval-tm-strict a)
-       [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))]
-       [v `(app ,v ,(eval-tm-strict b))])]))
+;; (define (eval-tm a)
+;;   (match a
+;;     [(list 'var _) a]
+;;     [(list 'λ a) `(λ ,(eval-tm a))]
+;;     [(list 'app a b)
+;;      (match (eval-tm a)
+;;        [(list 'λ a) (eval-tm (subst1 b a))]
+;;        [v `(app ,v ,(eval-tm b))])]))
 
-;; 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)]
-    [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (η-eq? u0 u1) (η-eq? v0 v1))]
-    [`((var ,i) (var ,j)) (eqv? i j)]
-    [_ false]))
+;; (define (eval-tm-strict a)
+;;   (match a
+;;     [(list 'var _) a]
+;;     [(list 'λ a) `(λ ,(eval-tm-strict a))]
+;;     [(list 'app a b)
+;;      (match (eval-tm-strict a)
+;;        [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))]
+;;        [v `(app ,v ,(eval-tm-strict b))])]))
+
+;; ;; 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)]
+;;     [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (η-eq? u0 u1) (η-eq? v0 v1))]
+;;     [`((var ,i) (var ,j)) (eqv? i j)]
+;;     [_ false]))
 
 
-(define (βη-eq? a b)
-  (η-eq? (normalize a) (normalize b)))
+;; (define (βη-eq? a b)
+;;   (η-eq? (normalize a) (normalize b)))
 
-(define (β-eq? a b)
-  (equal? (normalize a) (normalize b)))
+;; (define (β-eq? a b)
+;;   (equal? (normalize a) (normalize b)))
 
-(provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)
+;; (provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)

From 212cbdbceb819115203c93fa0274c8648de67bdd Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Sat, 10 May 2025 12:36:00 -0400
Subject: [PATCH 3/7] Implement nbe in typed racket

---
 nbe-test.rkt |  62 ++++++++++++++----------
 nbe.rkt      | 133 +++++++++++++++++++++------------------------------
 2 files changed, 91 insertions(+), 104 deletions(-)

diff --git a/nbe-test.rkt b/nbe-test.rkt
index 0e3df78..10b3d39 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -1,6 +1,6 @@
-#lang racket
+#lang typed/racket
 
-(require rackunit "nbe.rkt")
+(require typed/rackunit "nbe.rkt")
 
 (define-syntax tm-app
   (syntax-rules ()
@@ -11,64 +11,74 @@
 (define-syntax-rule (tm-var a) `(var ,a))
 (define-syntax-rule (tm-abs a) `(λ ,a))
 
+(: tm-id Term)
 (define tm-id '(λ (var 0)))
 
+(: tm-fst Term)
 (define tm-fst '(λ (λ (var 1))))
 
+(: tm-snd Term)
 (define tm-snd '(λ (λ (var 0))))
 
+(: tm-pair Term)
 (define tm-pair `(λ (λ (λ ,(tm-app '(var 0) '(var 2) '(var 1))))))
 
-(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))))
+;; (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))))
 
+(: tm-zero Term)
 (define tm-zero tm-snd)
 
+(: tm-suc (-> Term Term))
 (define (tm-suc a) (tm-abs (tm-abs (tm-app (tm-var 1) (tm-app a (tm-var 1) (tm-var 0))))))
 
+(: tm-add (-> Term Term Term))
 (define (tm-add a b)
   (tm-abs (tm-abs
            (tm-app b (tm-var 1) (tm-app a (tm-var 1) (tm-var 0))))))
 
+(: tm-compose (-> Term Term Term))
 (define (tm-compose a b)
   (tm-abs (tm-app a (tm-app b (tm-var 0)))))
 
+(: tm-mult (-> Term Term Term))
 (define (tm-mult a b) (tm-compose a b))
 
+(: tm-nat (-> V Term))
 (define (tm-nat n)
   (if (positive? n)
       (tm-suc (tm-nat (- n 1)))
       tm-zero))
 
-(define (tm-pnat n)
-  (if (positive? n)
-      `(succ ,(tm-pnat (- n 1)))
-      '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-ifz a b c)
+;;   `(if-zero ,a ,b ,c))
 
-(define (tm-psuc a)
-  `(succ ,a))
+;; (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-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))
+;; (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)
 (check-equal? (normalize (tm-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
 (check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
-(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 6) (tm-nat 7)) (tm-nat 42))
-(check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3))
-(check βη-eq? (tm-padd (tm-pnat 8) (tm-pnat 11)) (tm-pnat 19))
-(check βη-eq? (tm-padd (tm-pnat 2) (tm-psuc (tm-var 0))) '(succ (succ (succ (var 0)))))
+;; (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 6) (tm-nat 7)) (tm-nat 42))
+;; (check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3))
+;; (check βη-eq? (tm-padd (tm-pnat 8) (tm-pnat 11)) (tm-pnat 19))
+;; (check βη-eq? (tm-padd (tm-pnat 2) (tm-psuc (tm-var 0))) '(succ (succ (succ (var 0)))))
diff --git a/nbe.rkt b/nbe.rkt
index a300468..0d06562 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -3,19 +3,10 @@
 ;; t := λ t | app t t | i
 
 (define-type V Nonnegative-Integer)
+(define-type Term (∪ (List 'var V) (List 'λ Term) (List 'app Term Term)))
 
-(define-type Term (∪ Var Abs App))
-(struct Var ([get : V]))
-(struct Abs ([body : Term]))
-(struct App ([fun : Term] [arg : Term]))
-
-(define-type D (∪ D-ne Clos))
-(struct Idx ([get : V]))
-(struct D-ne ([get : (∪ Idx DApp)]))
-(struct Clos ([get : (-> (Promise D) (Promise D))] ))
-(struct DApp ([fun : D-ne] [arg : (Promise D)]))
-
-
+(define-type D (∪ (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
+(define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
 
 (: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
 (define (ext ρ a)
@@ -24,53 +15,31 @@
         a
         (ρ (- i 1)))))
 
-(: ap (-> (Promise D) (Promise D) D))
-(define (ap a b)
-  (match (force a)
-    [(Clos f) (force (f b))]
-    [(D-ne u) (D-ne (DApp (D-ne u) b))]))
 
-;; (define-syntax-rule (ap a b)
-;;   (match (force a)
-;;     [`(fun ,f) (force (f b))]
-;;     [`(neu ,u) `(neu (app ,u ,b))]
-;;     [_ (error "ap: type error")]))
+(define-syntax-rule (ap a b)
+  (match a
+    [`(fun ,f) (f (delay b))]
+    [`(neu ,u) `(neu (app ,u ,b))]))
 
 
+(define-syntax-rule (interp-fun a ρ)
+  (list 'fun (λ (x) (interp a (ext ρ x)))))
+
+
+(: interp (-> Term (-> V (Promise D)) D))
+(define (interp a ρ)
+  (match a
+    [`(var ,i) (force (ρ i))]
+    ;; ['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 ρ))]))
+
 ;; Domain
 ;; 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-syntax-rule (ap a b)
-;;   (match (force a)
-;;     [`(fun ,f) (force (f b))]
-;;     [`(neu ,u) `(neu (app ,u ,b))]
-;;     [_ (error "ap: type error")]))
-
-;; (define-syntax-rule (ifz a b c)
-;;   (match (force a)
-;;     ['zero (force b)]
-;;     [`(succ ,u) (ap c u)]
-;;     [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
-
-;; (define-syntax-rule (ext ρ a)
-;;   (lambda (i)
-;;     (if (zero? i)
-;;         a
-;;         (ρ (- i 1)))))
-
-;; (define-syntax-rule (interp-fun a ρ)
-;;   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
 ;; (: interp (-> Term (-> Term)))
 
@@ -83,38 +52,44 @@
 ;;     [`(λ ,a) (interp-fun a ρ)]
 ;;     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])))
 
-;; (define (reify n a)
-;;   (match (force a)
-;;     ['zero 'zero]
-;;     [`(succ ,a) `(succ ,(reify n a))]
-;;     [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
-;;     [`(neu ,a) (reify-neu n a)]))
+(: reify (-> V D Term))
+(define (reify n a)
+  (match a
+    ;; ['zero 'zero]
+    ;; [`(succ ,a) `(succ ,(reify n a))]
+    [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
+    [`(neu ,a) (reify-neu n a)]
+    ))
 
 ;; (define (extract-body a)
 ;;   (match a
 ;;     [`(λ ,a) a]
 ;;     [_ (error "reify-neu: not reifiable")]))
 
-;; (define (reify-neu n a)
-;;   (match a
-;;     [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
-;;     [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
-;;     [`(var ,i) (list 'var (- n (+ i 1)))]))
+(: reify-neu (-> V D-ne Term))
+(define (reify-neu n a)
+  (match a
+    ;; [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+    [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
+    [`(idx ,i) (list 'var (max 0 (- n (+ i 1))))]))
 
-;; (define (idsub s i) `(neu (var ,(- s (+ i 1)))))
+(: idsub (-> V V D))
+(define (idsub s i) `(neu (idx ,(max 0 (- s (+ i 1))))))
 
-;; (define (scope a)
-;;   (match a
-;;     ['zero 0]
-;;     [`(succ ,a) (scope a)]
-;;     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
-;;     [`(λ ,a) (max 0 (- (scope a) 1))]
-;;     [`(app ,a ,b) (max (scope a) (scope b))]
-;;     [`(var ,i) (+ i 1)]))
+(: scope (-> Term V))
+(define (scope a)
+  (match a
+    ['zero 0]
+    [`(succ ,a) (scope a)]
+    [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
+    [`(λ ,a) (max 0 (- (scope a) 1))]
+    [`(app ,a ,b) (max (scope a) (scope b))]
+    [`(var ,i) (+ i 1)]))
 
-;; (define (normalize a)
-;;   (let ([sa (scope a)])
-;;     (reify sa (interp a (curry idsub sa)))))
+(: normalize (-> Term Term))
+(define (normalize a)
+  (let ([sa (scope a)])
+    (reify sa (interp a (λ (x) (delay (idsub sa x)))))))
 
 ;; (define (subst ρ a)
 ;;   (match a
@@ -146,6 +121,7 @@
 ;;        [v `(app ,v ,(eval-tm-strict b))])]))
 
 ;; ;; Coquand's algorithm but for β-normal forms
+;; (: η-eq? (-> Term Term Boolean))
 ;; (define (η-eq? a b)
 ;;   (match (list a b)
 ;;     ['(zero zero) true]
@@ -163,7 +139,8 @@
 ;; (define (βη-eq? a b)
 ;;   (η-eq? (normalize a) (normalize b)))
 
-;; (define (β-eq? a b)
-;;   (equal? (normalize a) (normalize b)))
+(: β-eq? (-> Term Term Boolean))
+(define (β-eq? a b)
+  (equal? (normalize a) (normalize b)))
 
-;; (provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)
+(provide reify interp normalize β-eq? Term D V)

From eb4291f6a0ec5755d39efeea709d87af25f8884b Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 11 May 2025 17:55:50 -0400
Subject: [PATCH 4/7] Add back peano numbers

---
 nbe-test.rkt | 30 +++++++++++++++++++++++-------
 nbe.rkt      | 17 +++++++++--------
 2 files changed, 32 insertions(+), 15 deletions(-)

diff --git a/nbe-test.rkt b/nbe-test.rkt
index 10b3d39..04d6697 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -23,9 +23,10 @@
 (: tm-pair Term)
 (define tm-pair `(λ (λ (λ ,(tm-app '(var 0) '(var 2) '(var 1))))))
 
-;; (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))))
+(: tm-fix Term)
+(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))))
 
 (: tm-zero Term)
 (define tm-zero tm-snd)
@@ -51,10 +52,23 @@
       (tm-suc (tm-nat (- n 1)))
       tm-zero))
 
-;; (define (tm-pnat n)
-;;   (if (positive? n)
-;;       `(succ ,(tm-pnat (- n 1)))
-;;       'zero))
+(: tm-const Term)
+(define tm-const tm-fst)
+
+(: tm-loop Term)
+(define tm-loop
+  (let ([g (tm-abs (tm-app (tm-var 0) (tm-var 0)))])
+    (tm-app g g)))
+
+(: tm-nat-to-pnat Term)
+(define tm-nat-to-pnat
+  (tm-abs (tm-app (tm-var 0) (tm-abs '(succ (var 0))) 'zero)))
+
+(: tm-pnat (-> V Term))
+(define (tm-pnat n)
+  (if (positive? n)
+      `(succ ,(tm-pnat (- n 1)))
+      'zero))
 
 ;; (define (tm-ifz a b c)
 ;;   `(if-zero ,a ,b ,c))
@@ -75,6 +89,8 @@
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id)
 (check-equal? (normalize (tm-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
 (check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
+(check-equal? (normalize (tm-app tm-const (tm-nat 0) tm-loop)) (normalize (tm-nat 0)))
+(check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10))
 ;; (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))))
diff --git a/nbe.rkt b/nbe.rkt
index 0d06562..2814c1c 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -3,9 +3,11 @@
 ;; t := λ t | app t t | i
 
 (define-type V Nonnegative-Integer)
-(define-type Term (∪ (List 'var V) (List 'λ Term) (List 'app Term Term)))
+(define-type Term (∪ 'zero (List 'succ Term) (List 'var V) (List 'λ Term) (List 'app Term Term)))
 
-(define-type D (∪ (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
+
+
+(define-type D (∪ 'zero (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
 (define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
 
 (: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
@@ -30,8 +32,8 @@
 (define (interp a ρ)
   (match a
     [`(var ,i) (force (ρ i))]
-    ;; ['zero 'zero]
-    ;; [`(succ ,a) `(succ ,(interp a ρ))]
+    ['zero 'zero]
+    [`(succ ,a) `(succ ,(delay (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 ρ))]))
@@ -55,11 +57,10 @@
 (: reify (-> V D Term))
 (define (reify n a)
   (match a
-    ;; ['zero 'zero]
-    ;; [`(succ ,a) `(succ ,(reify n a))]
+    ['zero 'zero]
+    [`(succ ,a) `(succ ,(reify n (force a)))]
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
-    [`(neu ,a) (reify-neu n a)]
-    ))
+    [`(neu ,a) (reify-neu n a)]))
 
 ;; (define (extract-body a)
 ;;   (match a

From 4f2f5b47c02e182d3ce0b22f5a673563bcaa48c0 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 11 May 2025 18:28:40 -0400
Subject: [PATCH 5/7] Add syntax form for ind

---
 nbe.rkt | 36 +++++++++++++++++++++++++++---------
 1 file changed, 27 insertions(+), 9 deletions(-)

diff --git a/nbe.rkt b/nbe.rkt
index 2814c1c..be32bdb 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -2,39 +2,56 @@
 ;; Grammar (Λ)
 ;; t := λ t | app t t | i
 
+(define-type denv (-> V (Promise D)))
 (define-type V Nonnegative-Integer)
-(define-type Term (∪ 'zero (List 'succ Term) (List 'var V) (List 'λ Term) (List 'app Term Term)))
+(define-type Term (∪ 'zero
+                     (List 'succ Term)
+                     (List 'var V)
+                     (List 'λ Term)
+                     (List 'app Term Term)
+                     (List 'ind Term Term Term)))
 
+(define-type D (∪ 'zero
+                  (List 'succ (Promise D))
+                  (List 'fun (-> (Promise D) D))
+                  (List 'fun2 (-> (Promise D) (Promise D) D))
+                  (List 'neu D-ne)
+                  ;; (List 'ind (-> (Promise D) (Promise D) D))
+                  ))
 
-
-(define-type D (∪ 'zero (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
 (define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
 
-(: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
+(: ext (-> denv (Promise D) denv))
 (define (ext ρ a)
     (lambda (i)
     (if (zero? i)
         a
         (ρ (- i 1)))))
 
-
 (define-syntax-rule (ap a b)
   (match a
     [`(fun ,f) (f (delay b))]
     [`(neu ,u) `(neu (app ,u ,b))]))
 
-
-(define-syntax-rule (interp-fun a ρ)
+(: interp-fun (-> Term denv D))
+(define (interp-fun a ρ)
   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
+(: interp-ind (-> D (Promise D) (Promise D) denv D))
+(define (interp-ind a b c ρ)
+  (match a
+    [_ (error "unimplemented")]))
 
-(: interp (-> Term (-> V (Promise D)) D))
+(: interp (-> Term denv D))
 (define (interp a ρ)
   (match a
     [`(var ,i) (force (ρ i))]
     ['zero 'zero]
     [`(succ ,a) `(succ ,(delay (interp a ρ)))]
-    ;; [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
+    [`(ind ,a ,b ,c) (interp-ind
+                      (interp a ρ)
+                      (delay (interp b ρ))
+                      (delay (interp c ρ)) ρ)]
     [`(λ ,a) (interp-fun a ρ)]
     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
 
@@ -82,6 +99,7 @@
   (match a
     ['zero 0]
     [`(succ ,a) (scope a)]
+    (`(ind ,a ,b ,c) (max (scope a) (scope b) (scope c)))
     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
     [`(λ ,a) (max 0 (- (scope a) 1))]
     [`(app ,a ,b) (max (scope a) (scope b))]

From cc59960e790ce1e3fcf463e810167d7d54242844 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Mon, 12 May 2025 00:48:47 -0400
Subject: [PATCH 6/7] Finish adding natural numbers

---
 nbe-test.rkt | 35 ++++++++++++---------------
 nbe.rkt      | 68 ++++++++++++++++++++++++----------------------------
 2 files changed, 46 insertions(+), 57 deletions(-)

diff --git a/nbe-test.rkt b/nbe-test.rkt
index 04d6697..b7b4b81 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -39,6 +39,14 @@
   (tm-abs (tm-abs
            (tm-app b (tm-var 1) (tm-app a (tm-var 1) (tm-var 0))))))
 
+(: tm-ind (-> Term Term Term Term))
+(define (tm-ind a b c)
+  `(ind ,a ,b ,c))
+
+(: tm-padd (-> Term Term Term))
+(define (tm-padd a b)
+  (tm-app (tm-ind a tm-id (tm-abs (tm-psuc (tm-app (tm-var 1) (tm-var 0))))) b))
+
 (: tm-compose (-> Term Term Term))
 (define (tm-compose a b)
   (tm-abs (tm-app a (tm-app b (tm-var 0)))))
@@ -70,19 +78,9 @@
       `(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))
+(: tm-psuc (-> Term Term))
+(define (tm-psuc a)
+  `(succ ,a))
 
 (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)
@@ -91,10 +89,7 @@
 (check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
 (check-equal? (normalize (tm-app tm-const (tm-nat 0) tm-loop)) (normalize (tm-nat 0)))
 (check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10))
-;; (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 6) (tm-nat 7)) (tm-nat 42))
-;; (check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3))
-;; (check βη-eq? (tm-padd (tm-pnat 8) (tm-pnat 11)) (tm-pnat 19))
-;; (check βη-eq? (tm-padd (tm-pnat 2) (tm-psuc (tm-var 0))) '(succ (succ (succ (var 0)))))
+(check-equal? (normalize `(ind ,(tm-pnat 3) ,(tm-pnat 0) (var 1))) (tm-pnat 2))
+(check-equal? (normalize `(ind ,(tm-pnat 3) ,tm-loop (var 1))) (tm-pnat 2))
+(check-equal? (normalize (tm-padd (tm-pnat 10000) (tm-pnat 2000)))
+              (tm-pnat 12000))
diff --git a/nbe.rkt b/nbe.rkt
index be32bdb..57db916 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -14,12 +14,11 @@
 (define-type D (∪ 'zero
                   (List 'succ (Promise D))
                   (List 'fun (-> (Promise D) D))
-                  (List 'fun2 (-> (Promise D) (Promise D) D))
-                  (List 'neu D-ne)
-                  ;; (List 'ind (-> (Promise D) (Promise D) D))
-                  ))
+                  (List 'neu D-ne)))
 
-(define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
+(define-type D-ne (∪ (List 'app D-ne D)
+                     (List 'idx V)
+                     (List 'ind D-ne D (-> (Promise D) (Promise D) D))))
 
 (: ext (-> denv (Promise D) denv))
 (define (ext ρ a)
@@ -28,19 +27,30 @@
         a
         (ρ (- i 1)))))
 
-(define-syntax-rule (ap a b)
-  (match a
-    [`(fun ,f) (f (delay b))]
-    [`(neu ,u) `(neu (app ,u ,b))]))
+
 
 (: interp-fun (-> Term denv D))
 (define (interp-fun a ρ)
   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
-(: interp-ind (-> D (Promise D) (Promise D) denv D))
-(define (interp-ind a b c ρ)
+(: interp-fun2 (-> Term denv (-> (Promise D) (Promise D) D)))
+(define (interp-fun2 a ρ)
+  (λ (x y) (interp a (ext (ext ρ x) y))))
+
+(: interp-ind (-> D (Promise D) (-> (Promise D) (Promise D) D) D))
+(define (interp-ind a b c)
   (match a
-    [_ (error "unimplemented")]))
+    [`(neu ,u) `(neu (ind ,u ,(force b) ,c))]
+    ['zero (force b)]
+    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]))
+
+(: ap (-> D Term denv D))
+(define (ap a b ρ)
+  (match a
+    ['zero (error "type-error: ap zero")]
+    [`(succ ,_) (error "type-error: ap succ")]
+    [`(fun ,f) (f (delay (interp b ρ)))]
+    [`(neu ,u) `(neu (app ,u ,(interp b ρ)))]))
 
 (: interp (-> Term denv D))
 (define (interp a ρ)
@@ -51,25 +61,9 @@
     [`(ind ,a ,b ,c) (interp-ind
                       (interp a ρ)
                       (delay (interp b ρ))
-                      (delay (interp c ρ)) ρ)]
+                      (interp-fun2 c ρ))]
     [`(λ ,a) (interp-fun a ρ)]
-    [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
-
-;; Domain
-;; D := neu D_ne | fun [(var -> var) -> D → D]
-;; D_ne := var i | app D_ne D
-
-
-;; (: interp (-> Term (-> Term)))
-
-;; (define (interp a ρ)
-;;   (delay (match a
-;;     [`(var ,i) (force (ρ i))]
-;;     ['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 ρ))])))
+    [`(app ,a ,b) (ap (interp a ρ) b ρ)]))
 
 (: reify (-> V D Term))
 (define (reify n a)
@@ -79,15 +73,15 @@
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
     [`(neu ,a) (reify-neu n a)]))
 
-;; (define (extract-body a)
-;;   (match a
-;;     [`(λ ,a) a]
-;;     [_ (error "reify-neu: not reifiable")]))
-
 (: reify-neu (-> V D-ne Term))
 (define (reify-neu n a)
   (match a
-    ;; [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+    [`(ind ,a ,b ,c) (list 'ind
+                           (reify-neu n a)
+                           (reify n b)
+                           (reify (+ n 2)
+                                  (c (delay `(neu (idx ,n)))
+                                     (delay `(neu (idx ,(+ 1 n)))))))]
     [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
     [`(idx ,i) (list 'var (max 0 (- n (+ i 1))))]))
 
@@ -99,7 +93,7 @@
   (match a
     ['zero 0]
     [`(succ ,a) (scope a)]
-    (`(ind ,a ,b ,c) (max (scope a) (scope b) (scope c)))
+    (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
     [`(λ ,a) (max 0 (- (scope a) 1))]
     [`(app ,a ,b) (max (scope a) (scope b))]

From 814d5fa73d3b7f4ec34cd13b3d9c0f5b6a6c5f08 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Mon, 12 May 2025 00:58:49 -0400
Subject: [PATCH 7/7] Update the README file

---
 README.md | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 16ea495..a7ceb45 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# Kripke-style untyped NbE in racket
+# untyped NbE in racket
 [![status-badge](https://woodpecker.electriclam.com/api/badges/4/status.svg)](https://woodpecker.electriclam.com/repos/4)
 
 An implementation of normalization by evaluation loosely based on [A
@@ -10,7 +10,3 @@ Since the implementation is untyped, the `normalize` function only
 gives you β-normal forms. However, you can get a little bit of
 βη-equivalence by invoking Coquand's algorithm (`η-eq?`) on
 β-normal forms.
-
-I'm hoping to expand the repository into a benchmark suite where I can
-visualize the performance trade-off of type-directed NbE compared to
-untyped NbE composed with Coquand's algorithm.