Deterministic machine acceptance is in PTIME

Stage 2b of the machine bridge: a deterministic run is exactly a least fixed point, so DescriptiveComplexity.DTMAccept is FO(LFP) definable – DescriptiveComplexity.dtmAccept_lfpDefinable – and hence, through the formalized translation DescriptiveComplexity.lfpDefinable_iff_sigmaSOHornDefinable, SO-Horn definable, that is, in PTIME (DescriptiveComplexity.dtmAccept_mem_PTIME).

The fixed point

Three relation variables, indexed by the time positions of the run exactly as in the Σ₁ membership proof of NTMAccept: Q t q (the state at time t), H t p (the head cell) and T t p a (the tape). The rules are the step relation read as an inductive definition:

• at the lowest position, the state is a start state, the head is on the lowest position, and the tape is the input (DescriptiveComplexity.TMData.InitTape);
• along each SuccPos t t', a transition applicable in the current state to the symbol under the head – and able to fire: a destination, a written symbol and a neighbour in its direction must exist, else the machine halts and nothing is derived at t' – advances the state, moves the head, writes its symbol, and leaves every other cell unchanged.

All the conditions are first-order over the input vocabulary, so they sit in the guards of the Horn clauses; the body atoms are the three variables read at time t, at most four per rule.

The output sentence is where FO(LFP) earns its keep over bare SO-Horn: it states positively that an accepting state occurs in the fixed point – a thing no goal clause can say – conjoined with the first-order promises (DescriptiveComplexity.TMData.WellFormed, DescriptiveComplexity.TMData.Deterministic) that DTMAccept folds into its yes-instances.

Why determinism is what makes this correct

The fixed point derives everything any run does. For a deterministic machine the run from the (unique) initial configuration is unique (DescriptiveComplexity.TMData.stepsIn_functional), so the derived atoms describe it and nothing else: soundness (DescriptiveComplexity.DTFix.derives_sound) is an induction on derivations, completeness (DescriptiveComplexity.DTFix.derivedAt_of_run) an induction along the rank of the time position, and together they make the output read exactly “the machine accepts within its budget”.

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.tmOrd : FirstOrder.Language

The ordered expansion of the machine vocabulary.

Equations

• DescriptiveComplexity.DTFix.tmOrd = FirstOrder.Language.turing.sum FirstOrder.Language.order

Guards over the machine vocabulary

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dPosnSym : tmOrd.Relations 1

The position symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dPosnSym = Sum.inl FirstOrder.Language.tmPosn

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dTrSym : tmOrd.Relations 1

The transition symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dTrSym = Sum.inl FirstOrder.Language.tmTr

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dStartSym : tmOrd.Relations 1

The start-state symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dStartSym = Sum.inl FirstOrder.Language.tmStart

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dAccSym : tmOrd.Relations 1

The accepting-state symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dAccSym = Sum.inl FirstOrder.Language.tmAcc

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dBlankSym : tmOrd.Relations 1

The blank symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dBlankSym = Sum.inl FirstOrder.Language.tmBlank

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dRightSym : tmOrd.Relations 1

The move-right symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dRightSym = Sum.inl FirstOrder.Language.tmRight

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dLeSym : tmOrd.Relations 2

The machine's own order symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dLeSym = Sum.inl FirstOrder.Language.tmLe

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dSrcSym : tmOrd.Relations 2

The transition-source symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dSrcSym = Sum.inl FirstOrder.Language.tmSrc

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dReadSym : tmOrd.Relations 2

The transition-read symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dReadSym = Sum.inl FirstOrder.Language.tmRead

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dDstSym : tmOrd.Relations 2

The transition-destination symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dDstSym = Sum.inl FirstOrder.Language.tmDst

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dWriteSym : tmOrd.Relations 2

The transition-write symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dWriteSym = Sum.inl FirstOrder.Language.tmWrite

@[reducible, inline]

abbrev DescriptiveComplexity.DTFix.dInpSym : tmOrd.Relations 2

