Confluence of module-expression reduction

The two open facts about ModuleExpression.MultiStepReduction that everything downstream of reduce rests on: reduction is confluent (stuck reducts are unique), and termination is invariant along it. Split off from ModuleExpressionBasics.lean so the syntax, typing, reduction and normal-form development there stays independent of them; ModuleExpression.lean is where their consequences live.

The argument of a δ-redex

inst.toModuleExpr is a closed tuple of procedures: it determines inst, and — once parallel reduction is in place — nothing reduces inside it. Together with the renaming/substitution invariance proved in ModuleExpressionBasics.lean, these say the δ-rule has no critical pair with anything.

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_injective {holes : HoleSigs} (inst inst' : holes.Instantiation) : inst.toModuleExpr = inst'.toModuleExpr → inst = inst'

Distinct instantiations give distinct tuples: the δ-rule's contractum is determined by the redex.

Parallel reduction

ParStep contracts any set of redexes of a term at once (Tait–Martin-Löf). It sits between ReductionStep and MultiStepReduction, so it has the same transitive-reflexive closure, and — unlike ReductionStep — it has the diamond property, which is what gives confluence.

inductive GaudisCrypt.ModuleExpression.ParStep : ModuleExpression → ModuleExpression → Prop

Parallel reduction: contract any set of the redexes present in the term, simultaneously. A δ-redex needs no premise for its argument: inst.toModuleExpr has no redexes inside.

• proc {sig : ProcedureSignature} (p : Procedure sig) : (ModuleExpression.proc p).ParStep (ModuleExpression.proc p)
• procHoles {holes : HoleSigs} {sig : ProcedureSignature} (ne : holes.NonEmpty) (p : ProcedureWithHoles holes sig) : (ModuleExpression.procHoles ne p).ParStep (ModuleExpression.procHoles ne p)
• var (n : ℕ) : (ModuleExpression.var n).ParStep (ModuleExpression.var n)
• unit : ModuleExpression.unit.ParStep ModuleExpression.unit
• abs {b b' : ModuleExpression} : b.ParStep b' → b.abs.ParStep b'.abs
• app {f f' a a' : ModuleExpression} : f.ParStep f' → a.ParStep a' → (f.app a).ParStep (f'.app a')
• beta {b b' a a' : ModuleExpression} : b.ParStep b' → a.ParStep a' → (b.abs.app a).ParStep (b'.substitute a')
• pair {a a' b b' : ModuleExpression} : a.ParStep a' → b.ParStep b' → (a.pair b).ParStep (a'.pair b')
• fst {e e' : ModuleExpression} : e.ParStep e' → e.fst.ParStep e'.fst
• fstPair {a a' b : ModuleExpression} : a.ParStep a' → (a.pair b).fst.ParStep a'
• snd {e e' : ModuleExpression} : e.ParStep e' → e.snd.ParStep e'.snd
• sndPair {a b b' : ModuleExpression} : b.ParStep b' → (a.pair b).snd.ParStep b'
• delta {holes : HoleSigs} {sigs : ProcedureSignature} (ne : holes.NonEmpty) (p : ProcedureWithHoles holes sigs) (inst : holes.Instantiation) : ((ModuleExpression.procHoles ne p).app inst.toModuleExpr).ParStep (ModuleExpression.proc (p.instantiate inst))

theorem GaudisCrypt.ModuleExpression.ParStep.refl (m : ModuleExpression) : m.ParStep m

Parallel reduction is reflexive: contract nothing.

theorem GaudisCrypt.ModuleExpression.ParStep.of_reductionStep {m n : ModuleExpression} (h : m.ReductionStep n) : m.ParStep n

A single reduction step is a parallel step.

theorem GaudisCrypt.ModuleExpression.ParStep.multiStepReduction {m n : ModuleExpression} (h : m.ParStep n) : m.MultiStepReduction n

A parallel step is a multi-step reduction.

theorem GaudisCrypt.ModuleExpression.ParStep.rename {m n : ModuleExpression} : m.ParStep n → ∀ (ρ : ℕ → ℕ), (ModuleExpression.rename ρ m).ParStep (ModuleExpression.rename ρ n)

Parallel reduction survives a renaming.

theorem GaudisCrypt.ModuleExpression.ParStep.liftSubst_of_forall {σ τ : ℕ → ModuleExpression} (h : ∀ (n : ℕ), (σ n).ParStep (τ n)) (n : ℕ) : (liftSubst σ n).ParStep (liftSubst τ n)

Two substitutions that agree up to parallel reduction still do so under a binder.

theorem GaudisCrypt.ModuleExpression.ParStep.substituteSimultaneously {m n : ModuleExpression} : m.ParStep n → ∀ {σ τ : ℕ → ModuleExpression}, (∀ (k : ℕ), (σ k).ParStep (τ k)) → (ModuleExpression.substituteSimultaneously σ m).ParStep (ModuleExpression.substituteSimultaneously τ n)

Parallel reduction survives a simultaneous substitution that itself reduces in parallel.

theorem GaudisCrypt.ModuleExpression.ParStep.substitute {b b' a a' : ModuleExpression} (hb : b.ParStep b') (ha : a.ParStep a') : (b.substitute a).ParStep (b'.substitute a')

Parallel reduction survives β-substitution: the key lemma behind the diamond property.

theorem GaudisCrypt.ModuleExpression.ParStep.eq_toModuleExpr {holes : HoleSigs} (inst : holes.Instantiation) {n : ModuleExpression} : inst.toModuleExpr.ParStep n → n = inst.toModuleExpr

Nothing reduces inside the argument of a δ-redex.

Inversion

theorem GaudisCrypt.ModuleExpression.ParStep.abs_inv {b n : ModuleExpression} (h : b.abs.ParStep n) : ∃ (b' : ModuleExpression), n = b'.abs ∧ b.ParStep b'

theorem GaudisCrypt.ModuleExpression.ParStep.pair_inv {a b n : ModuleExpression} (h : (a.pair b).ParStep n) : ∃ (a' : ModuleExpression) (b' : ModuleExpression), n = a'.pair b' ∧ a.ParStep a' ∧ b.ParStep b'

theorem GaudisCrypt.ModuleExpression.ParStep.procHoles_inv {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} {n : ModuleExpression} (h : (ModuleExpression.procHoles ne p).ParStep n) : n = ModuleExpression.procHoles ne p

The complete development

completeDevelopment m contracts every redex m has, and nothing else (a δ-redex counts only when its argument is already a procedure tuple). Takahashi's triangle property — every parallel reduct of m reduces in parallel to completeDevelopment m — gives the diamond property, hence confluence. Noncomputable only because of the classical test for the δ-rule.

noncomputable def GaudisCrypt.ModuleExpression.completeDevelopment : ModuleExpression → ModuleExpression

Contract every redex of m simultaneously.

Equations

• One or more equations did not get rendered due to their size.
• (b.abs.app a).completeDevelopment = b.completeDevelopment.substitute a.completeDevelopment
• (f.app a).completeDevelopment = f.completeDevelopment.app a.completeDevelopment
• (a.pair a_1).fst.completeDevelopment = a.completeDevelopment
• e.fst.completeDevelopment = e.completeDevelopment.fst
• (a.pair b).snd.completeDevelopment = b.completeDevelopment
• e.snd.completeDevelopment = e.completeDevelopment.snd
• b.abs.completeDevelopment = b.completeDevelopment.abs
• (a.pair b).completeDevelopment = a.completeDevelopment.pair b.completeDevelopment
• (GaudisCrypt.ModuleExpression.proc p).completeDevelopment = GaudisCrypt.ModuleExpression.proc p
• (GaudisCrypt.ModuleExpression.procHoles ne p).completeDevelopment = GaudisCrypt.ModuleExpression.procHoles ne p
• (GaudisCrypt.ModuleExpression.var n).completeDevelopment = GaudisCrypt.ModuleExpression.var n
• GaudisCrypt.ModuleExpression.unit.completeDevelopment = GaudisCrypt.ModuleExpression.unit

theorem GaudisCrypt.ModuleExpression.completeDevelopment_delta {holes : HoleSigs} {sigs : ProcedureSignature} (ne : holes.NonEmpty) (p : ProcedureWithHoles holes sigs) (inst : holes.Instantiation) : ((procHoles ne p).app inst.toModuleExpr).completeDevelopment = proc (p.instantiate inst)

A δ-redex develops to its contractum.

theorem GaudisCrypt.ModuleExpression.completeDevelopment_app_procHoles {holes : HoleSigs} {sigs : ProcedureSignature} (ne : holes.NonEmpty) (p : ProcedureWithHoles holes sigs) (a : ModuleExpression) (h : ¬∃ (inst : holes.Instantiation), a = inst.toModuleExpr) : ((procHoles ne p).app a).completeDevelopment = (procHoles ne p).app a.completeDevelopment

An application of a procedure with holes whose argument is not a procedure tuple develops componentwise.

theorem GaudisCrypt.ModuleExpression.ParStep.triangle {m n : ModuleExpression} (h : m.ParStep n) : n.ParStep m.completeDevelopment

Takahashi's triangle property: every parallel reduct of m parallel-reduces to the complete development of m.

Confluence

The diamond property of ParStep is Takahashi's triangle read twice; Relation.church_rosser turns it into confluence of the transitive-reflexive closure, and that closure is MultiStepReduction because ParStep sits between ReductionStep and it.

theorem GaudisCrypt.ModuleExpression.ParStep.diamond {m n1 n2 : ModuleExpression} (h1 : m.ParStep n1) (h2 : m.ParStep n2) : ∃ (d : ModuleExpression), n1.ParStep d ∧ n2.ParStep d

Diamond property of parallel reduction.

theorem GaudisCrypt.ModuleExpression.reflTransGen_parStep_of_multiStepReduction {m n : ModuleExpression} (h : m.MultiStepReduction n) : Relation.ReflTransGen ParStep m n

theorem GaudisCrypt.ModuleExpression.multiStepReduction_of_reflTransGen_parStep {m n : ModuleExpression} (h : Relation.ReflTransGen ParStep m n) : m.MultiStepReduction n

theorem GaudisCrypt.ModuleExpression.multiStepReduction_confluent {m n1 n2 : ModuleExpression} (h1 : m.MultiStepReduction n1) (h2 : m.MultiStepReduction n2) : ∃ (d : ModuleExpression), n1.MultiStepReduction d ∧ n2.MultiStepReduction d

Church–Rosser: a term's reducts can always be brought back together.

theorem GaudisCrypt.ModuleExpression.Stuck.eq_of_multiStepReduction {m n : ModuleExpression} (hm : m.Stuck) (h : m.MultiStepReduction n) : m = n

A stuck expression reduces to nothing but itself.