From 31e29cf18ed6be74e8e6327aab042217748b7610 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 16:57:44 -0400 Subject: [PATCH 1/8] Add more exports --- nbe.rkt | 2 +- type-checker.rkt | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) create mode 100644 type-checker.rkt diff --git a/nbe.rkt b/nbe.rkt index 2c309dd..62bfb4c 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -168,4 +168,4 @@ (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 D-ne V βη-eq? ext subst1 subst idsub-tm) diff --git a/type-checker.rkt b/type-checker.rkt new file mode 100644 index 0000000..0ad77af --- /dev/null +++ b/type-checker.rkt @@ -0,0 +1,2 @@ +#lang typed/racket +(require "nbe.rkt") From ff0e48af9523195ef599652406bbd725b4f1acbf Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 13 May 2025 15:38:03 -0400 Subject: [PATCH 2/8] Port Coquand's algorithm to the semantic domain --- nbe.rkt | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/nbe.rkt b/nbe.rkt index 62bfb4c..85f0adc 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -70,6 +70,38 @@ [`(λ ,a) (list 'fun (interp-fun a ρ))] [`(app ,a ,b) (ap a b ρ)])) +(: open-dom (-> V (-> (Promise D) D) D)) +(define (open-dom n f) + (f (delay `(neu (idx ,n))))) + +(: open-dom2 (-> V (-> (Promise D) (Promise D) D) D)) +(define (open-dom2 n f) + (f (delay `(neu (idx ,n))) (delay `(neu (idx ,(add1 n)))))) + +(: compare (-> V D D Boolean)) +(define (compare n a0 a1) + (match (list a0 a1) + [`((Π ,A0 ,B0) (Π ,A1 ,B1)) + (and (compare n (force A0) (force A1)) + (compare (add1 n) (open-dom n B0) (open-dom n B1)))] + ['(nat nat) #t] + [`((U ,i) (U ,j)) (eqv? i j)] + ['(zero zero) #t] + [`((succ ,a) (succ ,b)) (compare n (force a) (force b))] + [`((fun ,f) (neu ,u)) (compare (add1 n) (open-dom n f) `(neu (app ,u (neu (idx ,n)))))] + [`((neu ,_) (fun ,_)) (compare n a1 a0)] + [`((neu ,a) (neu ,b)) (compare-neu n a b)] + [(list _ _) #f])) + +(: compare-neu (-> V D-ne D-ne Boolean)) +(define (compare-neu n a0 a1) + (match (list a0 a1) + [`((idx ,i) (idx ,j)) (eqv? i j)] + [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (compare-neu n u0 u1) (compare n v0 v1))] + [`((ind ,a0 ,b0 ,c0) (ind ,a1 ,b1 ,c1)) (and (compare-neu n a0 a1) + (compare n b0 b1) + (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))])) + (: reify (-> V D Term)) (define (reify n a) (match a @@ -143,6 +175,7 @@ (subst (ext idsub-tm b) a)) ;; Coquand's algorithm but for β-normal forms +;; Subsumed by the compare function (: η-eq? (-> Term Term Boolean)) (define (η-eq? a b) (match (list a b) From 1d04feebec1abfc9daa0e7b42e56ebce0854035c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 13 May 2025 15:44:17 -0400 Subject: [PATCH 3/8] Add missing case for lambdas --- nbe-test.rkt | 5 +++++ nbe.rkt | 8 +++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/nbe-test.rkt b/nbe-test.rkt index 300a90b..25c5b04 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -98,4 +98,9 @@ (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? '(succ zero) '(var 0))) +(check βη-eq? (tm-app (tm-var 0) (tm-var 1)) (tm-app (tm-var 0) (tm-var 1))) +(check βη-eq? (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)) (tm-ind (tm-var 0) (tm-var 1) (tm-var 2))) +(check-false (βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 1)))) +(check-false (βη-eq? (tm-app (tm-var 0) (tm-var 0)) (tm-ind (tm-var 0) 'zero 'zero))) (check-false (βη-eq? '(U 0) '(var 0))) diff --git a/nbe.rkt b/nbe.rkt index 85f0adc..b083ddb 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -91,7 +91,7 @@ [`((fun ,f) (neu ,u)) (compare (add1 n) (open-dom n f) `(neu (app ,u (neu (idx ,n)))))] [`((neu ,_) (fun ,_)) (compare n a1 a0)] [`((neu ,a) (neu ,b)) (compare-neu n a b)] - [(list _ _) #f])) + [_ #f])) (: compare-neu (-> V D-ne D-ne Boolean)) (define (compare-neu n a0 a1) @@ -100,7 +100,8 @@ [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (compare-neu n u0 u1) (compare n v0 v1))] [`((ind ,a0 ,b0 ,c0) (ind ,a1 ,b1 ,c1)) (and (compare-neu n a0 a1) (compare n b0 b1) - (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))])) + (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))] + [_ #f])) (: reify (-> V D Term)) (define (reify n a) @@ -195,7 +196,8 @@ (: βη-eq? (-> Term Term Boolean)) (define (βη-eq? a b) - (η-eq? (normalize a) (normalize b))) + (let ([n (max (scope a) (scope b))]) + (compare n (interp a (λ (x) (delay (idsub n x)))) (interp b (λ (x) (delay (idsub n x))))))) (: β-eq? (-> Term Term Boolean)) (define (β-eq? a b) From 193be1168ec32fec4fdd498ef9cfac13ebfd8a4c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 13 May 2025 16:43:00 -0400 Subject: [PATCH 4/8] Add stub for the typechecker --- nbe.rkt | 2 -- type-checker.rkt | 28 ++++++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 2 deletions(-) diff --git a/nbe.rkt b/nbe.rkt index b083ddb..ffded3a 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -1,6 +1,4 @@ #lang typed/racket -;; Grammar (Λ) -;; t := λ t | app t t | i (define-type denv (-> V (Promise D))) (define-type V Nonnegative-Integer) diff --git a/type-checker.rkt b/type-checker.rkt index 0ad77af..d895735 100644 --- a/type-checker.rkt +++ b/type-checker.rkt @@ -1,2 +1,30 @@ #lang typed/racket + (require "nbe.rkt") + +(define-type context (Immutable-HashTable V Term)) + +(: context-len (-> context V)) +(define (context-len Γ) + (hash-count Γ)) + +(: context-ext (-> context Term context)) +(define (context-ext Γ A) + (hash-set Γ (context-len Γ) A)) + +(: context-get (-> context V Term)) +(define (context-get Γ i) + (if (< i (context-len Γ)) + (subst (λ (j) `(var ,(+ i j 1))) (hash-ref Γ (- (context-len Γ) (add1 i)))) + (error "context-get: out of bound"))) + +(: context-empty context) +(define context-empty (hash)) + +(: synth (-> context Term Term)) +(define (synth Γ a) + (error "unimplmented")) + +(: check (-> context Term D Boolean)) +(define (check Γ a A) + (error "unimplemented")) From f5fe22c419afcfd383d932946999ef34bf78f507 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 13 May 2025 17:08:48 -0400 Subject: [PATCH 5/8] Minor --- nbe.rkt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/nbe.rkt b/nbe.rkt index ffded3a..67745d9 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -146,6 +146,10 @@ [`(app ,a ,b) (max (scope a) (scope b))] [`(var ,i) (+ i 1)])) +(: interp-with-scope (-> V Term D)) +(define (interp-with-scope n a) + (interp a (λ (x) (delay (idsub n x))))) + (: normalize (-> Term Term)) (define (normalize a) (let ([sa (scope a)]) From c6528de647e55df9d78f0294edfbd9c44e2ea634 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 13 May 2025 19:13:44 -0400 Subject: [PATCH 6/8] Remove levels from the universe --- nbe-test.rkt | 6 +++--- nbe.rkt | 16 ++++++++-------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/nbe-test.rkt b/nbe-test.rkt index 25c5b04..68208df 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -83,7 +83,7 @@ `(succ ,a)) (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id) -(check βη-eq? `(app ,tm-id (U 0)) '(U 0)) +(check βη-eq? `(app ,tm-id U) 'U) (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) @@ -97,10 +97,10 @@ (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 βη-eq? `(Π U (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π U (Π (var 0) (var 1)))) (check-false (βη-eq? '(succ zero) '(var 0))) (check βη-eq? (tm-app (tm-var 0) (tm-var 1)) (tm-app (tm-var 0) (tm-var 1))) (check βη-eq? (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)) (tm-ind (tm-var 0) (tm-var 1) (tm-var 2))) (check-false (βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 1)))) (check-false (βη-eq? (tm-app (tm-var 0) (tm-var 0)) (tm-ind (tm-var 0) 'zero 'zero))) -(check-false (βη-eq? '(U 0) '(var 0))) +(check-false (βη-eq? 'U '(var 0))) diff --git a/nbe.rkt b/nbe.rkt index 67745d9..86f2917 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -10,14 +10,14 @@ (List 'app Term Term) (List 'ind Term Term Term) (List 'Π Term Term) - (List 'U V))) + 'U)) (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))) + 'U)) (define-type D-ne (∪ (List 'app D-ne D) (List 'idx V) @@ -56,7 +56,7 @@ (: interp (-> Term denv D)) (define (interp a ρ) (match a - [`(U ,_) a] + ['U a] [`(Π ,A ,B) `(Π ,(delay (interp A ρ)) ,(interp-fun B ρ))] [`(var ,i) (force (ρ i))] ['zero 'zero] @@ -83,7 +83,7 @@ (and (compare n (force A0) (force A1)) (compare (add1 n) (open-dom n B0) (open-dom n B1)))] ['(nat nat) #t] - [`((U ,i) (U ,j)) (eqv? i j)] + ['(U U) #t] ['(zero zero) #t] [`((succ ,a) (succ ,b)) (compare n (force a) (force b))] [`((fun ,f) (neu ,u)) (compare (add1 n) (open-dom n f) `(neu (app ,u (neu (idx ,n)))))] @@ -107,7 +107,7 @@ [`(Π ,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] + ['U a] [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))] [`(neu ,a) (reify-neu n a)])) @@ -137,7 +137,7 @@ (define (scope a) (match a [`(Π ,A ,B) (max (scope A) (- (scope B) 2))] - [`(U ,_) 0] + ['U 0] ['zero 0] [`(succ ,a) (scope a)] (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2))) @@ -162,7 +162,7 @@ (: subst (-> (-> V Term) Term Term)) (define (subst ρ a) (match a - [`(U ,_) a] + ['U a] [`(Π ,A ,B) `(Π ,(subst ρ A) ,(subst (up 1 ρ) B))] [`(var ,i) (ρ i)] [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))] @@ -182,7 +182,7 @@ (: η-eq? (-> Term Term Boolean)) (define (η-eq? a b) (match (list a b) - [`((U ,i) (U ,j)) (eqv? i j) ] + ['(U U) #t ] [`((Π ,A0 ,B0) (Π ,A1 ,B1)) (and (η-eq? A0 A1) (η-eq? B0 B1))] ['(zero zero) true] From 9dc599396ab517c134b9338e8187ebed1406c7df Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 30 May 2025 16:41:50 -0400 Subject: [PATCH 7/8] Tighten up the signature --- nbe.rkt | 23 +++++++++++++++++++++-- type-checker.rkt | 6 +++++- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/nbe.rkt b/nbe.rkt index 86f2917..9c6701d 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -2,6 +2,7 @@ (define-type denv (-> V (Promise D))) (define-type V Nonnegative-Integer) + (define-type Term (∪ 'zero 'nat (List 'succ Term) @@ -12,6 +13,24 @@ (List 'Π Term Term) 'U)) +(define-type Neu (∪ (List 'ind Neu Norm Norm) + (List 'var V) + (List 'app Neu Norm))) + +(define-type Norm (∪ Neu + 'zero + 'nat + (List 'λ Norm) + (List 'U V) + (List 'succ Norm) + (List 'Π Norm Norm))) + +(: embed (-> Neu Term)) +(define (embed a) a) + +(: embed-norm (-> Norm Term)) +(define (embed-norm a) a) + (define-type D (∪ 'zero (List 'Π (Promise D) (-> (Promise D) D)) (List 'succ (Promise D)) @@ -101,7 +120,7 @@ (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))] [_ #f])) -(: reify (-> V D Term)) +(: reify (-> V D Norm)) (define (reify n a) (match a [`(Π ,A ,B) `(Π ,(reify n (force A)) ,(reify (+ n 1) (B (delay `(neu (idx ,n))))))] @@ -118,7 +137,7 @@ (error "variable to index conversion failed") ret))) -(: reify-neu (-> V D-ne Term)) +(: reify-neu (-> V D-ne Neu)) (define (reify-neu n a) (match a [`(ind ,a ,b ,c) (list 'ind diff --git a/type-checker.rkt b/type-checker.rkt index d895735..5b42c9c 100644 --- a/type-checker.rkt +++ b/type-checker.rkt @@ -23,7 +23,11 @@ (: synth (-> context Term Term)) (define (synth Γ a) - (error "unimplmented")) + (match a + [`(var ,i) (context-get Γ i)] + [`(app ,a ,b) + (let ([A (synth Γ a)] + [D (interp-with-scope (context-len Γ) A)]))])) (: check (-> context Term D Boolean)) (define (check Γ a A) From cc24f42e9107d8c42d2cacb2d216da96da075845 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 30 May 2025 16:43:54 -0400 Subject: [PATCH 8/8] Minor --- nbe.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nbe.rkt b/nbe.rkt index 9c6701d..cf227be 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -21,7 +21,7 @@ 'zero 'nat (List 'λ Norm) - (List 'U V) + 'U (List 'succ Norm) (List 'Π Norm Norm)))