A run is a walk along the positions

The one lemma both halves of the machine bridge consume, DescriptiveComplexity.TMData.accepts_iff_exists_walk: acceptance – an ℕ-indexed run, shorter than the number of positions – is equivalent to a family of configurations indexed by the position elements themselves, in order.

This is where the unary time bound is cashed in. A first-order kernel cannot talk about “the n-th step”; it can talk about “the configuration at time t” for t ranging over the universe, related to “the configuration at time t'” whenever t' is the immediate successor of t. DescriptiveComplexity.TMData.IsWalk is exactly that, and it is what the Σ₁ definition guesses.

The translation is by the rank of a position – DescriptiveComplexity.bitRank, the number of positions strictly below it – which turns the walk into arithmetic: rank 0 at the lowest position, +1 along DescriptiveComplexity.SuccPos, and Nat.card - 1 at the highest. Those three facts are proved here first.

Because a stalled machine has no successor configuration, the walk allows a stutter – but only in an accepting state, so that a walk that has accepted stays accepted until the last position, where acceptance is read off.

The rank of a position

theorem DescriptiveComplexity.bitRank_succPos {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q : A} (h : SuccPos Le Posn p q) : bitRank Le Posn q = bitRank Le Posn p + 1

Rank increases by one along an immediate successor.

theorem DescriptiveComplexity.bitRank_lt_card {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} {p : A} (hp : Posn p) : bitRank Le Posn p < Nat.card { x : A // Posn x }

The rank of a position is below the number of positions.

def DescriptiveComplexity.TMData.IsWalk {A : Type} (M : TMData A) (conf : A → Config A) : Prop

A run laid out along the positions: a configuration for each position, initial at the lowest, related by a step – or by a stutter in an accepting state, for a machine that has already accepted – at each immediate successor, and accepting at the highest.

Equations

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

theorem DescriptiveComplexity.TMData.IsWalk.exists_stepsIn {A : Type} {M : TMData A} [Finite A] (hlin : IsLinOrd M.Le) {conf : A → Config A} (h : M.IsWalk conf) {p₀ : A} (hp₀ : MinPos M.Le M.Posn p₀) (p : A) : M.Posn p → ∃ n ≤ bitRank M.Le M.Posn p, M.StepsIn n (conf p₀) (conf p)

A walk is a run: the configuration at a position is reached from the one at the lowest position in at most as many steps as the position has positions below it, a stutter costing none.

theorem DescriptiveComplexity.TMData.accepts_iff_exists_walk {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) : M.Accepts ↔ ∃ (conf : A → Config A), M.IsWalk conf

Acceptance is a walk along the positions.

The relational form of a walk

A first-order kernel cannot guess a function A → Config A; it guesses relations. DescriptiveComplexity.TMData.RelWalk is the walk written with the three relations a Σ₁ block can supply – Q t q, “the state at time t is q”, H t p, “the head is on p”, and T t p a, “the cell p holds a” – each asserted to be functional, which is where the equivalence with a walk by configurations is bought.

Every clause below is a literal transcription target for DescriptiveComplexity.Problems.Machine.Membership: nothing here quantifies over anything but elements of the universe.

def DescriptiveComplexity.TMData.RelStep {A : Type} (M : TMData A) (Q H : A → A → Prop) (T : A → A → A → Prop) (t t' : A) : Prop

The step clause, relationally: some transition takes the configuration at t to the one at t'.

Equations

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

def DescriptiveComplexity.TMData.RelStutter {A : Type} (M : TMData A) (Q H : A → A → Prop) (T : A → A → A → Prop) (t t' : A) : Prop

The stutter clause, relationally: an accepting configuration repeated.

Equations

• M.RelStutter Q H T t t' = ((∀ (q : A), Q t q → M.Acc q) ∧ (∀ (q : A), Q t' q ↔ Q t q) ∧ (∀ (p : A), H t' p ↔ H t p) ∧ ∀ (p a : A), T t' p a ↔ T t p a)

structure DescriptiveComplexity.TMData.RelWalk {A : Type} (M : TMData A) (Q H : A → A → Prop) (T : A → A → A → Prop) : Prop

A walk, guessed as three relations.

• qex (t : A) : ∃ (q : A), Q t q

  There is a state at each time.

• quniq (t q q' : A) : Q t q → Q t q' → q = q'

  There is only one.

• hex (t : A) : ∃ (p : A), H t p

  The head is somewhere at each time.

• huniq (t p p' : A) : H t p → H t p' → p = p'

  It is in only one place.

• tex (t p : A) : ∃ (a : A), T t p a

  Every cell holds a symbol at each time.

• tuniq (t p a a' : A) : T t p a → T t p a' → a = a'

  It holds only one.

• init (t : A) : MinPos M.Le M.Posn t → (∀ (q : A), Q t q → M.Start q) ∧ (∀ (p : A), H t p → MinPos M.Le M.Posn p) ∧ ∀ (p a : A), T t p a → M.InitTape p a

  At the lowest time the configuration is initial.

• step (t t' : A) : SuccPos M.Le M.Posn t t' → M.RelStep Q H T t t' ∨ M.RelStutter Q H T t t'

  Consecutive times are related by a step or by an accepting stutter.

• acc (t : A) : MaxPos M.Le M.Posn t → ∀ (q : A), Q t q → M.Acc q

  At the highest time the state is accepting.

noncomputable def DescriptiveComplexity.TMData.RelWalk.conf {A : Type} {M : TMData A} {Q H : A → A → Prop} {T : A → A → A → Prop} (h : M.RelWalk Q H T) (t : A) : Config A

The configurations a relational walk describes: at each time, the state, the head cell and the tape contents the three functional relations name.

Equations

• h.conf t = { state := ⋯.choose, head := ⋯.choose, tape := fun (p : A) => ⋯.choose }

theorem DescriptiveComplexity.TMData.RelWalk.isWalk {A : Type} {M : TMData A} {Q H : A → A → Prop} {T : A → A → A → Prop} (h : M.RelWalk Q H T) : M.IsWalk h.conf

A relational walk is a walk, through the configurations it describes.

theorem DescriptiveComplexity.TMData.IsWalk.relWalk {A : Type} {M : TMData A} {conf : A → Config A} (h : M.IsWalk conf) : M.RelWalk (fun (t q : A) => q = (conf t).state) (fun (t p : A) => p = (conf t).head) fun (t p a : A) => a = (conf t).tape p

A walk is a relational walk, through the graphs of its configurations.

theorem DescriptiveComplexity.TMData.exists_relWalk_iff_exists_walk {A : Type} {M : TMData A} : (∃ (Q : A → A → Prop) (H : A → A → Prop) (T : A → A → A → Prop), M.RelWalk Q H T) ↔ ∃ (conf : A → Config A), M.IsWalk conf

The two forms of a walk agree. Left to right the relations are read off the configurations; right to left the configurations are chosen, which is what the functionality clauses make well defined.