From c2faa6b4b6bc95f805467ce0cedc4a1868203f13 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 5 May 2025 00:46:52 -0400 Subject: [PATCH 1/5] Update README --- README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 16ea495..14c0e91 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,5 @@ 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. +A more efficient version of NbE based on de Bruijn levels (inverted de +bruijn indices) can be found in the `debruijn-levels` branch. From aa233cc86b3213198a5dc328fea183a0f3409ecc Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 01:00:46 -0400 Subject: [PATCH 2/5] Minor --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a7ceb45..20a9095 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# untyped NbE in racket +# Untyped NbE in Typed 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 From 755119316b389d47f43c116c477f665624e7eada Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 11:24:56 -0400 Subject: [PATCH 3/5] Add back beta-eta equality --- nbe-test.rkt | 3 ++ nbe.rkt | 83 +++++++++++++++++++++++----------------------------- 2 files changed, 39 insertions(+), 47 deletions(-) diff --git a/nbe-test.rkt b/nbe-test.rkt index b7b4b81..3dca756 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -91,5 +91,8 @@ (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))) diff --git a/nbe.rkt b/nbe.rkt index 57db916..d1b8e20 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -20,15 +20,13 @@ (List 'idx V) (List 'ind D-ne D (-> (Promise D) (Promise D) D)))) -(: ext (-> denv (Promise D) denv)) +(: ext (All (A) (-> (-> V A) A (-> V A)))) (define (ext ρ a) (lambda (i) (if (zero? i) a (ρ (- i 1))))) - - (: interp-fun (-> Term denv D)) (define (interp-fun a ρ) (list 'fun (λ (x) (interp a (ext ρ x))))) @@ -104,56 +102,47 @@ (let ([sa (scope a)]) (reify sa (interp a (λ (x) (delay (idsub sa x))))))) -;; (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))])) +(: up (-> V (-> V Term) (-> V Term))) +(define (up n ρ) + (ext (λ ([x : V]) (subst (λ (i) `(var ,(+ i n))) (ρ x))) '(var 0))) -;; (define (idsub-tm i) `(var ,i)) -;; (define (subst1 b a) -;; (subst (ext idsub-tm b) a)) +(: subst (-> (-> V Term) Term Term)) +(define (subst ρ a) + (match a + [`(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 (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))])])) +(: 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-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 +(: η-eq? (-> Term Term Boolean)) +(define (η-eq? a b) + (match (list a b) + ['(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])) -;; ;; 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) + (η-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) +(provide reify interp normalize β-eq? Term D V βη-eq?) From da9ea4ed936ec1f77ce2b329d0a665938ef9fb68 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 12:07:37 -0400 Subject: [PATCH 4/5] Add universes --- nbe-test.rkt | 2 ++ nbe.rkt | 25 ++++++++++++++++--------- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/nbe-test.rkt b/nbe-test.rkt index 3dca756..c85d1ff 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -83,6 +83,7 @@ `(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) @@ -96,3 +97,4 @@ (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-false (βη-eq? '(U 0) '(var 0))) diff --git a/nbe.rkt b/nbe.rkt index d1b8e20..5cda917 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -9,12 +9,14 @@ (List 'var V) (List 'λ Term) (List 'app Term Term) - (List 'ind Term Term Term))) + (List 'ind Term Term Term) + (List 'U V))) (define-type D (∪ 'zero (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) - (List 'neu D-ne))) + (List 'neu D-ne) + (List 'U V))) (define-type D-ne (∪ (List 'app D-ne D) (List 'idx V) @@ -40,19 +42,20 @@ (match a [`(neu ,u) `(neu (ind ,u ,(force b) ,c))] ['zero (force b)] - [`(succ ,a) (c a (delay (interp-ind (force a) b c)))])) + [`(succ ,a) (c a (delay (interp-ind (force a) b c)))] + [_ (error "type-error: ind")])) -(: ap (-> D Term denv D)) +(: ap (-> Term Term denv D)) (define (ap a b ρ) - (match a - ['zero (error "type-error: ap zero")] - [`(succ ,_) (error "type-error: ap succ")] + (match (interp a ρ) [`(fun ,f) (f (delay (interp b ρ)))] - [`(neu ,u) `(neu (app ,u ,(interp b ρ)))])) + [`(neu ,u) `(neu (app ,u ,(interp b ρ)))] + [_ (error "type-error: ap")])) (: interp (-> Term denv D)) (define (interp a ρ) (match a + [`(U ,_) a] [`(var ,i) (force (ρ i))] ['zero 'zero] [`(succ ,a) `(succ ,(delay (interp a ρ)))] @@ -61,13 +64,14 @@ (delay (interp b ρ)) (interp-fun2 c ρ))] [`(λ ,a) (interp-fun a ρ)] - [`(app ,a ,b) (ap (interp a ρ) b ρ)])) + [`(app ,a ,b) (ap a b ρ)])) (: reify (-> V D Term)) (define (reify n a) (match a ['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)])) @@ -89,6 +93,7 @@ (: scope (-> Term V)) (define (scope a) (match a + [`(U ,_) 0] ['zero 0] [`(succ ,a) (scope a)] (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2))) @@ -109,6 +114,7 @@ (: subst (-> (-> V Term) Term Term)) (define (subst ρ a) (match a + [`(U ,_) a] [`(var ,i) (ρ i)] [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))] [`(λ ,a) `(λ ,(subst (up 1 ρ) a))] @@ -126,6 +132,7 @@ (: η-eq? (-> Term Term Boolean)) (define (η-eq? a b) (match (list a b) + [`((U ,i) (U ,j)) (eqv? i j) ] ['(zero zero) true] [`((succ ,a) (succ ,b)) (η-eq? a b)] [`((ind ,a ,b ,c) (ind ,a0 ,b0 ,c0)) From f418c383f3edeff41396cadb4589114b729397aa Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 16:28:54 -0400 Subject: [PATCH 5/5] Add pi types --- .gitignore | 1 + nbe-test.rkt | 1 + nbe.rkt | 26 +++++++++++++++++++++----- 3 files changed, 23 insertions(+), 5 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a13427f --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +compiled \ No newline at end of file diff --git a/nbe-test.rkt b/nbe-test.rkt index c85d1ff..300a90b 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -97,4 +97,5 @@ (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))) diff --git a/nbe.rkt b/nbe.rkt index 5cda917..2c309dd 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -5,14 +5,17 @@ (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))) (define-type D (∪ 'zero + (List 'Π (Promise D) (-> (Promise D) D)) (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) (List 'neu D-ne) @@ -29,9 +32,9 @@ a (ρ (- i 1))))) -(: interp-fun (-> Term denv D)) +(: interp-fun (-> Term denv (-> (Promise D) D))) (define (interp-fun a ρ) - (list 'fun (λ (x) (interp a (ext ρ x))))) + (λ (x) (interp a (ext ρ x)))) (: interp-fun2 (-> Term denv (-> (Promise D) (Promise D) D))) (define (interp-fun2 a ρ) @@ -56,6 +59,7 @@ (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 ρ)))] @@ -63,18 +67,26 @@ (interp a ρ) (delay (interp b ρ)) (interp-fun2 c ρ))] - [`(λ ,a) (interp-fun a ρ)] + [`(λ ,a) (list 'fun (interp-fun a ρ))] [`(app ,a ,b) (ap 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 @@ -85,14 +97,15 @@ (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))))])) + [`(idx ,i) (list 'var (var-to-idx n i))])) (: idsub (-> V V D)) -(define (idsub s i) `(neu (idx ,(max 0 (- s (+ i 1)))))) +(define (idsub s i) `(neu (idx ,(var-to-idx s i)))) (: scope (-> Term V)) (define (scope a) (match a + [`(Π ,A ,B) (max (scope A) (- (scope B) 2))] [`(U ,_) 0] ['zero 0] [`(succ ,a) (scope a)] @@ -115,6 +128,7 @@ (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))] @@ -133,6 +147,8 @@ (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))