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

Add back peano numbers

Browse source
This commit is contained in:
Yiyun Liu 2025-05-11 17:55:50 -04:00
parent 212cbdbceb
commit eb4291f6a0
2 changed files with 32 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

30
nbe-test.rkt
View file

@ -23,9 +23,10 @@
(: tm-pair Term) (: tm-pair Term)
(define tm-pair `(λ (λ (λ ,(tm-app '(var 0) '(var 2) '(var 1)))))) (define tm-pair `(λ (λ (λ ,(tm-app '(var 0) '(var 2) '(var 1))))))
;; (define tm-fix (: tm-fix Term)
;; (let ([g (tm-abs (tm-app (tm-var 1) (tm-app (tm-var 0) (tm-var 0))))]) (define tm-fix
;; (tm-abs (tm-app g g)))) (let ([g (tm-abs (tm-app (tm-var 1) (tm-app (tm-var 0) (tm-var 0))))])
(tm-abs (tm-app g g))))
(: tm-zero Term) (: tm-zero Term)
(define tm-zero tm-snd) (define tm-zero tm-snd)
@ -51,10 +52,23 @@
(tm-suc (tm-nat (- n 1))) (tm-suc (tm-nat (- n 1)))
tm-zero)) tm-zero))
;; (define (tm-pnat n) (: tm-const Term)
;; (if (positive? n) (define tm-const tm-fst)
;; `(succ ,(tm-pnat (- n 1)))
;; 'zero)) (: tm-loop Term)
(define tm-loop
(let ([g (tm-abs (tm-app (tm-var 0) (tm-var 0)))])
(tm-app g g)))
(: tm-nat-to-pnat Term)
(define tm-nat-to-pnat
(tm-abs (tm-app (tm-var 0) (tm-abs '(succ (var 0))) 'zero)))
(: tm-pnat (-> V Term))
(define (tm-pnat n)
(if (positive? n)
`(succ ,(tm-pnat (- n 1)))
'zero))
;; (define (tm-ifz a b c) ;; (define (tm-ifz a b c)
;; `(if-zero ,a ,b ,c)) ;; `(if-zero ,a ,b ,c))
@ -75,6 +89,8 @@
(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)
(check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499)))) (check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
(check-equal? (normalize (tm-app tm-const (tm-nat 0) tm-loop)) (normalize (tm-nat 0)))
(check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10))
;; (check-equal? (normalize (tm-mult (tm-nat 3) (tm-nat 2))) (normalize (tm-nat 6))) ;; (check-equal? (normalize (tm-mult (tm-nat 3) (tm-nat 2))) (normalize (tm-nat 6)))
;; (check-equal? (normalize (tm-mult (tm-nat 11) (tm-nat 116))) (normalize (tm-nat 1276))) ;; (check-equal? (normalize (tm-mult (tm-nat 11) (tm-nat 116))) (normalize (tm-nat 1276)))
;; (check η-eq? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499)))) ;; (check η-eq? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))

17
nbe.rkt
View file

@ -3,9 +3,11 @@
;; t := λ t | app t t | i ;; t := λ t | app t t | i
(define-type V Nonnegative-Integer) (define-type V Nonnegative-Integer)
(define-type Term (∪ (List 'var V) (List 'λ Term) (List 'app Term Term))) (define-type Term (∪ 'zero (List 'succ Term) (List 'var V) (List 'λ Term) (List 'app Term Term)))
(define-type D (∪ (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
(define-type D (∪ 'zero (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) (List 'neu D-ne)))
(define-type D-ne (∪ (List 'app D-ne D) (List 'idx V))) (define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
(: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D)))) (: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
@ -30,8 +32,8 @@
(define (interp a ρ) (define (interp a ρ)
(match a (match a
[`(var ,i) (force (ρ i))] [`(var ,i) (force (ρ i))]
;; ['zero 'zero] ['zero 'zero]
;; [`(succ ,a) `(succ ,(interp a ρ))] [`(succ ,a) `(succ ,(delay (interp a ρ)))]
;; [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))] ;; [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
[`(λ ,a) (interp-fun a ρ)] [`(λ ,a) (interp-fun a ρ)]
[`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])) [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
@ -55,11 +57,10 @@
(: reify (-> V D Term)) (: reify (-> V D Term))
(define (reify n a) (define (reify n a)
(match a (match a
;; ['zero 'zero] ['zero 'zero]
;; [`(succ ,a) `(succ ,(reify n a))] [`(succ ,a) `(succ ,(reify n (force 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)]))
))
;; (define (extract-body a) ;; (define (extract-body a)
;; (match a ;; (match a