yiyunliu/nbe-kripke-racket
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove levels from the universe

Browse source
This commit is contained in:
Yiyun Liu 2025-05-13 19:13:44 -04:00
parent f5fe22c419
commit c6528de647
2 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
nbe-test.rkt
View file

@ -83,7 +83,7 @@
`(succ ,a)) `(succ ,a))
(check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id) (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-snd)) tm-fst)
(check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id) (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-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
@ -97,10 +97,10 @@
(tm-pnat 12000)) (tm-pnat 12000))
(check βη-eq? (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? (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-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-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 βη-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-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? (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)))

16
nbe.rkt
View file

@ -10,14 +10,14 @@
(List 'app Term Term) (List 'app Term Term)
(List 'ind Term Term Term) (List 'ind Term Term Term)
(List 'Π Term Term) (List 'Π Term Term)
(List 'U V))) 'U))
(define-type D (∪ 'zero (define-type D (∪ 'zero
(List 'Π (Promise D) (-> (Promise D) D)) (List 'Π (Promise D) (-> (Promise D) D))
(List 'succ (Promise D)) (List 'succ (Promise D))
(List 'fun (-> (Promise D) D)) (List 'fun (-> (Promise D) D))
(List 'neu D-ne) (List 'neu D-ne)
(List 'U V))) 'U))
(define-type D-ne (∪ (List 'app D-ne D) (define-type D-ne (∪ (List 'app D-ne D)
(List 'idx V) (List 'idx V)
@ -56,7 +56,7 @@
(: interp (-> Term denv D)) (: interp (-> Term denv D))
(define (interp a ρ) (define (interp a ρ)
(match a (match a
[`(U ,_) a] ['U a]
[`(Π ,A ,B) `(Π ,(delay (interp A ρ)) ,(interp-fun B ρ))] [`(Π ,A ,B) `(Π ,(delay (interp A ρ)) ,(interp-fun B ρ))]
[`(var ,i) (force (ρ i))] [`(var ,i) (force (ρ i))]
['zero 'zero] ['zero 'zero]
@ -83,7 +83,7 @@
(and (compare n (force A0) (force A1)) (and (compare n (force A0) (force A1))
(compare (add1 n) (open-dom n B0) (open-dom n B1)))] (compare (add1 n) (open-dom n B0) (open-dom n B1)))]
['(nat nat) #t] ['(nat nat) #t]
[`((U ,i) (U ,j)) (eqv? i j)] ['(U U) #t]
['(zero zero) #t] ['(zero zero) #t]
[`((succ ,a) (succ ,b)) (compare n (force a) (force b))] [`((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)))))] [`((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))))))] [`(Π ,A ,B) `(Π ,(reify n (force A)) ,(reify (+ n 1) (B (delay `(neu (idx ,n))))))]
['zero 'zero] ['zero 'zero]
[`(succ ,a) `(succ ,(reify n (force a)))] [`(succ ,a) `(succ ,(reify n (force a)))]
[`(U ,_) a] ['U a]
[`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))] [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
[`(neu ,a) (reify-neu n a)])) [`(neu ,a) (reify-neu n a)]))
@ -137,7 +137,7 @@
(define (scope a) (define (scope a)
(match a (match a
[`(Π ,A ,B) (max (scope A) (- (scope B) 2))] [`(Π ,A ,B) (max (scope A) (- (scope B) 2))]
[`(U ,_) 0] ['U 0]
['zero 0] ['zero 0]
[`(succ ,a) (scope a)] [`(succ ,a) (scope a)]
(`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2))) (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
@ -162,7 +162,7 @@
(: subst (-> (-> V Term) Term Term)) (: subst (-> (-> V Term) Term Term))
(define (subst ρ a) (define (subst ρ a)
(match a (match a
[`(U ,_) a] ['U a]
[`(Π ,A ,B) `(Π ,(subst ρ A) ,(subst (up 1 ρ) B))] [`(Π ,A ,B) `(Π ,(subst ρ A) ,(subst (up 1 ρ) B))]
[`(var ,i) (ρ i)] [`(var ,i) (ρ i)]
[`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))] [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
@ -182,7 +182,7 @@
(: η-eq? (-> Term Term Boolean)) (: η-eq? (-> Term Term Boolean))
(define (η-eq? a b) (define (η-eq? a b)
(match (list a b) (match (list a b)
[`((U ,i) (U ,j)) (eqv? i j) ] ['(U U) #t ]
[`((Π ,A0 ,B0) (Π ,A1 ,B1)) [`((Π ,A0 ,B0) (Π ,A1 ,B1))
(and (η-eq? A0 A1) (η-eq? B0 B1))] (and (η-eq? A0 A1) (η-eq? B0 B1))]
['(zero zero) true] ['(zero zero) true]