;; =============================================================================
;;
;; lambda-sigma.ss - by Dave Herman
;; version 5, 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)
    (define simple-relation
      (reduction-relation
       lang
       ;; (λa)b = a[b ∙ id]
       [--> (app (lambda e_body) e_arg)
            (subst e_body (∙ e_arg id))
            "Beta"]
       ;; n[id] = n
       [--> (subst number_n id)
            number_n
            "VarId"]
       ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] = an
       [--> (subst 1 (∙ e_first s_rest))
            e_first
            "VarCons1"]
       ;; n[a1 ∙ a2 ∙ ... ∙ an ∙ s] = an
       [--> (subst number_n (∙ e_first s_rest))
            (subst ,(sub1 (term number_n)) s_rest)
            (side-condition (> (term number_n) 1))
            "VarCons2"]
       ;; (ba)[s] = (b[s])(a[s])
       [--> (subst (app e_rator e_rand) s_1)
            (app (subst e_rator s_1) (subst e_rand s_1))
            "App"]
       ;; (λa)[s] = λ(a[1 ∙ (s ∘ ↑)])
       [--> (subst (lambda e_body) s_1)
            (lambda (subst e_body (∙ 1 (∘ s_1 ↑))))
            "Abs"]
       ;; a[s][t] = a[s ∘ t]
       [--> (subst (subst e_body s_1) s_2)
            (subst e_body (∘ s_1 s_2))
            "Clos"]
       ;; id ∘ s = s
       [--> (∘ id s_1)
            s_1
            "IdL"]
       ;; ↑ ∘ id = ↑
       [--> (∘ ↑ id)
            ↑
            "ShiftId"]
       ;; ↑ ∘ (a ∙ s) = s
       [--> (∘ ↑ (∙ e_first s_rest))
            s_rest
            "ShiftCons"]
       ;; (a ∙ s) ∘ t = a[t] ∙ (s ∘ t)
       [--> (∘ (∙ e_first s_rest) s_2)
            (∙ (subst e_first s_2) (∘ s_rest s_2))
            "Map"]
       ;; (s1 ∘ s2) ∘ s3 = s1 ∘ (s2 ∘ s3)
       [--> (∘ (∘ s_1 s_2) s_3)
            (∘ s_1 (∘ s_2 s_3))
            "Assoc"]))
    (context-closure simple-relation lang E))

  ;; ===========================================================================
  ;; 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)))