From 807c4d7851468c2adb10f55763537bb9490144b3 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Mon, 23 Mar 2015 17:39:02 -0400 Subject: [PATCH 1/2] Added Type shorthand for tests --- redex-curnel.rkt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index fe8b6ba..0555070 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -34,6 +34,7 @@ (module+ test (require rackunit) + (define-term Type (Unv 0)) (check-true (x? (term T))) (check-true (x? (term truth))) (check-true (x? (term zero))) @@ -43,6 +44,7 @@ (check-true (x? (term nat))) (check-true (t? (term nat))) (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)))) From a46889081770540d1073d747c115737fdf9d9a0e Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 24 Mar 2015 20:11:18 -0400 Subject: [PATCH 2/2] Reduced complexity of substitution --- redex-curnel.rkt | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 0555070..be89387 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -22,7 +22,6 @@ (i ::= natural) (U ::= (Unv i)) (x ::= variable-not-otherwise-mentioned) - ;; TODO: Having 2 binders is stupid. (v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U) (t e ::= (case e (x e) ...) v (t t))) @@ -94,15 +93,11 @@ [(subst U x t) U] [(subst x x t) t] [(subst x_0 x t) x_0] - [(subst (Π (x : t_0) t_1) x t) (Π (x : (subst t_0 x t)) t_1)] - [(subst (λ (x : t_0) t_1) x t) (λ (x : (subst t_0 x t)) t_1)] - [(subst (μ (x : t_0) t_1) x t) (μ (x : (subst t_0 x t)) t_1)] + [(subst (any (x : t_0) t_1) x t) (any (x : (subst t_0 x t)) t_1)] ;; TODO: Broken: needs capture avoiding, but currently require ;; binders to be the same in term/type, so this is not a local ;; change. - [(subst (Π (x_0 : t_0) t_1) x t) (Π (x_0 : (subst t_0 x t)) (subst t_1 x t)) ] - [(subst (λ (x_0 : t_0) t_1) x t) (λ (x_0 : (subst t_0 x t)) (subst t_1 x t))] - [(subst (μ (x_0 : t_0) t_1) x t) (μ (x_0 : (subst t_0 x t)) (subst t_1 x t))] + [(subst (any (x_0 : t_0) t_1) x t) (any (x_0 : (subst t_0 x t)) (subst t_1 x t)) ] [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))] [(subst (case e (x_0 e_0) ...) x t) (case (subst e x t)