Running a phase of a machine

The reusable half of the hardness reductions. A machine built by a reduction runs in phases, each of which sweeps along a stretch of the positions doing the same thing at every cell: the guess phase of SAT ≤ᶠᵒ[≤] NTMAccept writes a truth value at each variable cell, the check phase folds a flag over them, the propagation phase of HORNSAT ≤ᶠᵒ[≤] DTMAccept marks variables. Reasoning about such a phase should not require redoing an induction along the order each time.

DescriptiveComplexity.TMData.stepsIn_of_segment is that induction, done once: given a family of configurations indexed by the positions and a step between each consecutive pair of a segment [p₀, p₁], the machine walks from p₀ to any position of the segment, in exactly as many steps as their ranks differ. The segment is bounded at both ends because a phase stops – at a marker, or where the next phase begins – and the transitions that carry it need not exist beyond. A phase is then described by exhibiting its intended configuration at each position and checking a single step, which is a statement about the transition table rather than about runs.

The count is DescriptiveComplexity.bitRank – the number of positions strictly below a given one – so phases compose by arithmetic on ranks: sweeping [p₀, p₁] and then [p₁, p₂] takes (rank p₁ - rank p₀) + (rank p₂ - rank p₁) steps, and the budget obligation of the reduction is a comparison of ranks with Nat.card {p // Posn p}.

theorem DescriptiveComplexity.TMData.bitRank_le_of_le {A : Type} [Finite A] {M : TMData A} (hlin : IsLinOrd M.Le) {p q : A} (hp : M.Posn p) (hle : M.Le p q) : bitRank M.Le M.Posn p ≤ bitRank M.Le M.Posn q

The rank of a position is monotone along the order.

theorem DescriptiveComplexity.TMData.succPos_right_unique {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {p q q' : A} (h : SuccPos M.Le M.Posn p q) (h' : SuccPos M.Le M.Posn p q') : q = q'

The successor of a position is unique. DescriptiveComplexity.succPos_left_unique gives the predecessor; a step of a machine needs this direction, since the head moves to the neighbour in the direction the transition names.

theorem DescriptiveComplexity.TMData.step_functional {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) (hdet : M.Deterministic) {c c₁ c₂ : Config A} (h₁ : M.Step c c₁) (h₂ : M.Step c c₂) : c₁ = c₂

A deterministic machine takes at most one step from any configuration: the transition is pinned by the state and the symbol read, its effect by the functionality of Dst and Write, and the new head by uniqueness of the neighbour in the direction the transition names.

theorem DescriptiveComplexity.TMData.stepsIn_functional {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) (hdet : M.Deterministic) {n : ℕ} {c d d' : Config A} : M.StepsIn n c d → M.StepsIn n c d' → d = d'

Deterministic runs of equal length agree: the run is unique, which is what lets a least fixed point compute it.

theorem DescriptiveComplexity.TMData.exists_succPos' {A : Type} [Finite A] {M : TMData A} (hlin : IsLinOrd M.Le) {p : A} (hp : M.Posn p) (hmax : ¬MaxPos M.Le M.Posn p) : ∃ (q : A), SuccPos M.Le M.Posn p q

Every position that is not the highest has one immediately above it – the mirror of DescriptiveComplexity.exists_predPos, read in the reversed order.

theorem DescriptiveComplexity.TMData.stepsIn_of_segment_down {A : Type} [Finite A] {M : TMData A} (hlin : IsLinOrd M.Le) {conf : A → Config A} {p₀ p₁ : A} (hp₁ : M.Posn p₁) (hstep : ∀ (p q : A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf q) (conf p)) (p : A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.StepsIn (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn p) (conf p₁) (conf p)

Running a phase leftwards. The mirror of DescriptiveComplexity.TMData.stepsIn_of_segment: when each consecutive pair of a segment carries a step downwards, the machine walks from the top of the segment to any position of it. The check sweeps of a reduction alternate direction, so both readings are needed.

theorem DescriptiveComplexity.TMData.stepsIn_of_segment {A : Type} [Finite A] {M : TMData A} (hlin : IsLinOrd M.Le) {conf : A → Config A} {p₀ p₁ : A} (hp₀ : M.Posn p₀) (hstep : ∀ (p q : A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf p) (conf q)) (p : A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.StepsIn (bitRank M.Le M.Posn p - bitRank M.Le M.Posn p₀) (conf p₀) (conf p)

Running a phase. If from p₀ onwards every immediate successor of positions carries a step of the machine, then the machine runs from p₀ to any later position, in exactly the number of steps their ranks differ by.

This is the sweep primitive: a reduction describes a phase by giving its intended configuration at each position and discharging the single-step obligation, with no induction of its own.