lambda-sigma.ss
```;; =============================================================================
;;
;; 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://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)))
```