From b95de692b9ee1ed82fa5074a8a2f0fdd2bac6933 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 29 Sep 2015 17:52:33 -0400 Subject: [PATCH] Fixed notion of values, and cached reduction * Made the primitive form of elim (elim t_0 t_1), allowing this form to be considered a value when t_0 and t_1 are values. * Moved definition of values to reduction language, and fixed it. This fixed issues with unique decomposition, and thus fixed reduction of eliminators. * Enabled caching in apply-reduction-relation* to speed up results of recursive calls. --- curnel/redex-core.rkt | 136 +++++++++++++++++++++--------------------- curnel/redex-lang.rkt | 2 +- stdlib/nat.rkt | 10 ++-- 3 files changed, 73 insertions(+), 75 deletions(-) diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index a1ede7d..09ae1c3 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -35,14 +35,11 @@ (i ::= natural) (U ::= (Unv i)) (x ::= variable-not-otherwise-mentioned) - (v ::= (Π (x : t) t) (λ (x : t) t) elim x U capp) - (capp ::= (x v) (capp v)) - (t e ::= v (t t))) + (t e ::= (Π (x : t) t) (λ (x : t) t) (elim t t) x U (t t))) (define x? (redex-match? cicL x)) (define t? (redex-match? cicL t)) (define e? (redex-match? cicL e)) -(define v? (redex-match? cicL v)) (define U? (redex-match? cicL U)) (module+ test @@ -61,14 +58,8 @@ (check-true (U? (term (Unv 0)))) (check-true (U? (term Type))) (check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) - (check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))) - (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))) - (check-true - (v? (term (refl Nat)))) - (check-true - (v? (term ((refl Nat) z)))) - ) + (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) ;; 'A' ;; Types of Universes @@ -104,10 +95,10 @@ #:contract (α-equivalent t t) [----------------- "α-x" - (α-equivalent x x)] + (α-equivalent x x)] [----------------- "α-U" - (α-equivalent U U)] + (α-equivalent U U)] [(α-equivalent t_1 (subst t_3 x_1 x_0)) (α-equivalent t_0 t_2) @@ -125,8 +116,8 @@ (check-holds (α-equivalent (λ (x : A) x) (λ (y : A) y)))) (define-metafunction cicL - fresh-x : any ... -> x - [(fresh-x any ...) ,(variable-not-in (term (any ...)) (term x))]) + fresh-x : any ... -> x + [(fresh-x any ...) ,(variable-not-in (term (any ...)) (term x))]) ;; NB: Substitution is hard ;; NB: Copy and pasted from Redex examples @@ -156,7 +147,7 @@ (term (x_0 t_0 x t t_1)) (term x_0)))] [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))] - [(subst elim x t) elim]) + [(subst (elim e_0 e_1) x t) (elim (subst e_0 x t) (subst e_1 x t))]) (module+ test (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B)))))) (check-holds @@ -175,23 +166,32 @@ ;; TODO: I think a lot of things can be simplified if I rethink how ;; TODO: model contexts, telescopes, and such. (define-extended-language cic-redL cicL + ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. + ;; TODO: Perhaps (elim x U) should step to an eta-expanded version of elim + (v ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U))) ;; call-by-value, plus reduce under Π (helps with typing checking) - (E ::= hole (v E) (E e) - (Π (x : (in-hole Θ x)) E) + (E ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)) + ;; TODO: Σ should probably be moved to cicL, since elim is there. ;; Σ (signature). (inductive-name : type ((constructor : type) ...)) (Σ ::= ∅ (Σ (x : t ((x : t) ...)))) (Ξ Φ ::= hole (Π (x : t) Ξ)) ;;(Telescope) ;; NB: Does an apply context correspond to a substitution (γ)? - (Θ ::= hole (Θ e))) ;;(Apply context) + (Θ ::= hole (Θ e)) ;;(Apply context) + (Θv ::= hole (Θv v))) (define Σ? (redex-match? cic-redL Σ)) (define Ξ? (redex-match? cic-redL Ξ)) (define Φ? (redex-match? cic-redL Φ)) (define Θ? (redex-match? cic-redL Θ)) +(define Θv? (redex-match? cic-redL Θv)) (define E? (redex-match? cic-redL E)) +(define v? (redex-match? cic-redL v)) (module+ test + (check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) + (check-true (v? (term (refl Nat)))) + (check-true (v? (term ((refl Nat) z)))) ;; TODO: Rename these signatures, and use them in all future tests. (define Σ (term ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))) (bool : (Unv 0) ((true : bool) (false : bool)))))) @@ -231,7 +231,6 @@ ((append-Σ Σ_2 Σ_1) (x : t ((x_c : t_c) ...)))]) ;; TODO: Test -;; TODO: Isn't this just plug? ;; TODO: Maybe this should be called "apply-to-telescope" (define-metafunction cic-redL apply-telescope : t Ξ -> t @@ -274,7 +273,7 @@ (in-hole Θ_i (hole (in-hole Θ_r x_ci))) (x_c0 ... x_ci x_c1 ...)) ((elim-recur x_D U e_P Θ Θ_m Θ_i (x_c0 ... x_ci x_c1 ...)) - (in-hole (Θ (in-hole Θ_r x_ci)) (((elim x_D) U) e_P)))] + (in-hole (Θ (in-hole Θ_r x_ci)) ((elim x_D U) e_P)))] [(elim-recur x_D U e_P Θ Θ_i Θ_nr (x ...)) hole]) (module+ test (check-true @@ -285,7 +284,7 @@ ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (hole zero) (zero s))) - (term (hole ((((((elim nat) Type) (λ (x : nat) nat)) + (term (hole (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))) @@ -295,7 +294,7 @@ ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (hole (s zero)) (zero s))) - (term (hole ((((((elim nat) Type) (λ (x : nat) nat)) + (term (hole (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s zero)))))) @@ -327,16 +326,16 @@ (--> (Σ (in-hole E ((any (x : t_0) t_1) t_2))) (Σ (in-hole E (subst t_1 x t_2))) -->β) - (--> (Σ (in-hole E (in-hole Θ (((elim x_D) U) e_P)))) - (Σ (in-hole E (in-hole Θ_r (in-hole Θ_i e_mi)))) + (--> (Σ (in-hole E (in-hole Θv ((elim x_D U) v_P)))) + (Σ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi)))) #| | The elim form must appear applied like so: - | (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i a ...)) + | (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...)) | | Where: | x_D is the inductive being eliminated | U is the universe of the result of the motive - | e_P is the motive + | v_P is the motive | m_{0..n} are the methods | p ... are the parameters of x_D | c_i is a constructor of x_d @@ -344,11 +343,11 @@ | Unfortunately, Θ contexts turn all this inside out: | TODO: Write better abstractions for this notation |# - (where (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m) - Θ) + (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) + Θv) ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other ;; arguments. - (judgment-holds (telescope-match Θ_p (parameters-of Σ x_D))) + (judgment-holds (telescope-match Θv_p (parameters-of Σ x_D))) ;; Ensure x_ci is actually a constructor for x_D (where ((x_c* : t_c*) ...) (constructors-for Σ x_D)) @@ -356,11 +355,11 @@ (x_c* ...)) ;; There should be a number of methods equal to the number of constructors; to ensure E ;; doesn't capture methods and Θ_m doesn't capture other arguments - (judgment-holds (length-match Θ_m (x_c* ...))) + (judgment-holds (length-match Θv_m (x_c* ...))) ;; Find the method for constructor x_ci, relying on the order of the arguments. - (where e_mi (method-lookup Σ x_D x_ci Θ_m)) + (where v_mi (method-lookup Σ x_D x_ci Θv_m)) ;; Generate the inductive recursion - (where Θ_r (elim-recur x_D U e_P (in-hole Θ_p Θ_m) Θ_m Θ_i (x_c* ...))) + (where Θ_r (elim-recur x_D U v_P (in-hole Θv_p Θv_m) Θv_m Θv_i (x_c* ...))) -->elim))) (define-metafunction cic-redL @@ -373,7 +372,8 @@ reduce : Σ e -> e [(reduce Σ e) e_r - (where (_ e_r) ,(let ([r (apply-reduction-relation* cic--> (term (Σ e)))]) + (where (_ e_r) ,(let ([r (apply-reduction-relation* cic--> (term (Σ e)) + #:cache-all? #t)]) (unless (null? (cdr r)) (error "Church-rosser broken" r)) (car r)))]) @@ -386,19 +386,19 @@ (term (Π (x : t) (Unv 0)))) (check-equal? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x)))) (term (Π (x : t) (x x)))) - (check-equal? (term (reduce ,Σ ((((((elim nat) Type) (λ (x : nat) nat)) + (check-equal? (term (reduce ,Σ (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero))) (term (s zero))) - (check-equal? (term (reduce ,Σ ((((((elim nat) Type) (λ (x : nat) nat)) + (check-equal? (term (reduce ,Σ (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s zero)))) (term (s (s zero)))) - (check-equal? (term (reduce ,Σ ((((((elim nat) Type) (λ (x : nat) nat)) + (check-equal? (term (reduce ,Σ (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) (s (s (s zero)))))) @@ -406,21 +406,21 @@ (check-equal? (term (reduce ,Σ - ((((((elim nat) Type) (λ (x : nat) nat)) + (((((elim nat Type) (λ (x : nat) nat)) (s (s zero))) (λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (s (s zero))))) (term (s (s (s (s zero)))))) (check-equal? (term (step ,Σ - ((((((elim nat) Type) (λ (x : nat) nat)) + (((((elim nat Type) (λ (x : nat) nat)) (s (s zero))) (λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (s (s zero))))) (term (((λ (x : nat) (λ (ih-x : nat) (s ih-x))) (s zero)) - ((((((elim nat) Type) (λ (x : nat) nat)) + (((((elim nat Type) (λ (x : nat) nat)) (s (s zero))) (λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (s zero))))) @@ -428,7 +428,7 @@ (term (step ,Σ (step ,Σ (((λ (x : nat) (λ (ih-x : nat) (s ih-x))) (s zero)) - ((((((elim nat) Type) (λ (x : nat) nat)) + (((((elim nat Type) (λ (x : nat) nat)) (s (s zero))) (λ (x : nat) (λ (ih-x : nat) (s ih-x)))) (s zero)))))) @@ -437,7 +437,7 @@ ((λ (ih-x1 : nat) (s ih-x1)) (((λ (x : nat) (λ (ih-x : nat) (s ih-x))) zero) - ((((((elim nat) Type) (λ (x : nat) nat)) + (((((elim nat Type) (λ (x : nat) nat)) (s (s zero))) (λ (x : nat) (λ (ih-x : nat) (s ih-x)))) zero)))))) @@ -804,8 +804,8 @@ ;; The types of the methods for this inductive. (where Ξ_m (methods-for x_D x_P (constructors-for Σ x_D))) ----------------- "DTR-Elim_D" - (type-infer Σ Γ ((elim x_D) U) - ;; The type of ((elim x_D) U) is something like: + (type-infer Σ Γ (elim x_D U) + ;; The type of (elim x_D U) is something like: ;; (∀ (P : (∀ a -> ... -> (D a ...) -> U)) ;; (method_ci ...) -> ... -> ;; (a -> ... -> (D a ...) -> @@ -858,8 +858,8 @@ ;; TODO: Clean up/Reorganize these tests (check-true (redex-match? cic-typingL - (in-hole Θ_m ((((elim x_D) U) e_D) e_P)) - (term (((((elim truth) Type) T) (Π (x : truth) (Unv 1))) (Unv 0))))) + (in-hole Θ_m (((elim x_D U) e_D) e_P)) + (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0))))) (define Σtruth (term (∅ (truth : (Unv 0) ((T : truth)))))) (check-holds (type-infer ,Σtruth ∅ truth (in-hole Ξ U))) (check-holds (type-infer ,Σtruth ∅ T (in-hole Θ_ai truth))) @@ -872,15 +872,15 @@ (methods-for truth (λ (x : truth) (Unv 1)) ((T : truth))))) - (check-holds (type-infer ,Σtruth ∅ ((elim truth) Type) t)) + (check-holds (type-infer ,Σtruth ∅ (elim truth Type) t)) (check-holds (type-check (∅ (truth : (Unv 0) ((T : truth)))) ∅ - (((((elim truth) (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0)) + ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0)) T) (Unv 1))) (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth)))) ∅ - (((((elim truth) (Unv 1)) Type) Type) T) + ((((elim truth (Unv 1)) Type) Type) T) (Unv 1))) (check-holds (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U)) @@ -898,7 +898,7 @@ (check-holds (type-check ,Σ syn ...))) (nat-test ∅ (Π (x : nat) nat) (Unv 0)) (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat)) - (nat-test ∅ ((((((elim nat) Type) (λ (x : nat) nat)) zero) + (nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) zero) nat) (nat-test ∅ nat (Unv 0)) @@ -907,38 +907,38 @@ (nat-test ∅ (s zero) nat) ;; TODO: Meta-function auto-currying and such (check-holds - (type-infer ,Σ ∅ (((((elim nat) (Unv 0)) (λ (x : nat) nat)) + (type-infer ,Σ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) t)) - (nat-test ∅ ((((((elim nat) (Unv 0)) (λ (x : nat) nat)) + (nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) zero) nat) - (nat-test ∅ ((((((elim nat) (Unv 0)) (λ (x : nat) nat)) + (nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero) nat) - (nat-test ∅ ((((((elim nat) Type) (λ (x : nat) nat)) + (nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero) nat) (nat-test (∅ n : nat) - ((((((elim nat) (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n) + (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n) nat) (check-holds (type-check (,Σ (bool : (Unv 0) ((btrue : bool) (bfalse : bool)))) (∅ n2 : nat) - ((((((elim nat) (Unv 0)) (λ (x : nat) bool)) + (((((elim nat (Unv 0)) (λ (x : nat) bool)) btrue) (λ (x : nat) (λ (ih-x : bool) bfalse))) n2) bool)) (check-not-holds (type-check ,Σ ∅ - (((((elim nat) (Unv 0)) nat) (s zero)) zero) + ((((elim nat (Unv 0)) nat) (s zero)) zero) nat)) (define lam (term (λ (nat : (Unv 0)) nat))) (check-equal? @@ -997,7 +997,7 @@ (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P)))) (check-holds (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅ - (((((((elim and) (Unv 0)) + ((((((elim and (Unv 0)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))) (λ (A : (Unv 0)) @@ -1034,7 +1034,7 @@ (check-holds (type-check ,Σ4 (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)) - (((((((elim and) (Unv 0)) + ((((((elim and (Unv 0)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))) (λ (A : (Unv 0)) @@ -1054,7 +1054,7 @@ t)) (check-holds (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅ - (((((((elim and) (Unv 0)) + ((((((elim and (Unv 0)) (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))) (λ (A : (Unv 0)) @@ -1086,17 +1086,17 @@ (in-hole Ξ (Π (x : (in-hole Θ false)) U)))) (check-true (redex-match? cic-typingL - ((in-hole Θ_m (((elim x_D) U) e_P)) e_D) - (term ((((elim false) (Unv 1)) (λ (y : false) (Π (x : Type) x))) + ((in-hole Θ_m ((elim x_D U) e_P)) e_D) + (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x))) x)))) (check-holds (type-check ,sigma (,gamma x : false) - ((((elim false) (Unv 0)) (λ (y : false) (Π (x : Type) x))) x) + (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x) (Π (x : (Unv 0)) x))) ;; nat-equal? tests (define zero? - (term (((((elim nat) Type) (λ (x : nat) bool)) + (term ((((elim nat Type) (λ (x : nat) bool)) true) (λ (x : nat) (λ (x_ih : bool) false))))) (check-holds @@ -1108,7 +1108,7 @@ (term (reduce ,Σ (,zero? (s zero)))) (term false)) (define ih-equal? - (term (((((elim nat) Type) (λ (x : nat) bool)) + (term ((((elim nat Type) (λ (x : nat) bool)) false) (λ (x : nat) (λ (y : bool) (x_ih x)))))) (check-holds @@ -1122,7 +1122,7 @@ (check-holds (type-infer ,Σ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0)))) (define nat-equal? - (term (((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool))) + (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool))) ,zero?) (λ (x : nat) (λ (x_ih : (Π (x : nat) bool)) ,ih-equal?))))) @@ -1143,7 +1143,7 @@ (check-true (Σ? Σ=)) (define refl-elim - (term ((((((((elim ==) (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== + (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) @@ -1154,7 +1154,7 @@ (check-true (redex-match? cic-redL - (Σ (in-hole E (in-hole Θ (((elim x_D) U) e_P)))) + (Σ (in-hole E (in-hole Θ ((elim x_D U) e_P)))) (term (,Σ= ,refl-elim)))) (check-true (redex-match? diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index b8ca1e7..87ec328 100644 --- a/curnel/redex-lang.rkt +++ b/curnel/redex-lang.rkt @@ -173,7 +173,7 @@ [(elim t1 t2) (let* ([t1 (cur->datum #'t1)] [t2 (cur->datum #'t2)]) - (term ((elim ,t1) ,t2)))] + (term (elim ,t1 ,t2)))] [(#%app e1 e2) (term (,(cur->datum #'e1) ,(cur->datum #'e2)))])))) (unless (and inner-expand? (type-infer/term reified-term)) diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt index ebb2307..f7bf650 100644 --- a/stdlib/nat.rkt +++ b/stdlib/nat.rkt @@ -47,22 +47,20 @@ (check-equal? (nat-equal? z (s z)) false) (check-equal? (nat-equal? (s z) (s z)) true)) -#| TODO: Disabled until #20 fixed (define (even? (n : Nat)) (elim Nat Type (lambda (x : Nat) Bool) - false + true (lambda* (n : Nat) (odd? : Bool) (not odd?)) n)) (define (odd? (n : Nat)) - (and (not (even? n)) - (not (nat-equal? n z)))) + (not (even? n))) (module+ test (check-equal? (even? z) - false) + true) (check-equal? (even? (s z)) false) @@ -81,4 +79,4 @@ (check-equal? (odd? (s (s (s z)))) true)) -|# +