The number written by a machine is in FP

DescriptiveComplexity.dtmNumber_mem_FP: a definition in QFO(LFP) of DescriptiveComplexity.DTMNumber.

• The fixed point is the one of deterministic machine acceptance (DescriptiveComplexity.DTFix.dtRules): the state, the head and the tape of the run, indexed by the time positions.
• The machine halts at a time whose configuration admits no step, and accepts when the state there is accepting: a first-order condition on the fixed point (DescriptiveComplexity.MachNum.halted_iff); a negation, which the output of a definition in QFO(LFP) is free to use.
• The output is the term Σp. [p is an output cell holding a one at the halting time] · Πq. ([q is an output cell before p on the tape] + 1), as for the number written by a circuit.

Halting, read off the fixed point

def DescriptiveComplexity.MachNum.Core {A : Type} [FirstOrder.Language.turing.Structure A] (q h a : A) : Prop

Some transition applies in the state q to the symbol a with the head at h, and can fire.

Equations

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

theorem DescriptiveComplexity.MachNum.halted_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) (p s : A) : (∃ (t : A) (q : A) (h : A) (a : A), DTFix.DQ t q ∧ DTFix.DH t h ∧ DTFix.DT t h a ∧ ¬Core q h a ∧ TMAcc q ∧ DTFix.DT t p s) ↔ ∃ (c : Config A), (tmData A).Halts c ∧ (tmData A).Acc c.state ∧ c.tape p = s

The halting configuration, in the fixed point: a cell holds a symbol when the machine halts exactly when the fixed point has a time whose configuration admits no step and whose tape holds that symbol there.

The definition

@[reducible, inline]

abbrev DescriptiveComplexity.MachNum.numLang : FirstOrder.Language

The vocabulary of the rules: machines writing a number, with the order.

Equations

• DescriptiveComplexity.MachNum.numLang = FirstOrder.Language.turingOut.sum FirstOrder.Language.order

def DescriptiveComplexity.MachNum.ordHom : DTFix.tmOrd →ᴸ numLang

The vocabulary of the rules of machine acceptance, read in the one of the rules here.

Equations

• DescriptiveComplexity.MachNum.ordHom = FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id FirstOrder.Language.order)

instance DescriptiveComplexity.MachNum.ordHom_isExpansionOn (A : Type) [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] : ordHom.IsExpansionOn A

noncomputable def DescriptiveComplexity.MachNum.numRules : List (HornClause numLang DTFix.dtBlock 9)

The rules of the run, over the larger vocabulary.

Equations

• DescriptiveComplexity.MachNum.numRules = List.map (DescriptiveComplexity.HornClause.onLang DescriptiveComplexity.MachNum.ordHom) DescriptiveComplexity.DTFix.dtRules

@[reducible, inline]

abbrev DescriptiveComplexity.MachNum.outLang : FirstOrder.Language

The vocabulary of the output: the rules', and the relations of the run.

Equations

• DescriptiveComplexity.MachNum.outLang = DescriptiveComplexity.MachNum.numLang.sum DescriptiveComplexity.DTFix.dtBlock.lang

def DescriptiveComplexity.MachNum.outHom : DTFix.tmOrd →ᴸ outLang

The vocabulary of the guards, read in the one of the output.

Equations

• DescriptiveComplexity.MachNum.outHom = FirstOrder.Language.LHom.sumInl.comp DescriptiveComplexity.MachNum.ordHom

noncomputable def DescriptiveComplexity.MachNum.outA {γ : Type} (x : γ) : outLang.Formula γ

“Is an output cell”.

Equations

