Budgets for deterministic walks

A deterministic machine that simulates a functional walk – one where every node has at most one successor – cannot afford to follow it forever: the walk may cycle, and the machine would then never come back to try anything else. It must give up after a number of steps it can count, and the two halves of that argument are here, both independent of any machine.

The walk is an iterated function

A functional relation is a partial function, and DescriptiveComplexity.stepNext makes it total by leaving a node without successor where it is. Reachability is then iteration (DescriptiveComplexity.reach_iff_iterate), and the budget is the pigeonhole: a reachable node is reachable in fewer steps than the type has elements (DescriptiveComplexity.exists_iterate_lt_card), because a shortest walk cannot visit a node twice – splicing out the loop would shorten it.

The counter can count that far

The counter a machine can afford is an element of a finite linear order walked along covers, so what it must be shown is that enough covers are available: DescriptiveComplexity.Ticks n z says n of them are, and DescriptiveComplexity.ticks_of_orank says that this holds as soon as DescriptiveComplexity.orank z + n is less than the number of elements – at the bottom, one cover short of the whole order. Matching the two halves is then a matter of counting the nodes and the counter values with the same number.

A functional relation, walked as a function

noncomputable def DescriptiveComplexity.stepNext {N : Type} (R : N → N → Prop) (a : N) : N

The successor along a functional relation, a node without one being left where it is: the walk as a total function, so that reachability becomes iteration.

Equations

• DescriptiveComplexity.stepNext R a = if h : ∃ (b : N), R a b then h.choose else a

theorem DescriptiveComplexity.step_stepNext {N : Type} {R : N → N → Prop} {a : N} (h : ∃ (b : N), R a b) : R a (stepNext R a)

theorem DescriptiveComplexity.stepNext_eq_self {N : Type} {R : N → N → Prop} {a : N} (h : ¬∃ (b : N), R a b) : stepNext R a = a

theorem DescriptiveComplexity.stepNext_eq {N : Type} {R : N → N → Prop} {a b : N} (hfun : ∀ (u v w : N), R u v → R u w → v = w) (h : R a b) : stepNext R a = b

On a functional relation the walk follows the only step there is.

theorem DescriptiveComplexity.reach_iff_iterate {N : Type} {R : N → N → Prop} (hfun : ∀ (u v w : N), R u v → R u w → v = w) (a b : N) : Relation.ReflTransGen R a b ↔ ∃ (n : ℕ), (stepNext R)^[n] a = b

Reachability along a functional relation is iteration.

theorem DescriptiveComplexity.exists_iterate_lt_card {N : Type} {R : N → N → Prop} [Finite N] {a b : N} (h : ∃ (n : ℕ), (stepNext R)^[n] a = b) : ∃ n < Nat.card N, (stepNext R)^[n] a = b

The step budget: a node reachable along a functional relation is reachable in fewer steps than the type has elements. A shortest walk visits distinct nodes – a repeat could be spliced out.

How far a counter can count

def DescriptiveComplexity.Ticks {C : Type} [LinearOrder C] : ℕ → C → Prop

n covers are available above z: what a counter must have left for a machine to afford n more steps.

Equations

• DescriptiveComplexity.Ticks 0 x✝ = True
• DescriptiveComplexity.Ticks n.succ x✝ = ∃ (z' : C), x✝ ⋖ z' ∧ DescriptiveComplexity.Ticks n z'

theorem DescriptiveComplexity.ticks_zero {C : Type} [LinearOrder C] (z : C) : Ticks 0 z

theorem DescriptiveComplexity.ticks_succ {C : Type} [LinearOrder C] {n : ℕ} {z z' : C} (h : z ⋖ z') (ht : Ticks n z') : Ticks (n + 1) z

theorem DescriptiveComplexity.ticks_of_orank {C : Type} [LinearOrder C] [Finite C] {z : C} {n : ℕ} (h : orank z + n < Nat.card C) : Ticks n z

A counter can tick as often as its rank leaves room: at the bottom, one tick short of the whole order.

theorem DescriptiveComplexity.ticks_bot {C : Type} [LinearOrder C] [Finite C] {z : C} {n : ℕ} (hz : ∀ (a : C), z ≤ a) (h : n < Nat.card C) : Ticks n z

The bottom of the order can tick through all of it.