URM Execution Semantics

Single-step and multi-step execution semantics for URMs.

Main definitions

• URM.Step: Single-step execution relation
• URM.Steps: Multi-step execution (reflexive-transitive closure of Step)
• URM.Halts: A program halts on given inputs
• URM.Diverges: A program diverges on given inputs
• URM.HaltsWithResult: A program halts on given inputs with a specific result

Bridge lemmas:

• isHalted_iff_normal: s.isHalted p ↔ Relation.Normal (Step p) s
• halts_iff_normalizable: Halts p inputs ↔ Relation.Normalizable (Step p) (State.init inputs)
• step_confluent: The step relation is confluent (follows from determinism)

Notation (scoped to URM namespace)

Standard computability theory notation:

• p ↓ inputs — program p halts on inputs
• p ↑ inputs — program p diverges on inputs
• p ↓ inputs ≫ result — program p halts on inputs with result in R[0]

Main results

• Step.deterministic: The step relation is deterministic
• step_confluent: The step relation is confluent (from determinism)
• haltsWithResult_iff_eval: p ↓ inputs ≫ result ↔ eval p inputs = Part.some result

inductive Cslib.URM.Step (p : Program) : State → State → Prop

Single-step execution relation for URMs.

Each constructor corresponds to one of the four instruction types:

• zero: Execute Z n (set register n to 0)
• succ: Execute S n (increment register n)
• transfer: Execute T m n (copy register m to register n)
• jump_eq: Execute J m n q when registers m and n are equal (jump to q)
• jump_ne: Execute J m n q when registers m and n differ (proceed to next)

• zero {p : Program} {s : State} {n : ℕ} (h : p[s.pc]? = some (Instr.Z n)) : Step p s { pc := s.pc + 1, regs := s.regs.write n 0 }
• succ {p : Program} {s : State} {n : ℕ} (h : p[s.pc]? = some (Instr.S n)) : Step p s { pc := s.pc + 1, regs := s.regs.write n (s.regs.read n + 1) }
• transfer {p : Program} {s : State} {m n : ℕ} (h : p[s.pc]? = some (Instr.T m n)) : Step p s { pc := s.pc + 1, regs := s.regs.write n (s.regs.read m) }
• jump_eq {p : Program} {s : State} {m n q : ℕ} (h : p[s.pc]? = some (Instr.J m n q)) (heq : s.regs.read m = s.regs.read n) : Step p s { pc := q, regs := s.regs }
• jump_ne {p : Program} {s : State} {m n q : ℕ} (h : p[s.pc]? = some (Instr.J m n q)) (hne : s.regs.read m ≠ s.regs.read n) : Step p s { pc := s.pc + 1, regs := s.regs }

@[reducible, inline]

abbrev Cslib.URM.Steps (p : Program) : State → State → Prop

Multi-step execution: the reflexive-transitive closure of Step.

Equations

• Cslib.URM.Steps p = Relation.ReflTransGen (Cslib.URM.Step p)

theorem Cslib.URM.Step.deterministic {p : Program} : Relator.RightUnique (Step p)

The step relation is deterministic: each state has at most one successor.

