From cc59960e790ce1e3fcf463e810167d7d54242844 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 00:48:47 -0400 Subject: [PATCH] Finish adding natural numbers --- nbe-test.rkt | 35 ++++++++++++--------------- nbe.rkt | 68 ++++++++++++++++++++++++---------------------------- 2 files changed, 46 insertions(+), 57 deletions(-) diff --git a/nbe-test.rkt b/nbe-test.rkt index 04d6697..b7b4b81 100644 --- a/nbe-test.rkt +++ b/nbe-test.rkt @@ -39,6 +39,14 @@ (tm-abs (tm-abs (tm-app b (tm-var 1) (tm-app a (tm-var 1) (tm-var 0)))))) +(: tm-ind (-> Term Term Term Term)) +(define (tm-ind a b c) + `(ind ,a ,b ,c)) + +(: tm-padd (-> Term Term Term)) +(define (tm-padd a b) + (tm-app (tm-ind a tm-id (tm-abs (tm-psuc (tm-app (tm-var 1) (tm-var 0))))) b)) + (: tm-compose (-> Term Term Term)) (define (tm-compose a b) (tm-abs (tm-app a (tm-app b (tm-var 0))))) @@ -70,19 +78,9 @@ `(succ ,(tm-pnat (- n 1))) 'zero)) -;; (define (tm-ifz a b c) -;; `(if-zero ,a ,b ,c)) - -;; (define (tm-psuc a) -;; `(succ ,a)) - -;; (define (tm-double m) -;; (tm-app tm-fix -;; (tm-abs (tm-abs (tm-ifz (tm-var 0) 'zero 'zero))) m )) - -;; (define (tm-padd m n) -;; (tm-app tm-fix -;; (tm-abs (tm-abs (tm-abs (tm-ifz (tm-var 1) (tm-var 0) (tm-psuc (tm-app (tm-var 3) (tm-var 0) (tm-var 1))))))) m n)) +(: tm-psuc (-> Term Term)) +(define (tm-psuc a) + `(succ ,a)) (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id) (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst) @@ -91,10 +89,7 @@ (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 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? (tm-mult (tm-nat 6) (tm-nat 7)) (tm-nat 42)) -;; (check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3)) -;; (check βη-eq? (tm-padd (tm-pnat 8) (tm-pnat 11)) (tm-pnat 19)) -;; (check βη-eq? (tm-padd (tm-pnat 2) (tm-psuc (tm-var 0))) '(succ (succ (succ (var 0))))) +(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 10000) (tm-pnat 2000))) + (tm-pnat 12000)) diff --git a/nbe.rkt b/nbe.rkt index be32bdb..57db916 100644 --- a/nbe.rkt +++ b/nbe.rkt @@ -14,12 +14,11 @@ (define-type D (∪ 'zero (List 'succ (Promise D)) (List 'fun (-> (Promise D) D)) - (List 'fun2 (-> (Promise D) (Promise D) D)) - (List 'neu D-ne) - ;; (List 'ind (-> (Promise D) (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) + (List 'ind D-ne D (-> (Promise D) (Promise D) D)))) (: ext (-> denv (Promise D) denv)) (define (ext ρ a) @@ -28,19 +27,30 @@ a (ρ (- i 1))))) -(define-syntax-rule (ap a b) - (match a - [`(fun ,f) (f (delay b))] - [`(neu ,u) `(neu (app ,u ,b))])) + (: interp-fun (-> Term denv D)) (define (interp-fun a ρ) (list 'fun (λ (x) (interp a (ext ρ x))))) -(: interp-ind (-> D (Promise D) (Promise D) denv D)) -(define (interp-ind a b c ρ) +(: interp-fun2 (-> Term denv (-> (Promise D) (Promise D) D))) +(define (interp-fun2 a ρ) + (λ (x y) (interp a (ext (ext ρ x) y)))) + +(: interp-ind (-> D (Promise D) (-> (Promise D) (Promise D) D) D)) +(define (interp-ind a b c) (match a - [_ (error "unimplemented")])) + [`(neu ,u) `(neu (ind ,u ,(force b) ,c))] + ['zero (force b)] + [`(succ ,a) (c a (delay (interp-ind (force a) b c)))])) + +(: ap (-> D Term denv D)) +(define (ap a b ρ) + (match a + ['zero (error "type-error: ap zero")] + [`(succ ,_) (error "type-error: ap succ")] + [`(fun ,f) (f (delay (interp b ρ)))] + [`(neu ,u) `(neu (app ,u ,(interp b ρ)))])) (: interp (-> Term denv D)) (define (interp a ρ) @@ -51,25 +61,9 @@ [`(ind ,a ,b ,c) (interp-ind (interp a ρ) (delay (interp b ρ)) - (delay (interp c ρ)) ρ)] + (interp-fun2 c ρ))] [`(λ ,a) (interp-fun a ρ)] - [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])) - -;; Domain -;; D := neu D_ne | fun [(var -> var) -> D → D] -;; D_ne := var i | app D_ne D - - -;; (: interp (-> Term (-> Term))) - -;; (define (interp a ρ) -;; (delay (match a -;; [`(var ,i) (force (ρ i))] -;; ['zero 'zero] -;; [`(succ ,a) `(succ ,(interp a ρ))] -;; [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))] -;; [`(λ ,a) (interp-fun a ρ)] -;; [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))) + [`(app ,a ,b) (ap (interp a ρ) b ρ)])) (: reify (-> V D Term)) (define (reify n a) @@ -79,15 +73,15 @@ [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))] [`(neu ,a) (reify-neu n a)])) -;; (define (extract-body a) -;; (match a -;; [`(λ ,a) a] -;; [_ (error "reify-neu: not reifiable")])) - (: reify-neu (-> V D-ne Term)) (define (reify-neu n a) (match a - ;; [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))] + [`(ind ,a ,b ,c) (list 'ind + (reify-neu n a) + (reify n b) + (reify (+ n 2) + (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))))])) @@ -99,7 +93,7 @@ (match a ['zero 0] [`(succ ,a) (scope a)] - (`(ind ,a ,b ,c) (max (scope a) (scope b) (scope c))) + (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2))) [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))] [`(λ ,a) (max 0 (- (scope a) 1))] [`(app ,a ,b) (max (scope a) (scope b))]