Configuration graphs on register tuples

The compact configuration graph packs the registers of a view into one radix-B number. This file states the same graph directly on register tuples, without packing: RegisterStep reads the input symbol under the input head straight from the input word, matches the observations of a permitted transition and applies nextRegisters. Halted tuples step only to themselves.

Register-tuple reachability from startRegisters is exactly the set of registers of reachable views (reflTransGen_registerStep_iff), so acceptance is reachability of a halted tuple with output tag 1 (accepts_iff_registerStep). When every reachable view fits a radix B, the same holds on tuples of type Register k → Fin B (accepts_iff_registerStep_fin). These are the forms used by logical descriptions of configuration graphs, in which a configuration is a fixed tuple of universe elements.

RegisterStep is RegisterStepWith for the read inputAt w. The packed graph reads one supplied symbol with blanks forced at the boundaries, another read function; its target uniqueness for deterministic machines (edgeWithSymbol_target_unique) is derived from rightUnique_registerStepWith.

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.startRegisters: the initial register tuple.
• Turing.MultiTapeNTM.ConfigurationGraph.RegisterStepWith: one step on register tuples, reading the input through a supplied function.
• Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep: one step on the register tuples of an input word.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStepWith, Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStep, Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStep_fin: a deterministic machine has at most one successor at every register tuple, with no validity premise.
• Turing.MultiTapeNTM.ConfigurationGraph.reflTransGen_registerStep_iff: reachable tuples are the registers of reachable views.
• Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_registerStep: acceptance on ℕ-valued tuples.
• Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_registerStep_fin: acceptance on bounded tuples.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.startRegisters {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : Register k → ℕ

The registers of the initial view: input head on the first cell, the initial control and blank work tapes.

def Turing.MultiTapeNTM.ConfigurationGraph.RegisterStepWith {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (n : ℕ) (read : ℕ → Option Bool) (r r' : Register k → ℕ) : Prop

One step on register tuples of a machine whose input has length n and whose input symbol at head position p is read p. A tuple whose control is the halting tag steps to itself. Otherwise some permitted transition observes the control, the input symbol under the input head and the work-tape head symbols, and the successor is nextRegisters.

def Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (w : List Bool) : (Register k → ℕ) → (Register k → ℕ) → Prop

One step on register tuples over the input w: RegisterStepWith reading w through inputAt.

theorem Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStepWith {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (hdet : ntm.IsDeterministic) (n : ℕ) (read : ℕ → Option Bool) : Relator.RightUnique (RegisterStepWith ntm n read)

A deterministic machine steps uniquely on register tuples, for every input length and input read, on every tuple of naturals.

There is no validity or reachability premise. The successor is computed from the tuple alone: the halting tag allows only the tuple itself; otherwise the injective codes fix the observed state and head symbols, determinism fixes the action, and the successor is nextRegisters of the tuple. So several tuples describing one configuration, or tuples describing none, are harmless: each still has at most one successor. Restricting to tuples with bounded entries (Register k → Fin B) keeps uniqueness: a successor that overflows the bound is absent, not wrapped.

theorem Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStep {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hdet : ntm.IsDeterministic) : Relator.RightUnique (RegisterStep ntm w)

A deterministic machine steps uniquely on the register tuples of an input.

theorem Turing.MultiTapeNTM.ConfigurationGraph.rightUnique_registerStep_fin {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hdet : ntm.IsDeterministic) {B : ℕ} : Relator.RightUnique fun (x y : Register k → Fin B) => RegisterStep ntm w (fun (i : Register k) => ↑(x i)) fun (i : Register k) => ↑(y i)

A deterministic machine steps uniquely on bounded register tuples Register k → Fin B. A successor whose entries overflow B is not a bounded tuple, so it is absent rather than wrapped, and uniqueness needs no bound on the source.

theorem Turing.MultiTapeNTM.ConfigurationGraph.registers_initView {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) : registers (ntm.initView w) = startRegisters ntm

The initial view has the start registers.

theorem Turing.MultiTapeNTM.ConfigurationGraph.registerStep_of_viewStep {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {v v' : FiniteCfg k Bool State} (h : ntm.ViewStep v v') : RegisterStep ntm v.input (registers v) (registers v')

Every view step is a register step on the view's input.

theorem Turing.MultiTapeNTM.ConfigurationGraph.exists_viewStep_of_registerStep {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {v : FiniteCfg k Bool State} {r : Register k → ℕ} (h : RegisterStep ntm v.input (registers v) r) : ∃ (v' : FiniteCfg k Bool State), ntm.ViewStep v v' ∧ v'.input = v.input ∧ registers v' = r

Every register step out of the registers of a view is the registers of a view step.

theorem Turing.MultiTapeNTM.ConfigurationGraph.reflTransGen_registerStep_iff {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (r : Register k → ℕ) : Relation.ReflTransGen (RegisterStep ntm w) (startRegisters ntm) r ↔ ∃ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v ∧ registers v = r

Reachable register tuples are the registers of reachable views.

theorem Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_registerStep {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} : ntm.Accepts w ↔ ∃ (r : Register k → ℕ), Relation.ReflTransGen (RegisterStep ntm w) (startRegisters ntm) r ∧ r Register.control = stateCode none ∧ r Register.output = 1

Acceptance is register-tuple reachability: a machine accepts exactly when a tuple with the halting control tag and output tag 1 is reachable from the start registers.

theorem Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_registerStep_fin {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {B : ℕ} (hfit : ∀ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Fits B (registers v)) : ntm.Accepts w ↔ ∃ (x : Register k → Fin B) (y : Register k → Fin B), (∀ (i : Register k), ↑(x i) = startRegisters ntm i) ∧ Relation.ReflTransGen (fun (x y : Register k → Fin B) => RegisterStep ntm w (fun (i : Register k) => ↑(x i)) fun (i : Register k) => ↑(y i)) x y ∧ ↑(y Register.control) = stateCode none ∧ ↑(y Register.output) = 1

Acceptance on bounded register tuples: when every reachable view fits the radix B, acceptance is reachability between tuples of elements of Fin B, from a tuple holding the start registers to one with the halting control tag and output tag 1.