Compact configuration graph: local arithmetic

The graph stores no input word. A vertex is a fixed tuple of natural registers packed in a radix B: the input position, control, output summary, and three registers per work tape. Logarithmic space uses the radix (n+2)^D (Turing.MultiTapeNTM.ConfigurationGraph.radix); larger space bounds use larger radices. An edge consults at most the input bit at queryIndex; the supplied symbol is ignored at the blank boundaries. The transition table is fixed independently of n.

Every edge checks both vertex bounds, the semantic tag ranges and successor-register overflow. The three output tags mean empty, exactly true, and permanently rejecting. In particular, an emission after either nonempty output tag gives the rejecting tag.

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.vertexID: pack the input-free view.
• Turing.MultiTapeNTM.ConfigurationGraph.vertexWidth: the number of bits of a vertex ID.
• Turing.MultiTapeNTM.ConfigurationGraph.queryIndex: the only requested input-bit position.
• Turing.MultiTapeNTM.ConfigurationGraph.edgeWithSymbol: guarded local edge query.
• Turing.MultiTapeNTM.ConfigurationGraph.bad: accepting halted vertices.
• Turing.MultiTapeNTM.ConfigurationGraph.overflow: vertices whose source step leaves the radix.

References

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

inductive Turing.MultiTapeNTM.ConfigurationGraph.Register (k : ℕ) : Type

The fixed register names for a machine with k tapes.

• inputPos {k : ℕ} : Register k
• control {k : ℕ} : Register k
• output {k : ℕ} : Register k
• head {k : ℕ} (i : Fin k) : Register k
• left {k : ℕ} (i : Fin k) : Register k
• right {k : ℕ} (i : Fin k) : Register k

@[instance_reducible]

instance Turing.MultiTapeNTM.ConfigurationGraph.instDecidableEqRegister {k✝ : ℕ} : DecidableEq (Register k✝)

def Turing.MultiTapeNTM.ConfigurationGraph.instDecidableEqRegister.decEq {k✝ : ℕ} (x✝ x✝¹ : Register k✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Turing.MultiTapeNTM.ConfigurationGraph.instFintypeRegister {k✝ : ℕ} : Fintype (Register k✝)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.stateCode {State : Type} [Fintype State] (q : Option State) : ℕ

A fixed finite control tag, including a distinct halting tag.

def Turing.MultiTapeNTM.ConfigurationGraph.outputCode (w : List Bool) : ℕ

Empty output is zero; the singleton true is one; everything else is rejecting.

def Turing.MultiTapeNTM.ConfigurationGraph.outputStep (o : ℕ) : Option Bool → ℕ

Update the acceptance summary on an optional emission.

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

The fixed tuple of input-free registers of a view.

def Turing.MultiTapeNTM.ConfigurationGraph.radix (D n : ℕ) : ℕ

The radix (n+2)^D used in logarithmic space, with an exponent fixed with the source machine and its space constant.

def Turing.MultiTapeNTM.ConfigurationGraph.vertexBound {k : ℕ} (B : ℕ) : ℕ

Number of vertices in the ambient graph of radix B, including invalid IDs.

def Turing.MultiTapeNTM.ConfigurationGraph.vertexWidth (k B : ℕ) : ℕ

The number of bits of a vertex of the graph of radix B: every vertex ID is below 2 ^ vertexWidth k B.

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexBound_lt_two_pow_vertexWidth (k B : ℕ) : vertexBound B < 2 ^ vertexWidth k B

Every vertex ID of the graph of radix B fits in vertexWidth k B bits.

def Turing.MultiTapeNTM.ConfigurationGraph.Fits {k : ℕ} (B : ℕ) (r : Register k → ℕ) : Prop

All components fit below the radix.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.vertexID {k : ℕ} {State : Type} [Fintype State] (B : ℕ) (v : FiniteCfg k Bool State) : ℕ

Packed input-free configuration ID.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.readRegisters {k : ℕ} (B u : ℕ) : Register k → ℕ

Read the registers of an arbitrary ID.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.queryIndex {k : ℕ} (B u : ℕ) : ℕ

The input bit to request, in the native zero-based word indexing. Boundary requests are ignored by inputSymbol; the right boundary may request the absent bit at n.

def Turing.MultiTapeNTM.ConfigurationGraph.inputSymbol (n p : ℕ) (symbol : Option Bool) : Option Bool

Force blank at both boundaries; otherwise use the one externally supplied input symbol.

def Turing.MultiTapeNTM.ConfigurationGraph.inputMove (n p : ℕ) : SignType → ℕ

Clamped movement of the input head, computed on its binary position.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.nextRegisters {k : ℕ} {State : Type} [Fintype State] (n : ℕ) (r : Register k → ℕ) (a : Action k Bool State) : Register k → ℕ

Update the fixed register tuple by a fixed native action.

def Turing.MultiTapeNTM.ConfigurationGraph.actionEquiv {k : ℕ} {State : Type} : Action k Bool State ≃ SignType × (Fin k → Option (Option Bool) × SignType) × Option Bool × Option State

The finite tuple of fields of a native action.

@[instance_reducible]

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.instFintypeActionBool {k : ℕ} {State : Type} [Fintype State] : Fintype (Action k Bool State)

Native actions form a finite type over finite control and a fixed tape count.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.ConfigurationGraph.Instruction (k : ℕ) (State : Type) : Type

One entry in the machine's fixed finite transition table.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.instructions {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : List (Instruction k State)

The finite table is selected once from the source transition relation. Its selection need not be uniform in the machine; no runtime input influences this table.

theorem Turing.MultiTapeNTM.ConfigurationGraph.mem_instructions {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (t : Instruction k State) : t ∈ instructions ntm ↔ ntm.Tr t.1 t.2.1 t.2.2.1 t.2.2.2

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.valid {k : ℕ} {State : Type} [Fintype State] (B n u : ℕ) : Bool

Syntactic validity of an ID. All ternary stack naturals are canonical; only finite tags, input geometry, and the overall bound require guards.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.matchesEntry {k : ℕ} {State : Type} [Fintype State] (n : ℕ) (r : Register k → ℕ) (symbol : Option Bool) (t : Instruction k State) : Bool

Check that a decoded source has the observations of a fixed table entry.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.fitsB {k : ℕ} (B : ℕ) (r : Register k → ℕ) : Bool

Guard every successor component against radix overflow.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.edgeWithSymbol {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B n u v : ℕ) (symbol : Option Bool) : Bool

One actual input read suffices for this edge predicate. The work is arithmetic on the short stored arguments and a fixed finite transition table.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.bad {k : ℕ} {State : Type} [Fintype State] (B n u : ℕ) : Bool

Accepting halted vertices, the bad set for complement reachability.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.overflow {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B n u : ℕ) (symbol : Option Bool) : Bool

Vertices with a matching transition whose successor overflows the radix. These are the represented views from which the source leaves the graph of radix B.

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

The start vertex depends only on the radix, since initial storage is blank.

def Turing.MultiTapeNTM.ConfigurationGraph.Edge {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (w : List Bool) (u v : ℕ) : Prop

The graph on an actual input; it reads no other bit than queryIndex.

def Turing.MultiTapeNTM.ConfigurationGraph.Overflow {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (w : List Bool) (u : ℕ) : Prop

The overflow test on an actual input, reading the bit at queryIndex.