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

Add back beta-eta equality
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Yiyun Liu 2025-05-12 11:24:56 -04:00
parent aa233cc86b
commit 755119316b
2 changed files with 39 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

3
nbe-test.rkt
View file

@ -91,5 +91,8 @@
(check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10)) (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-pnat 0) (var 1))) (tm-pnat 2))
(check-equal? (normalize `(ind ,(tm-pnat 3) ,tm-loop (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))) (check-equal? (normalize (tm-padd (tm-pnat 10000) (tm-pnat 2000)))
(tm-pnat 12000)) (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)))

83
nbe.rkt
View file

@ -20,15 +20,13 @@
(List 'idx V) (List 'idx V)
(List 'ind D-ne D (-> (Promise D) (Promise D) D)))) (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) (define (ext ρ a)
(lambda (i) (lambda (i)
(if (zero? i) (if (zero? i)
a a
(ρ (- i 1))))) (ρ (- i 1)))))
(: interp-fun (-> Term denv D)) (: interp-fun (-> Term denv D))
(define (interp-fun a ρ) (define (interp-fun a ρ)
(list 'fun (λ (x) (interp a (ext ρ x))))) (list 'fun (λ (x) (interp a (ext ρ x)))))
@ -104,56 +102,47 @@
(let ([sa (scope a)]) (let ([sa (scope a)])
(reify sa (interp a (λ (x) (delay (idsub sa x))))))) (reify sa (interp a (λ (x) (delay (idsub sa x)))))))
;; (define (subst ρ a) (: up (-> V (-> V Term) (-> V Term)))
;; (match a (define (up n ρ)
;; [`(var ,i) (ρ i)] (ext (λ ([x : V]) (subst (λ (i) `(var ,(+ i n))) (ρ x))) '(var 0)))
;; [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
;; [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
;; '(var 0)) a))]))
;; (define (idsub-tm i) `(var ,i)) (: subst (-> (-> V Term) Term Term))
;; (define (subst1 b a) (define (subst ρ a)
;; (subst (ext idsub-tm b) 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) (: idsub-tm (-> V Term))
;; (match a (define (idsub-tm i) `(var ,i))
;; [(list 'var _) a] (: subst1 (-> Term Term Term))
;; [(list 'λ a) `(λ ,(eval-tm a))] (define (subst1 b a)
;; [(list 'app a b) (subst (ext idsub-tm b) a))
;; (match (eval-tm a)
;; [(list 'λ a) (eval-tm (subst1 b a))]
;; [v `(app ,v ,(eval-tm b))])]))
;; (define (eval-tm-strict a) ;; Coquand's algorithm but for β-normal forms
;; (match a (: η-eq? (-> Term Term Boolean))
;; [(list 'var _) a] (define (η-eq? a b)
;; [(list 'λ a) `(λ ,(eval-tm-strict a))] (match (list a b)
;; [(list 'app a b) ['(zero zero) true]
;; (match (eval-tm-strict a) [`((succ ,a) (succ ,b)) (η-eq? a b)]
;; [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))] [`((ind ,a ,b ,c) (ind ,a0 ,b0 ,c0))
;; [v `(app ,v ,(eval-tm-strict b))])])) (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))
;; (: η-eq? (-> Term Term Boolean)) (define (βη-eq? a b)
;; (define (η-eq? a b) (η-eq? (normalize a) (normalize 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)) (: β-eq? (-> Term Term Boolean))
(define (β-eq? a b) (define (β-eq? a b)
(equal? (normalize a) (normalize b))) (equal? (normalize a) (normalize b)))
(provide reify interp normalize β-eq? Term D V) (provide reify interp normalize β-eq? Term D V βη-eq?)