The space-bounded machine problems are in PSPACE

The membership half of the machine bridge for PSPACE. A configuration of a machine is a state, a head position and a tape, and each of the three is a relation on the universe: the tape is a binary relation (the graph of a function), the state and the head are unary marks (singletons). So a configuration is an assignment of a three-variable block (DescriptiveComplexity.mBlock), one step of the machine is a first-order condition on two consecutive assignments, and acceptance – reachability in the configuration graph, since DescriptiveComplexity.TMData.AcceptsSpace has no step bound – is a transitive closure over those assignments. That is an SO(TC) specification on the nose.

This is the same phenomenon as for SUCCINCT-REACH: the problem is the syntactic image of the logic, so membership is a transcription rather than a construction. Nothing here plays the role of DescriptiveComplexity.Problems.Machine.Walk, which exists only to cash in the unary time bound of the time-bounded model by indexing a run by the positions; with the bound dropped a run may be exponentially long and no longer fits in the structure, which is precisely why the space-bounded problems are SO(TC) rather than Σ₁.

The one wrinkle is that an assignment of the block is an arbitrary triple of relations, while a configuration is a functional total tape and two singletons. That is a first-order condition (DescriptiveComplexity.cfgS), it holds of every assignment coming from a configuration, and the transition sentence demands it of the state it moves to, so every state along an accepting walk is a configuration.

The formula builders

Kept in a namespace of their own: the shapes below (wfF, stepF, …) are the transcription of one machine model into sentences, and their names are the generic ones the other reduction layers of the catalog also use.

Generic sentence shapes

Each builder is parameterized by the relation symbols it reads, so that the same one serves over the one-copy and the two-copy expansions.

noncomputable def DescriptiveComplexity.SpaceTM.totalF {L' : FirstOrder.Language} {γ : Type} (t : L'.Relations 2) : L'.Formula γ

The tape is total: every cell holds a symbol.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.funcF {L' : FirstOrder.Language} {γ : Type} (t : L'.Relations 2) : L'.Formula γ

The tape is functional: a cell holds at most one symbol.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.someF {L' : FirstOrder.Language} {γ : Type} (s : L'.Relations 1) : L'.Formula γ

The mark is inhabited.

Equations

• DescriptiveComplexity.SpaceTM.someF s = FirstOrder.Language.Formula.iExs (Fin 1) (s.formula₁ (FirstOrder.Language.var (Sum.inr 0)))

noncomputable def DescriptiveComplexity.SpaceTM.uniqF {L' : FirstOrder.Language} {γ : Type} (s : L'.Relations 1) : L'.Formula γ

