β-confluence for the λ-calculus

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

A parallel β-reduction step.

• fvar {Var : Type u} (x : Var) : (Term.fvar x).Parallel (Term.fvar x)

  Free variables parallel step to themselves.

• app {Var : Type u} {L L' M M' : Term Var} : L.Parallel L' → M.Parallel M' → (L.app M).Parallel (L'.app M')

  A parallel left and right congruence rule for application.

• abs {Var : Type u} {m m' : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (m.open' (Term.fvar x)).Parallel (m'.open' (Term.fvar x))) → m.abs.Parallel m'.abs

  Congruence rule for lambda terms.

• beta {Var : Type u} {m m' n n' : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (m.open' (Term.fvar x)).Parallel (m'.open' (Term.fvar x))) → n.Parallel n' → (m.abs.app n).Parallel (m'.open' n')

  A parallel β-reduction.

def «term_↠ₚ_» : Lean.TrailingParserDescr

Equations

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

def «term_⭢ₚ_».«delab_app.ReductionSystem.Red» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «term_↠ₚ_».«delab_app.ReductionSystem.MRed» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «term_⭢ₚ_» : Lean.TrailingParserDescr

Equations

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

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_lc_l {Var : Type u} {M N : Term Var} (step : M ⭢ₚ N) : M.LC

The left side of a parallel reduction is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.Parallel.lc_refl {Var : Type u} (M : Term Var) (lc : M.LC) : M ⭢ₚ M

Parallel reduction is reflexive for locally closed terms.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_lc_r {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (step : M ⭢ₚ N) : N.LC

The right side of a parallel reduction is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.step_to_para {Var : Type u} {M N : Term Var} (step : M ⭢βᶠ N) : M ⭢ₚ N

A single β-reduction implies a single parallel reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_to_redex {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (para : M ⭢ₚ N) : M ↠βᶠ N

A single parallel reduction implies a multiple β-reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.parachain_iff_redex {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] : M ↠ₚ N ↔ M ↠βᶠ N

Multiple parallel reduction is equivalent to multiple β-reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_subst {Var : Type u} {M M' N N' : Term Var} [HasFresh Var] [DecidableEq Var] (x : Var) (pm : M ⭢ₚ M') (pn : N ⭢ₚ N') : M[x:=N] ⭢ₚ M'[x:=N']

Parallel reduction respects substitution.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_open_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (x y : Var) (z : ℕ) (para : M ⭢ₚ M') : y ∉ M.fv ∪ M'.fv ∪ {x} → openRec z (fvar y) (closeRec z x M) ⭢ₚ openRec z (fvar y) (closeRec z x M')

Parallel substitution respects closing and opening.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_open_out {Var : Type u} {M M' N N' : Term Var} [HasFresh Var] [DecidableEq Var] (L : Finset Var) (mem : ∀ x ∉ L, M.open' (fvar x) ⭢ₚ N.open' (fvar x)) (para : M' ⭢ₚ N') : M.open' M' ⭢ₚ N.open' N'

Parallel substitution respects fresh opening.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_diamond {Var : Type u} [HasFresh Var] [DecidableEq Var] : Diamond Parallel

Parallel reduction has the diamond property.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.para_confluence {Var : Type u} [HasFresh Var] [DecidableEq Var] : Confluence Parallel

Parallel reduction is confluent.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.confluence_beta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Confluence FullBeta

β-reduction is confluent.