;; ============================================================================= ;; ;; lambda-sigma.ss - by Dave Herman ;; version 4, 2007-05-01 ;; ;; The reduction semantics for the calculus of explicit substitutions ;; lambda-sigma, by Abadi, Cardelli, Curien, and Lévy: ;; ;; http://citeseer.lcs.mit.edu/abadi91explicit.html ;; http://portal.acm.org/citation.cfm?id=96712 ;; ;; I've added one small syntactic feature to the calculus: although the core ;; calculus only allows a de Bruijn index of 1 and encodes an index n > 1 as ;; 1[↑ ∘ ↑ ∘ ... ∘ ↑] with n-1 shifts, my implementation allows you to use any ;; n >= 1. This requires a generalization of two rewrite rules. First VarCons: ;; ;; 1[a ∙ s] = a ;; ;; This generalizes to ;; ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] = an ;; ;; This is valid by a simple induction on n. The original rule satisfies the ;; n = 1 case; when n > 1, we have ;; ;; n = 1[↑ (n-1 times)] ;; = 1[↑ (n-2 times) ∘ ↑] (Assoc rule) ;; = 1[↑ (n-2 times)][↑] (Clos rule) ;; (*) = n-1[↑] ;; ;; The validity of the generalization of VarCons then follows from ;; ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] ;; = n-1[↑][a1 ∙ a2 ∙ ... ∙ an ∙ s] (*) ;; = n-1[↑ ∘ a1 ∙ a2 ∙ ... ∙ an ∙ s] (Clos rule) ;; = n-1[a2 ∙ ... ∙ an ∙ s] (ShiftCons rule) ;; = an (induction) ;; ;; The VarId rule 1[id] = 1 generalizes to ;; ;; n[id] = n ;; ;; Again, we have n = n-1[↑], so ;; ;; n[id] ;; = n-1[↑][id] (*) ;; = n-1[↑ ∘ id] (Clos rule) ;; = n-1[↑] (ShiftId rule) ;; = n (*) ;; ;; This file is in the public domain. ;; ;; ============================================================================= (module lambda-sigma mzscheme (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3 8)) (planet "gui.ss" ("robby" "redex.plt" 3 8)) (lib "match.ss")) ;; =========================================================================== ;; The core language of the lambda-sigma calculus. ;; =========================================================================== (define λσ (language [e number (app e e) (lambda e) (subst e s)] [s id ↑ (∙ e s) (∘ s s)])) ;; =========================================================================== ;; The lambda-sigma calculus with arbitrary evaluation. ;; =========================================================================== (define λσ/full (extend-language λσ [E (app e E) (app E e) (subst E s) (subst e S) (lambda E) hole] [S (∙ E s) (∙ e S) (∘ S s) (∘ s S) hole])) ;; =========================================================================== ;; The lambda-sigma calculus with a normal-order strategy (section 3.4). ;; =========================================================================== (define λσ/normal-order (extend-language λσ ;; E ::= [] | (E e) | n[S] [E hole (app E e) (subst number S)] ;; S ::= [] | (↑ ∘ s) [S hole (∘ ↑ S)])) ;; =========================================================================== ;; Reduction rules for the lambda-sigma calculus. ;; =========================================================================== (define (reductions lang) (reduction-relation lang ;; (λa)b = a[b ∙ id] [--> (in-hole E_1 (app (lambda e_body) e_arg)) (in-hole E_1 (subst e_body (∙ e_arg id))) "Beta"] ;; n[id] = n [--> (in-hole E_1 (subst number_n id)) (in-hole E_1 number_n) "VarId"] ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] = an [--> (in-hole E_1 (subst 1 (∙ e_first s_rest))) (in-hole E_1 e_first) "VarCons1"] ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] = an [--> (in-hole E_1 (subst number_n (∙ e_first s_rest))) (in-hole E_1 (subst ,(sub1 (term number_n)) s_rest)) (side-condition (> (term number_n) 1)) "VarCons2"] ;; (ba)[s] = (b[s])(a[s]) [--> (in-hole E_1 (subst (app e_rator e_rand) s_1)) (in-hole E_1 (app (subst e_rator s_1) (subst e_rand s_1))) "App"] ;; (λa)[s] = λ(a[1 ∙ (s ∘ ↑)]) [--> (in-hole E_1 (subst (lambda e_body) s_1)) (in-hole E_1 (lambda (subst e_body (∙ 1 (∘ s_1 ↑))))) "Abs"] ;; a[s][t] = a[s ∘ t] [--> (in-hole E_1 (subst (subst e_body s_1) s_2)) (in-hole E_1 (subst e_body (∘ s_1 s_2))) "Clos"] ;; id ∘ s = s [--> (in-hole E_1 (∘ id s_1)) (in-hole E_1 s_1) "IdL"] ;; ↑ ∘ id = ↑ [--> (in-hole E_1 (∘ ↑ id)) (in-hole E_1 ↑) "ShiftId"] ;; ↑ ∘ (a ∙ s) = s [--> (in-hole E_1 (∘ ↑ (∙ e_first s_rest))) (in-hole E_1 s_rest) "ShiftCons"] ;; (a ∙ s) ∘ t = a[t] ∙ (s ∘ t) [--> (in-hole E_1 (∘ (∙ e_first s_rest) s_2)) (in-hole E_1 (∙ (subst e_first s_2) (∘ s_rest s_2))) "Map"] ;; (s1 ∘ s2) ∘ s3 = s1 ∘ (s2 ∘ s3) [--> (in-hole E_1 (∘ (∘ s_1 s_2) s_3)) (in-hole E_1 (∘ s_1 (∘ s_2 s_3))) "Assoc"])) ;; =========================================================================== ;; Front-end. ;; =========================================================================== ;; whnf? : any -> boolean ;; determines whether a lambda-sigma expression is in weak head normal form (define (whnf? x) (match x [('lambda _) #t] [_ #f])) ;; =========================================================================== ;; Example reductions. ;; =========================================================================== ;; (λx.x)(λx.x) (define example1 (term (app (lambda 1) (lambda 1)))) ;; ((λx.λy.y)(λx.x))(λx.x) (define example2 (term (app (app (lambda (lambda 1)) (lambda 1)) (lambda 1)))) ;; ((λx.λy.xy)(λx.x))(λx.λy.x) (define example3 (term (app (app (lambda (lambda (app 2 1))) (lambda 1)) (lambda (lambda 2))))) (define (reduction-graph example) (traces λσ/normal-order (reductions λσ/normal-order) example)) (provide (all-defined)))