Machine acceptance as a decision problem

The vocabulary of the machine bridge, and the problem the bridge is about: a nondeterministic Turing machine is data in an instance, and

does this machine accept its input within as many steps as there are positions?

is DescriptiveComplexity.NTMAccept, an ordinary iso-invariant problem of the catalog. The semantics it reads is DescriptiveComplexity.TMData, defined without a vocabulary in DescriptiveComplexity.Machines.

The vocabulary

FirstOrder.Language.turing carries, following design decision (a) of the plan, no relation of arity above two: a transition is an element τ of the universe with four binary attributes tsrc/tread/tdst/twrite and a unary mark right, rather than a single 5-ary symbol. An FOInterpretation supplies one defining formula per tuple of tags, so a 5-ary symbol would mean |Tag|⁵ formula cases; keeping every symbol binary keeps the reductions of stages 3 and 4 in the regime the rest of the catalog lives in.

Positions are both tape cells and time steps (design decision (b)), so the budget of DescriptiveComplexity.TMData.Accepts is unary by construction and no arithmetic is needed anywhere.

Well-formedness

Being a linear order is not automatic for a relation symbol, so – exactly as DescriptiveComplexity.IsLinOrd for Knapsack, and WidthAtMostThree for 3SAT – it is folded into the yes-instances, together with the other promises of DescriptiveComplexity.TMData.WellFormed. All of them are first-order, so the Σ₁ kernel of the membership proof can check them.

A deviation from the plan, recorded

The original machine design listed state and sym sorts alongside posn and tr. They are omitted here because nothing in the semantics or in the membership proof reads them: a junk element is harmless as a state, since it is reachable only through a transition, and a reduction controls which elements it marks accepting. If stage 3 turns out to want them, adding a unary symbol is a local change to this file and to the well-formedness predicate.

inductive FirstOrder.Language.turingRel : ℕ → Type

Relation symbols of machine instances.

• posn : turingRel 1

  posn p: p is a position – a tape cell, and equally a time step.

• tr : turingRel 1

  tr τ: τ is a transition.

• start : turingRel 1

  start q: q is a start state.

• acc : turingRel 1

  acc q: q is an accepting state.

• blank : turingRel 1

  blank a: a is the blank symbol.

• right : turingRel 1

  right τ: the transition τ moves the head right.

• le : turingRel 2

  le p q: the linear order along which the head moves.

• tsrc : turingRel 2

  tsrc τ q: τ applies in the state q.

• tread : turingRel 2

  tread τ a: τ applies when reading the symbol a.

• tdst : turingRel 2

  tdst τ q: τ moves to the state q.

• twrite : turingRel 2

  twrite τ a: τ writes the symbol a.

