Alternating machine acceptance as a decision problem

The vocabulary of the machine bridge for the polynomial hierarchy, and the problem the bridge is about: an alternating Turing machine with k quantifier blocks is data in an instance, and

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

is DescriptiveComplexity.ATMAccept k start, an ordinary iso-invariant problem of the catalog. The semantics it reads is DescriptiveComplexity.ATMData, defined without a vocabulary in DescriptiveComplexity.MachinesAlt.

The vocabulary

FirstOrder.Language.turingAlt k is FirstOrder.Language.turing – every symbol of which it carries verbatim, under the constructor base – together with k unary marks blk i splitting the states into quantifier blocks, exactly as FirstOrder.Language.qbf k extends the vocabulary of SAT by k marks on the propositional variables. The two families of marks meet in the hardness proof, which turns the block of a variable into the block of the state guessing it.

Making the marks a family indexed by Fin k, rather than a fixed pair of marks “existential”/“universal”, is what lets the alternation bound be first-order: a transition may not decrease the block index, and may raise it by at most one, so a run passes through the blocks in order and alternates at most k - 1 times. That promise – DescriptiveComplexity.ATMData.BlocksWellFormed – is folded into the yes-instances alongside DescriptiveComplexity.TMData.WellFormed, in the style of DescriptiveComplexity.IsLinOrd for Knapsack.

The two families

ATMAccept k true starts with an existential block and is the Σₖᵖ candidate; ATMAccept k false starts with a universal one and is the Πₖᵖ candidate. The two are the same problem up to the polarity parameter, so the Πₖᵖ half of the bridge costs nothing beyond swapping the marks – the machine-side reading of DescriptiveComplexity.QBF and DescriptiveComplexity.QBFPi sharing a single reduction.

inductive FirstOrder.Language.turingAltRel (k : ℕ) : ℕ → Type

Relation symbols of alternating machine instances: those of FirstOrder.Language.turing, and one unary mark per quantifier block.

• base {k n : ℕ} : turingRel n → turingAltRel k n

  A symbol of the underlying machine vocabulary.

• blk {k : ℕ} : Fin k → turingAltRel k 1

  blk i q: the state q belongs to the i-th quantifier block.

def FirstOrder.Language.turingAlt (k : ℕ) : Language

The relational vocabulary of alternating machine instances with k quantifier blocks.

Equations

• FirstOrder.Language.turingAlt k = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.turingAltRel k }

instance FirstOrder.Language.instIsRelationalTuringAlt (k : ℕ) : (Language.turingAlt k).IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.atmPosn {k : ℕ} : (Language.turingAlt k).Relations 1

The position symbol.

Equations

• FirstOrder.Language.atmPosn = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.posn

@[reducible, inline]

abbrev FirstOrder.Language.atmTr {k : ℕ} : (Language.turingAlt k).Relations 1

The transition symbol.

Equations

• FirstOrder.Language.atmTr = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.tr

@[reducible, inline]

abbrev FirstOrder.Language.atmStart {k : ℕ} : (Language.turingAlt k).Relations 1

The start-state symbol.

Equations

• FirstOrder.Language.atmStart = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.start

@[reducible, inline]

abbrev FirstOrder.Language.atmAcc {k : ℕ} : (Language.turingAlt k).Relations 1

The accepting-state symbol.

Equations

• FirstOrder.Language.atmAcc = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.acc

@[reducible, inline]

abbrev FirstOrder.Language.atmBlank {k : ℕ} : (Language.turingAlt k).Relations 1

The blank symbol.

Equations

• FirstOrder.Language.atmBlank = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.blank

@[reducible, inline]

abbrev FirstOrder.Language.atmRight {k : ℕ} : (Language.turingAlt k).Relations 1

The move-right symbol.

Equations

• FirstOrder.Language.atmRight = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.right

@[reducible, inline]

abbrev FirstOrder.Language.atmLe {k : ℕ} : (Language.turingAlt k).Relations 2

The order symbol.

Equations

• FirstOrder.Language.atmLe = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.le

@[reducible, inline]

abbrev FirstOrder.Language.atmSrc {k : ℕ} : (Language.turingAlt k).Relations 2

The transition-source symbol.

Equations

• FirstOrder.Language.atmSrc = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.tsrc

@[reducible, inline]

abbrev FirstOrder.Language.atmRead {k : ℕ} : (Language.turingAlt k).Relations 2

The transition-read symbol.

Equations

• FirstOrder.Language.atmRead = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.tread

@[reducible, inline]

abbrev FirstOrder.Language.atmDst {k : ℕ} : (Language.turingAlt k).Relations 2

The transition-destination symbol.

Equations

• FirstOrder.Language.atmDst = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.tdst

@[reducible, inline]

abbrev FirstOrder.Language.atmWrite {k : ℕ} : (Language.turingAlt k).Relations 2

The transition-write symbol.

Equations

• FirstOrder.Language.atmWrite = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.twrite

@[reducible, inline]

abbrev FirstOrder.Language.atmInp {k : ℕ} : (Language.turingAlt k).Relations 2

The input symbol.

Equations

• FirstOrder.Language.atmInp = FirstOrder.Language.turingAltRel.base FirstOrder.Language.turingRel.inp

@[reducible, inline]

abbrev FirstOrder.Language.atmBlk {k : ℕ} (i : Fin k) : (Language.turingAlt k).Relations 1

The mark of the i-th quantifier block.

Equations

