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://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)))