Simulating a machine that walks an expanded universe

What every exponential class rests on: a walk over an expanded universe, performed by a machine that only ever holds finitely many points of it, is a walk over the base – an DescriptiveComplexity.SOTCSpec, since a point of the expansion is an assignment of a block and k of them are an assignment of one merged block. This file builds that specification out of a DescriptiveComplexity.HeadAutomaton and proves the two walks step for step equivalent.

Why an automaton rather than an FO(TC) specification: the tests a DescriptiveComplexity.HeadAutomaton performs are quantifier-free by fiat (DescriptiveComplexity.HeadAutomaton.test_qf), so DescriptiveComplexity.ExpExpansion.translQF translates them as they stand and no quantifier over the expanded universe is ever evaluated. Everything else the machine does is an order primitive – stay, copy, jump to an end, step to a neighbor – and those are written down in DescriptiveComplexity.Exponential.Increment.

The one hypothesis

A move to the immediate successor is the increment of the assignment only when every tagged assignment is a point, i.e., when the expansion's domain sentence is trivial. That is the hypothesis htot the correctness theorems carry; DescriptiveComplexity.ExpExpansion.trivialize is how a general expansion is brought into that shape, and DescriptiveComplexity.ExpExpansion.trivialize_domHolds is the hypothesis discharged.

Slots

Everything the transition sentence says is about one or two points, sitting somewhere inside a bigger block: one of the k rounds of the current state, or one of the k rounds of the next one. A DescriptiveComplexity.ExpExpansion.PtSlot is that placement – an arity-preserving map of the point block into a host block – and each of the five things the machine can ask about points is written once, at an arbitrary slot of an arbitrary host:

• DescriptiveComplexity.ExpExpansion.slotTagF – the point at a slot carries a given tag;
• DescriptiveComplexity.ExpExpansion.slotGuardF – a slot holds a point at all;
• DescriptiveComplexity.ExpExpansion.eqPtF, DescriptiveComplexity.ExpExpansion.covPtF, DescriptiveComplexity.ExpExpansion.minPtF, DescriptiveComplexity.ExpExpansion.maxPtF – equality, the covering relation and the two endpoints.

The state block is then (repMerged X.pointBlock k).withTag M.State, the two copies of it that a transition sentence sees are SOBlock.replicate 2, and both hosts are addressed by the same slot machinery.

Every merged assignment is one assignment per round

theorem DescriptiveComplexity.repBlockAssign_surjective (B : SOBlock) (A : Type) (k : ℕ) : Function.Surjective (repBlockAssign B A k)

A merged assignment splits into its rounds: the assembly map of DescriptiveComplexity.repBlockAssign is onto, so a guessed state of the walk below really is k guessed points.

Slots

structure DescriptiveComplexity.ExpExpansion.PtSlot {L : FirstOrder.Language} (X : ExpExpansion L) (H : SOBlock) : Type

A slot: where one point of an expanded universe sits inside a host block. Both hosts the simulation uses – the state block and two copies of it – are addressed through this one interface.

• ix : X.pointBlock.ι → H.ι

  The relation variable of the host carrying each variable of the point block.

• arity (x : X.pointBlock.ι) : H.arity (self.ix x) = X.pointBlock.arity x

  The placement preserves arities.

def DescriptiveComplexity.ExpExpansion.PtSlot.lhom {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) : (L.sum FirstOrder.Language.order).sum X.pointBlock.lang →ᴸ (L.sum FirstOrder.Language.order).sum H.lang

The vocabulary map reading a sentence about one point at the slot.

Equations

• s.lhom = (FirstOrder.Language.LHom.id (L.sum FirstOrder.Language.order)).sumMap (DescriptiveComplexity.SOBlock.homLHom s.ix ⋯)

def DescriptiveComplexity.ExpExpansion.PtSlot.read {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) {A : Type} (σ : H.Assignment A) : X.pointBlock.Assignment A

The assignment of the point block a slot reads out of a host assignment.

Equations

• s.read σ = DescriptiveComplexity.SOBlock.homAssign s.ix ⋯ σ

