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} {s s' s'' : State} (h1 : Step p s s') (h2 : Step p s s'') : s' = s''

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.

For a deterministic relation, any two execution paths from the same state must follow the same sequence of steps, so if both reach some state, they reach the same state. We prove this directly rather than via Diamond since Diamond requires the relation to always have successors.

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.

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 }