.gitignore

@@ -1 +0,0 @@
-compiled

README.md

@@ -1,4 +1,4 @@
-# Untyped NbE in Typed 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

nbe-test.rkt

@@ -83,7 +83,6 @@
   `(succ ,a))
 
 (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id)
-(check βη-eq? `(app ,tm-id (U 0)) '(U 0))
 (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)
@@ -92,10 +91,5 @@
 (check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10))
 (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 1) '(succ (var 0)))) '(succ (succ (var 0))))
 (check-equal? (normalize (tm-padd (tm-pnat 10000) (tm-pnat 2000)))
               (tm-pnat 12000))
-(check βη-eq? (tm-padd (tm-pnat 10000) (tm-pnat 2000)) (tm-pnat 12000))
-(check βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 0)))
-(check βη-eq? `(Π (U 0) (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π (U 0) (Π (var 0) (var 1))))
-(check-false (βη-eq? '(U 0) '(var 0)))

nbe.rkt

@@ -5,36 +5,33 @@
 (define-type denv (-> V (Promise D)))
 (define-type V Nonnegative-Integer)
 (define-type Term (∪ 'zero
-                     'nat
                      (List 'succ Term)
                      (List 'var V)
                      (List 'λ Term)
                      (List 'app Term Term)
-                     (List 'ind Term Term Term)
-                     (List 'Π Term Term)
-                     (List 'U V)))
+                     (List 'ind Term Term Term)))
 
 (define-type D (∪ 'zero
-                  (List 'Π (Promise D) (-> (Promise D) D))
                   (List 'succ (Promise D))
                   (List 'fun (-> (Promise D) D))
-                  (List 'neu D-ne)
-                  (List 'U V)))
+                  (List 'neu D-ne)))
 
 (define-type D-ne (∪ (List 'app D-ne D)
                      (List 'idx V)
                      (List 'ind D-ne D (-> (Promise D) (Promise D) D))))
 
-(: ext (All (A) (-> (-> V A) A (-> V A))))
+(: ext (-> denv (Promise D) denv))
 (define (ext ρ a)
     (lambda (i)
     (if (zero? i)
         a
         (ρ (- i 1)))))
 
-(: interp-fun (-> Term denv (-> (Promise D) D)))
+
+
+(: interp-fun (-> Term denv D))
 (define (interp-fun a ρ)
-  (λ (x) (interp a (ext ρ x))))
+  (list 'fun (λ (x) (interp a (ext ρ x)))))
 
 (: interp-fun2 (-> Term denv (-> (Promise D) (Promise D) D)))
 (define (interp-fun2 a ρ)
@@ -45,21 +42,19 @@
   (match a
     [`(neu ,u) `(neu (ind ,u ,(force b) ,c))]
     ['zero (force b)]
-    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]
-    [_ (error "type-error: ind")]))
+    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]))
 
-(: ap (-> Term Term denv D))
+(: ap (-> D Term denv D))
 (define (ap a b ρ)
-  (match (interp a ρ)
+  (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 ρ)))]
-    [_ (error "type-error: ap")]))
+    [`(neu ,u) `(neu (app ,u ,(interp b ρ)))]))
 
 (: interp (-> Term denv D))
 (define (interp a ρ)
   (match a
-    [`(U ,_) a]
-    [`(Π ,A ,B) `(Π ,(delay (interp A ρ)) ,(interp-fun B ρ))]
     [`(var ,i) (force (ρ i))]
     ['zero 'zero]
     [`(succ ,a) `(succ ,(delay (interp a ρ)))]
@@ -67,26 +62,17 @@
                       (interp a ρ)
                       (delay (interp b ρ))
                       (interp-fun2 c ρ))]
-    [`(λ ,a) (list 'fun (interp-fun a ρ))]
-    [`(app ,a ,b) (ap a b ρ)]))
+    [`(λ ,a) (interp-fun a ρ)]
+    [`(app ,a ,b) (ap (interp a ρ) b ρ)]))
 
 (: reify (-> V D Term))
 (define (reify n a)
   (match a
-    [`(Π ,A ,B) `(Π ,(reify n (force A)) ,(reify (+ n 1) (B (delay `(neu (idx ,n))))))]
     ['zero 'zero]
     [`(succ ,a) `(succ ,(reify n (force a)))]