theorem DescriptiveComplexity.ExpExpansion.PtSlot.realize_lhom {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) {A : Type} [L.Structure A] [LinearOrder A] (σ : H.Assignment A) (φ : ((L.sum FirstOrder.Language.order).sum X.pointBlock.lang).Sentence) : A ⊨ s.lhom.onSentence φ ↔ A ⊨ φ

Reading a sentence at a slot is reading it at the slot's assignment.

def DescriptiveComplexity.ExpExpansion.PtSlot.At {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) {A : Type} (σ : H.Assignment A) (p : X.Point A) : Prop

The slot of σ holds the point p.

Equations

• s.At σ p = (s.read σ = DescriptiveComplexity.SOBlock.tagAssign p.1 p.2)

What a slot can be asked

noncomputable def DescriptiveComplexity.ExpExpansion.slotTagF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) (t : X.Tag) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

The atom “the point at this slot carries the tag t”.

Equations

• DescriptiveComplexity.ExpExpansion.slotTagF s t = s.lhom.onSentence (X.B.tagBitF X.Tag t)

noncomputable def DescriptiveComplexity.ExpExpansion.slotGuardF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

The guard “this slot holds a point of the expanded universe”.

Equations

• DescriptiveComplexity.ExpExpansion.slotGuardF s = s.lhom.onSentence X.pointGuardF

theorem DescriptiveComplexity.ExpExpansion.realize_slotTagF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {s : X.PtSlot H} {σ : H.Assignment A} {p : X.Point A} (hs : s.At σ p) (t : X.Tag) : A ⊨ slotTagF s t ↔ t = p.1

theorem DescriptiveComplexity.ExpExpansion.realize_slotGuardF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (s : X.PtSlot H) (σ : H.Assignment A) : A ⊨ slotGuardF s ↔ ∃ (p : X.Map A), s.At σ ↑p

Two slots at once

def DescriptiveComplexity.ExpExpansion.pairIx {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s₀ s₁ : X.PtSlot H) : (X.B.replicate 2).ι → H.ι

Two slots, read as a placement of the expansion's block replicated twice: copy 0 is the first slot, copy 1 the second.

Equations

• DescriptiveComplexity.ExpExpansion.pairIx s₀ s₁ p = (![s₀, s₁] p.1).ix (Sum.inr p.2)

theorem DescriptiveComplexity.ExpExpansion.pairIx_arity {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s₀ s₁ : X.PtSlot H) (p : (X.B.replicate 2).ι) : H.arity (pairIx s₀ s₁ p) = (X.B.replicate 2).arity p

def DescriptiveComplexity.ExpExpansion.pairLHom {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s₀ s₁ : X.PtSlot H) : (L.sum FirstOrder.Language.order).sum (X.B.replicate 2).lang →ᴸ (L.sum FirstOrder.Language.order).sum H.lang

The vocabulary map reading a sentence about two assignments of the expansion's block at two slots.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_pairLHom {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {s₀ s₁ : X.PtSlot H} {σ : H.Assignment A} {p₀ p₁ : X.Point A} (h₀ : s₀.At σ p₀) (h₁ : s₁.At σ p₁) (φ : ((L.sum FirstOrder.Language.order).sum (X.B.replicate 2).lang).Sentence) : A ⊨ (pairLHom s₀ s₁).onSentence φ ↔ A ⊨ φ

Reading a two-copy sentence at two slots is reading it at the two assignments those slots hold.

The static half: facts about tags

A point is a tag and an assignment, and the tag half of every order question is decided at formula-construction time: there are finitely many tags, so which one is least, which is greatest and which covers which are conditions on the disjunct, not conditions the sentence has to express.

def DescriptiveComplexity.ExpExpansion.IsMinTag {L : FirstOrder.Language} (X : ExpExpansion L) (t : X.Tag) : Prop

The tag is the least one.

Equations