• inp : turingRel 2

  inp p a: the cell p initially holds the symbol a.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTuringRel {a✝ : ℕ} : DecidableEq (turingRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTuringRel = FirstOrder.Language.instDecidableEqTuringRel.decEq

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

Equations

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

def FirstOrder.Language.turing : Language

The relational language of machine instances: positions with their order, transitions with their attributes, the distinguished states and symbol, and the initial tape.

Equations

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

instance FirstOrder.Language.instIsRelationalTuring : Language.turing.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tmPosn : Language.turing.Relations 1

The position symbol.

Equations

• FirstOrder.Language.tmPosn = FirstOrder.Language.turingRel.posn

@[reducible, inline]

abbrev FirstOrder.Language.tmTr : Language.turing.Relations 1

The transition symbol.

Equations

• FirstOrder.Language.tmTr = FirstOrder.Language.turingRel.tr

@[reducible, inline]

abbrev FirstOrder.Language.tmStart : Language.turing.Relations 1

The start-state symbol.

Equations

• FirstOrder.Language.tmStart = FirstOrder.Language.turingRel.start

@[reducible, inline]

abbrev FirstOrder.Language.tmAcc : Language.turing.Relations 1

The accepting-state symbol.

Equations

• FirstOrder.Language.tmAcc = FirstOrder.Language.turingRel.acc

@[reducible, inline]

abbrev FirstOrder.Language.tmBlank : Language.turing.Relations 1

The blank symbol.

Equations

• FirstOrder.Language.tmBlank = FirstOrder.Language.turingRel.blank

@[reducible, inline]

abbrev FirstOrder.Language.tmRight : Language.turing.Relations 1

The move-right symbol.

Equations

• FirstOrder.Language.tmRight = FirstOrder.Language.turingRel.right

@[reducible, inline]

abbrev FirstOrder.Language.tmLe : Language.turing.Relations 2

The order symbol.

Equations

• FirstOrder.Language.tmLe = FirstOrder.Language.turingRel.le

@[reducible, inline]

abbrev FirstOrder.Language.tmSrc : Language.turing.Relations 2

The transition-source symbol.

Equations

• FirstOrder.Language.tmSrc = FirstOrder.Language.turingRel.tsrc

@[reducible, inline]

abbrev FirstOrder.Language.tmRead : Language.turing.Relations 2

The transition-read symbol.

Equations

• FirstOrder.Language.tmRead = FirstOrder.Language.turingRel.tread

@[reducible, inline]

abbrev FirstOrder.Language.tmDst : Language.turing.Relations 2

The transition-destination symbol.

Equations

• FirstOrder.Language.tmDst = FirstOrder.Language.turingRel.tdst

@[reducible, inline]

abbrev FirstOrder.Language.tmWrite : Language.turing.Relations 2

The transition-write symbol.

Equations

• FirstOrder.Language.tmWrite = FirstOrder.Language.turingRel.twrite

@[reducible, inline]

abbrev FirstOrder.Language.tmInp : Language.turing.Relations 2

The input symbol.

Equations

• FirstOrder.Language.tmInp = FirstOrder.Language.turingRel.inp

The shorthands of the vocabulary

def DescriptiveComplexity.TMPosn {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Being a position.

Equations

• DescriptiveComplexity.TMPosn a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![a]

def DescriptiveComplexity.TMTr {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Being a transition.

Equations

• DescriptiveComplexity.TMTr a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmTr ![a]

def DescriptiveComplexity.TMStart {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Being a start state.

Equations

• DescriptiveComplexity.TMStart a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmStart ![a]

def DescriptiveComplexity.TMAcc {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Being an accepting state.

Equations

• DescriptiveComplexity.TMAcc a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmAcc ![a]

def DescriptiveComplexity.TMBlank {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Being the blank symbol.

Equations

• DescriptiveComplexity.TMBlank a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmBlank ![a]

def DescriptiveComplexity.TMRight {A : Type} [FirstOrder.Language.turing.Structure A] (a : A) : Prop

Moving the head right.

Equations

• DescriptiveComplexity.TMRight a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmRight ![a]

def DescriptiveComplexity.TMLe {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The order on positions.

Equations

• DescriptiveComplexity.TMLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![a, b]

def DescriptiveComplexity.TMSrc {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The state a transition applies in.

Equations

• DescriptiveComplexity.TMSrc a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmSrc ![a, b]

def DescriptiveComplexity.TMRead {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The symbol a transition reads.

Equations

• DescriptiveComplexity.TMRead a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmRead ![a, b]

def DescriptiveComplexity.TMDst {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The state a transition moves to.

Equations

• DescriptiveComplexity.TMDst a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmDst ![a, b]

def DescriptiveComplexity.TMWrite {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The symbol a transition writes.

Equations

• DescriptiveComplexity.TMWrite a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmWrite ![a, b]

def DescriptiveComplexity.TMInp {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) : Prop

The initial contents of a cell.

Equations

• DescriptiveComplexity.TMInp a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmInp ![a, b]

def DescriptiveComplexity.tmData (A : Type) [FirstOrder.Language.turing.Structure A] : TMData A

The machine an instance describes.

Equations

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

The problem

theorem DescriptiveComplexity.agree_of_equiv {A B : Type} [FirstOrder.Language.turing.Structure A] [FirstOrder.Language.turing.Structure B] (e : FirstOrder.Language.turing.Equiv A B) : TMData.Agree e.symm.toEquiv (tmData B) (tmData A)

An isomorphism makes the two machines agree. Every symbol of the vocabulary transports, which is all DescriptiveComplexity.TMData.Agree asks for.

def DescriptiveComplexity.NTMAccept : DecisionProblem FirstOrder.Language.turing

Machine acceptance. Does the machine described by the instance accept its input within as many steps as there are positions? The well-formedness promises of DescriptiveComplexity.TMData.WellFormed are folded into the yes-instances.

Equations

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

def DescriptiveComplexity.DTMAccept : DecisionProblem FirstOrder.Language.turing

Deterministic machine acceptance. The same question with the extra promise DescriptiveComplexity.TMData.Deterministic folded into the yes-instances, exactly as the Horn condition is folded into DescriptiveComplexity.HORNSAT: the table is functional, so the run is unique – the shape a least fixed point can compute, which is what puts this problem in PTIME.

Equations

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

def DescriptiveComplexity.NTMAcceptSpace : DecisionProblem FirstOrder.Language.turing

Machine acceptance in bounded space: the same question as DescriptiveComplexity.NTMAccept with the step bound dropped. Nothing else changes – the tape is indexed by the positions, so the space a machine may use is bounded by construction and a reduction of dimension d buys nᵈ cells exactly as it buys nᵈ steps – but a run may now visit exponentially many configurations, so acceptance is reachability in the configuration graph.

Equations

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

def DescriptiveComplexity.DTMAcceptSpace : DecisionProblem FirstOrder.Language.turing

Deterministic machine acceptance in bounded space, with determinism folded into the yes-instances as in DescriptiveComplexity.DTMAccept. That this problem and DescriptiveComplexity.NTMAcceptSpace are complete for the same class is the content of PSPACE = NPSPACE.

Equations

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