The input symbol over the ordered expansion.

Equations

• DescriptiveComplexity.DTFix.dInpSym = Sum.inl FirstOrder.Language.tmInp

noncomputable def DescriptiveComplexity.DTFix.posnG {α : Type} (x : α) : tmOrd.Formula α

x is a position, as a guard.

Equations

• DescriptiveComplexity.DTFix.posnG x = DescriptiveComplexity.DTFix.dPosnSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.trG {α : Type} (x : α) : tmOrd.Formula α

x is a transition, as a guard.

Equations

• DescriptiveComplexity.DTFix.trG x = DescriptiveComplexity.DTFix.dTrSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.startG {α : Type} (x : α) : tmOrd.Formula α

x is a start state, as a guard.

Equations

• DescriptiveComplexity.DTFix.startG x = DescriptiveComplexity.DTFix.dStartSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.accG {α : Type} (x : α) : tmOrd.Formula α

x is an accepting state, as a guard.

Equations

• DescriptiveComplexity.DTFix.accG x = DescriptiveComplexity.DTFix.dAccSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.blankG {α : Type} (x : α) : tmOrd.Formula α

x is the blank symbol, as a guard.

Equations

• DescriptiveComplexity.DTFix.blankG x = DescriptiveComplexity.DTFix.dBlankSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.rightG {α : Type} (x : α) : tmOrd.Formula α

The transition x moves the head right, as a guard.

Equations

• DescriptiveComplexity.DTFix.rightG x = DescriptiveComplexity.DTFix.dRightSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.DTFix.leG {α : Type} (x y : α) : tmOrd.Formula α

x ≤ y in the machine's own order, as a guard.

Equations

• DescriptiveComplexity.DTFix.leG x y = DescriptiveComplexity.DTFix.dLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.srcG {α : Type} (x y : α) : tmOrd.Formula α

The transition x applies in the state y, as a guard.

Equations

• DescriptiveComplexity.DTFix.srcG x y = DescriptiveComplexity.DTFix.dSrcSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.readG {α : Type} (x y : α) : tmOrd.Formula α

The transition x reads the symbol y, as a guard.

Equations

• DescriptiveComplexity.DTFix.readG x y = DescriptiveComplexity.DTFix.dReadSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.dstG {α : Type} (x y : α) : tmOrd.Formula α

The transition x moves to the state y, as a guard.

Equations

• DescriptiveComplexity.DTFix.dstG x y = DescriptiveComplexity.DTFix.dDstSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.writeG {α : Type} (x y : α) : tmOrd.Formula α

The transition x writes the symbol y, as a guard.

Equations

• DescriptiveComplexity.DTFix.writeG x y = DescriptiveComplexity.DTFix.dWriteSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.inpG {α : Type} (x y : α) : tmOrd.Formula α

The cell x initially holds the symbol y, as a guard.

Equations

• DescriptiveComplexity.DTFix.inpG x y = DescriptiveComplexity.DTFix.dInpSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.eqG {α : Type} (x y : α) : tmOrd.Formula α

x = y, as a guard.

Equations

• DescriptiveComplexity.DTFix.eqG x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DTFix.neG {α : Type} (x y : α) : tmOrd.Formula α

x ≠ y, as a guard.

Equations

• DescriptiveComplexity.DTFix.neG x y = FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.DTFix.eqG x y)

noncomputable def DescriptiveComplexity.DTFix.minPosG {α : Type} (x : α) : tmOrd.Formula α

x is the lowest position, as a guard.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.succPosG {α : Type} (x y : α) : tmOrd.Formula α

y is the position immediately above x, as a guard.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.initTapeG {α : Type} (x y : α) : tmOrd.Formula α

The cell x initially holds the symbol y: the input where defined, the blank elsewhere.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.existsDstG {α : Type} (x : α) : tmOrd.Formula α

The transition x has a destination, as a guard.

Equations

