β-confluence for the λ-calculus

inductive Cslib.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 Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢ₚ_» : Lean.TrailingParserDescr

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠ₚ_» : Lean.TrailingParserDescr

Equations

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

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

The left side of a parallel reduction is locally closed.

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

Parallel reduction is reflexive for locally closed terms.

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

The right side of a parallel reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.le_parallel {Var : Type u} : (fun (x1 x2 : Term Var) => x1.FullBeta x2) ≤ fun (x1 x2 : Term Var) => x1.Parallel x2

The inclusion (· ⭢βᶠ ·) ≤ (· ⭢ₚ ·).

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Parallel.le_reflTransGen_fullBeta {Var : Type u} [HasFresh Var] [DecidableEq Var] : (fun (x1 x2 : Term Var) => x1.Parallel x2) ≤ fun (x1 x2 : Term Var) => Relation.ReflTransGen FullBeta x1 x2

The inclusion (· ⭢ₚ ·) ≤ (· ↠βᶠ ·).

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.reflTransGen_parallel_fullBeta {Var : Type u} [HasFresh Var] [DecidableEq Var] : (fun (x1 x2 : Term Var) => Relation.ReflTransGen Parallel x1 x2) = fun (x1 x2 : Term Var) => Relation.ReflTransGen FullBeta x1 x2

Multiple parallel reduction is equal to multiple β-reduction.

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

Parallel reduction respects substitution.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_open_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (x y : Var) (z : ℕ) (para : M.Parallel M') : (openRec z (fvar y) (closeRec z x M)).Parallel (openRec z (fvar y) (closeRec z x M'))

Parallel substitution respects closing and opening.

theorem Cslib.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)).Parallel (N.open' (fvar x))) (para : M'.Parallel N') : (M.open' M').Parallel (N.open' N')

Parallel substitution respects fresh opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.parallel_diamond {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.Diamond fun (x1 x2 : Term Var) => x1.Parallel x2

Parallel reduction has the diamond property.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_parallel {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.Confluent fun (x1 x2 : Term Var) => x1.Parallel x2

Parallel reduction is confluent.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_fullBeta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Relation.Confluent fun (x1 x2 : Term Var) => x1.FullBeta x2

β-reduction is confluent.