Programs: two-way multi-head automata, written with guarded transitions

DescriptiveComplexity.HeadAutomaton is the machine model of the logarithmic-space level, and it is stated the way a finished machine wants to be stated: a fixed list of tests, and a transition table indexed by every outcome those tests may have. That presentation is exactly wrong for building a machine, where one wants to write one transition at a time, each carrying its own guard, and to paste machines together.

This file is the assembly language. A DescriptiveComplexity.HeadProgram is the same model with the transitions presented individually –

• a guard, a quantifier-free formula of the head positions;
• a move for every head;
• a target: another state of the program, or one of two exits, true and false

– and a compilation back into the finished form, DescriptiveComplexity.HeadProgram.compile: it enables every transition whose guard holds, or, priority on, the first one, so that the compiled table has at most one entry per reading and DescriptiveComplexity.HeadAutomaton.IsDeterministic holds outright. Programs whose guards are mutually exclusive (DescriptiveComplexity.HeadProgram.Deterministic) run the same way under both.

What a program is proved to do

Two exits rather than one is what makes programs composable: a fragment can be used as a test by another fragment. The specification of a fragment is DescriptiveComplexity.HeadProgram.Runs: a relation R x b y describing which exits b, with which head positions y, are reachable from the entry at head positions x. It has two halves, and they are not symmetric –

• soundness: every reachable exit satisfies R – the fragment never lies;
• completeness: every R-related outcome is reachable up to the scratch heads, the ones a fragment is allowed to leave dirty.

The scratch heads are the point of the number m carried by Runs: heads below m are the fragment's protected interface, heads from m on are workspace. DescriptiveComplexity.HeadAgree and DescriptiveComplexity.HeadLocal2 say “agrees on the interface” and “depends only on the interface”.

Composition

Everything is built from four pieces:

• DescriptiveComplexity.HeadProgram.exitP – exit at once;
• DescriptiveComplexity.HeadProgram.leafP – test a quantifier-free formula;
• DescriptiveComplexity.HeadProgram.moveP – move the heads;
• DescriptiveComplexity.HeadProgram.wireP – the combinator: a finite family of fragments, one per node of a control graph, each node saying where to go when its fragment exits true and where when it exits false.

wireP subsumes sequencing, branching and looping, and DescriptiveComplexity.HeadProgram.runs_wireP reduces the runs of the assembled program to a walk in the control graph whose steps are the runs of the fragments. Every later construction – the formula evaluator, and the drivers that turn a DescriptiveComplexity.TCSpec into a machine – is a control graph over fragments, and its correctness proof is an argument about that walk, never about states.

The engine room is DescriptiveComplexity.HeadProgram.Embeds: a fragment sitting inside a larger program, with the two lemmas that a run of the fragment is a run of the program, and – the one that does the work – that a run of the program which starts inside the fragment either is still inside it or has left it through one of its exits.

Agreement on an interface

def DescriptiveComplexity.HeadAgree {K : ℕ} (m : ℕ) {A : Type} (x y : Fin K → A) : Prop

Two head assignments agree on the first m heads: the interface a fragment must preserve, the rest being scratch.

Equations

• DescriptiveComplexity.HeadAgree m x y = ∀ (j : Fin K), ↑j < m → x j = y j

theorem DescriptiveComplexity.HeadAgree.refl {K m : ℕ} {A : Type} (x : Fin K → A) : HeadAgree m x x

