λ-calculus

The untyped λ-calculus.

References

• [H. Barendregt, Introduction to Lambda Calculus] [84]

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

Syntax of terms.

• var {Var : Type u} (x : Var) : Term Var
• abs {Var : Type u} (x : Var) (m : Term Var) : Term Var
• app {Var : Type u} (m n : Term Var) : Term Var

instance LambdaCalculus.instDecidableEqTerm {Var✝ : Type u_1} [DecidableEq Var✝] : DecidableEq (Term Var✝)

Equations

• LambdaCalculus.instDecidableEqTerm = LambdaCalculus.decEqTerm✝

def LambdaCalculus.Term.fv {Var : Type u} [DecidableEq Var] (m : Term Var) : Finset Var

Free variables.

Equations

• (LambdaCalculus.Term.var x).fv = {x}
• (LambdaCalculus.Term.abs x m_2).fv = m_2.fv.erase x
• (m_2.app n).fv = m_2.fv ∪ n.fv

def LambdaCalculus.Term.bv {Var : Type u} [DecidableEq Var] (m : Term Var) : Finset Var

Bound variables.

Equations

• (LambdaCalculus.Term.var x).bv = ∅
• (LambdaCalculus.Term.abs x m_2).bv = m_2.bv ∪ {x}
• (m_2.app n).bv = m_2.bv ∪ n.bv

def LambdaCalculus.Term.vars {Var : Type u} [DecidableEq Var] (m : Term Var) : Finset Var

Variable names (free and bound) in a term.

Equations

• m.vars = m.fv ∪ m.bv

inductive LambdaCalculus.Term.Subst {Var : Type u} [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop

Capture-avoiding substitution, as an inference system.

• varHit {Var : Type u} [DecidableEq Var] {x : Var} {r : Term Var} : (var x).Subst x r r
• varMiss {Var : Type u} [DecidableEq Var] {x y : Var} {r : Term Var} : x ≠ y → (var y).Subst x r (var y)
• absShadow {Var : Type u} [DecidableEq Var] {x : Var} {m r : Term Var} : (abs x m).Subst x r (abs x m)
• absIn {Var : Type u} [DecidableEq Var] {x y : Var} {m r m' : Term Var} : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
• app {Var : Type u} [DecidableEq Var] {m n : Term Var} {x : Var} {r m' n' : Term Var} : m.Subst x r m' → n.Subst x r n' → (m.app n).Subst x r (m'.app n')

def LambdaCalculus.Term.rename {Var : Type u} [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var

Renaming, or variable substitution. m.rename x y renames x into y in m.

Equations

• (LambdaCalculus.Term.var x_1).rename x y = if x_1 = x then LambdaCalculus.Term.var y else LambdaCalculus.Term.var x_1
• (LambdaCalculus.Term.abs x_1 m_2).rename x y = if x_1 = x then LambdaCalculus.Term.abs x_1 m_2 else LambdaCalculus.Term.abs x_1 (m_2.rename x y)
• (m_2.app n).rename x y = (m_2.rename x y).app (n.rename x y)

theorem LambdaCalculus.Term.rename.eq_sizeOf {Var : Type u} {m : Term Var} {x y : Var} [DecidableEq Var] : sizeOf (m.rename x y) = sizeOf m

Renaming preserves size.

@[irreducible]

def LambdaCalculus.Term.subst {Var : Type u} [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var

Capture-avoiding substitution. m.subst x r replaces the free occurrences of variable x in m with r.

Equations

• One or more equations did not get rendered due to their size.
• (LambdaCalculus.Term.var x_1).subst x r = if x_1 = x then r else LambdaCalculus.Term.var x_1
• (m_2.app n).subst x r = (m_2.subst x r).app (n.subst x r)

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

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

Equations

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

inductive LambdaCalculus.Context (Var : Type u) : Type u

Contexts.

• hole {Var : Type u} : Context Var
• abs {Var : Type u} (x : Var) (c : Context Var) : Context Var
• appL {Var : Type u} (c : Context Var) (m : Term Var) : Context Var
• appR {Var : Type u} (m : Term Var) (c : Context Var) : Context Var

instance LambdaCalculus.instDecidableEqContext {Var✝ : Type u_1} [DecidableEq Var✝] : DecidableEq (Context Var✝)

Equations

• LambdaCalculus.instDecidableEqContext = LambdaCalculus.decEqContext✝

def LambdaCalculus.Context.fill {Var : Type u} (c : Context Var) (m : Term Var) : Term Var

Replaces the hole in a Context with a Term.

Equations

• LambdaCalculus.Context.hole.fill m = m
• (LambdaCalculus.Context.abs x c_2).fill m = LambdaCalculus.Term.abs x (c_2.fill m)
• (c_2.appL n).fill m = (c_2.fill m).app n
• (LambdaCalculus.Context.appR n c_2).fill m = n.app (c_2.fill m)

theorem LambdaCalculus.Context.complete {Var : Type u} (m : Term Var) : ∃ (c : Context Var) (x : Var), m = c.fill (Term.var x)

Any Term can be obtained by filling a Context with a variable. This proves that Context completely captures the syntax of terms.

inductive LambdaCalculus.Term.AlphaEquiv {Var : Type u} [DecidableEq Var] : Rel (Term Var) (Term Var)

α-equivalence.

• ax {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} : y ∉ m.fv → (abs x m).AlphaEquiv (abs y (m.rename x y))
• refl {Var : Type u} [DecidableEq Var] {m : Term Var} : m.AlphaEquiv m
• symm {Var : Type u} [DecidableEq Var] {m n : Term Var} : m.AlphaEquiv n → n.AlphaEquiv m
• trans {Var : Type u} [DecidableEq Var] {m1 m2 m3 : Term Var} : m1.AlphaEquiv m2 → m2.AlphaEquiv m3 → m1.AlphaEquiv m3
• ctx {Var : Type u} [DecidableEq Var] {c : Context Var} {m n : Term Var} : m.AlphaEquiv n → (c.fill m).AlphaEquiv (c.fill n)

instance LambdaCalculus.instHasAlphaEquivTerm {Var : Type u} [DecidableEq Var] : HasAlphaEquiv (Term Var)

Instance for the notation m =α n.

Equations

• LambdaCalculus.instHasAlphaEquivTerm = { AlphaEquiv := LambdaCalculus.Term.AlphaEquiv }