• FirstOrder.Language.atmBlk i = FirstOrder.Language.turingAltRel.blk i

The shorthands of the vocabulary

def DescriptiveComplexity.ATMPosn {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Being a position.

Equations

• DescriptiveComplexity.ATMPosn a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmPosn ![a]

def DescriptiveComplexity.ATMTr {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Being a transition.

Equations

• DescriptiveComplexity.ATMTr a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmTr ![a]

def DescriptiveComplexity.ATMStart {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Being a start state.

Equations

• DescriptiveComplexity.ATMStart a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmStart ![a]

def DescriptiveComplexity.ATMAcc {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Being an accepting state.

Equations

• DescriptiveComplexity.ATMAcc a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmAcc ![a]

def DescriptiveComplexity.ATMBlank {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Being the blank symbol.

Equations

• DescriptiveComplexity.ATMBlank a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmBlank ![a]

def DescriptiveComplexity.ATMRight {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a : A) : Prop

Moving the head right.

Equations

• DescriptiveComplexity.ATMRight a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmRight ![a]

def DescriptiveComplexity.ATMLe {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The order on positions.

Equations

• DescriptiveComplexity.ATMLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmLe ![a, b]

def DescriptiveComplexity.ATMSrc {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The state a transition applies in.

Equations

• DescriptiveComplexity.ATMSrc a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmSrc ![a, b]

def DescriptiveComplexity.ATMRead {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The symbol a transition reads.

Equations

• DescriptiveComplexity.ATMRead a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmRead ![a, b]

def DescriptiveComplexity.ATMDst {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The state a transition moves to.

Equations

• DescriptiveComplexity.ATMDst a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmDst ![a, b]

def DescriptiveComplexity.ATMWrite {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The symbol a transition writes.

Equations

• DescriptiveComplexity.ATMWrite a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmWrite ![a, b]

def DescriptiveComplexity.ATMInp {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (a b : A) : Prop

The initial contents of a cell.

Equations

• DescriptiveComplexity.ATMInp a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.atmInp ![a, b]

def DescriptiveComplexity.ATMBlk {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] (j : ℕ) (a : A) : Prop

The block of a state, read off the marks: the marks of the vocabulary are indexed by Fin k, so a block index beyond k marks nothing. This is what makes the “exactly one mark, below k” clause of DescriptiveComplexity.ATMData.BlocksWellFormed a first-order statement.

Equations

• DescriptiveComplexity.ATMBlk j a = ∃ (h : j < k), FirstOrder.Language.Structure.RelMap (FirstOrder.Language.atmBlk ⟨j, h⟩) ![a]

def DescriptiveComplexity.atmData (k : ℕ) (A : Type) [(FirstOrder.Language.turingAlt k).Structure A] : ATMData A

The alternating machine an instance describes.

Equations

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

The problem

theorem DescriptiveComplexity.altAgree_of_equiv {k : ℕ} {A B : Type} [(FirstOrder.Language.turingAlt k).Structure A] [(FirstOrder.Language.turingAlt k).Structure B] (e : (FirstOrder.Language.turingAlt k).Equiv A B) : ATMData.AltAgree e.symm.toEquiv (atmData k B) (atmData k A)

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

def DescriptiveComplexity.ATMAccept (k : ℕ) (start : Bool) : DecisionProblem (FirstOrder.Language.turingAlt k)

Alternating machine acceptance. Does the alternating machine described by the instance accept its input within as many steps as there are positions? The prefix starts with an existential block when start is true.

Both promises are folded into the yes-instances, as DescriptiveComplexity.NTMAccept folds in DescriptiveComplexity.TMData.WellFormed: the machine is well formed, and its k block marks partition the states into blocks entered in order.

Equations

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

Reading the block marks

The marks of the vocabulary are indexed by Fin k, so DescriptiveComplexity.ATMBlk is False beyond k by construction; the two lemmas below are the only unfolding the rest of the development needs.

theorem DescriptiveComplexity.not_atmBlk_of_le {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] {j : ℕ} (h : k ≤ j) (a : A) : ¬ATMBlk j a

A block index beyond the marks of the vocabulary marks nothing.

theorem DescriptiveComplexity.lt_of_atmBlk {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] {j : ℕ} {a : A} (h : ATMBlk j a) : j < k

A marked state has a block index below k.

theorem DescriptiveComplexity.atmBlk_iff {k : ℕ} {A : Type} [(FirstOrder.Language.turingAlt k).Structure A] {j : ℕ} (h : j < k) (a : A) : ATMBlk j a ↔ FirstOrder.Language.Structure.RelMap (FirstOrder.Language.atmBlk ⟨j, h⟩) ![a]

The mark of a block, with its index bound supplied.

The one-block instances

At k = 1 the vocabulary has a single mark, the only block is 0 and its polarity is that of start; so for start = true no state is universal, and the alternating model is the nondeterministic one (DescriptiveComplexity.ATMData.altAccepts_iff_accepts).

theorem DescriptiveComplexity.not_isUniv_one {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] (q : A) : ¬(atmData 1 A).IsUniv true q

At one block nothing is universal, when the prefix starts existentially: the only block is 0, whose polarity is true.

theorem DescriptiveComplexity.blocksWellFormed_one_iff {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] : (atmData 1 A).BlocksWellFormed 1 ↔ ∀ (q : A), ATMBlk 0 q

At one block, well-formedness of the block structure is just that every state is marked. Uniqueness and monotonicity are automatic: there is only one mark to carry.