theorem DescriptiveComplexity.HeadAgree.trans {K m : ℕ} {A : Type} {x y z : Fin K → A} (h : HeadAgree m x y) (h' : HeadAgree m y z) : HeadAgree m x z

def DescriptiveComplexity.HeadLocal {K : ℕ} (m : ℕ) {A : Type} (P : (Fin K → A) → Prop) : Prop

A property of the heads depends only on the first m of them.

Equations

• DescriptiveComplexity.HeadLocal m P = ∀ (x y : Fin K → A), DescriptiveComplexity.HeadAgree m x y → (P x ↔ P y)

def DescriptiveComplexity.HeadLocal2 {K : ℕ} (m : ℕ) {A : Type} (R : (Fin K → A) → Bool → (Fin K → A) → Prop) : Prop

A relation between two head assignments and an exit depends only on the first m heads of each.

Equations

• DescriptiveComplexity.HeadLocal2 m R = ∀ (x x' y y' : Fin K → A), DescriptiveComplexity.HeadAgree m x x' → DescriptiveComplexity.HeadAgree m y y' → ∀ (b : Bool), R x b y ↔ R x' b y'

theorem DescriptiveComplexity.HeadLocal.mono {K m m' : ℕ} {A : Type} {P : (Fin K → A) → Prop} (hm : m' ≤ m) (h : HeadLocal m' P) : HeadLocal m P

Depending on fewer heads is depending on more.

Guarded transitions

structure DescriptiveComplexity.HeadTrans (L : FirstOrder.Language) (K : ℕ) (S : Type) : Type

A guarded transition: a quantifier-free guard on the current head positions, a move for every head, and where to go – another state, or an exit.

• guard : (L.sum FirstOrder.Language.order).Formula (Fin K)

  The guard: the transition is available only where it holds.

• moves : Fin K → HeadMove K

  What each head does.

• target : S ⊕ Bool

  Where the transition goes: a state, or an exit.

def DescriptiveComplexity.HeadTrans.retarget {L : FirstOrder.Language} {K : ℕ} {S S' : Type} (f : S ⊕ Bool → S' ⊕ Bool) (t : HeadTrans L K S) : HeadTrans L K S'

Rewiring a transition, for pasting a fragment into a larger program.

Equations

• DescriptiveComplexity.HeadTrans.retarget f t = { guard := t.guard, moves := t.moves, target := f t.target }

@[simp]

theorem DescriptiveComplexity.HeadTrans.retarget_guard {L : FirstOrder.Language} {K : ℕ} {S S' : Type} (f : S ⊕ Bool → S' ⊕ Bool) (t : HeadTrans L K S) : (retarget f t).guard = t.guard

@[simp]

theorem DescriptiveComplexity.HeadTrans.retarget_moves {L : FirstOrder.Language} {K : ℕ} {S S' : Type} (f : S ⊕ Bool → S' ⊕ Bool) (t : HeadTrans L K S) : (retarget f t).moves = t.moves

@[simp]

theorem DescriptiveComplexity.HeadTrans.retarget_target {L : FirstOrder.Language} {K : ℕ} {S S' : Type} (f : S ⊕ Bool → S' ⊕ Bool) (t : HeadTrans L K S) : (retarget f t).target = f t.target

Programs

structure DescriptiveComplexity.HeadProgram (L : FirstOrder.Language) (K : ℕ) : Type 1

A program: a two-way K-head automaton with its transitions presented one at a time, each with its own quantifier-free guard, and with two exits.

• St : Type

  The states.

• stFinite : Finite self.St

  Finitely many states: that is what makes this a machine.

• entry : self.St

  Where a run starts.

• tr : self.St → List (HeadTrans L K self.St)

  The transitions available at each state, in order of priority.

• guard_qf (s : self.St) (t : HeadTrans L K self.St) : t ∈ self.tr s → FirstOrder.Language.BoundedFormula.IsQF t.guard

  The guards are quantifier-free, as the tests of a machine must be.

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.Site {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) : Type

Where a run can be: at a state, or at one of the two exits.

Equations

• F.Site = (F.St ⊕ Bool)

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.Conf {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (A : Type) : Type

A configuration: a site together with the head positions.

Equations

• F.Conf A = (F.Site × (Fin K → A))

def DescriptiveComplexity.HeadProgram.Step {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) {A : Type} [L.Structure A] [LinearOrder A] (c d : F.Conf A) : Prop

One step: some transition of the current state whose guard holds, with each head moving as it prescribes.

Equations

• F.Step c d = ∃ (s : F.St), c.1 = Sum.inl s ∧ ∃ t ∈ F.tr s, t.guard.Realize c.2 ∧ d.1 = t.target ∧ ∀ (j : Fin K), (t.moves j).Holds c.2 j (d.2 j)

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.Reach {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) {A : Type} [L.Structure A] [LinearOrder A] : F.Conf A → F.Conf A → Prop

Reachability: the reflexive-transitive closure of a step.

Equations

• F.Reach = Relation.ReflTransGen F.Step

What a fragment does

structure DescriptiveComplexity.HeadProgram.Runs {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (A : Type) [L.Structure A] [LinearOrder A] (m : ℕ) (R : (Fin K → A) → Bool → (Fin K → A) → Prop) : Prop

The specification of a fragment: R x b y describes the exits reachable from the entry at head positions x. Soundness is exact – every reachable exit is R-related – while completeness is up to the scratch heads, those from m on.

• sound {x : Fin K → A} {b : Bool} {y : Fin K → A} : F.Reach (Sum.inl F.entry, x) (Sum.inr b, y) → R x b y

  Every reachable exit is R-related to the entry.

• complete {x : Fin K → A} {b : Bool} {y : Fin K → A} : R x b y → ∃ (y' : Fin K → A), HeadAgree m y y' ∧ F.Reach (Sum.inl F.entry, x) (Sum.inr b, y')

  Every R-related outcome is reached, up to the scratch heads.

theorem DescriptiveComplexity.HeadProgram.Runs.weaken {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} {m m' : ℕ} {R : (Fin K → A) → Bool → (Fin K → A) → Prop} (h : F.Runs A m R) (hle : m' ≤ m) : F.Runs A m' R

Leaving more heads dirty is allowed: a fragment protecting m heads protects any smaller interface.

def DescriptiveComplexity.HeadProgram.Decides {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (A : Type) [L.Structure A] [LinearOrder A] (m : ℕ) (P : (Fin K → A) → Prop) : Prop

A fragment that decides a property: it exits true exactly where the property holds, and gives the interface heads back unchanged.

Equations

• F.Decides A m P = F.Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => (b = true ↔ P x) ∧ DescriptiveComplexity.HeadAgree m x y

theorem DescriptiveComplexity.HeadProgram.Decides.runs {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} {m : ℕ} {P : (Fin K → A) → Prop} (h : F.Decides A m P) : F.Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => (b = true ↔ P x) ∧ HeadAgree m x y

Fragments inside programs

def DescriptiveComplexity.HeadProgram.esite {L : FirstOrder.Language} {K : ℕ} {F P : HeadProgram L K} (e : F.St → P.St) (xt : Bool → P.Site) : F.Site → P.Site

Where a site of the fragment sits in the larger program.

Equations

• DescriptiveComplexity.HeadProgram.esite e xt = Sum.elim (fun (s : F.St) => Sum.inl (e s)) xt

def DescriptiveComplexity.HeadProgram.Embeds {L : FirstOrder.Language} {K : ℕ} (F P : HeadProgram L K) (e : F.St → P.St) (xt : Bool → P.Site) : Prop

The fragment F sits inside P at e, its exits wired to xt: the transitions of P at an embedded state are exactly those of F, retargeted.

Equations

• F.Embeds P e xt = ∀ (s : F.St), P.tr (e s) = List.map (DescriptiveComplexity.HeadTrans.retarget (DescriptiveComplexity.HeadProgram.esite e xt)) (F.tr s)

theorem DescriptiveComplexity.HeadProgram.Embeds.step {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F P : HeadProgram L K} {e : F.St → P.St} {xt : Bool → P.Site} (h : F.Embeds P e xt) {c d : F.Conf A} (hcd : F.Step c d) : P.Step (esite e xt c.1, c.2) (esite e xt d.1, d.2)

A step of the fragment is a step of the program.

theorem DescriptiveComplexity.HeadProgram.Embeds.reach {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F P : HeadProgram L K} {e : F.St → P.St} {xt : Bool → P.Site} (h : F.Embeds P e xt) {c d : F.Conf A} (hcd : F.Reach c d) : P.Reach (esite e xt c.1, c.2) (esite e xt d.1, d.2)

A run of the fragment is a run of the program.

theorem DescriptiveComplexity.HeadProgram.Embeds.reach_cases {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F P : HeadProgram L K} {e : F.St → P.St} {xt : Bool → P.Site} (h : F.Embeds P e xt) {s : F.St} {u : Fin K → A} {d : P.Conf A} (hd : P.Reach (Sum.inl (e s), u) d) : (∃ (s' : F.St) (w : Fin K → A), d = (Sum.inl (e s'), w) ∧ F.Reach (Sum.inl s, u) (Sum.inl s', w)) ∨ ∃ (b : Bool) (w : Fin K → A), F.Reach (Sum.inl s, u) (Sum.inr b, w) ∧ P.Reach (xt b, w) d

The decomposition lemma: a run of the program that starts inside the fragment either is still inside it, or has left it through one of its exits – in which case the program's run splits at that exit.

Determinism

def DescriptiveComplexity.HeadProgram.Deterministic {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (A : Type) [L.Structure A] [LinearOrder A] : Prop

A program is deterministic when the transitions available at a state never disagree: any two whose guards hold at the same head positions have the same target and the same moves.

Equations

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

theorem DescriptiveComplexity.HeadProgram.Deterministic.functional {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} (h : F.Deterministic A) {c d d' : F.Conf A} (hd : F.Step c d) (hd' : F.Step c d') : d = d'

A deterministic program has a functional step relation: at most one successor per configuration.

The pieces: exiting, testing, moving

def DescriptiveComplexity.HeadProgram.exitP {L : FirstOrder.Language} {K : ℕ} (b : Bool) : HeadProgram L K

Exit at once, with the given answer.

Equations

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

def DescriptiveComplexity.HeadProgram.leafP {L : FirstOrder.Language} {K : ℕ} (φ : (L.sum FirstOrder.Language.order).Formula (Fin K)) (hφ : FirstOrder.Language.BoundedFormula.IsQF φ) : HeadProgram L K

Test a quantifier-free formula: exit true where it holds and false where it does not, without moving a head.

Equations

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

def DescriptiveComplexity.HeadProgram.moveP {L : FirstOrder.Language} {K : ℕ} (mvs : Fin K → HeadMove K) : HeadProgram L K

Move the heads and exit true.

Equations

• DescriptiveComplexity.HeadProgram.moveP mvs = { St := Unit, stFinite := ⋯, entry := (), tr := fun (x : Unit) => [{ guard := ⊤, moves := mvs, target := Sum.inr true }], guard_qf := ⋯ }

theorem DescriptiveComplexity.HeadProgram.Runs.mono {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {F : HeadProgram L K} {R R' : (Fin K → A) → Bool → (Fin K → A) → Prop} (h : F.Runs A m R) (hsound : ∀ (x : Fin K → A) (b : Bool) (y : Fin K → A), R x b y → R' x b y) (hcomplete : ∀ (x : Fin K → A) (b : Bool) (y : Fin K → A), R' x b y → ∃ (y' : Fin K → A), HeadAgree m y y' ∧ R x b y') : F.Runs A m R'

Weakening what a fragment is known to run: any relation implied by R and whose outcomes R already realizes up to the scratch heads.

The transition tables of the pieces

@[simp]

theorem DescriptiveComplexity.HeadProgram.tr_exitP {L : FirstOrder.Language} {K : ℕ} (b : Bool) (s : (exitP b).St) : (exitP b).tr s = [{ guard := ⊤, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr b }]

@[simp]

theorem DescriptiveComplexity.HeadProgram.tr_leafP {L : FirstOrder.Language} {K : ℕ} (φ : (L.sum FirstOrder.Language.order).Formula (Fin K)) (hφ : FirstOrder.Language.BoundedFormula.IsQF φ) (s : (leafP φ hφ).St) : (leafP φ hφ).tr s = [{ guard := φ, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr true }, { guard := FirstOrder.Language.BoundedFormula.not φ, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr false }]

@[simp]

theorem DescriptiveComplexity.HeadProgram.tr_moveP {L : FirstOrder.Language} {K : ℕ} (mvs : Fin K → HeadMove K) (s : (moveP mvs).St) : (moveP mvs).tr s = [{ guard := ⊤, moves := mvs, target := Sum.inr true }]

Wiring fragments into a control graph

def DescriptiveComplexity.HeadProgram.wireTo {L : FirstOrder.Language} {K : ℕ} {C : Type} (Fam : C → HeadProgram L K) (w : C → Bool → C ⊕ Bool) (c : C) (b : Bool) : (c : C) × (Fam c).St ⊕ Bool

Where a run goes when the fragment at control node c exits with b: to the entry of the fragment at the next control node, or out of the program.

Equations

• DescriptiveComplexity.HeadProgram.wireTo Fam w c b = match w c b with | Sum.inl c' => Sum.inl ⟨c', (Fam c').entry⟩ | Sum.inr b' => Sum.inr b'

def DescriptiveComplexity.HeadProgram.wireP {L : FirstOrder.Language} {K : ℕ} {C : Type} [Finite C] (Fam : C → HeadProgram L K) (w : C → Bool → C ⊕ Bool) (c₀ : C) : HeadProgram L K

The control graph combinator: run the fragment at the current control node, and on its exit follow the wiring w – to another control node, or out. Sequencing, branching and looping are all instances.

Equations

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

def DescriptiveComplexity.HeadProgram.wireStep {K : ℕ} {C A : Type} (R : C → (Fin K → A) → Bool → (Fin K → A) → Prop) (w : C → Bool → C ⊕ Bool) (u v : C × (Fin K → A)) : Prop

One step of the control walk: the fragment at u.1 runs from u.2 to some exit, which the wiring sends on to the next control node.

Equations

• DescriptiveComplexity.HeadProgram.wireStep R w u v = ∃ (b : Bool), R u.1 u.2 b v.2 ∧ w u.1 b = Sum.inl v.1

def DescriptiveComplexity.HeadProgram.wireExit {K : ℕ} {C A : Type} (R : C → (Fin K → A) → Bool → (Fin K → A) → Prop) (w : C → Bool → C ⊕ Bool) (u : C × (Fin K → A)) (b' : Bool) (y : Fin K → A) : Prop

How the control walk leaves the program.

Equations

• DescriptiveComplexity.HeadProgram.wireExit R w u b' y = ∃ (b : Bool), R u.1 u.2 b y ∧ w u.1 b = Sum.inr b'

theorem DescriptiveComplexity.HeadProgram.runs_wireP {L : FirstOrder.Language} {K : ℕ} {C : Type} [Finite C] (Fam : C → HeadProgram L K) (w : C → Bool → C ⊕ Bool) {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {R : C → (Fin K → A) → Bool → (Fin K → A) → Prop} (hR : ∀ (c : C), (Fam c).Runs A m (R c)) (hloc : ∀ (c : C), HeadLocal2 m (R c)) (c₀ : C) : (wireP Fam w c₀).Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => ∃ (u : C × (Fin K → A)), Relation.ReflTransGen (wireStep R w) (c₀, x) u ∧ wireExit R w u b y

What an assembled program runs is the control walk: its exits are those reached by walking the control graph, each step being a run of the fragment sitting at that node. This is the lemma every later construction is proved with.

Compiling a program into an automaton

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.TestOf {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) : Type

The tests a compiled program reads: the guard of each of its transitions.

Equations

• F.TestOf = ((s : F.St) × Fin (F.tr s).length)

def DescriptiveComplexity.HeadProgram.entryOf {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (i : F.TestOf) : F.Site × (Fin K → HeadMove K)

The entry a transition contributes to the compiled transition table.

Equations

• F.entryOf i = (((F.tr i.fst).get i.snd).target, ((F.tr i.fst).get i.snd).moves)

def DescriptiveComplexity.HeadProgram.enabled {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (s : F.St) (r : F.TestOf → Bool) : List (Fin (F.tr s).length)

The transitions of a state that a reading enables, by index.

Equations

• F.enabled s r = List.filter (fun (i : Fin (F.tr s).length) => r ⟨s, i⟩) (List.finRange (F.tr s).length)

def DescriptiveComplexity.HeadProgram.compile {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (pri : Bool) : HeadAutomaton L K

The compiled automaton. At pri := false every transition whose guard holds is enabled – the nondeterministic reading of a program. At pri := true only the first one is, so that the table has at most one entry per reading and DescriptiveComplexity.HeadAutomaton.IsDeterministic holds whatever the guards are.

Equations

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

@[simp]

theorem DescriptiveComplexity.HeadProgram.trans_compile_inl {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (pri : Bool) (s : F.St) (r : F.TestOf → Bool) : (F.compile pri).trans (Sum.inl s) r = List.map (fun (i : Fin (F.tr s).length) => F.entryOf ⟨s, i⟩) (if pri = true then List.take 1 (F.enabled s r) else F.enabled s r)

@[simp]

theorem DescriptiveComplexity.HeadProgram.trans_compile_inr {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) (pri b : Bool) (r : F.TestOf → Bool) : (F.compile pri).trans (Sum.inr b) r = []