What the promises of a wide machine come to

DescriptiveComplexity.WideAccept folds DescriptiveComplexity.TMData.WellFormed into its yes-instances, and that promise is about the machine's universe – the addresses – rather than about the instance. This file discharges it: the promise holds exactly when the instance itself is well formed (DescriptiveComplexity.wideData_wellFormed_iff), namely when

• its order wmLe is linear,
• its input is functional, and
• it has exactly one blank symbol.

The same holds of the determinism promise (DescriptiveComplexity.wideData_deterministic_iff), which is what lets the deterministic side of EXPSPACE be proved hard and the nondeterministic one inherit it.

Nothing is asked of the addresses, which is the point: the binary-number order a linear order induces on the subsets of a finite set is linear (DescriptiveComplexity.isLinOrd_wmSetLe), and it is inherited from DescriptiveComplexity.setLinearOrder rather than proved again – the same reduction DescriptiveComplexity.Exponential.Order makes for the order on an expanded universe.

This is the lemma a reduction into a wide machine will need: an interpretation writing a wide machine down owes only three first-order conditions about the instance it draws, and none about its power set.

def DescriptiveComplexity.WideWF (A : Type) [FirstOrder.Language.wide.Structure A] : Prop

Well-formedness of a wide-machine instance: a linear order, a functional input, and exactly one blank. Every conjunct is first-order over the instance.

Equations

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

def DescriptiveComplexity.WideDet (A : Type) [FirstOrder.Language.wide.Structure A] : Prop

Determinism of a wide-machine instance: one start state, at most one transition per state and symbol read, and functional destination and written symbol. Every conjunct is first-order over the instance, exactly as for DescriptiveComplexity.TMData.Deterministic itself.

Equations

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

theorem DescriptiveComplexity.wideData_deterministic_iff {A : Type} [FirstOrder.Language.wide.Structure A] : (wideData A).Deterministic ↔ WideDet A

A wide machine is deterministic exactly when its instance is. The addresses contribute nothing – no address is a state, a symbol or a transition – so the promise DescriptiveComplexity.DWideAcceptSpace folds in is again a first-order condition about the instance, which is what lets the deterministic side be proved hard and the nondeterministic one inherit it.

theorem DescriptiveComplexity.eq_of_wmDown {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) {s : A → Prop} {x y : A} (hx : WMDown WMLe s x) (hy : WMDown WMLe s y) : x = y

Two elements cutting the same initial segment are equal.

theorem DescriptiveComplexity.isLinOrd_wmSetLe {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) : IsLinOrd (WMSetLe Le)

The binary-number order on addresses is a linear order, inherited from DescriptiveComplexity.setLinearOrder: the comparison is the same, so DescriptiveComplexity.isLinOrd_of_key at the identity key transports the axioms. Stated at an arbitrary order relation, since everything the address layer says is independent of where the order comes from.

theorem DescriptiveComplexity.isLinOrd_wpLe {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : IsLinOrd wpLe

The order of a wide machine is linear as soon as the instance's is: the addresses are ordered as binary numbers, the control elements as in the instance, and the addresses come first.

theorem DescriptiveComplexity.wideData_wellFormed_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] : (wideData A).WellFormed ↔ WideWF A

The promise of a wide machine is a promise about its instance: the universe of addresses contributes nothing, so an interpretation writing a wide machine down owes three first-order conditions and no more.