The wide machine as an exponential expansion

The construction that makes the wide machine a member of an exponential class: an DescriptiveComplexity.ExpExpansion of FirstOrder.Language.wide-structures whose expanded vocabulary is FirstOrder.Language.turing. Read on an instance A, it produces exactly the ordinary machine instance whose universe is DescriptiveComplexity.WPoint A – so a wide machine is an ordinary machine, one exponential up, and nothing has to be said about resources.

Three things fix the whole design.

• The block is one unary relation variable (addrBlock), so an assignment is a subset of the instance and the expanded universe is its power set. There is no padding to worry about, and the binary-number order on addresses can be written directly rather than through DescriptiveComplexity.SOBlock.ordLeF, which would compare padded atoms against the ambient order rather than against the instance's own.
• Two tags (DescriptiveComplexity.AddrExp.WTag): addr, whose domain sentence is ⊤, so those points are all the addresses; and ctrl, whose domain sentence says the variable is a singleton, so those points are the elements of the instance. This is the standard way of keeping the base universe visible inside an expanded one.
• Every defining sentence is a static choice on the tags followed by one of five sentences: a mark of the control (markS), a binary attribute of it (binS), the singleton condition (singleS), the order on addresses (addrLeS) and the initial tape (inpS). Every quantifier in them ranges over the base – an element, never an address – which is exactly what keeps them first-order there.

The vocabularies, the block and the sentences

All of it is the address expansion's (DescriptiveComplexity.AddrExp), written once for an arbitrary base vocabulary with an order symbol; what is here is the naming at FirstOrder.Language.wide and the two sentences that read its order and its input relation.

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.wOrd : FirstOrder.Language

The ordered vocabulary of wide-machine instances: what an expansion's sentences may read besides the block.

Equations

• DescriptiveComplexity.Wide.wOrd = DescriptiveComplexity.AddrExp.aeOrd FirstOrder.Language.wide

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.addrBlock : SOBlock

The block whose assignments are the addresses: a single unary relation variable, so an assignment is a subset of the instance.

Equations

• DescriptiveComplexity.Wide.addrBlock = DescriptiveComplexity.AddrExp.addrBlock

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.wide1 : FirstOrder.Language

The base vocabulary expanded by one copy of the block.

Equations

• DescriptiveComplexity.Wide.wide1 = DescriptiveComplexity.AddrExp.aeLang1 FirstOrder.Language.wide

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.wide2 : FirstOrder.Language

The base vocabulary expanded by two copies of the block.

Equations

• DescriptiveComplexity.Wide.wide2 = DescriptiveComplexity.AddrExp.aeLang2 FirstOrder.Language.wide

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.wbits {A : Type} (ρ : addrBlock.Assignment A) : A → Prop

The address an assignment is: the elements its relation variable holds of.

Equations

• DescriptiveComplexity.Wide.wbits ρ = DescriptiveComplexity.AddrExp.aeBits ρ

noncomputable def DescriptiveComplexity.Wide.ltG {γ : Type} (x y : γ) : wOrd.Formula γ

x is strictly below y in the instance's own order.

Equations

• DescriptiveComplexity.Wide.ltG x y = DescriptiveComplexity.AddrExp.ltG FirstOrder.Language.wmLe x y

noncomputable def DescriptiveComplexity.Wide.addrLeS : wide2.Sentence

The order on addresses: the two addresses agree, or, at some element the first is out of and the second in, they agree at every strictly smaller element.

Equations

• DescriptiveComplexity.Wide.addrLeS = DescriptiveComplexity.AddrExp.addrLeS FirstOrder.Language.wmLe

noncomputable def DescriptiveComplexity.Wide.inpS : wide2.Sentence

The initial tape: the first address is the initial segment cut by some element x, the second point is a symbol y, and y is the input at x.

Equations

• DescriptiveComplexity.Wide.inpS = DescriptiveComplexity.AddrExp.inpS FirstOrder.Language.wmLe FirstOrder.Language.wmInp

@[simp]

theorem DescriptiveComplexity.Wide.realize_ltG {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (ltG x y).Realize v ↔ WMLe (v x) (v y) ∧ ¬WMLe (v y) (v x)

theorem DescriptiveComplexity.Wide.realize_addrLeS {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (ρ σ : addrBlock.Assignment A) : A ⊨ addrLeS ↔ WMSetLe WMLe (wbits ρ) (wbits σ)

theorem DescriptiveComplexity.Wide.realize_inpS {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (ρ σ : addrBlock.Assignment A) : A ⊨ inpS ↔ ∃ (x : A) (y : A), WMDown WMLe (wbits ρ) x ∧ wbits σ y ∧ WMInp x y

The tags, and the defining sentences

noncomputable def DescriptiveComplexity.Wide.posnT : WTag → wide1.Sentence

Being a position: the addresses are the positions.

Equations

• DescriptiveComplexity.Wide.posnT DescriptiveComplexity.AddrExp.WTag.addr = ⊤
• DescriptiveComplexity.Wide.posnT DescriptiveComplexity.AddrExp.WTag.ctrl = ⊥

noncomputable def DescriptiveComplexity.Wide.markT (r : FirstOrder.Language.wide.Relations 1) : WTag → wide1.Sentence

A mark of the control, at a tag: only control elements carry it.

Equations

• DescriptiveComplexity.Wide.markT r DescriptiveComplexity.AddrExp.WTag.addr = ⊥
• DescriptiveComplexity.Wide.markT r DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.markS r

noncomputable def DescriptiveComplexity.Wide.binT (r : FirstOrder.Language.wide.Relations 2) : WTag → WTag → wide2.Sentence

A binary attribute of the control, at a pair of tags.

Equations

• DescriptiveComplexity.Wide.binT r DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.binS r
• DescriptiveComplexity.Wide.binT r x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.Wide.leT : WTag → WTag → wide2.Sentence

The order of the machine, at a pair of tags: the addresses come first, in the binary-number order, then the control elements in the instance's order.

Equations

• DescriptiveComplexity.Wide.leT DescriptiveComplexity.AddrExp.WTag.addr DescriptiveComplexity.AddrExp.WTag.addr = DescriptiveComplexity.Wide.addrLeS
• DescriptiveComplexity.Wide.leT DescriptiveComplexity.AddrExp.WTag.addr DescriptiveComplexity.AddrExp.WTag.ctrl = ⊤
• DescriptiveComplexity.Wide.leT DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.addr = ⊥
• DescriptiveComplexity.Wide.leT DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.binS FirstOrder.Language.wmLe

noncomputable def DescriptiveComplexity.Wide.inpT : WTag → WTag → wide2.Sentence

The initial tape, at a pair of tags: an address holds a symbol.

Equations

• DescriptiveComplexity.Wide.inpT DescriptiveComplexity.AddrExp.WTag.addr DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.Wide.inpS
• DescriptiveComplexity.Wide.inpT x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.Wide.wideExp : ExpExpansion FirstOrder.Language.wide

The expansion of a wide-machine instance: the address expansion (DescriptiveComplexity.AddrExp.addrExp) at the vocabulary of ordinary machines, every symbol of which is defined by a static choice on the tags followed by one of the five sentences.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.Wide.wideStructure (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] : FirstOrder.Language.turing.Structure (wideExp.Map A)

The expanded structure of DescriptiveComplexity.wideExp, at the vocabulary of machines – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• DescriptiveComplexity.Wide.wideStructure A = DescriptiveComplexity.AddrExp.addrStructure A