• X.IsMinTag t = ∀ (t' : X.Tag), t ≤ t'

def DescriptiveComplexity.ExpExpansion.IsMaxTag {L : FirstOrder.Language} (X : ExpExpansion L) (t : X.Tag) : Prop

The tag is the greatest one.

Equations

• X.IsMaxTag t = ∀ (t' : X.Tag), t' ≤ t

def DescriptiveComplexity.ExpExpansion.TagCovBy {L : FirstOrder.Language} (X : ExpExpansion L) (t₁ t₂ : X.Tag) : Prop

The second tag is the immediate successor of the first.

Equations

• X.TagCovBy t₁ t₂ = (t₁ < t₂ ∧ ∀ (t : X.Tag), ¬(t₁ < t ∧ t < t₂))

The four questions a machine asks about points

noncomputable def DescriptiveComplexity.ExpExpansion.eqPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s₀ s₁ : X.PtSlot H) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

“The two slots hold the same point”: their tag bits agree, and their assignments hold of the same atoms.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.covPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s₀ s₁ : X.PtSlot H) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

“The point of the second slot is the immediate successor of the point of the first”: one disjunct per pair of tags, the tag comparison decided statically and the assignment half being either the binary increment or the roll-over from the full assignment to the empty one.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.minPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

“The point of this slot is the least point”: the least tag, holding of nothing.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.maxPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} (s : X.PtSlot H) : ((L.sum FirstOrder.Language.order).sum H.lang).Sentence

“The point of this slot is the greatest point”: the greatest tag, holding of everything.

Equations

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

Their correctness

theorem DescriptiveComplexity.ExpExpansion.realize_eqPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {s₀ s₁ : X.PtSlot H} {σ : H.Assignment A} {p₀ p₁ : X.Point A} (h₀ : s₀.At σ p₀) (h₁ : s₁.At σ p₁) : A ⊨ eqPtF s₀ s₁ ↔ p₀ = p₁

theorem DescriptiveComplexity.ExpExpansion.realize_covPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {s₀ s₁ : X.PtSlot H} {σ : H.Assignment A} {p₀ p₁ : X.Point A} (h₀ : s₀.At σ p₀) (h₁ : s₁.At σ p₁) : A ⊨ covPtF s₀ s₁ ↔ p₀ < p₁ ∧ ∀ (r : X.Point A), ¬(p₀ < r ∧ r < p₁)

theorem DescriptiveComplexity.ExpExpansion.realize_minPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {s : X.PtSlot H} {σ : H.Assignment A} {p : X.Point A} (hs : s.At σ p) : A ⊨ minPtF s ↔ ∀ (q : X.Point A), p ≤ q

