A least fixed point for the native deterministic computation tableau

One ternary relation stores (feature tag, time, position). Its positive transformer adds initial facts and consequences of the preceding row. The least fixed point is exactly the native deterministic run, uniformly for every finite domain large enough to hold the input endmarkers and the fixed finite collection of tags.

Main definitions

• tagIndex: input-independent numerical feature tags.
• initial: the initial native row, independent of the input bits.
• traceRow: project a ternary relation to a named row.
• traceStep: the monotone tableau transformer.

Main results

• traceStep_lfp: the least fixed point equals the native run tableau.
• traceRow_lfp: a named row of the fixed point agrees with the corresponding native run.

noncomputable def Cslib.Complexity.ImmermanVardi.Tableau.tagIndex {m : ℕ} {State : Type} [Fintype State] (q : Tag m State) : ℕ

A fixed numerical encoding of the finite set of feature names.

theorem Cslib.Complexity.ImmermanVardi.Tableau.tagIndex_injective {m : ℕ} {State : Type} [Fintype State] : Function.Injective tagIndex

The tag encoding is injective.

theorem Cslib.Complexity.ImmermanVardi.Tableau.tagIndex_lt {m B : ℕ} {State : Type} [Fintype State] (hB : Fintype.card (Tag m State) ≤ B) (q : Tag m State) : tagIndex q < B

Every feature tag fits in a domain at least as large as the set of names.

def Cslib.Complexity.ImmermanVardi.Tableau.initial {m B : ℕ} {State : Type} (tm : Turing.MultiTapeTM m Bool State) : Row m State B

The initial row of a native machine, with blank work tapes and input head at one.

theorem Cslib.Complexity.ImmermanVardi.Tableau.initial_iff {m B : ℕ} {State : Type} (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (q : Tag m State) (a : Fin B) : initial tm q a ↔ row (tm.initCfg input) q a

The explicit initial row agrees with the actual native initial configuration.

def Cslib.Complexity.ImmermanVardi.Tableau.traceRow {m B : ℕ} {State : Type} [Fintype State] (R : Set (Fin 3 → Fin B)) (t : Fin B) : Row m State B

The row of a ternary relation at time t, using the fixed feature tags.

noncomputable def Cslib.Complexity.ImmermanVardi.Tableau.traceStep {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) : Set (Fin 3 → Fin B) →o Set (Fin 3 → Fin B)

The positive, time-indexed tableau transformer.

def Cslib.Complexity.ImmermanVardi.Tableau.runTable {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) : Set (Fin 3 → Fin B)

The canonical ternary relation of all rows of the bounded native run.

theorem Cslib.Complexity.ImmermanVardi.Tableau.traceRow_runTable {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (hB : Fintype.card (Tag m State) ≤ B) (t : Fin B) (q : Tag m State) (a : Fin B) : traceRow (runTable tm input) t q a ↔ row (Turing.MultiTapeTM.runFrom (tm.initCfg input) ↑t) q a

Projecting the canonical ternary table recovers exactly the desired native row.

theorem Cslib.Complexity.ImmermanVardi.Tableau.traceStep_runTable_le {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : (traceStep tm input) (runTable tm input) ⊆ runTable tm input

The exact native table is closed under all positive tableau rules.

theorem Cslib.Complexity.ImmermanVardi.Tableau.runTable_le_traceStep_lfp {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : runTable tm input ⊆ OrderHom.lfp (traceStep tm input)

The least fixed point contains every native row.

theorem Cslib.Complexity.ImmermanVardi.Tableau.traceStep_lfp {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : OrderHom.lfp (traceStep tm input) = runTable tm input

The native deterministic tableau is exactly a least fixed point of positive local rules.

theorem Cslib.Complexity.ImmermanVardi.Tableau.traceRow_lfp {m B : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) (t : Fin B) (q : Tag m State) (a : Fin B) : traceRow (OrderHom.lfp (traceStep tm input)) t q a ↔ row (Turing.MultiTapeTM.runFrom (tm.initCfg input) ↑t) q a

Each named row of the least fixed point is the corresponding native configuration.