def MeTTaIL.AC.RewStepModAC (acOp : Label → Bool) (p : Presentation) (t t' : AST) : Prop

Rewriting modulo AC, the standard relation →_{R/AC}: t rewrites to t' when t is AC-equivalent to some u that takes one base step to u', with u' AC-equivalent to t'.

Equations

• MeTTaIL.AC.RewStepModAC acOp p t t' = ∃ (u : MeTTaIL.AST) (u' : MeTTaIL.AST), MeTTaIL.AC.ACEq acOp t u ∧ MeTTaIL.RewStep p u u' ∧ MeTTaIL.AC.ACEq acOp u' t'

def MeTTaIL.AC.oneStepAC (acOp : Label → Bool) (p : Presentation) (t : AST) : Option AST

One step of rewriting modulo AC: canonicalise, take a base step, recanonicalise.

Equations

• MeTTaIL.AC.oneStepAC acOp p t = Option.map (MeTTaIL.AC.canon acOp) (MeTTaIL.oneStep p (MeTTaIL.AC.canon acOp t))

theorem MeTTaIL.AC.oneStepAC_respects (acOp : Label → Bool) {p : Presentation} {t t2 : AST} (h : ACEq acOp t t2) : oneStepAC acOp p t = oneStepAC acOp p t2

The engine is well-defined on AC-equivalence classes: AC-equivalent inputs give identical results. This is the coherence the canonical form provides, since canon is constant on each class.

theorem MeTTaIL.AC.oneStepAC_sound (acOp : Label → Bool) {p : Presentation} {t t' : AST} (h : oneStepAC acOp p t = some t') : RewStepModAC acOp p t t'

Soundness: every step the modulo-AC engine takes is a genuine →_{R/AC} step. The input is AC-equivalent to its canonical form, the base engine takes a real RewStep there, and the output is the recanonicalised reduct, AC-equivalent to that reduct.

def MeTTaIL.AC.evalAC (acOp : Label → Bool) (p : Presentation) : ℕ → AST → AST

Fuel-bounded normalization modulo AC: iterate the modulo-AC step.

Equations

• MeTTaIL.AC.evalAC acOp p 0 x✝ = x✝
• MeTTaIL.AC.evalAC acOp p n.succ x✝ = match MeTTaIL.AC.oneStepAC acOp p x✝ with | some t' => MeTTaIL.AC.evalAC acOp p n t' | none => x✝

theorem MeTTaIL.AC.evalAC_sound (acOp : Label → Bool) (p : Presentation) (fuel : ℕ) (t : AST) : Relation.ReflTransGen (RewStepModAC acOp p) t (evalAC acOp p fuel t)

Soundness of the modulo-AC normalizer: its result is reachable from the input by →_{R/AC} steps.

def MeTTaIL.AC.IsNormalModAC (acOp : Label → Bool) (p : Presentation) (t : AST) : Prop

A term is normal modulo AC for this engine when no modulo-AC step applies, equivalently when its canonical form is a base normal form.

Equations

• MeTTaIL.AC.IsNormalModAC acOp p t = (MeTTaIL.AC.oneStepAC acOp p t = none)

Completeness: when the engine acts, and coherence

The engine takes a step exactly when the canonical form has a base redex. Whether that captures every →_{R/AC} step is the coherence question: the canonical form must not lose a redex that some other AC-representative has. CoherentAC names that condition, and under it the engine is complete.

theorem MeTTaIL.AC.oneStepAC_isSome (acOp : Label → Bool) (p : Presentation) (t : AST) : (oneStepAC acOp p t).isSome = hasRedex p (canon acOp t)

The engine takes a step exactly when the canonical form has a base redex. No coherence assumption is needed for this characterization; it follows from base-engine completeness on the canonical form.

theorem MeTTaIL.AC.isNormalModAC_iff_hasRedex (acOp : Label → Bool) (p : Presentation) (t : AST) : IsNormalModAC acOp p t ↔ hasRedex p (canon acOp t) = false

Being normal modulo AC means the canonical form has no base redex anywhere.

theorem MeTTaIL.AC.exists_rewStep_of_hasRedex {p : Presentation} {u : AST} (hu : hasRedex p u = true) : ∃ (u' : AST), RewStep p u u'

Every base redex gives a genuine context rewrite (the easy half of the engine/relation bridge).

def MeTTaIL.AC.CoherentAC (acOp : Label → Bool) (p : Presentation) : Prop

Coherence of a presentation with AC: canonicalising never loses a redex that some AC-equivalent term has. This is the condition (Maude's coherence) under which the canonical-form strategy is complete: it makes the canonical form a redex-maximal representative of its AC-equivalence class. It is an assumed side-condition, not established here for arbitrary presentations (a syntactic criterion guaranteeing it is future work); coherentAC_of_no_rewrites shows it is at least satisfiable, so the completeness result below is conditional but not vacuous.

Equations

• MeTTaIL.AC.CoherentAC acOp p = ∀ (t u : MeTTaIL.AST), MeTTaIL.AC.ACEq acOp t u → MeTTaIL.hasRedex p u = true → MeTTaIL.hasRedex p (MeTTaIL.AC.canon acOp t) = true

theorem MeTTaIL.AC.oneStepAC_complete (acOp : Label → Bool) {p : Presentation} (hco : CoherentAC acOp p) {t u : AST} (htu : ACEq acOp t u) (hu : hasRedex p u = true) : (oneStepAC acOp p t).isSome = true

Completeness under the assumed coherence side-condition CoherentAC: if any AC-representative of t has a redex, the modulo-AC engine takes a step. With exists_rewStep_of_hasRedex this says the engine never stalls while some AC-equivalent term can still be rewritten. The result is conditional on coherence, which is assumed rather than proven in general (see CoherentAC).

theorem MeTTaIL.AC.hasRedex_false_of_no_rewrites {p : Presentation} (hp : p.rewrites = []) (t : AST) : hasRedex p t = false

With no rewrite rules, no term has a redex anywhere.

theorem MeTTaIL.AC.hasRedexList_false_of_no_rewrites {p : Presentation} (hp : p.rewrites = []) (ts : List AST) : hasRedexList p ts = false

theorem MeTTaIL.AC.coherentAC_of_no_rewrites (acOp : Label → Bool) {p : Presentation} (hp : p.rewrites = []) : CoherentAC acOp p

Coherence is satisfiable: a presentation with no rewrite rules is coherent, vacuously, since nothing is reducible. So CoherentAC is a consistent side-condition rather than an empty one, and oneStepAC_complete is a real (if conditional) completeness statement.