inductive MeTTaIL.RewStepMany (p : Presentation) : AST → AST → Prop

Many-step context rewriting: the reflexive-transitive closure of RewStep.

• refl {p : Presentation} {t : AST} : RewStepMany p t t
• tail {p : Presentation} {t u v : AST} : RewStepMany p t u → RewStep p u v → RewStepMany p t v

theorem MeTTaIL.RewStepMany.single {p : Presentation} {t t' : AST} (h : RewStep p t t') : RewStepMany p t t'

A single step is a many-step.

theorem MeTTaIL.RewStepMany.trans {p : Presentation} {t u v : AST} (h₁ : RewStepMany p t u) (h₂ : RewStepMany p u v) : RewStepMany p t v

Many-step rewriting composes.

def MeTTaIL.eval (p : Presentation) : Nat → AST → AST

The fuel-bounded normalizer: apply oneStep until no step applies or the fuel runs out. Total, no partial; the fuel makes the driver structurally recursive even when reduction may not terminate.

Equations

• MeTTaIL.eval p 0 x✝ = x✝
• MeTTaIL.eval p fuel.succ x✝ = match MeTTaIL.oneStep p x✝ with | some t' => MeTTaIL.eval p fuel t' | none => x✝

def MeTTaIL.IsNormal (p : Presentation) (t : AST) : Prop

A term is normal when no one-step reduction applies. Decidable, since oneStep is computable.

Equations

• MeTTaIL.IsNormal p t = (MeTTaIL.oneStep p t = none)

theorem MeTTaIL.eval_sound (p : Presentation) (fuel : Nat) (t : AST) : RewStepMany p t (eval p fuel t)

Soundness: the normalizer's result is reachable from the input by many context rewrites. Every run of the runtime is a genuine reduction sequence of the presentation's semantics.

theorem MeTTaIL.eval_fixed_of_normal (p : Presentation) (t : AST) (h : IsNormal p t) (fuel : Nat) : eval p (fuel + 1) t = t

A normal term is a fixpoint of the normalizer.