theorem DescriptiveComplexity.ExpExpansion.realize_maxPtF {L : FirstOrder.Language} {X : ExpExpansion L} {H : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {s : X.PtSlot H} {σ : H.Assignment A} {p : X.Point A} (hs : s.At σ p) : A ⊨ maxPtF s ↔ ∀ (q : X.Point A), q ≤ p

The configurations of a machine, as one block

A configuration is a control state and k points. The control state is a bit vector (DescriptiveComplexity.SOBlock.withTag), the k points are the k rounds of DescriptiveComplexity.repMerged, and the two configurations a transition sentence compares are the two copies of DescriptiveComplexity.SOBlock.replicate.

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.cfgBlock {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] : SOBlock

The block whose assignments are the configurations: one bit per control state, and k rounds each holding one point of the expanded universe.

Equations

• X.cfgBlock k S = (DescriptiveComplexity.repMerged X.pointBlock k).withTag S

def DescriptiveComplexity.ExpExpansion.cfgSlot {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] (i : Fin k) : X.PtSlot (X.cfgBlock k S)

The slot of the i-th round inside the configuration block.

Equations

• X.cfgSlot k S i = { ix := fun (x : X.pointBlock.ι) => Sum.inr (DescriptiveComplexity.ExpExpansion.roundOneIx i X x), arity := ⋯ }

def DescriptiveComplexity.ExpExpansion.stepSlot {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] (c : Fin 2) (i : Fin k) : X.PtSlot ((X.cfgBlock k S).replicate 2)

The slot of the i-th round of the c-th of two configurations.

Equations

• X.stepSlot k S c i = { ix := fun (x : X.pointBlock.ι) => (c, (X.cfgSlot k S i).ix x), arity := ⋯ }

def DescriptiveComplexity.ExpExpansion.copyLHom {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] (c : Fin 2) : (L.sum FirstOrder.Language.order).sum (X.cfgBlock k S).lang →ᴸ (L.sum FirstOrder.Language.order).sum ((X.cfgBlock k S).replicate 2).lang

Reading a sentence about one configuration inside the c-th of two copies.

Equations

• X.copyLHom k S c = (FirstOrder.Language.LHom.id (L.sum FirstOrder.Language.order)).sumMap (DescriptiveComplexity.SOBlock.homLHom (fun (y : (X.cfgBlock k S).ι) => (c, y)) ⋯)

noncomputable def DescriptiveComplexity.ExpExpansion.ctrlF {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] (s : S) : ((L.sum FirstOrder.Language.order).sum (X.cfgBlock k S).lang).Sentence

The atom “the control is in the state s”.

Equations

• X.ctrlF k S s = (DescriptiveComplexity.repMerged X.pointBlock k).tagBitF S s

noncomputable def DescriptiveComplexity.ExpExpansion.cfgGuardF {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] : ((L.sum FirstOrder.Language.order).sum (X.cfgBlock k S).lang).Sentence

The guard “this assignment is a configuration”: it names a control state, and each of its k rounds holds a point of the expanded universe.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.cfgAssign {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} [L.Structure A] [LinearOrder A] (s : S) (pts : Fin k → X.Map A) : (X.cfgBlock k S).Assignment A

The configuration assignment: the control state in the tag bits, the k points in the k rounds.

Equations

• X.cfgAssign k S s pts = DescriptiveComplexity.SOBlock.tagAssign s (DescriptiveComplexity.repBlockAssign X.pointBlock A k (DescriptiveComplexity.ExpExpansion.roundAssign pts))

theorem DescriptiveComplexity.ExpExpansion.cfgSlot_read {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} (s : S) (μ : (repMerged X.pointBlock k).Assignment A) (i : Fin k) : (X.cfgSlot k S i).read (SOBlock.tagAssign s μ) = SOBlock.homAssign (roundOneIx i X) ⋯ μ

A round of a tagged assignment is read past the tag bits.

theorem DescriptiveComplexity.ExpExpansion.cfgSlot_at {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} [L.Structure A] [LinearOrder A] (s : S) (pts : Fin k → X.Map A) (i : Fin k) : (X.cfgSlot k S i).At (X.cfgAssign k S s pts) ↑(pts i)

The i-th round of a configuration holds the i-th point.

theorem DescriptiveComplexity.ExpExpansion.stepSlot_at {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} (σs : Fin 2 → (X.cfgBlock k S).Assignment A) (c : Fin 2) (i : Fin k) {p : X.Point A} (h : (X.cfgSlot k S i).At (σs c) p) : (X.stepSlot k S c i).At ((X.cfgBlock k S).replicateAssign σs) p

A round of one of two copies is that round of that copy.

theorem DescriptiveComplexity.ExpExpansion.realize_copyLHom {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} [L.Structure A] [LinearOrder A] (σs : Fin 2 → (X.cfgBlock k S).Assignment A) (c : Fin 2) (φ : ((L.sum FirstOrder.Language.order).sum (X.cfgBlock k S).lang).Sentence) : A ⊨ (X.copyLHom k S c).onSentence φ ↔ A ⊨ φ

Reading a configuration sentence in a copy is reading it at that copy's assignment.

theorem DescriptiveComplexity.ExpExpansion.realize_ctrlF {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} [L.Structure A] [LinearOrder A] (s s' : S) (pts : Fin k → X.Map A) : A ⊨ X.ctrlF k S s ↔ s = s'

theorem DescriptiveComplexity.ExpExpansion.realize_cfgGuardF {L : FirstOrder.Language} (X : ExpExpansion L) (k : ℕ) (S : Type) [Finite S] {A : Type} [L.Structure A] [LinearOrder A] (σ : (X.cfgBlock k S).Assignment A) : A ⊨ X.cfgGuardF k S ↔ ∃ (s : S) (pts : Fin k → X.Map A), σ = X.cfgAssign k S s pts

The guard is exactly “this is a configuration”.

The walk that simulates the machine

noncomputable def DescriptiveComplexity.ExpExpansion.testF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin k)) : ((L.sum FirstOrder.Language.order).sum (X.cfgBlock k M.State).lang).Sentence

