The number written by a machine: definition

The function counterpart of deterministic machine acceptance (DescriptiveComplexity.DTMAccept): the machine is data in the instance, and the problem is to compute the number it leaves on its tape.

• The vocabulary is the one of machine instances (FirstOrder.Language.turing) with two more symbols (FirstOrder.Language.tapeOut): out marks the output cells and one marks the symbols read as the digit 1.
• The machine halts (DescriptiveComplexity.TMData.Halts) in a configuration reached from the initial one within the clock – fewer steps than there are positions, as for acceptance – from which no step is possible. A deterministic machine halts in at most one configuration (DescriptiveComplexity.TMData.halts_unique).
• DescriptiveComplexity.machineNumber: an output cell holding, when the machine halts in an accepting state, a symbol marked one contributes 2 ^ r, where r is the number of output cells strictly before it on the tape: the digits are read in tape order, the lowest cell holding the least significant one. A machine that does not halt within its clock, or halts without accepting, writes 0, and so does an instance that is not a well-formed deterministic machine.

@[reducible, inline]

abbrev FirstOrder.Language.tpOne : Language.tapeOut.Relations 1

one a: the symbol a is read as the digit 1.

Equations

• FirstOrder.Language.tpOne = FirstOrder.Language.tapeOutRel.one

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTapeOutRel {a✝ : ℕ} : DecidableEq (tapeOutRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTapeOutRel = FirstOrder.Language.instDecidableEqTapeOutRel.decEq

inductive FirstOrder.Language.tapeOutRel : ℕ → Type

The relation symbols of the language.

• out : tapeOutRel 1

  out p: the cell p is an output cell, holding one digit.

• one : tapeOutRel 1

  one a: the symbol a is read as the digit 1.

def FirstOrder.Language.instDecidableEqTapeOutRel.decEq {a✝ : ℕ} (x✝ x✝¹ : tapeOutRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqTapeOutRel.decEq FirstOrder.Language.tapeOutRel.out FirstOrder.Language.tapeOutRel.out = isTrue FirstOrder.Language.instDecidableEqTapeOutRel.decEq._proof_1
• FirstOrder.Language.instDecidableEqTapeOutRel.decEq FirstOrder.Language.tapeOutRel.out FirstOrder.Language.tapeOutRel.one = isFalse FirstOrder.Language.instDecidableEqTapeOutRel.decEq._proof_3
• FirstOrder.Language.instDecidableEqTapeOutRel.decEq FirstOrder.Language.tapeOutRel.one FirstOrder.Language.tapeOutRel.out = isFalse FirstOrder.Language.instDecidableEqTapeOutRel.decEq._proof_4
• FirstOrder.Language.instDecidableEqTapeOutRel.decEq FirstOrder.Language.tapeOutRel.one FirstOrder.Language.tapeOutRel.one = isTrue FirstOrder.Language.instDecidableEqTapeOutRel.decEq._proof_2

@[reducible, inline]

abbrev FirstOrder.Language.tpOut : Language.tapeOut.Relations 1

out p: the cell p is an output cell, holding one digit.

Equations

• FirstOrder.Language.tpOut = FirstOrder.Language.tapeOutRel.out

def FirstOrder.Language.tapeOut : Language

The symbols reading a number off the tape of a machine.

Equations

• FirstOrder.Language.tapeOut = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.tapeOutRel }

instance FirstOrder.Language.instIsRelationalTapeOut : Language.tapeOut.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.turingOut : Language

The relational language of machines writing a number.

Equations

• FirstOrder.Language.turingOut = FirstOrder.Language.turing.sum FirstOrder.Language.tapeOut

Halting

def DescriptiveComplexity.TMData.Halts {A : Type} (M : TMData A) (c : Config A) : Prop

The machine halts in the configuration c: c is reached from an initial configuration within the clock, and no step is possible from it.

Equations

• M.Halts c = ∃ (c₀ : DescriptiveComplexity.Config A) (n : ℕ), M.IsInit c₀ ∧ n < Nat.card { p : A // M.Posn p } ∧ M.StepsIn n c₀ c ∧ ∀ (e : DescriptiveComplexity.Config A), ¬M.Step c e

theorem DescriptiveComplexity.TMData.halts_unique {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) (hdet : M.Deterministic) {c d : Config A} (hc : M.Halts c) (hd : M.Halts d) : c = d

A deterministic machine halts in at most one configuration.

theorem DescriptiveComplexity.TMData.Agree.trans {A : Type} {M : TMData A} {B C : Type} {u : B ≃ A} {v : C ≃ B} {N : TMData B} {K : TMData C} (h₁ : Agree v K N) (h₂ : Agree u N M) : Agree (v.trans u) K M

Agreements compose.

The number

@[reducible, inline]

abbrev DescriptiveComplexity.mnOut : FirstOrder.Language.turingOut.Relations 1

“Is an output cell”, in the vocabulary of machines writing a number.

Equations

• DescriptiveComplexity.mnOut = Sum.inr FirstOrder.Language.tpOut

@[reducible, inline]

abbrev DescriptiveComplexity.mnOne : FirstOrder.Language.turingOut.Relations 1

“Is read as the digit 1”, in the vocabulary of machines writing a number.

Equations

• DescriptiveComplexity.mnOne = Sum.inr FirstOrder.Language.tpOne

@[reducible, inline]

abbrev DescriptiveComplexity.mnLe : FirstOrder.Language.turingOut.Relations 2

The order of the tape, in the vocabulary of machines writing a number.

Equations

• DescriptiveComplexity.mnLe = Sum.inl FirstOrder.Language.tmLe

@[instance_reducible]

instance DescriptiveComplexity.turingOutStructure (A : Type) [FirstOrder.Language.turingOut.Structure A] : FirstOrder.Language.turing.Structure A

A machine writing a number is a machine.

Equations

• DescriptiveComplexity.turingOutStructure A = FirstOrder.Language.LHom.sumInl.reduct A

def DescriptiveComplexity.OutDigit {A : Type} [FirstOrder.Language.turingOut.Structure A] (p : A) : Prop

The output cell p holds the digit 1 when the machine halts, in an accepting state.

Equations

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

def DescriptiveComplexity.LowerCell {A : Type} [FirstOrder.Language.turingOut.Structure A] (p q : A) : Prop

q is an output cell strictly before p on the tape.

Equations

• DescriptiveComplexity.LowerCell p q = (FirstOrder.Language.Structure.RelMap DescriptiveComplexity.mnOut ![q] ∧ q ≠ p ∧ FirstOrder.Language.Structure.RelMap DescriptiveComplexity.mnLe ![q, p])

noncomputable def DescriptiveComplexity.cellRank {A : Type} [FirstOrder.Language.turingOut.Structure A] (p : A) : ℕ

The rank of a cell among the output cells: the number of output cells strictly before it on the tape.

Equations

• DescriptiveComplexity.cellRank p = Nat.card { q : A // DescriptiveComplexity.LowerCell p q }

noncomputable def DescriptiveComplexity.machineNumber (A : Type) [FirstOrder.Language.turingOut.Structure A] : ℕ

The number written by a machine: each output cell holding the digit 1 when the machine halts and accepts contributes two to the power of its rank among the output cells. Instances that are not well-formed deterministic machines write 0.

Equations

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

Isomorphism-invariance and the bundled problem

theorem DescriptiveComplexity.machineNumber_iso {A B : Type} [FirstOrder.Language.turingOut.Structure A] [FirstOrder.Language.turingOut.Structure B] (e : FirstOrder.Language.turingOut.Equiv A B) : machineNumber A = machineNumber B

The number written is isomorphism-invariant.

noncomputable def DescriptiveComplexity.DTMNumber : CountingProblem FirstOrder.Language.turingOut

The number written by a deterministic machine, as a counting problem on Language.turingOut-structures: the function counterpart of DescriptiveComplexity.DTMAccept.

Equations

• DescriptiveComplexity.DTMNumber = { Count := fun (A : Type) (inst : FirstOrder.Language.turingOut.Structure A) => DescriptiveComplexity.machineNumber A, iso_invariant := ⋯ }