Documentation

Cslib.Languages.LambdaCalculus.Named.Untyped.Basic

λ-calculus #

The untyped λ-calculus, with a named representation of variables. This file contains the definitions of α-equivalence and capture-avoiding substitution.

References #

H. Barendregt, Introduction to Lambda Calculus
Definition of α-equivalence M. Gabbay and A. Pitts, A New Approach to Abstract Syntax with Variable Binding

inductive Cslib.LambdaCalculus.Named.Untyped.Term (Var : 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

Instances For

@[instance_reducible]

instance Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm {Var✝ : Type u_1} [DecidableEq Var✝] :

DecidableEq (Term Var✝)

Equations

Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm = Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq

def Cslib.LambdaCalculus.Named.Untyped.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.Untyped.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Untyped.Term.var x_2) (Cslib.LambdaCalculus.Named.Untyped.Term.abs x_3 m) = isFalse ⋯
Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Untyped.Term.var x_2) (m.app n) = isFalse ⋯
Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Untyped.Term.abs x_2 m) (Cslib.LambdaCalculus.Named.Untyped.Term.var x_3) = isFalse ⋯
Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq (Cslib.LambdaCalculus.Named.Untyped.Term.abs x_2 m) (m_1.app n) = isFalse ⋯
Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq (m.app n) (Cslib.LambdaCalculus.Named.Untyped.Term.var x_2) = isFalse ⋯
Cslib.LambdaCalculus.Named.Untyped.instDecidableEqTerm.decEq (m.app n) (Cslib.LambdaCalculus.Named.Untyped.Term.abs x_2 m_1) = isFalse ⋯

Instances For

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

Term Var → Finset Var

Free variables.

Equations

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

Instances For

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

Term Var → Finset Var

Bound variables.

Equations

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

Instances For

def Cslib.LambdaCalculus.Named.Untyped.Term.vars {Var : Type u} [DecidableEq Var] :

Term Var → Finset Var

Variable names (free and bound) in a term.

Equations

(Cslib.LambdaCalculus.Named.Untyped.Term.var x_1).vars = {x_1}
(Cslib.LambdaCalculus.Named.Untyped.Term.abs x_1 m).vars = m.vars ∪ {x_1}
(m.app n).vars = m.vars ∪ n.vars

Instances For

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

Term Var

Variable renaming, applying to both free and bound variables. m.rename x y changes all occurrences of x into y in m.

Equations

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

Instances For

@[simp]

theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_eq_sizeOf {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :

sizeOf (m.rename x y) = sizeOf m

Renaming preserves size.

inductive Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv {Var : Type u} [DecidableEq Var] :

Term Var → Term Var → Prop

α-equivalence.

var {Var : Type u} [DecidableEq Var] {x : Var} : (Term.var x).AlphaEquiv (Term.var x)
abs {Var : Type u} [DecidableEq Var] {y x1 x2 : Var} {m1 m2 : Term Var} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (m1.rename x1 y).AlphaEquiv (m2.rename x2 y) → (Term.abs x1 m1).AlphaEquiv (Term.abs x2 m2)
app {Var : Type u} [DecidableEq Var] {m1 n1 m2 n2 : Term Var} : m1.AlphaEquiv n1 → m2.AlphaEquiv n2 → (m1.app m2).AlphaEquiv (n1.app n2)

Instances For

@[instance_reducible]

instance Cslib.LambdaCalculus.Named.Untyped.Term.instHasAlphaEquivTerm {Var : Type u} [DecidableEq Var] :

HasAlphaEquiv (Term Var)

Instance for the notation m =α n.

Equations

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

@[simp]

theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv_def {Var : Type u} [DecidableEq Var] (m n : Term Var) :

m =α n ↔ m.AlphaEquiv n

Allow grind to recognise the notation of α-equivalence.

inductive Cslib.LambdaCalculus.Named.Untyped.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} : y ≠ x → (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} : y ∉ r.fv ∪ {x} → 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')
alpha {Var : Type u} [DecidableEq Var] {m m' r r' n n' : Term Var} {x : Var} : m =α m' → r =α r' → n =α n' → m.Subst x r n → m'.Subst x r' n'

Instances For

@[irreducible]

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

Instances For

@[instance_reducible]

instance Cslib.LambdaCalculus.Named.Untyped.Term.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.Untyped.Term.instHasSubstitutionTerm = { subst := Cslib.LambdaCalculus.Named.Untyped.Term.subst }

@[simp]

theorem Cslib.LambdaCalculus.Named.Untyped.Term.subst_def {Var : Type u} [DecidableEq Var] [HasFresh Var] (m r : Term Var) (x : Var) :

m[x := r] = m.subst x r

Allow grind to recognise the notation of substitution.

inductive Cslib.LambdaCalculus.Named.Untyped.Term.Context (Var : 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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance Cslib.LambdaCalculus.Named.Untyped.Term.instDecidableEqContext {Var✝ : Type u_1} [DecidableEq Var✝] :

DecidableEq (Context Var✝)

Equations

Cslib.LambdaCalculus.Named.Untyped.Term.instDecidableEqContext = Cslib.LambdaCalculus.Named.Untyped.Term.instDecidableEqContext.decEq

def Cslib.LambdaCalculus.Named.Untyped.Term.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.Untyped.Term.Context.hole.fill m = m
(Cslib.LambdaCalculus.Named.Untyped.Term.Context.abs x c_2).fill m = Cslib.LambdaCalculus.Named.Untyped.Term.abs x (c_2.fill m)
(c_2.appL n).fill m = (c_2.fill m).app n
(Cslib.LambdaCalculus.Named.Untyped.Term.Context.appR n c_2).fill m = n.app (c_2.fill m)

Instances For

def Cslib.LambdaCalculus.Named.Untyped.Term.Context.vars {Var : Type u} [DecidableEq Var] :

Context Var → Finset Var

Variables (both free and bound) in a context.

Equations

Cslib.LambdaCalculus.Named.Untyped.Term.Context.hole.vars = ∅
(Cslib.LambdaCalculus.Named.Untyped.Term.Context.abs x c_1).vars = c_1.vars ∪ {x}
(c_1.appL n).vars = c_1.vars ∪ n.vars
(Cslib.LambdaCalculus.Named.Untyped.Term.Context.appR n c_1).vars = n.vars ∪ c_1.vars

Instances For