λ-calculus

The untyped λ-calculus, with a locally nameless representation of syntax.

References

• A. Chargueraud, The Locally Nameless Representation
• See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which this is partially adapted

inductive LambdaCalculus.LocallyNameless.Untyped.Term (Var : Type u) : Type u

Syntax of locally nameless lambda terms, with free variables over Var.

• bvar {Var : Type u} : ℕ → Term Var

  Bound variables that appear under a lambda abstraction, using a de-Bruijn index.

• fvar {Var : Type u} : Var → Term Var

  Free variables.

• abs {Var : Type u} : Term Var → Term Var

  Lambda abstraction, introducing a new bound variable.

• app {Var : Type u} : Term Var → Term Var → Term Var

  Function application.

def LambdaCalculus.LocallyNameless.Untyped.Term.openRec {Var : Type u} (i : ℕ) (sub : Term Var) : Term Var → Term Var

Variable opening of the ith bound variable.

Equations

• One or more equations did not get rendered due to their size.
• LambdaCalculus.LocallyNameless.Untyped.Term.openRec i sub (LambdaCalculus.LocallyNameless.Untyped.Term.bvar i') = if i = i' then sub else LambdaCalculus.LocallyNameless.Untyped.Term.bvar i'
• LambdaCalculus.LocallyNameless.Untyped.Term.openRec i sub (LambdaCalculus.LocallyNameless.Untyped.Term.fvar x_1) = LambdaCalculus.LocallyNameless.Untyped.Term.fvar x_1
• LambdaCalculus.LocallyNameless.Untyped.Term.openRec i sub M.abs = (LambdaCalculus.LocallyNameless.Untyped.Term.openRec (i + 1) sub M).abs

def LambdaCalculus.LocallyNameless.Untyped.Term.«term_⟦_↝_⟧» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.openRec_bvar {i : ℕ} {Var✝ : Type u_1} {s : Term Var✝} {i' : ℕ} : openRec i s (bvar i') = if i = i' then s else bvar i'

theorem LambdaCalculus.LocallyNameless.Untyped.Term.openRec_fvar {i : ℕ} {Var✝ : Type u_1} {s : Term Var✝} {x : Var✝} : openRec i s (fvar x) = fvar x

theorem LambdaCalculus.LocallyNameless.Untyped.Term.openRec_app {i : ℕ} {Var✝ : Type u_1} {s l r : Term Var✝} : openRec i s (l.app r) = (openRec i s l).app (openRec i s r)

theorem LambdaCalculus.LocallyNameless.Untyped.Term.openRec_abs {i : ℕ} {Var✝ : Type u_1} {s M : Term Var✝} : openRec i s M.abs = (openRec (i + 1) s M).abs

def LambdaCalculus.LocallyNameless.Untyped.Term.open' {X : Type u_1} (e u : Term X) : Term X

Variable opening of the closest binding.

Equations

• e.open' u = LambdaCalculus.LocallyNameless.Untyped.Term.openRec 0 u e

def LambdaCalculus.LocallyNameless.Untyped.Term.«term_^_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LambdaCalculus.LocallyNameless.Untyped.Term.closeRec {Var : Type u} [DecidableEq Var] (k : ℕ) (x : Var) : Term Var → Term Var

Variable closing, replacing a free fvar x with bvar k

Equations

• One or more equations did not get rendered due to their size.
• LambdaCalculus.LocallyNameless.Untyped.Term.closeRec k x (LambdaCalculus.LocallyNameless.Untyped.Term.bvar i) = LambdaCalculus.LocallyNameless.Untyped.Term.bvar i
• LambdaCalculus.LocallyNameless.Untyped.Term.closeRec k x t.abs = (LambdaCalculus.LocallyNameless.Untyped.Term.closeRec (k + 1) x t).abs

def LambdaCalculus.LocallyNameless.Untyped.Term.«term_⟦_↜_⟧» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LambdaCalculus.LocallyNameless.Untyped.Term.close {Var : Type u_1} [DecidableEq Var] (e : Term Var) (u : Var) : Term Var

Variable closing of the closest binding.

Equations

• e.close u = LambdaCalculus.LocallyNameless.Untyped.Term.closeRec 0 u e

def LambdaCalculus.LocallyNameless.Untyped.Term.«term_^*_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LambdaCalculus.LocallyNameless.Untyped.Term.subst {Var : Type u} [DecidableEq Var] (m : Term Var) (x : Var) (sub : Term Var) : Term Var

Equations

• (LambdaCalculus.LocallyNameless.Untyped.Term.bvar i').subst x sub = LambdaCalculus.LocallyNameless.Untyped.Term.bvar i'
• (LambdaCalculus.LocallyNameless.Untyped.Term.fvar x_2).subst x sub = if x = x_2 then sub else LambdaCalculus.LocallyNameless.Untyped.Term.fvar x_2
• (l.app r).subst x sub = (l.subst x sub).app (r.subst x sub)
• M.abs.subst x sub = (M.subst x sub).abs

instance LambdaCalculus.LocallyNameless.Untyped.Term.instHasSubstitutionTerm {Var : Type u} [DecidableEq Var] : HasSubstitution (Term Var) Var

Term.subst is a substitution for λ-terms. Gives access to the notation m[x := n].

Equations

• LambdaCalculus.LocallyNameless.Untyped.Term.instHasSubstitutionTerm = { subst := LambdaCalculus.LocallyNameless.Untyped.Term.subst }

def LambdaCalculus.LocallyNameless.Untyped.Term.fv {Var : Type u} [DecidableEq Var] : Term Var → Finset Var

Free variables of a term.

Equations

• (LambdaCalculus.LocallyNameless.Untyped.Term.bvar a).fv = ∅
• (LambdaCalculus.LocallyNameless.Untyped.Term.fvar x_1).fv = {x_1}
• e1.abs.fv = e1.fv
• (l.app r).fv = l.fv ∪ r.fv

inductive LambdaCalculus.LocallyNameless.Untyped.Term.LC {Var : Type u} : Term Var → Prop

Locally closed terms.

• fvar {Var : Type u} (x : Var) : (Term.fvar x).LC
• abs {Var : Type u} (L : Finset Var) (e : Term Var) : (∀ x ∉ L, (e.open' (Term.fvar x)).LC) → e.abs.LC
• app {Var : Type u} {l r : Term Var} : l.LC → r.LC → (l.app r).LC

inductive LambdaCalculus.LocallyNameless.Untyped.Term.Value {Var : Type u} : Term Var → Prop

• abs {Var : Type u} (e : Term Var) : e.abs.LC → e.abs.Value

theorem LambdaCalculus.LocallyNameless.Untyped.Term.closeRec_bvar {Var : Type u} [DecidableEq Var] {x : Var} {k i : ℕ} : closeRec k x (bvar i) = bvar i

theorem LambdaCalculus.LocallyNameless.Untyped.Term.closeRec_fvar {Var : Type u} [DecidableEq Var] {x : Var} {k : ℕ} {x' : Var} : closeRec k x (fvar x') = if x = x' then bvar k else fvar x'

theorem LambdaCalculus.LocallyNameless.Untyped.Term.closeRec_app {Var : Type u} [DecidableEq Var] {x : Var} {k : ℕ} {l r : Term Var} : closeRec k x (l.app r) = (closeRec k x l).app (closeRec k x r)

theorem LambdaCalculus.LocallyNameless.Untyped.Term.closeRec_abs {Var : Type u} [DecidableEq Var] {x : Var} {k : ℕ} {t : Term Var} : closeRec k x t.abs = (closeRec (k + 1) x t).abs

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_bvar {Var : Type u} [DecidableEq Var] {x : Var} {i : ℕ} {n : Term Var} : (bvar i)[x:=n] = bvar i

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_fvar {Var : Type u} [DecidableEq Var] {x x' : Var} {n : Term Var} : (fvar x')[x:=n] = if x = x' then n else fvar x'

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_app {Var : Type u} [DecidableEq Var] {x : Var} {n l r : Term Var} : (l.app r)[x:=n] = l[x:=n].app (r[x:=n])

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_abs {Var : Type u} [DecidableEq Var] {x : Var} {n M : Term Var} : M.abs[x:=n] = M[x:=n].abs

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_def {Var : Type u} [DecidableEq Var] (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x:=n]