-    [`(U ,_) a]
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
     [`(neu ,a) (reify-neu n a)]))
 
-(: var-to-idx (-> V V V))
-(define (var-to-idx s v)
-  (let ([ret (- s (+ v 1))])
-    (if (< ret 0)
-        (error "variable to index conversion failed")
-        ret)))
-
 (: reify-neu (-> V D-ne Term))
 (define (reify-neu n a)
   (match a
@@ -97,16 +83,14 @@
                                   (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 (var-to-idx n i))]))
+    [`(idx ,i) (list 'var (max 0 (- n (+ i 1))))]))
 
 (: idsub (-> V V D))
-(define (idsub s i) `(neu (idx ,(var-to-idx s i))))
+(define (idsub s i) `(neu (idx ,(max 0 (- s (+ i 1))))))
 
 (: scope (-> Term V))
 (define (scope a)
   (match a
-    [`(Π ,A ,B) (max (scope A) (- (scope B) 2))]
-    [`(U ,_) 0]
     ['zero 0]
     [`(succ ,a) (scope a)]
     (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
@@ -120,52 +104,56 @@
   (let ([sa (scope a)])
     (reify sa (interp a (λ (x) (delay (idsub sa x)))))))
 
-(: up (-> V (-> V Term) (-> V Term)))
-(define (up n ρ)
-  (ext (λ ([x : V]) (subst (λ (i) `(var ,(+ i n))) (ρ x))) '(var 0)))
+;; (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))]))
 
-(: subst (-> (-> V Term) Term Term))
-(define (subst ρ a)
-  (match a
-    [`(U ,_) a]
-    [`(Π ,A ,B) `(Π ,(subst ρ A) ,(subst (up 1 ρ) B))]
-    [`(var ,i) (ρ i)]
-    [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
-    [`(λ ,a) `(λ ,(subst (up 1 ρ) a))]
-    ['zero 'zero]
-    [`(succ ,a) `(succ ,(subst ρ a))]
-    [`(ind ,a ,b ,c) `(ind ,(subst ρ a) ,(subst ρ b) ,(subst (up 2 ρ) c))]))
+;; (define (idsub-tm i) `(var ,i))
+;; (define (subst1 b a)
+;;   (subst (ext idsub-tm b) a))
 
-(: idsub-tm (-> V Term))
-(define (idsub-tm i) `(var ,i))
-(: subst1 (-> Term Term Term))
-(define (subst1 b a)
-  (subst (ext idsub-tm b) 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))])]))
 
-;; Coquand's algorithm but for β-normal forms
-(: η-eq? (-> Term Term Boolean))
-(define (η-eq? a b)
-  (match (list a b)
-    [`((U ,i) (U ,j)) (eqv? i j) ]
-    [`((Π ,A0 ,B0) (Π ,A1 ,B1))
-     (and (η-eq? A0 A1) (η-eq? B0 B1))]
-    ['(zero zero) true]
-    [`((succ ,a) (succ ,b)) (η-eq? a b)]
-    [`((ind ,a ,b ,c) (ind ,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))])]))
 
-(: βη-eq? (-> Term Term Boolean))
-(define (βη-eq? a b)
-  (η-eq? (normalize a) (normalize b)))
+;; ;; Coquand's algorithm but for β-normal forms
+;; (: η-eq? (-> Term Term Boolean))
+;; (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)))
 
 (: β-eq? (-> Term Term Boolean))
 (define (β-eq? a b)
   (equal? (normalize a) (normalize b)))
 
-(provide reify interp normalize β-eq? Term D V βη-eq?)
+(provide reify interp normalize β-eq? Term D V)