A quantifier-free formula about the k points of a configuration, read as a sentence about the configuration.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.readingF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) (r : M.TestIx → Bool) : ((L.sum FirstOrder.Language.order).sum (X.cfgBlock k M.State).lang).Sentence

“The tests come out as the reading r says.”

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.moveF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) : HeadMove k → Fin k → ((L.sum FirstOrder.Language.order).sum ((X.cfgBlock k M.State).replicate 2).lang).Sentence

The move of one head, as a sentence about two configurations. Each case is one of the four questions of DescriptiveComplexity.ExpExpansion.eqPtF and its siblings, asked of the round the move reads and the round it writes.

Equations

• DescriptiveComplexity.ExpExpansion.moveF M DescriptiveComplexity.HeadMove.stay x✝ = DescriptiveComplexity.ExpExpansion.eqPtF (X.stepSlot k M.State 0 x✝) (X.stepSlot k M.State 1 x✝)
• DescriptiveComplexity.ExpExpansion.moveF M DescriptiveComplexity.HeadMove.toMin x✝ = DescriptiveComplexity.ExpExpansion.minPtF (X.stepSlot k M.State 1 x✝)
• DescriptiveComplexity.ExpExpansion.moveF M DescriptiveComplexity.HeadMove.toMax x✝ = DescriptiveComplexity.ExpExpansion.maxPtF (X.stepSlot k M.State 1 x✝)
• DescriptiveComplexity.ExpExpansion.moveF M (DescriptiveComplexity.HeadMove.copy i) x✝ = DescriptiveComplexity.ExpExpansion.eqPtF (X.stepSlot k M.State 0 i) (X.stepSlot k M.State 1 x✝)
• DescriptiveComplexity.ExpExpansion.moveF M (DescriptiveComplexity.HeadMove.succ i) x✝ = DescriptiveComplexity.ExpExpansion.covPtF (X.stepSlot k M.State 0 i) (X.stepSlot k M.State 1 x✝)
• DescriptiveComplexity.ExpExpansion.moveF M (DescriptiveComplexity.HeadMove.pred i) x✝ = DescriptiveComplexity.ExpExpansion.covPtF (X.stepSlot k M.State 1 x✝) (X.stepSlot k M.State 0 i)

noncomputable def DescriptiveComplexity.ExpExpansion.transF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) (s : M.State) (r : M.TestIx → Bool) (p : M.State × (Fin k → HeadMove k)) : ((L.sum FirstOrder.Language.order).sum ((X.cfgBlock k M.State).replicate 2).lang).Sentence

One transition of the machine, as a sentence about two configurations: the control state of each copy, the reading of the first, the guard of the second, and the move of every head.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.machStepF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) : ((L.sum FirstOrder.Language.order).sum ((X.cfgBlock k M.State).replicate 2).lang).Sentence

The transition sentence of the simulation: some transition of the machine, at some control state and some reading.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) : SOTCSpec L

The walk over the base that simulates the machine: its states are the configurations, its transition sentence is the machine's table, its starting states are the initial configurations and its accepting states are the ones whose control accepts.

Equations

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

Correctness

