λ-calculus

The untyped λ-calculus.

References

• H. Barendregt, Introduction to Lambda Calculus

inductive Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.instDecidableEqTerm {Var✝ : Type u_1} [DecidableEq Var✝] : DecidableEq (Term Var✝)

Equations

• Cslib.LambdaCalculus.Named.instDecidableEqTerm = Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq

def Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq {Var✝ : Type u_1} [DecidableEq Var✝] (x✝ x✝¹ : Term Var✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Term.var a) (Cslib.LambdaCalculus.Named.Term.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Term.var x_2) (Cslib.LambdaCalculus.Named.Term.abs x_3 m) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Term.var x_2) (m.app n) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Term.abs x_2 m) (Cslib.LambdaCalculus.Named.Term.var x_3) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Term.abs x_2 m) (m_1.app n) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (m.app n) (Cslib.LambdaCalculus.Named.Term.var x_2) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqTerm.decEq (m.app n) (Cslib.LambdaCalculus.Named.Term.abs x_2 m_1) = isFalse ⋯

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

Free variables.

Equations

• (Cslib.LambdaCalculus.Named.Term.var x_1).fv = {x_1}
• (Cslib.LambdaCalculus.Named.Term.abs x_1 m).fv = m.fv.erase x_1
• (m.app n).fv = m.fv ∪ n.fv

def Cslib.LambdaCalculus.Named.Term.bv {Var : Type u} [DecidableEq Var] : Term Var → Finset Var

Bound variables.

Equations

• (Cslib.LambdaCalculus.Named.Term.var x_1).bv = ∅
• (Cslib.LambdaCalculus.Named.Term.abs x_1 m).bv = m.bv ∪ {x_1}
• (m.app n).bv = m.bv ∪ n.bv

def Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.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

• (Cslib.LambdaCalculus.Named.Term.var x_2).rename x y = if x_2 = x then Cslib.LambdaCalculus.Named.Term.var y else Cslib.LambdaCalculus.Named.Term.var x_2
• (Cslib.LambdaCalculus.Named.Term.abs x_2 m_1).rename x y = if x_2 = x then Cslib.LambdaCalculus.Named.Term.abs x_2 m_1 else Cslib.LambdaCalculus.Named.Term.abs x_2 (m_1.rename x y)
• (m_1.app n).rename x y = (m_1.rename x y).app (n.rename x y)

@[simp]

theorem Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.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.
• (Cslib.LambdaCalculus.Named.Term.var x_2).subst x r = if x_2 = x then r else Cslib.LambdaCalculus.Named.Term.var x_2
• (m_1.app n).subst x r = (m_1.subst x r).app (n.subst x r)

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

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

Equations

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

inductive Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.instDecidableEqContext {Var✝ : Type u_1} [DecidableEq Var✝] : DecidableEq (Context Var✝)

Equations

• Cslib.LambdaCalculus.Named.instDecidableEqContext = Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq

def Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq {Var✝ : Type u_1} [DecidableEq Var✝] (x✝ x✝¹ : Context Var✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq Cslib.LambdaCalculus.Named.Context.hole Cslib.LambdaCalculus.Named.Context.hole = isTrue ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq Cslib.LambdaCalculus.Named.Context.hole (Cslib.LambdaCalculus.Named.Context.abs x_2 c) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq Cslib.LambdaCalculus.Named.Context.hole (c.appL m) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq Cslib.LambdaCalculus.Named.Context.hole (Cslib.LambdaCalculus.Named.Context.appR m c) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.abs x_2 c) Cslib.LambdaCalculus.Named.Context.hole = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.abs x_2 c) (c_1.appL m) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.abs x_2 c) (Cslib.LambdaCalculus.Named.Context.appR m c_1) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (c.appL m) Cslib.LambdaCalculus.Named.Context.hole = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (c.appL m) (Cslib.LambdaCalculus.Named.Context.abs x_2 c_1) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (c.appL m) (Cslib.LambdaCalculus.Named.Context.appR m_1 c_1) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.appR m c) Cslib.LambdaCalculus.Named.Context.hole = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.appR m c) (Cslib.LambdaCalculus.Named.Context.abs x_2 c_1) = isFalse ⋯
• Cslib.LambdaCalculus.Named.instDecidableEqContext.decEq (Cslib.LambdaCalculus.Named.Context.appR m c) (c_1.appL m_1) = isFalse ⋯

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

Replaces the hole in a Context with a Term.

Equations

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

theorem Cslib.LambdaCalculus.Named.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 Cslib.LambdaCalculus.Named.Term.AlphaEquiv {Var : Type u} [DecidableEq Var] : Term Var → Term Var → Prop

α-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 Cslib.LambdaCalculus.Named.instHasAlphaEquivTerm {Var : Type u} [DecidableEq Var] : HasAlphaEquiv (Term Var)

Instance for the notation m =α n.

Equations

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