The mark holds of at most one element.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.cfgF {L' : FirstOrder.Language} {γ : Type} (t : L'.Relations 2) (s h : L'.Relations 1) : L'.Formula γ

The assignment is a configuration: a total functional tape and two singleton marks.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_totalF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (t : L'.Relations 2) : (totalF t).Realize v ↔ ∀ (p : M), ∃ (a : M), FirstOrder.Language.Structure.RelMap t ![p, a]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_funcF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (t : L'.Relations 2) : (funcF t).Realize v ↔ ∀ (p a b : M), FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap t ![p, b] → a = b

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_someF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (s : L'.Relations 1) : (someF s).Realize v ↔ ∃ (q : M), FirstOrder.Language.Structure.RelMap s ![q]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_uniqF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (s : L'.Relations 1) : (uniqF s).Realize v ↔ ∀ (q q' : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap s ![q'] → q = q'

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_cfgF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (t : L'.Relations 2) (s h : L'.Relations 1) : (cfgF t s h).Realize v ↔ ((∀ (p : M), ∃ (a : M), FirstOrder.Language.Structure.RelMap t ![p, a]) ∧ ∀ (p a b : M), FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap t ![p, b] → a = b) ∧ ((∃ (q : M), FirstOrder.Language.Structure.RelMap s ![q]) ∧ ∀ (q q' : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap s ![q'] → q = q') ∧ (∃ (p : M), FirstOrder.Language.Structure.RelMap h ![p]) ∧ ∀ (p p' : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap h ![p'] → p = p'

The guarded conjuncts

noncomputable def DescriptiveComplexity.SpaceTM.markImpF {L' : FirstOrder.Language} {γ : Type} (s r : L'.Relations 1) : L'.Formula γ

Everything the first mark holds of, the second holds of too.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.minPosF {L' : FirstOrder.Language} {γ : Type} (h posn : L'.Relations 1) (le : L'.Relations 2) : L'.Formula γ

The marked position is a least position.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.initTapeF {L' : FirstOrder.Language} {γ : Type} (t inp : L'.Relations 2) (blank : L'.Relations 1) : L'.Formula γ

The tape is an initial tape: each cell holds its input symbol where the input is defined, and the blank elsewhere.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_markImpF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (s r : L'.Relations 1) : (markImpF s r).Realize v ↔ ∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap r ![q]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_minPosF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (h posn : L'.Relations 1) (le : L'.Relations 2) : (minPosF h posn le).Realize v ↔ ∀ (p : M), FirstOrder.Language.Structure.RelMap h ![p] → MinPos (fun (x y : M) => FirstOrder.Language.Structure.RelMap le ![x, y]) (fun (x : M) => FirstOrder.Language.Structure.RelMap posn ![x]) p

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_initTapeF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (t inp : L'.Relations 2) (blank : L'.Relations 1) : (initTapeF t inp blank).Realize v ↔ ∀ (p a : M), FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap inp ![p, a] ∨ (∀ (b : M), ¬FirstOrder.Language.Structure.RelMap inp ![p, b]) ∧ FirstOrder.Language.Structure.RelMap blank ![a]

The conjuncts of the transition sentence

noncomputable def DescriptiveComplexity.SpaceTM.markArgF {L' : FirstOrder.Language} {γ : Type} (r : L'.Relations 2) (s : L'.Relations 1) (τ : L'.Term γ) : L'.Formula γ

The transition has the marked element as its source (or destination).

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.cellArgF {L' : FirstOrder.Language} {γ : Type} (r : L'.Relations 2) (h : L'.Relations 1) (t : L'.Relations 2) (τ : L'.Term γ) : L'.Formula γ

The transition reads (or writes) the symbol held by the marked cell.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.frameF {L' : FirstOrder.Language} {γ : Type} (t t' : L'.Relations 2) (h : L'.Relations 1) : L'.Formula γ

Cells other than the marked one hold the same symbol before and after.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.succPosF {L' : FirstOrder.Language} {γ : Type} (le : L'.Relations 2) (posn : L'.Relations 1) (x y : L'.Term γ) : L'.Formula γ

y is the position immediately after x.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.moveF {L' : FirstOrder.Language} {γ : Type} (right h h' posn : L'.Relations 1) (le : L'.Relations 2) (τ : L'.Term γ) : L'.Formula γ

The head moves to the neighbouring position in the direction the transition names.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_markArgF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (r : L'.Relations 2) (s : L'.Relations 1) (τ : L'.Term γ) : (markArgF r s τ).Realize v ↔ ∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap r ![FirstOrder.Language.Term.realize v τ, q]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_cellArgF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (r : L'.Relations 2) (h : L'.Relations 1) (t : L'.Relations 2) (τ : L'.Term γ) : (cellArgF r h t τ).Realize v ↔ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap r ![FirstOrder.Language.Term.realize v τ, a]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_frameF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (t t' : L'.Relations 2) (h : L'.Relations 1) : (frameF t t' h).Realize v ↔ ∀ (p a : M), ¬FirstOrder.Language.Structure.RelMap h ![p] → (FirstOrder.Language.Structure.RelMap t' ![p, a] ↔ FirstOrder.Language.Structure.RelMap t ![p, a])

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_succPosF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (le : L'.Relations 2) (posn : L'.Relations 1) (x y : L'.Term γ) : (succPosF le posn x y).Realize v ↔ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (FirstOrder.Language.Term.realize v x) (FirstOrder.Language.Term.realize v y)

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_moveF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (right h h' posn : L'.Relations 1) (le : L'.Relations 2) (τ : L'.Term γ) : (moveF right h h' posn le τ).Realize v ↔ (FirstOrder.Language.Structure.RelMap right ![FirstOrder.Language.Term.realize v τ] ∧ ∀ (p p' : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap h' ![p'] → SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p p') ∨ ¬FirstOrder.Language.Structure.RelMap right ![FirstOrder.Language.Term.realize v τ] ∧ ∀ (p p' : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap h' ![p'] → SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p' p

Well-formedness

noncomputable def DescriptiveComplexity.SpaceTM.linOrdF {L' : FirstOrder.Language} {γ : Type} (le : L'.Relations 2) : L'.Formula γ

The relation is a linear order.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.wfF {L' : FirstOrder.Language} {γ : Type} (le inp : L'.Relations 2) (posn blank : L'.Relations 1) : L'.Formula γ

Well-formedness of the instance, as a sentence: the order is linear, there is a position, the input is functional, and there is exactly one blank.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_linOrdF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (le : L'.Relations 2) : (linOrdF le).Realize v ↔ IsLinOrd fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_wfF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (le inp : L'.Relations 2) (posn blank : L'.Relations 1) : (wfF le inp posn blank).Realize v ↔ (IsLinOrd fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) ∧ (∃ (p : M), FirstOrder.Language.Structure.RelMap posn ![p]) ∧ (∀ (p a b : M), FirstOrder.Language.Structure.RelMap inp ![p, a] → FirstOrder.Language.Structure.RelMap inp ![p, b] → a = b) ∧ (∃ (b : M), FirstOrder.Language.Structure.RelMap blank ![b]) ∧ ∀ (a b : M), FirstOrder.Language.Structure.RelMap blank ![a] → FirstOrder.Language.Structure.RelMap blank ![b] → a = b

The transition sentence

noncomputable def DescriptiveComplexity.SpaceTM.stepF {L' : FirstOrder.Language} {γ : Type} (tr right posn : L'.Relations 1) (src rd dst wr le : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (s' h' : L'.Relations 1) (t' : L'.Relations 2) : L'.Formula γ

One step of the machine, as a condition on two consecutive assignments.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_stepF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr right posn : L'.Relations 1) (src rd dst wr le : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (s' h' : L'.Relations 1) (t' : L'.Relations 2) : (stepF tr right posn src rd dst wr le s h t s' h' t').Realize v ↔ ∃ (τ : M), (FirstOrder.Language.Structure.RelMap tr ![τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![τ, a]) ∧ ((∀ (q : M), FirstOrder.Language.Structure.RelMap s' ![q] → FirstOrder.Language.Structure.RelMap dst ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t' ![p, a] → FirstOrder.Language.Structure.RelMap wr ![τ, a]) ∧ (∀ (p a : M), ¬FirstOrder.Language.Structure.RelMap h ![p] → (FirstOrder.Language.Structure.RelMap t' ![p, a] ↔ FirstOrder.Language.Structure.RelMap t ![p, a])) ∧ ((FirstOrder.Language.Structure.RelMap right ![τ] ∧ ∀ (p p' : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap h' ![p'] → SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p p') ∨ ¬FirstOrder.Language.Structure.RelMap right ![τ] ∧ ∀ (p p' : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap h' ![p'] → SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p' p)

noncomputable def DescriptiveComplexity.SpaceTM.trUniqF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd : L'.Relations 2) : L'.Formula γ

At most one transition applies in a given state on a given symbol.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.detF {L' : FirstOrder.Language} {γ : Type} (tr start : L'.Relations 1) (src rd dst wr : L'.Relations 2) : L'.Formula γ

Determinism of the instance, as a sentence.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_trUniqF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd : L'.Relations 2) : (trUniqF tr src rd).Realize v ↔ ∀ (τ τ' q a : M), FirstOrder.Language.Structure.RelMap tr ![τ] → FirstOrder.Language.Structure.RelMap tr ![τ'] → FirstOrder.Language.Structure.RelMap src ![τ, q] → FirstOrder.Language.Structure.RelMap src ![τ', q] → FirstOrder.Language.Structure.RelMap rd ![τ, a] → FirstOrder.Language.Structure.RelMap rd ![τ', a] → τ = τ'

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_detF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr start : L'.Relations 1) (src rd dst wr : L'.Relations 2) : (detF tr start src rd dst wr).Realize v ↔ (∀ (q q' : M), FirstOrder.Language.Structure.RelMap start ![q] → FirstOrder.Language.Structure.RelMap start ![q'] → q = q') ∧ (∀ (τ τ' q a : M), FirstOrder.Language.Structure.RelMap tr ![τ] → FirstOrder.Language.Structure.RelMap tr ![τ'] → FirstOrder.Language.Structure.RelMap src ![τ, q] → FirstOrder.Language.Structure.RelMap src ![τ', q] → FirstOrder.Language.Structure.RelMap rd ![τ, a] → FirstOrder.Language.Structure.RelMap rd ![τ', a] → τ = τ') ∧ (∀ (τ q q' : M), FirstOrder.Language.Structure.RelMap dst ![τ, q] → FirstOrder.Language.Structure.RelMap dst ![τ, q'] → q = q') ∧ ∀ (τ a a' : M), FirstOrder.Language.Structure.RelMap wr ![τ, a] → FirstOrder.Language.Structure.RelMap wr ![τ, a'] → a = a'

The block and the specification

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mBlock : SOBlock

The block whose assignments are the configurations: the tape as a binary relation variable, the state and the head as unary marks.

Equations

• DescriptiveComplexity.SpaceTM.mBlock = { ι := Option Bool, ιFinite := ⋯, arity := fun (i : Option Bool) => match i with | none => 2 | some val => 1 }

def DescriptiveComplexity.SpaceTM.mSymT : mBlock.lang.Relations 2

The symbol for the tape.

Equations

• DescriptiveComplexity.SpaceTM.mSymT = ⟨none, DescriptiveComplexity.SpaceTM.mSymT._proof_1⟩

def DescriptiveComplexity.SpaceTM.mSymS : mBlock.lang.Relations 1

The symbol for the state.

Equations

• DescriptiveComplexity.SpaceTM.mSymS = ⟨some false, DescriptiveComplexity.SpaceTM.mSymS._proof_1⟩

def DescriptiveComplexity.SpaceTM.mSymH : mBlock.lang.Relations 1

The symbol for the head.

Equations

• DescriptiveComplexity.SpaceTM.mSymH = ⟨some true, DescriptiveComplexity.SpaceTM.mSymH._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mBase : FirstOrder.Language

The ordered expansion of the machine vocabulary.

Equations

• DescriptiveComplexity.SpaceTM.mBase = FirstOrder.Language.turing.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mLang₁ : FirstOrder.Language

The vocabulary of a one-copy expansion by the block.

Equations

• DescriptiveComplexity.SpaceTM.mLang₁ = DescriptiveComplexity.SpaceTM.mBase.sum DescriptiveComplexity.SpaceTM.mBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mLang₂ : FirstOrder.Language

The vocabulary of a two-copy expansion by the block.

Equations

• DescriptiveComplexity.SpaceTM.mLang₂ = DescriptiveComplexity.SpaceTM.mLang₁.sum DescriptiveComplexity.SpaceTM.mBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mIn₁ {n : ℕ} (r : FirstOrder.Language.turing.Relations n) : mLang₁.Relations n

A machine symbol in the one-copy expansion.

Equations

• DescriptiveComplexity.SpaceTM.mIn₁ r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mT₁ : mLang₁.Relations 2

The tape of the state, in the one-copy expansion.

Equations

• DescriptiveComplexity.SpaceTM.mT₁ = Sum.inr DescriptiveComplexity.SpaceTM.mSymT

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mS₁ : mLang₁.Relations 1

The state mark, in the one-copy expansion.

Equations

• DescriptiveComplexity.SpaceTM.mS₁ = Sum.inr DescriptiveComplexity.SpaceTM.mSymS

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mH₁ : mLang₁.Relations 1

The head mark, in the one-copy expansion.

Equations

• DescriptiveComplexity.SpaceTM.mH₁ = Sum.inr DescriptiveComplexity.SpaceTM.mSymH

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mIn₂ {n : ℕ} (r : FirstOrder.Language.turing.Relations n) : mLang₂.Relations n

A machine symbol in the two-copy expansion.

Equations

• DescriptiveComplexity.SpaceTM.mIn₂ r = Sum.inl (Sum.inl (Sum.inl r))

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mTc₂ : mLang₂.Relations 2

The tape of the current state.

Equations

• DescriptiveComplexity.SpaceTM.mTc₂ = Sum.inl (Sum.inr DescriptiveComplexity.SpaceTM.mSymT)

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mSc₂ : mLang₂.Relations 1

The state mark of the current state.

Equations

• DescriptiveComplexity.SpaceTM.mSc₂ = Sum.inl (Sum.inr DescriptiveComplexity.SpaceTM.mSymS)

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mHc₂ : mLang₂.Relations 1

The head mark of the current state.

Equations

• DescriptiveComplexity.SpaceTM.mHc₂ = Sum.inl (Sum.inr DescriptiveComplexity.SpaceTM.mSymH)

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mTn₂ : mLang₂.Relations 2

The tape of the next state.

Equations

• DescriptiveComplexity.SpaceTM.mTn₂ = Sum.inr DescriptiveComplexity.SpaceTM.mSymT

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mSn₂ : mLang₂.Relations 1

The state mark of the next state.

Equations

• DescriptiveComplexity.SpaceTM.mSn₂ = Sum.inr DescriptiveComplexity.SpaceTM.mSymS

@[reducible, inline]

abbrev DescriptiveComplexity.SpaceTM.mHn₂ : mLang₂.Relations 1

The head mark of the next state.

Equations

• DescriptiveComplexity.SpaceTM.mHn₂ = Sum.inr DescriptiveComplexity.SpaceTM.mSymH

noncomputable def DescriptiveComplexity.SpaceTM.mSpec : SOTCSpec FirstOrder.Language.turing

The specification: the states are the configurations, the transition is one step of the machine, the starting states are the initial configurations of a well-formed instance and the accepting ones are those in an accepting state.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.mSpecDet : SOTCSpec FirstOrder.Language.turing

The deterministic specification: the same walk, with determinism of the instance demanded of the starting states.

Equations

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

Reading a state back as a configuration

def DescriptiveComplexity.SpaceTM.mTape {A : Type} (ρ : mBlock.Assignment A) (p a : A) : Prop

The tape held by a state of the walk.

Equations

• DescriptiveComplexity.SpaceTM.mTape ρ p a = ρ none ![p, a]

def DescriptiveComplexity.SpaceTM.mState {A : Type} (ρ : mBlock.Assignment A) (q : A) : Prop

The state mark held by a state of the walk.

Equations

• DescriptiveComplexity.SpaceTM.mState ρ q = ρ (some false) ![q]

def DescriptiveComplexity.SpaceTM.mHead {A : Type} (ρ : mBlock.Assignment A) (p : A) : Prop

The head mark held by a state of the walk.

Equations

• DescriptiveComplexity.SpaceTM.mHead ρ p = ρ (some true) ![p]

def DescriptiveComplexity.SpaceTM.IsCfgOn {A : Type} (ρ : mBlock.Assignment A) : Prop

A state of the walk is a configuration: its tape is total and functional and its two marks are singletons.

Equations

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

def DescriptiveComplexity.SpaceTM.cfgAssign {A : Type} (c : Config A) : mBlock.Assignment A

The state of the walk that a configuration is.

Equations

• DescriptiveComplexity.SpaceTM.cfgAssign c none = fun (x : Fin (DescriptiveComplexity.SpaceTM.mBlock.arity none) → A) => c.tape (x 0) = x 1
• DescriptiveComplexity.SpaceTM.cfgAssign c (some false) = fun (x : Fin (DescriptiveComplexity.SpaceTM.mBlock.arity (some false)) → A) => x 0 = c.state
• DescriptiveComplexity.SpaceTM.cfgAssign c (some true) = fun (x : Fin (DescriptiveComplexity.SpaceTM.mBlock.arity (some true)) → A) => x 0 = c.head

@[simp]

theorem DescriptiveComplexity.SpaceTM.mTape_cfgAssign {A : Type} (c : Config A) (p a : A) : mTape (cfgAssign c) p a ↔ c.tape p = a

@[simp]

theorem DescriptiveComplexity.SpaceTM.mState_cfgAssign {A : Type} (c : Config A) (q : A) : mState (cfgAssign c) q ↔ q = c.state

@[simp]

theorem DescriptiveComplexity.SpaceTM.mHead_cfgAssign {A : Type} (c : Config A) (p : A) : mHead (cfgAssign c) p ↔ p = c.head

theorem DescriptiveComplexity.SpaceTM.isCfgOn_cfgAssign {A : Type} (c : Config A) : IsCfgOn (cfgAssign c)

noncomputable def DescriptiveComplexity.SpaceTM.cfgOf {A : Type} {ρ : mBlock.Assignment A} (h : IsCfgOn ρ) : Config A

The configuration a state of the walk is, when it is one.

Equations

• DescriptiveComplexity.SpaceTM.cfgOf h = { state := ⋯.choose, head := ⋯.choose, tape := fun (p : A) => ⋯.choose }

theorem DescriptiveComplexity.SpaceTM.mState_cfgOf {A : Type} {ρ : mBlock.Assignment A} (h : IsCfgOn ρ) (q : A) : mState ρ q ↔ q = (cfgOf h).state

theorem DescriptiveComplexity.SpaceTM.mHead_cfgOf {A : Type} {ρ : mBlock.Assignment A} (h : IsCfgOn ρ) (p : A) : mHead ρ p ↔ p = (cfgOf h).head

theorem DescriptiveComplexity.SpaceTM.mTape_cfgOf {A : Type} {ρ : mBlock.Assignment A} (h : IsCfgOn ρ) (p a : A) : mTape ρ p a ↔ (cfgOf h).tape p = a

The symbols, read back

theorem DescriptiveComplexity.SpaceTM.relMap_mIn₁ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {n : ℕ} (ρ : mBlock.Assignment A) (r : FirstOrder.Language.turing.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (mIn₁ r) w ↔ FirstOrder.Language.Structure.RelMap r w

theorem DescriptiveComplexity.SpaceTM.relMap_mT₁ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (p a : A) : FirstOrder.Language.Structure.RelMap mT₁ ![p, a] ↔ mTape ρ p a

theorem DescriptiveComplexity.SpaceTM.relMap_mS₁ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (q : A) : FirstOrder.Language.Structure.RelMap mS₁ ![q] ↔ mState ρ q

theorem DescriptiveComplexity.SpaceTM.relMap_mH₁ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (p : A) : FirstOrder.Language.Structure.RelMap mH₁ ![p] ↔ mHead ρ p

theorem DescriptiveComplexity.SpaceTM.relMap_mIn₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {n : ℕ} (ρ σ : mBlock.Assignment A) (r : FirstOrder.Language.turing.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (mIn₂ r) w ↔ FirstOrder.Language.Structure.RelMap r w

theorem DescriptiveComplexity.SpaceTM.relMap_mTc₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (p a : A) : FirstOrder.Language.Structure.RelMap mTc₂ ![p, a] ↔ mTape ρ p a

theorem DescriptiveComplexity.SpaceTM.relMap_mSc₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (q : A) : FirstOrder.Language.Structure.RelMap mSc₂ ![q] ↔ mState ρ q

theorem DescriptiveComplexity.SpaceTM.relMap_mHc₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (p : A) : FirstOrder.Language.Structure.RelMap mHc₂ ![p] ↔ mHead ρ p

theorem DescriptiveComplexity.SpaceTM.relMap_mTn₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (p a : A) : FirstOrder.Language.Structure.RelMap mTn₂ ![p, a] ↔ mTape σ p a

theorem DescriptiveComplexity.SpaceTM.relMap_mSn₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (q : A) : FirstOrder.Language.Structure.RelMap mSn₂ ![q] ↔ mState σ q

theorem DescriptiveComplexity.SpaceTM.relMap_mHn₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (p : A) : FirstOrder.Language.Structure.RelMap mHn₂ ![p] ↔ mHead σ p

theorem DescriptiveComplexity.SpaceTM.mRealize_inf₁ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (φ ψ : mLang₁.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

theorem DescriptiveComplexity.SpaceTM.mRealize_inf₂ {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) (φ ψ : mLang₂.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

def DescriptiveComplexity.SpaceTM.Represents {A : Type} (ρ : mBlock.Assignment A) (c : Config A) : Prop

A state of the walk represents a configuration.

Equations

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

theorem DescriptiveComplexity.SpaceTM.represents_cfgAssign {A : Type} (c : Config A) : Represents (cfgAssign c) c

theorem DescriptiveComplexity.SpaceTM.exists_represents {A : Type} {ρ : mBlock.Assignment A} (h : IsCfgOn ρ) : ∃ (c : Config A), Represents ρ c

theorem DescriptiveComplexity.SpaceTM.isCfgOn_of_represents {A : Type} {ρ : mBlock.Assignment A} {c : Config A} (h : Represents ρ c) : IsCfgOn ρ

Correctness

def DescriptiveComplexity.SpaceTM.StepOn {A : Type} [FirstOrder.Language.turing.Structure A] (ρ σ : mBlock.Assignment A) : Prop

One step of the machine, read off two states of the walk.

Equations

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

theorem DescriptiveComplexity.SpaceTM.mSpec_isSrc_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) : mSpec.IsSrc ρ ↔ (tmData A).WellFormed ∧ IsCfgOn ρ ∧ (∀ (q : A), mState ρ q → (tmData A).Start q) ∧ (∀ (p : A), mHead ρ p → MinPos (tmData A).Le (tmData A).Posn p) ∧ ∀ (p a : A), mTape ρ p a → (tmData A).InitTape p a

theorem DescriptiveComplexity.SpaceTM.mSpec_isTgt_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) : mSpec.IsTgt ρ ↔ ∀ (q : A), mState ρ q → (tmData A).Acc q

theorem DescriptiveComplexity.SpaceTM.mSpec_step_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ σ : mBlock.Assignment A) : mSpec.Step ρ σ ↔ StepOn ρ σ ∧ IsCfgOn σ

theorem DescriptiveComplexity.SpaceTM.stepOn_iff {A : Type} [FirstOrder.Language.turing.Structure A] {ρ σ : mBlock.Assignment A} {c d : Config A} (hρ : Represents ρ c) (hσ : Represents σ d) : StepOn ρ σ ↔ (tmData A).Step c d

The transition sentence is one step of the machine, on states that represent configurations.

theorem DescriptiveComplexity.SpaceTM.mSpec_reach {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {ρ σ : mBlock.Assignment A} (h : mSpec.Reach ρ σ) {c : Config A} (hρ : Represents ρ c) : ∃ (d : Config A), Represents σ d ∧ Relation.ReflTransGen (tmData A).Step c d

Every state reachable from one representing a configuration represents one too, and the walk is a run of the machine.

theorem DescriptiveComplexity.SpaceTM.mSpec_reach_of {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {c d : Config A} (h : Relation.ReflTransGen (tmData A).Step c d) : mSpec.Reach (cfgAssign c) (cfgAssign d)

theorem DescriptiveComplexity.SpaceTM.mSpec_accepts_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] : mSpec.Accepts A ↔ (tmData A).WellFormed ∧ (tmData A).AcceptsSpace

The specification is correct: its walk accepts exactly the well-formed instances whose machine accepts in bounded space.

theorem DescriptiveComplexity.SpaceTM.mSpecDet_isSrc_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) : mSpecDet.IsSrc ρ ↔ (tmData A).Deterministic ∧ mSpec.IsSrc ρ

theorem DescriptiveComplexity.SpaceTM.mSpecDet_accepts_iff {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] : mSpecDet.Accepts A ↔ (tmData A).Deterministic ∧ mSpec.Accepts A

The two problems are in PSPACE

theorem DescriptiveComplexity.ntmAcceptSpace_sotcDefinable : SOTCDefinable NTMAcceptSpace

The space-bounded nondeterministic machine problem is in PSPACE: a configuration is an assignment of the block, a step is a first-order condition on two of them, and an unbounded run is their transitive closure.

theorem DescriptiveComplexity.ntmAcceptSpace_mem_PSPACE : PSPACE.Mem NTMAcceptSpace

NTMAcceptSpace ∈ PSPACE.

theorem DescriptiveComplexity.dtmAcceptSpace_sotcDefinable : SOTCDefinable DTMAcceptSpace

The space-bounded deterministic machine problem is in PSPACE: the same walk, with determinism of the instance checked by the source sentence.

theorem DescriptiveComplexity.dtmAcceptSpace_mem_PSPACE : PSPACE.Mem DTMAcceptSpace

DTMAcceptSpace ∈ PSPACE.