theorem Cslib.URM.Step.no_step_of_halted {p : Program} {s s' : State} (hhalted : s.isHalted p) : ¬Step p s s'

A halted state has no successor in the step relation.

theorem Cslib.URM.Step.preserves_register {p : Program} {s s' : State} {r : ℕ} (hstep : Step p s s') (hr : ∀ (instr : Instr), p[s.pc]? = some instr → instr.writesTo ≠ some r) : s'.regs.read r = s.regs.read r

A single step preserves registers not written to by the current instruction.

This is a fundamental property of URM execution: each instruction modifies at most one register (Z, S, T write to one register; J writes to none).

Step Properties

theorem Cslib.URM.isHalted_iff_normal {p : Program} {s : State} : s.isHalted p ↔ Relation.Normal (Step p) s

A state is halted iff it is normal (has no successor) in the reduction system.

theorem Cslib.URM.step_confluent (p : Program) : Relation.Confluent (Step p)

The step relation is confluent.

theorem Cslib.URM.Steps.preserves_register {p : Program} {s s' : State} {r : ℕ} (hsteps : Steps p s s') (hr : ∀ instr ∈ p, instr.writesTo ≠ some r) : s'.regs.read r = s.regs.read r

Multi-step execution preserves registers not written by any executed instruction.

theorem Cslib.URM.Steps.eq_of_halts {p : Program} {init s₁ s₂ : State} (h1 : Steps p init s₁) (hh1 : s₁.isHalted p) (h2 : Steps p init s₂) (hh2 : s₂.isHalted p) : s₁ = s₂

If two halted states are reachable from the same start, they are equal.

This follows from confluence: since Step p is confluent and both s₁ and s₂ are normal forms reachable from init, they must be equal.

def Cslib.URM.Halts (p : Program) (inputs : List ℕ) : Prop

A program halts on given inputs if execution reaches a halted state.

This is equivalent to (Step p).Normalizable (State.init inputs) — see halts_iff_normalizable.

Equations

• Cslib.URM.Halts p inputs = ∃ (s : Cslib.URM.State), Cslib.URM.Steps p (Cslib.URM.State.init inputs) s ∧ s.isHalted p

theorem Cslib.URM.halts_iff_normalizable {p : Program} {inputs : List ℕ} : Halts p inputs ↔ Relation.Normalizable (Step p) (State.init inputs)

Halting is equivalent to normalizability in the reduction system.

def Cslib.URM.Diverges (p : Program) (inputs : List ℕ) : Prop

A program diverges on given inputs if it does not halt.

Equations

• Cslib.URM.Diverges p inputs = ¬Cslib.URM.Halts p inputs

def Cslib.URM.HaltsWithResult (p : Program) (inputs : List ℕ) (result : ℕ) : Prop

A program halts on given inputs with a specific result in R[0].

Equations

• Cslib.URM.HaltsWithResult p inputs result = ∃ (s : Cslib.URM.State), Cslib.URM.Steps p (Cslib.URM.State.init inputs) s ∧ s.isHalted p ∧ s.regs.output = result

def Cslib.URM.«term_↓_» : Lean.TrailingParserDescr

Notation for halting: p ↓ inputs means program p halts on inputs.

Equations

• Cslib.URM.«term_↓_» = Lean.ParserDescr.trailingNode `Cslib.URM.«term_↓_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↓ ") (Lean.ParserDescr.cat `term 51))

def Cslib.URM.«term_↑_» : Lean.TrailingParserDescr

Notation for divergence: p ↑ inputs means program p diverges on inputs.

Equations

• Cslib.URM.«term_↑_» = Lean.ParserDescr.trailingNode `Cslib.URM.«term_↑_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑ ") (Lean.ParserDescr.cat `term 51))

def Cslib.URM.«term_↓_≫_» : Lean.TrailingParserDescr

Notation for halting with result: p ↓ inputs ≫ result means program p halts on inputs with result in R[0].

Equations

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

theorem Cslib.URM.HaltsWithResult.toHalts {p : Program} {inputs : List ℕ} {result : ℕ} (h : HaltsWithResult p inputs result) : Halts p inputs

If a program halts with a result, it halts.

noncomputable def Cslib.URM.evalState (p : Program) (inputs : List ℕ) : Part State

Evaluation returning the full halting state.

Equations

• Cslib.URM.evalState p inputs = { Dom := Cslib.URM.Halts p inputs, get := fun (h : Cslib.URM.Halts p inputs) => Classical.choose h }

theorem Cslib.URM.evalState_spec (p : Program) {inputs : List ℕ} (h : (evalState p inputs).Dom) : have s := (evalState p inputs).get h; Steps p (State.init inputs) s ∧ s.isHalted p

Specification: the state from evalState satisfies Steps and isHalted.

theorem Cslib.URM.Halts.toHaltsWithResult {p : Program} {inputs : List ℕ} (h : Halts p inputs) : HaltsWithResult p inputs ((evalState p inputs).get h).regs.output

If a program halts, it halts with the output of the final state.

noncomputable def Cslib.URM.eval (p : Program) (inputs : List ℕ) : Part ℕ

Evaluation as a partial function using Part. Defined when the program halts, returning the value in register 0.

Equations

• Cslib.URM.eval p inputs = Part.map (fun (x : Cslib.URM.State) => x.regs.output) (Cslib.URM.evalState p inputs)

theorem Cslib.URM.haltsWithResult_iff_eval (p : Program) {inputs : List ℕ} {result : ℕ} : HaltsWithResult p inputs result ↔ eval p inputs = Part.some result

A program halts with result a iff evaluation returns Part.some a.

def Cslib.URM.ProgramEquiv (p q : Program) : Prop

Two programs are equivalent if they produce the same result for all inputs.

Equations

• Cslib.URM.ProgramEquiv p q = ∀ (inputs : List ℕ), Cslib.URM.eval p inputs = Cslib.URM.eval q inputs

theorem Cslib.URM.ProgramEquiv.equivalence : Equivalence ProgramEquiv

Program equivalence is an equivalence relation.

@[implicit_reducible]

instance Cslib.URM.instSetoidProgram : Setoid Program

Setoid instance for programs, enabling the ≈ notation.

Equations

• Cslib.URM.instSetoidProgram = { r := Cslib.URM.ProgramEquiv, iseqv := Cslib.URM.ProgramEquiv.equivalence }