• DescriptiveComplexity.DTFix.existsDstG x = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.DTFix.dstG (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.DTFix.existsWriteG {α : Type} (x : α) : tmOrd.Formula α

The transition x has a written symbol, as a guard.

Equations

• DescriptiveComplexity.DTFix.existsWriteG x = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.DTFix.writeG (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.DTFix.canMoveG {α : Type} (x h : α) : tmOrd.Formula α

The transition x, with the head at h, can move: there is a neighbour in its direction. Without this in every step rule the fixed point would run past a halt.

Equations

• One or more equations did not get rendered due to their size.

Realization of the guards

@[simp]

theorem DescriptiveComplexity.DTFix.realize_posnG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (posnG x).Realize v ↔ TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_trG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (trG x).Realize v ↔ TMTr (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_startG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (startG x).Realize v ↔ TMStart (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_accG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (accG x).Realize v ↔ TMAcc (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_blankG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (blankG x).Realize v ↔ TMBlank (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_rightG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (rightG x).Realize v ↔ TMRight (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_leG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (leG x y).Realize v ↔ TMLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_srcG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (srcG x y).Realize v ↔ TMSrc (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_readG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (readG x y).Realize v ↔ TMRead (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_dstG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (dstG x y).Realize v ↔ TMDst (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_writeG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (writeG x y).Realize v ↔ TMWrite (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_inpG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (inpG x y).Realize v ↔ TMInp (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_eqG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (eqG x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.DTFix.realize_neG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (neG x y).Realize v ↔ v x ≠ v y

@[simp]

theorem DescriptiveComplexity.DTFix.realize_minPosG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (minPosG x).Realize v ↔ MinPos TMLe TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_succPosG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (succPosG x y).Realize v ↔ SuccPos TMLe TMPosn (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_initTapeG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x y : α) : (initTapeG x y).Realize v ↔ (tmData A).InitTape (v x) (v y)

@[simp]

theorem DescriptiveComplexity.DTFix.realize_existsDstG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (existsDstG x).Realize v ↔ ∃ (q : A), TMDst (v x) q

@[simp]

theorem DescriptiveComplexity.DTFix.realize_existsWriteG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x : α) : (existsWriteG x).Realize v ↔ ∃ (a : A), TMWrite (v x) a

@[simp]

theorem DescriptiveComplexity.DTFix.realize_canMoveG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {α : Type} {v : α → A} (x h : α) : (canMoveG x h).Realize v ↔ (TMRight (v x) ∧ ∃ (p : A), SuccPos TMLe TMPosn (v h) p) ∨ ¬TMRight (v x) ∧ ∃ (p : A), SuccPos TMLe TMPosn p (v h)

The promises, as sentences

noncomputable def DescriptiveComplexity.DTFix.linReflS : tmOrd.Sentence

Reflexivity of the machine's order.

Equations

• DescriptiveComplexity.DTFix.linReflS = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.DTFix.leG (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.DTFix.linTransS : tmOrd.Sentence

Transitivity of the machine's order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.linAntisymmS : tmOrd.Sentence

Antisymmetry of the machine's order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.linTotalS : tmOrd.Sentence

Totality of the machine's order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.exPosnS : tmOrd.Sentence

There is a position.

Equations

• DescriptiveComplexity.DTFix.exPosnS = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.DTFix.posnG (Sum.inr 0))

noncomputable def DescriptiveComplexity.DTFix.inpFunS : tmOrd.Sentence

The input is functional.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.exBlankS : tmOrd.Sentence

There is a blank symbol.

Equations

• DescriptiveComplexity.DTFix.exBlankS = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.DTFix.blankG (Sum.inr 0))

noncomputable def DescriptiveComplexity.DTFix.blankUniqS : tmOrd.Sentence

The blank symbol is unique.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.startUniqS : tmOrd.Sentence

The start state is unique.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.trUniqS : tmOrd.Sentence

At most one transition applies in a given state on a given symbol.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dstFunS : tmOrd.Sentence

The destination of a transition is unique.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.writeFunS : tmOrd.Sentence

The written symbol of a transition is unique.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.wfS : tmOrd.Sentence

Well-formedness, as a sentence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.detS : tmOrd.Sentence

Determinism, as a sentence.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.DTFix.realize_wfS {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] : A ⊨ wfS ↔ (tmData A).WellFormed

theorem DescriptiveComplexity.DTFix.realize_detS {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] : A ⊨ detS ↔ (tmData A).Deterministic

The block and the rules

def DescriptiveComplexity.DTFix.dtBlock : SOBlock

The relation variables of the fixed point: the state Q t q, the head H t p and the tape T t p a of the run, indexed by the time positions.

Equations

• DescriptiveComplexity.DTFix.dtBlock = { ι := Option Bool, ιFinite := ⋯, arity := fun (i : Option Bool) => match i with | some true => 2 | some false => 2 | none => 3 }

def DescriptiveComplexity.DTFix.qAt (i j : Fin 9) : SOAtom dtBlock 9

The atom Q (xᵢ, xⱼ).

Equations

• DescriptiveComplexity.DTFix.qAt i j = { idx := some true, args := ![i, j] }

def DescriptiveComplexity.DTFix.hAt (i j : Fin 9) : SOAtom dtBlock 9

The atom H (xᵢ, xⱼ).

Equations

• DescriptiveComplexity.DTFix.hAt i j = { idx := some false, args := ![i, j] }

def DescriptiveComplexity.DTFix.tAt (i j l : Fin 9) : SOAtom dtBlock 9

The atom T (xᵢ, xⱼ, xₗ).

Equations

• DescriptiveComplexity.DTFix.tAt i j l = { idx := none, args := ![i, j, l] }

noncomputable def DescriptiveComplexity.DTFix.dtCQInit : HornClause tmOrd dtBlock 9

Initial state: at the lowest position, a start state.

Equations

• DescriptiveComplexity.DTFix.dtCQInit = { guard := DescriptiveComplexity.DTFix.minPosG 0 ⊓ DescriptiveComplexity.DTFix.startG 3, body := [], head := some (DescriptiveComplexity.DTFix.qAt 0 3) }

noncomputable def DescriptiveComplexity.DTFix.dtCHInit : HornClause tmOrd dtBlock 9

Initial head: at the lowest position, on the lowest position – times and cells being the same sort.

Equations

• DescriptiveComplexity.DTFix.dtCHInit = { guard := DescriptiveComplexity.DTFix.minPosG 0, body := [], head := some (DescriptiveComplexity.DTFix.hAt 0 0) }

noncomputable def DescriptiveComplexity.DTFix.dtCTInit : HornClause tmOrd dtBlock 9

Initial tape: the input, with the blank elsewhere.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtCoreG : tmOrd.Formula (Fin 9)

The shared core of the step rules: consecutive times, an applicable transition that can fire – a destination and a written symbol exist.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtBody : List (SOAtom dtBlock 9)

The shared body of the step rules: the state, the head, and the symbol under the head, at the current time.

Equations

• DescriptiveComplexity.DTFix.dtBody = [DescriptiveComplexity.DTFix.qAt 0 3, DescriptiveComplexity.DTFix.hAt 0 6, DescriptiveComplexity.DTFix.tAt 0 6 4]

noncomputable def DescriptiveComplexity.DTFix.dtCQStep : HornClause tmOrd dtBlock 9

Step, the state: the transition's destination.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtCHStepR : HornClause tmOrd dtBlock 9

Step, the head, moving right.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtCHStepL : HornClause tmOrd dtBlock 9

Step, the head, moving left.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtCWrite : HornClause tmOrd dtBlock 9

Step, the written cell.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtCFrame : HornClause tmOrd dtBlock 9

Step, the frame: every other cell is unchanged.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtRules : HornProgram tmOrd dtBlock 9

The rules of the fixed point: the step relation of the machine, read as an inductive definition along the time positions.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.DTFix.realize_dtCoreG {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : Fin 9 → A} : dtCoreG.Realize v ↔ SuccPos TMLe TMPosn (v 0) (v 1) ∧ TMTr (v 2) ∧ TMSrc (v 2) (v 3) ∧ TMRead (v 2) (v 4) ∧ (∃ (q : A), TMDst (v 2) q) ∧ ∃ (a : A), TMWrite (v 2) a

The output sentence

def DescriptiveComplexity.DTFix.dtAccAt : SOAtom dtBlock 2

The acceptance atom of the output, over two variables.

Equations

• DescriptiveComplexity.DTFix.dtAccAt = { idx := some true, args := ![0, 1] }

noncomputable def DescriptiveComplexity.DTFix.dtAccOut : (tmOrd.sum dtBlock.lang).Sentence

The positive part of the output: some time carries an accepting state in the fixed point – the statement no goal clause of a Horn program can make.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.DTFix.dtOut : (tmOrd.sum dtBlock.lang).Sentence

The output sentence: the promises, and acceptance at the fixed point.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.DTFix.dtAccAt_holds {A : Type} (ρ : dtBlock.Assignment A) (w : Fin 2 → A) : dtAccAt.Holds ρ w ↔ ρ (some true) ![w 0, w 1]

Reading the acceptance atom off an assignment.

theorem DescriptiveComplexity.DTFix.realize_dtAccOut {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : dtBlock.Assignment A) : A ⊨ dtAccOut ↔ ∃ (t : A) (q : A), ρ (some true) ![t, q] ∧ TMAcc q

theorem DescriptiveComplexity.DTFix.realize_dtOut {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : dtBlock.Assignment A) : A ⊨ dtOut ↔ (tmData A).WellFormed ∧ (tmData A).Deterministic ∧ ∃ (t : A) (q : A), ρ (some true) ![t, q] ∧ TMAcc q

Correctness

Soundness – everything derived is true of the (unique) run – is one induction on derivations; completeness – everything true of the run is derived – one induction along the rank of the time position. Determinism enters exactly where the plan said it would: a derived state atom carries some run to its time, the head and tape atoms hold of every run to theirs, and uniqueness of the run (DescriptiveComplexity.TMData.stepsIn_functional) is what lets the two readings meet in the step cases.

def DescriptiveComplexity.DTFix.DQ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (t q : A) : Prop

The derived state atoms.

Equations

• DescriptiveComplexity.DTFix.DQ t q = DescriptiveComplexity.Derives DescriptiveComplexity.DTFix.dtRules ⟨some true, ![t, q]⟩

def DescriptiveComplexity.DTFix.DH {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (t p : A) : Prop

The derived head atoms.

Equations

• DescriptiveComplexity.DTFix.DH t p = DescriptiveComplexity.Derives DescriptiveComplexity.DTFix.dtRules ⟨some false, ![t, p]⟩

def DescriptiveComplexity.DTFix.DT {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (t p a : A) : Prop

The derived tape atoms.

Equations

• DescriptiveComplexity.DTFix.DT t p a = DescriptiveComplexity.Derives DescriptiveComplexity.DTFix.dtRules ⟨none, ![t, p, a]⟩

theorem DescriptiveComplexity.DTFix.dq_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : Fin 9 → A} {i j : Fin 9} : Derives dtRules ⟨(qAt i j).idx, fun (l : Fin (dtBlock.arity (qAt i j).idx)) => v ((qAt i j).args l)⟩ ↔ DQ (v i) (v j)

theorem DescriptiveComplexity.DTFix.dh_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : Fin 9 → A} {i j : Fin 9} : Derives dtRules ⟨(hAt i j).idx, fun (l : Fin (dtBlock.arity (hAt i j).idx)) => v ((hAt i j).args l)⟩ ↔ DH (v i) (v j)

theorem DescriptiveComplexity.DTFix.dt_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : Fin 9 → A} {i j l : Fin 9} : Derives dtRules ⟨(tAt i j l).idx, fun (m : Fin (dtBlock.arity (tAt i j l).idx)) => v ((tAt i j l).args m)⟩ ↔ DT (v i) (v j) (v l)

theorem DescriptiveComplexity.DTFix.minPos_of_bitRank_eq_zero {A : Type} [FirstOrder.Language.turing.Structure A] [Finite A] (hlin : IsLinOrd TMLe) {p : A} (hp : TMPosn p) (h : bitRank TMLe TMPosn p = 0) : MinPos TMLe TMPosn p

A position of rank 0 is the lowest.

theorem DescriptiveComplexity.DTFix.exists_pos_bitRank {A : Type} [FirstOrder.Language.turing.Structure A] [Finite A] (hlin : IsLinOrd TMLe) (j : ℕ) : j < Nat.card { p : A // TMPosn p } → ∃ (t : A), TMPosn t ∧ bitRank TMLe TMPosn t = j

Every rank below the position count is realized by a position: this is where the run's ℕ-indexed clock is matched to the time positions.

def DescriptiveComplexity.DTFix.MeaningQ {A : Type} [FirstOrder.Language.turing.Structure A] (w : Fin 2 → A) : Prop

The meaning of a state atom: some run reaches its time in that state.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.DTFix.MeaningH {A : Type} [FirstOrder.Language.turing.Structure A] (w : Fin 2 → A) : Prop

The meaning of a head atom: every run to its time has the head there.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.DTFix.MeaningT {A : Type} [FirstOrder.Language.turing.Structure A] (w : Fin 3 → A) : Prop

The meaning of a tape atom: every run to its time reads that symbol.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.DTFix.Meaning {A : Type} [FirstOrder.Language.turing.Structure A] : BAtom dtBlock A → Prop

What a derived atom says about the run: a state atom carries some run to its time, a head or tape atom holds of every run to its time. The asymmetry is deliberate – the head and tape rules alone cannot certify a run exists, and the state rules can.

Equations

• DescriptiveComplexity.DTFix.Meaning ⟨some true, w⟩ = DescriptiveComplexity.DTFix.MeaningQ w
• DescriptiveComplexity.DTFix.Meaning ⟨some false, w⟩ = DescriptiveComplexity.DTFix.MeaningH w
• DescriptiveComplexity.DTFix.Meaning ⟨none, w⟩ = DescriptiveComplexity.DTFix.MeaningT w

theorem DescriptiveComplexity.DTFix.derives_sound {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) {x : BAtom dtBlock A} (h : Derives dtRules x) : Meaning x

Soundness: every derived atom is true of the run. Induction on derivations, one case per rule; in the step cases the step the rule took is compared with the run's own step through determinism.

theorem DescriptiveComplexity.DTFix.derivedAt_of_run {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] (hwf : (tmData A).WellFormed) {c₀ : Config A} (hinit : (tmData A).IsInit c₀) (k : ℕ) (t : A) : TMPosn t → bitRank TMLe TMPosn t = k → ∀ (d : Config A), (tmData A).StepsIn k c₀ d → DQ t d.state ∧ DH t d.head ∧ ∀ (p : A), DT t p (d.tape p)

Completeness: the run is derived, rank by rank. Determinism plays no role in this direction – the rules fire on whatever run is given.

theorem DescriptiveComplexity.DTFix.accepts_iff_derives {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) : (tmData A).Accepts ↔ ∃ (t : A) (q : A), DQ t q ∧ TMAcc q

The machine accepts exactly when the fixed point contains an accepting state: the two inductions above, glued by the surjectivity of the rank below the position count.

theorem DescriptiveComplexity.dtmAccept_lfpDefinable : LFPDefinable DTMAccept

Deterministic machine acceptance is FO(LFP) definable: the run is the least fixed point of the step rules, and the output states the promises and that an accepting state occurs.

theorem DescriptiveComplexity.dtmAccept_mem_PTIME : PTIME.Mem DTMAccept

Deterministic machine acceptance is in PTIME, through the formalized translation of FO(LFP) into the Horn fragment.