• DescriptiveComplexity.MachNum.outA x = FirstOrder.Language.Relations.formula₁ (Sum.inl (Sum.inl DescriptiveComplexity.mnOut)) (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.MachNum.oneA {γ : Type} (x : γ) : outLang.Formula γ

“Is read as the digit 1”.

Equations

• DescriptiveComplexity.MachNum.oneA x = FirstOrder.Language.Relations.formula₁ (Sum.inl (Sum.inl DescriptiveComplexity.mnOne)) (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.MachNum.leA {γ : Type} (x y : γ) : outLang.Formula γ

The order of the tape.

Equations

• DescriptiveComplexity.MachNum.leA x y = FirstOrder.Language.Relations.formula₂ (Sum.inl (Sum.inl DescriptiveComplexity.mnLe)) (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.MachNum.qA {γ : Type} (t q : γ) : outLang.Formula γ

The state of the run at a time.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.hA {γ : Type} (t h : γ) : outLang.Formula γ

The head of the run at a time.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.tA {γ : Type} (t p a : γ) : outLang.Formula γ

The tape of the run at a time.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.accA {γ : Type} (x : γ) : outLang.Formula γ

“Is an accepting state”.

Equations

• DescriptiveComplexity.MachNum.accA x = DescriptiveComplexity.MachNum.outHom.onFormula (DescriptiveComplexity.DTFix.accG x)

noncomputable def DescriptiveComplexity.MachNum.coreF {γ : Type} (q h a : γ) : outLang.Formula γ

Some transition applies and can fire.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.digitF : outLang.Formula (Empty ⊕ Fin 1)

“The instance is a well-formed deterministic machine, and p is an output cell holding a one when it halts.”

Equations

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

noncomputable def DescriptiveComplexity.MachNum.lowF : outLang.Formula ((Empty ⊕ Fin 1) ⊕ Fin 1)

“q is an output cell strictly before p”.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.numOut : QTerm outLang Empty

The output term.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.numDef : QLFPDef FirstOrder.Language.turingOut

The definition of the number written by a machine in QFO(LFP).

Equations

• DescriptiveComplexity.MachNum.numDef = { B := DescriptiveComplexity.DTFix.dtBlock, k := 9, rules := DescriptiveComplexity.MachNum.numRules, out := DescriptiveComplexity.MachNum.numOut }

The value of the definition

@[reducible, inline]

abbrev DescriptiveComplexity.MachNum.outStr (A : Type) [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] : outLang.Structure A

The structure the output is read in.

Equations

• DescriptiveComplexity.MachNum.outStr A = DescriptiveComplexity.MachNum.numLang.sumStructure DescriptiveComplexity.DTFix.dtBlock.lang A

instance DescriptiveComplexity.MachNum.outHom_isExpansionOn {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] : outHom.IsExpansionOn A

theorem DescriptiveComplexity.MachNum.lfp_numRules {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] (i : DTFix.dtBlock.ι) (x : Fin (DTFix.dtBlock.arity i) → A) : lfpAssign numRules i x ↔ Derives DTFix.dtRules ⟨i, x⟩

theorem DescriptiveComplexity.MachNum.realize_qA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (t q : γ) : (qA t q).Realize v ↔ DTFix.DQ (v t) (v q)

theorem DescriptiveComplexity.MachNum.realize_hA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (t h : γ) : (hA t h).Realize v ↔ DTFix.DH (v t) (v h)

theorem DescriptiveComplexity.MachNum.realize_tA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (t p a : γ) : (tA t p a).Realize v ↔ DTFix.DT (v t) (v p) (v a)

theorem DescriptiveComplexity.MachNum.realize_outA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (x : γ) : (outA x).Realize v ↔ FirstOrder.Language.Structure.RelMap mnOut ![v x]

theorem DescriptiveComplexity.MachNum.realize_oneA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (x : γ) : (oneA x).Realize v ↔ FirstOrder.Language.Structure.RelMap mnOne ![v x]

theorem DescriptiveComplexity.MachNum.realize_leA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (x y : γ) : (leA x y).Realize v ↔ FirstOrder.Language.Structure.RelMap mnLe ![v x, v y]

theorem DescriptiveComplexity.MachNum.realize_accA {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (x : γ) : (accA x).Realize v ↔ TMAcc (v x)

theorem DescriptiveComplexity.MachNum.realize_coreF {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] {γ : Type} (v : γ → A) (q h a : γ) : (coreF q h a).Realize v ↔ Core (v q) (v h) (v a)

theorem DescriptiveComplexity.MachNum.realize_digitF {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] [Finite A] (w : Fin 1 → A) : digitF.Realize (Sum.elim default w) ↔ ((tmData A).WellFormed ∧ (tmData A).Deterministic) ∧ OutDigit (w 0)

theorem DescriptiveComplexity.MachNum.realize_lowF {A : Type} [FirstOrder.Language.turingOut.Structure A] [LinearOrder A] (w u : Fin 1 → A) : lowF.Realize (Sum.elim (Sum.elim default w) u) ↔ LowerCell (w 0) (u 0)

theorem DescriptiveComplexity.dtmNumber_fpDefinable : FPDefinable DTMNumber

The number written by a machine is definable in QFO(LFP).

theorem DescriptiveComplexity.dtmNumber_mem_FP : FP.Mem DTMNumber

The number written by a deterministic machine is in FP.