theorem DescriptiveComplexity.ExpExpansion.forall_point_of_total {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (htot : ∀ (p : X.Point A), DomHolds p) (P : X.Point A → Prop) : (∀ (q : X.Map A), P ↑q) ↔ ∀ (q : X.Point A), P q

With a trivial domain, quantifying over the points of the expanded universe is quantifying over every tagged assignment.

theorem DescriptiveComplexity.ExpExpansion.realize_testF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (s : M.State) (pts : Fin k → X.Map A) {φ : (X.E.sum FirstOrder.Language.order).Formula (Fin k)} (hqf : FirstOrder.Language.BoundedFormula.IsQF φ) : A ⊨ testF M φ ↔ φ.Realize pts

theorem DescriptiveComplexity.ExpExpansion.realize_readingF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (s : M.State) (pts : Fin k → X.Map A) (r : M.TestIx → Bool) : A ⊨ readingF M r ↔ M.reading pts = r

theorem DescriptiveComplexity.ExpExpansion.realize_moveF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) (σs : Fin 2 → (X.cfgBlock k M.State).Assignment A) (s₀ s₁ : M.State) (x y : Fin k → X.Map A) (h₀ : σs 0 = X.cfgAssign k M.State s₀ x) (h₁ : σs 1 = X.cfgAssign k M.State s₁ y) (mv : HeadMove k) (j : Fin k) : A ⊨ moveF M mv j ↔ mv.Holds x j (y j)

theorem DescriptiveComplexity.ExpExpansion.realize_transF {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) (σs : Fin 2 → (X.cfgBlock k M.State).Assignment A) (s : M.State) (x : Fin k → X.Map A) (h₀ : σs 0 = X.cfgAssign k M.State s x) (s₀ : M.State) (r : M.TestIx → Bool) (p : M.State × (Fin k → HeadMove k)) : A ⊨ transF M s₀ r p ↔ s₀ = s ∧ M.reading x = r ∧ ∃ (y : Fin k → X.Map A), σs 1 = X.cfgAssign k M.State p.1 y ∧ ∀ (j : Fin k), (p.2 j).Holds x j (y j)

theorem DescriptiveComplexity.ExpExpansion.step_autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) (σ τ : (X.cfgBlock k M.State).Assignment A) (s : M.State) (x : Fin k → X.Map A) (hσ : σ = X.cfgAssign k M.State s x) : (autoSpec M).Step σ τ ↔ ∃ (s' : M.State) (y : Fin k → X.Map A), τ = X.cfgAssign k M.State s' y ∧ M.Step (s, x) (s', y)

theorem DescriptiveComplexity.ExpExpansion.isSrc_autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) (σ : (X.cfgBlock k M.State).Assignment A) : (autoSpec M).IsSrc σ ↔ ∃ (x : Fin k → X.Map A), σ = X.cfgAssign k M.State M.start x ∧ ∀ (j : Fin k) (b : X.Map A), x j ≤ b

theorem DescriptiveComplexity.ExpExpansion.isTgt_autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] (σ : (X.cfgBlock k M.State).Assignment A) (s : M.State) (x : Fin k → X.Map A) (hσ : σ = X.cfgAssign k M.State s x) : (autoSpec M).IsTgt σ ↔ M.accept s = true

theorem DescriptiveComplexity.ExpExpansion.reach_autoSpec_of {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) {σ τ : (X.cfgBlock k M.State).Assignment A} (s : M.State) (x : Fin k → X.Map A) (hσ : σ = X.cfgAssign k M.State s x) : Relation.ReflTransGen (autoSpec M).Step σ τ → ∃ (s' : M.State) (y : Fin k → X.Map A), τ = X.cfgAssign k M.State s' y ∧ Relation.ReflTransGen M.Step (s, x) (s', y)

A walk of the simulation that starts at a configuration stays at configurations, and is a run of the machine.

theorem DescriptiveComplexity.ExpExpansion.reach_autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) (a b : M.Config (X.Map A)) : Relation.ReflTransGen M.Step a b → Relation.ReflTransGen (autoSpec M).Step (X.cfgAssign k M.State a.1 a.2) (X.cfgAssign k M.State b.1 b.2)

A run of the machine is a walk of the simulation.

theorem DescriptiveComplexity.ExpExpansion.accepts_autoSpec {L : FirstOrder.Language} {X : ExpExpansion L} {k : ℕ} (M : HeadAutomaton X.E k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (htot : ∀ (p : X.Point A), DomHolds p) : (autoSpec M).Accepts A ↔ M.Accepts (X.Map A)

The simulation is correct: the walk over the base accepts exactly when the machine accepts the expanded structure.