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_eq_zero_of_minPos {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p : A} (h : MinPos Le Posn p) : bitRank Le Posn p = 0

The lowest position has rank 0.

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.

theorem DescriptiveComplexity.bitRank_maxPos {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} {p : A} (h : MaxPos Le Posn p) : bitRank Le Posn p + 1 = Nat.card { x : A // Posn x }

The highest position has the greatest rank.

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.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.

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.