The sweep of a wide machine

The primitive every program of a hardness reduction into a wide machine will cite, and the last piece of the address layer:

A machine that takes a step at every increment of its address runs from the empty address to any address, and does so within its clock.

DescriptiveComplexity.stepsIn_of_wideSweep and DescriptiveComplexity.accepts_of_wideSweep. So a phase is described by giving its intended configuration at each address and discharging a single-step obligation between an address and its increment – a statement about the transition table, with no induction and no counting.

Nothing here is new machinery: DescriptiveComplexity.TMData.stepsIn_of_segment already does the induction along the order, at an arbitrary position type, and DescriptiveComplexity.bitRank_lt_card already does the clock. What this file supplies is the identification of the three ends of that statement with the address layer – the empty address is the least position (DescriptiveComplexity.minPos_wpLe_iff), the full one is the last (DescriptiveComplexity.maxPos_wpLe_iff), and a step is the binary increment (DescriptiveComplexity.succPos_wpLe_iff) – so that a program never mentions SuccPos again.

The initial configuration is settled here too. A reduction has no use for the instance's input channel, its control being instance data already, so it leaves wmInp empty; then the initial tape is blank everywhere (DescriptiveComplexity.initTape_of_no_wmInp) and DescriptiveComplexity.isInit_wide exhibits the one initial configuration: a start state, the head on the empty address, every cell blank.

The two ends of the tape

theorem DescriptiveComplexity.minPos_wpLe_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (p : WPoint A) : MinPos wpLe wpPosn p ↔ p = Sum.inl fun (x : A) => False

The empty address is the only least position.

theorem DescriptiveComplexity.maxPos_wpLe_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (p : WPoint A) : MaxPos wpLe wpPosn p ↔ p = Sum.inl fun (x : A) => True

The full address is the only last position.

The initial configuration

theorem DescriptiveComplexity.initTape_of_no_wmInp {A : Type} [FirstOrder.Language.wide.Structure A] (hno : ∀ (x y : A), ¬WMInp x y) (p a : WPoint A) : (wideData A).InitTape p a ↔ (wideData A).Blank a

With no input in the instance the initial tape is blank everywhere. A reduction leaves wmInp empty: its machine's control is instance data already, so it has nothing to read.

theorem DescriptiveComplexity.isInit_wide {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (hno : ∀ (x y : A), ¬WMInp x y) {q₀ b : A} (hq : WMStart q₀) (hb : WMBlank b) : (wideData A).IsInit { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := fun (x : WPoint A) => Sum.inr b }

The initial configuration of a wide machine: a start state, the head on the empty address, every cell blank.

The sweep

theorem DescriptiveComplexity.step_ends_wide {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {p q : WPoint A} (hs : SuccPos wpLe wpPosn p q) : ∃ (s : A → Prop) (t : A → Prop), p = Sum.inl s ∧ q = Sum.inl t ∧ WMIncr WMLe s t

Both ends of a step of a wide machine are addresses, and the step is the binary increment.

theorem DescriptiveComplexity.stepsIn_of_wideSweep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : WPoint A → Config (WPoint A)} (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → (wideData A).Step (conf (Sum.inl s)) (conf (Sum.inl t))) (s : A → Prop) : (wideData A).StepsIn (bitRank (wideData A).Le (wideData A).Posn (Sum.inl s)) (conf (Sum.inl fun (x : A) => False)) (conf (Sum.inl s))

The sweep of a wide machine. A machine stepping at every increment of its address runs from the empty address to any address, in as many steps as that address has rank. The obligation is one step between an address and its increment: no induction along the tape, and no DescriptiveComplexity.SuccPos.

theorem DescriptiveComplexity.accepts_of_wideSweep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : WPoint A → Config (WPoint A)} (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → (wideData A).Step (conf (Sum.inl s)) (conf (Sum.inl t))) (hinit : (wideData A).IsInit (conf (Sum.inl fun (x : A) => False))) (s : A → Prop) (hacc : (wideData A).Acc (conf (Sum.inl s)).state) : (wideData A).Accepts

A sweep that ends accepting makes the machine accept: the clock counts the positions, so the rank of the address the sweep stops at is below it by construction.