Positive local rules for native deterministic tableaux

The finite collection of tape-feature names is independent of the input and time bound. rowStep computes the next row using only positive occurrences of the preceding row. In particular, a cell is preserved when a positively witnessed head is elsewhere. This avoids the negative recursive head test in an ordinary tableau constraint.

The semantics are the native Turing.MultiTapeTM configurations and transition function. These rules are the local part of the machine-to-LFP construction in the proof of the Immerman–Vardi theorem; they do not assume a machine-to-formula compiler.

Main definitions

• Tag: the finite feature names, with signed work-tape coordinates.
• row: the row described by a native configuration.
• rowStep: the positive local transition rules.

Main results

• rowStep_mono: monotonicity in every preceding-row fact.

References

• N. Immerman, Relational Queries Computable in Polynomial Time, Section 3.

inductive Cslib.Complexity.ImmermanVardi.Tableau.Tag (m : ℕ) (State : Type) : Type

The input-independent names of basic features. Unary facts use every coordinate.

• state {m : ℕ} {State : Type} (q : Option State) : Tag m State

  The control state, including the halted state.

• out {m : ℕ} {State : Type} (o : Turing.OutView) : Tag m State

  The finite view of the output word.

• inPos {m : ℕ} {State : Type} : Tag m State

  The position of the input head.

• head {m : ℕ} {State : Type} (i : Fin m) (sign : Bool) : Tag m State

  The position of a work head; true is the nonnegative orientation.

• cell {m : ℕ} {State : Type} (i : Fin m) (sign : Bool) (s : Option Bool) : Tag m State

  The contents of a signed work cell.

@[instance_reducible]

instance Cslib.Complexity.ImmermanVardi.Tableau.instDecidableEqTag {m✝ : ℕ} {State✝ : Type} [DecidableEq State✝] : DecidableEq (Tag m✝ State✝)

def Cslib.Complexity.ImmermanVardi.Tableau.instDecidableEqTag.decEq {m✝ : ℕ} {State✝ : Type} [DecidableEq State✝] (x✝ x✝¹ : Tag m✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.ImmermanVardi.Tableau.instFintypeTag {m✝ : ℕ} {State✝ : Type} [Fintype State✝] : Fintype (Tag m✝ State✝)

def Cslib.Complexity.ImmermanVardi.Tableau.offset {B : ℕ} (sign : Bool) (a : Fin B) : ℤ

Interpret an oriented coordinate as an integer tape offset.

def Cslib.Complexity.ImmermanVardi.Tableau.Tag.feature {m B : ℕ} {State : Type} : Tag m State → Fin B → Turing.MultiTapeTM.Feature m State

The feature named by a tag at the specified coordinate.

@[reducible, inline]

abbrev Cslib.Complexity.ImmermanVardi.Tableau.Row (m : ℕ) (State : Type) (B : ℕ) : Type

A row of facts, represented by its positive relation entries.

def Cslib.Complexity.ImmermanVardi.Tableau.row {m B : ℕ} {State : Type} {input : List Bool} (cfg : Turing.Cfg m Bool State input) : Row m State B

The row described by a native machine configuration.

def Cslib.Complexity.ImmermanVardi.Tableau.read {m B : ℕ} {State : Type} (R : Row m State B) (i : Fin m) (s : Option Bool) : Prop

A positive witness for the symbol under a work head.

def Cslib.Complexity.ImmermanVardi.Tableau.situation {m B : ℕ} {State : Type} (input : List Bool) (R : Row m State B) (y : Turing.MultiTapeTM.Situation m State) (a : Fin B) : Prop

A positive witness for a running situation.

def Cslib.Complexity.ImmermanVardi.Tableau.elsewhere {m B : ℕ} {State : Type} (R : Row m State B) (i : Fin m) (sign : Bool) (a : Fin B) : Prop

A head known positively to be somewhere other than the specified signed cell.

def Cslib.Complexity.ImmermanVardi.Tableau.inputPrev {m B : ℕ} {State : Type} (input : List Bool) (R : Row m State B) (d : SignType) (a : Fin B) : Prop

The positive predecessor rule for an input-head movement, including clamped end cells.

def Cslib.Complexity.ImmermanVardi.Tableau.headPrev {m B : ℕ} {State : Type} (R : Row m State B) (i : Fin m) (sign : Bool) (d : SignType) (a : Fin B) : Prop

The positive predecessor rule for a work-head movement, in the target orientation.

noncomputable def Cslib.Complexity.ImmermanVardi.Tableau.rowStep {m B : ℕ} {State : Type} (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) (R : Row m State B) : Row m State B

Positive local transition rules for each basic feature.

theorem Cslib.Complexity.ImmermanVardi.Tableau.rowStep_mono {m B : ℕ} {State : Type} (tm : Turing.MultiTapeTM m Bool State) (input : List Bool) {R S : Row m State B} (h : ∀ (q : Tag m State) (a : Fin B), R q a → S q a) (q : Tag m State) (a : Fin B) : rowStep tm input R q a → rowStep tm input S q a

Every recursive occurrence in the local transition rules is monotone.