Documentation

DescriptiveComplexity.HeadAutomaton

Two-way multi-head automata over a structure #

The machine model of the logarithmic-space level: a fixed finite control with k two-way heads, each head holding an element of the universe, with no work tape at all. This is the machine side of DescriptiveComplexity.LOGSPACE and DescriptiveComplexity.NL, and it is deliberately not the automaton of formal language theory.

Which automaton this is, and which it is not #

Mathlib's FirstOrder-free DFA/NFA consume a word by a one-way left fold over an alphabet. Neither half of that fits here:

So the model here is its own structure, in the style of DescriptiveComplexity.TMData (which likewise presents a machine as relations on a universe rather than as strings):

Nondeterminism is a list of transitions per state and reading; DescriptiveComplexity.HeadAutomaton.IsDeterministic restricts it to at most one, which is the machine-level counterpart of the determinization of DescriptiveComplexity.TCSpec.det.

What is proved here, and what is not #

A configuration – a control state with a k-tuple – is a DescriptiveComplexity.TCSpec.Node: the control is the mode and the heads are the tuple. So an automaton compiles into a specification (DescriptiveComplexity.HeadAutomaton.toSpec) by writing each transition as a first-order formula, and its acceptance is the acceptance of that specification (DescriptiveComplexity.HeadAutomaton.accepts_toSpec). Hence

This direction is the cheap one, and it is also a practical membership tool: exhibiting an automaton is often much easier than writing a DescriptiveComplexity.TCSpec by hand.

The converse – every FO(TC) definable problem is recognized by such an automaton – is proved in DescriptiveComplexity.HeadCapture, on top of the guarded-transition presentation of DescriptiveComplexity.HeadProgram and the formula evaluator of DescriptiveComplexity.HeadEval; together with the above it gives the capture theorem DescriptiveComplexity.tcDefinable_iff_automaton, and DescriptiveComplexity.mem_NL_iff_automaton. The deterministic level is DescriptiveComplexity.HeadCaptureDet, where a machine for an arbitrary FO(DTC) definition needs more than the evaluator – it has to search where the nondeterministic one guesses, and to bound its own walk with a step budget – giving DescriptiveComplexity.dtcDefinable_iff_automaton and DescriptiveComplexity.mem_LOGSPACE_iff_automaton.

Moves #

source
inductive DescriptiveComplexity.HeadMove (k : ℕ) :
Type

What a head may do in one step: stay where it is, jump to an end of the order, copy another head, or step to the immediate successor or predecessor of another head. All of it is definable from the order, which is what lets a transition become a first-order formula.

  • stay {k : ℕ} : HeadMove k

    Stay on the current element.

  • toMin {k : ℕ} : HeadMove k

    Jump to the least element.

  • toMax {k : ℕ} : HeadMove k

    Jump to the greatest element.

  • copy {k : ℕ} (i : Fin k) : HeadMove k

    Copy the position of head i.

  • succ {k : ℕ} (i : Fin k) : HeadMove k

    Move to the immediate successor of head i (disabled at the greatest element, which is how a head runs off the end).

  • pred {k : ℕ} (i : Fin k) : HeadMove k

    Move to the immediate predecessor of head i (disabled at the least element).

Instances For
    Dependency graph
    source
    def DescriptiveComplexity.instDecidableEqHeadMove.decEq {k✝ : ℕ} (x✝ x✝¹ : HeadMove k✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.instDecidableEqHeadMove {k✝ : ℕ} :
      DecidableEq (HeadMove k✝)
      Equations
      Dependency graph
      source
      def DescriptiveComplexity.HeadMove.Holds {k : ℕ} {A : Type} [LinearOrder A] (mv : HeadMove k) (x : Fin k → A) (j : Fin k) (y : A) :
      Prop

      The semantics of a move: where head j may be after it, the current heads being x.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.HeadMove.holds_unique {k : ℕ} {A : Type} [LinearOrder A] {mv : HeadMove k} {x : Fin k → A} {j : Fin k} {y y' : A} (h : mv.Holds x j y) (h' : mv.Holds x j y') :
        y = y'

        A move determines the new position of its head.

        Dependency graph
        source
        def DescriptiveComplexity.HeadMove.eqVarF (L : FirstOrder.Language) {γ : Type} (u v : γ) :
        (L.sum FirstOrder.Language.order).Formula γ

        Equality of two variables, as a formula.

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.HeadMove.toFormula (L : FirstOrder.Language) {k : ℕ} (j : Fin k) :
          HeadMove k → (L.sum FirstOrder.Language.order).Formula (Fin k ⊕ Fin k)

          A move, as a formula relating the current heads (left) to the new position of head j (right).

          Equations
          Instances For
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.HeadMove.realize_eqVarF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (u w : γ) :
            (eqVarF L u w).Realize v ↔ v u = v w
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.HeadMove.realize_toFormula {L : FirstOrder.Language} {k : ℕ} {A : Type} [LinearOrder A] [L.Structure A] (j : Fin k) (mv : HeadMove k) (x y : Fin k → A) :
            (toFormula L j mv).Realize (Sum.elim x y) ↔ mv.Holds x j (y j)
            Dependency graph

            The automaton #

            source
            structure DescriptiveComplexity.HeadAutomaton (L : FirstOrder.Language) (k : ℕ) :
            Type 1

            A two-way k-head automaton over L-structures: a finite control, a finite list of quantifier-free tests of the head positions, and, per state and per outcome of those tests, a list of possible transitions – a new state and one move per head. No work tape: all the storage is in the k heads.

            • State : Type

              The control states.

            • stateFinite : Finite self.State

              The control is finite: that is what makes this a machine.

            • start : self.State

              The initial state.

            • accept : self.State → Bool

              The accepting states.

            • TestIx : Type

              What the control reads at each step, indexed by a finite type.

            • testFinite : Finite self.TestIx

              Finitely many tests: a control that could read unboundedly many facts would not be a finite control.

            • test : self.TestIx → (L.sum FirstOrder.Language.order).Formula (Fin k)

              The tests: what the control sees of the current head positions.

            • test_qf (i : self.TestIx) : FirstOrder.Language.BoundedFormula.IsQF (self.test i)

              The tests are quantifier-free. The control may compare its heads and look at the relations holding between them, and nothing else; a quantified test would make the model first-order logic in disguise.

            • trans : self.State → (self.TestIx → Bool) → List (self.State × (Fin k → HeadMove k))

              The transitions available in a state, at a given outcome of the tests: a new state and a move for each head. Nondeterminism is the length of this list.

            Instances For
              Dependency graph
              source
              @[reducible, inline]
              abbrev DescriptiveComplexity.HeadAutomaton.Config {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) (A : Type) :
              Type

              A configuration: a control state together with the positions of the heads. It is exactly a node of a DescriptiveComplexity.TCSpec.

              Equations
              Instances For
                Dependency graph
                source
                noncomputable def DescriptiveComplexity.HeadAutomaton.reading {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (x : Fin k → A) :
                M.TestIx → Bool

                What the control reads at a configuration: the truth values of its tests.

                Equations
                Instances For
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HeadAutomaton.reading_iff {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (x : Fin k → A) (i : M.TestIx) :
                  M.reading x i = true ↔ (M.test i).Realize x
                  Dependency graph
                  source
                  def DescriptiveComplexity.HeadAutomaton.Step {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (a b : M.Config A) :
                  Prop

                  One step of the automaton: some transition available at the current state and reading leads to the new state, each head moving as it prescribes.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    def DescriptiveComplexity.HeadAutomaton.Accepts {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) (A : Type) [L.Structure A] [LinearOrder A] :
                    Prop

                    The automaton accepts the structure when an accepting state is reachable from an initial configuration – the initial state with every head on the least element.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      def DescriptiveComplexity.HeadAutomaton.IsDeterministic {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) :
                      Prop

                      The automaton is deterministic: at most one transition per state and reading.

                      Equations
                      Instances For
                        Dependency graph

                        Compiling an automaton into a specification #

                        source
                        noncomputable def DescriptiveComplexity.HeadAutomaton.allReadings (T : Type) [Finite T] :
                        List (T → Bool)

                        All outcomes the tests may have, as a list: the transition formula is a disjunction over them.

                        Equations
                        Instances For
                          Dependency graph
                          source
                          theorem DescriptiveComplexity.HeadAutomaton.mem_allReadings {T : Type} [Finite T] (r : T → Bool) :
                          r ∈ allReadings T
                          Dependency graph
                          source
                          noncomputable def DescriptiveComplexity.HeadAutomaton.allTests {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) :
                          List M.TestIx

                          The test indices, as a list.

                          Equations
                          Instances For
                            Dependency graph
                            source
                            theorem DescriptiveComplexity.HeadAutomaton.mem_allTests {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) (i : M.TestIx) :
                            i ∈ M.allTests
                            Dependency graph
                            source
                            noncomputable def DescriptiveComplexity.HeadAutomaton.readingF {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) (r : M.TestIx → Bool) :
                            (L.sum FirstOrder.Language.order).Formula (Fin k ⊕ Fin k)

                            The formula saying that the tests come out as r does.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Dependency graph
                              source
                              theorem DescriptiveComplexity.HeadAutomaton.realize_readingF {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (r : M.TestIx → Bool) (x y : Fin k → A) :
                              (M.readingF r).Realize (Sum.elim x y) ↔ M.reading x = r
                              Dependency graph
                              source
                              noncomputable def DescriptiveComplexity.HeadAutomaton.movesF {L : FirstOrder.Language} {k : ℕ} (mvs : Fin k → HeadMove k) :
                              (L.sum FirstOrder.Language.order).Formula (Fin k ⊕ Fin k)

                              The formula prescribing the moves of every head.

                              Equations
                              Instances For
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadAutomaton.realize_movesF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (mvs : Fin k → HeadMove k) (x y : Fin k → A) :
                                (movesF mvs).Realize (Sum.elim x y) ↔ ∀ (j : Fin k), (mvs j).Holds x j (y j)
                                Dependency graph
                                source
                                noncomputable def DescriptiveComplexity.HeadAutomaton.stepF {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) (s s' : M.State) :
                                (L.sum FirstOrder.Language.order).Formula (Fin k ⊕ Fin k)

                                The transition formula of the specification, at a pair of control states: a disjunction over the possible readings and over the transitions they enable that land in the second state.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Dependency graph
                                  source
                                  theorem DescriptiveComplexity.HeadAutomaton.realize_stepF {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (s s' : M.State) (x y : Fin k → A) :
                                  (M.stepF s s').Realize (Sum.elim x y) ↔ ∃ p ∈ M.trans s (M.reading x), p.1 = s' ∧ ∀ (j : Fin k), (p.2 j).Holds x j (y j)
                                  Dependency graph
                                  source
                                  noncomputable def DescriptiveComplexity.HeadAutomaton.toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) :
                                  TCSpec L

                                  The specification of the automaton's walk: the control states are the modes, the heads are the tuple, and the transitions are the step formulas.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Dependency graph
                                    source
                                    @[simp]
                                    theorem DescriptiveComplexity.HeadAutomaton.step_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (a b : M.Config A) :
                                    M.toSpec.Step a b ↔ M.Step a b
                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.HeadAutomaton.isSrc_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (a : M.Config A) :
                                    M.toSpec.IsSrc a ↔ a.1 = M.start ∧ ∀ (j : Fin k) (b : A), a.2 j ≤ b
                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.HeadAutomaton.isTgt_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (a : M.Config A) :
                                    M.toSpec.IsTgt a ↔ M.accept a.1 = true
                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.HeadAutomaton.reach_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (a b : M.Config A) :
                                    M.toSpec.Reach a b ↔ Relation.ReflTransGen M.Step a b

                                    The walk of the specification is the run of the automaton.

                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.HeadAutomaton.accepts_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] :
                                    M.toSpec.Accepts A ↔ M.Accepts A

                                    The compilation is correct: the specification accepts exactly the structures the automaton does.

                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.HeadAutomaton.functional_toSpec {L : FirstOrder.Language} {k : ℕ} (M : HeadAutomaton L k) {A : Type} [L.Structure A] [LinearOrder A] (hdet : M.IsDeterministic) :
                                    M.toSpec.Functional A

                                    A deterministic automaton has a functional walk: its transition list holds at most one transition, and each move determines where its head lands.

                                    Dependency graph

                                    Membership through an automaton #

                                    source
                                    theorem DescriptiveComplexity.tcDefinable_of_automaton {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (M : HeadAutomaton L k) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A) :
                                    TCDefinable P

                                    A problem recognized by a two-way multi-head automaton is FO(TC) definable – hence in DescriptiveComplexity.NL. The configurations of the automaton are the nodes of the specification: the control is the mode, the heads are the tuple.

                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.dtcDefinable_of_automaton {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (M : HeadAutomaton L k) (hdet : M.IsDeterministic) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A) :
                                    DTCDefinable P

                                    A problem recognized by a deterministic two-way multi-head automaton is FO(DTC) definable – hence in DescriptiveComplexity.LOGSPACE. Determinism of the control is exactly what makes the walk functional, so its determinization changes nothing.

                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.mem_NL_of_automaton {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (M : HeadAutomaton L k) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A) :
                                    NL.Mem P

                                    A problem recognized by a two-way multi-head automaton is in NL, the membership tool the compilation provides: exhibiting a machine is usually easier than writing a specification by hand.

                                    Dependency graph
                                    source
                                    theorem DescriptiveComplexity.mem_LOGSPACE_of_automaton {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (M : HeadAutomaton L k) (hdet : M.IsDeterministic) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A) :
                                    LOGSPACE.Mem P

                                    A problem recognized by a deterministic two-way multi-head automaton is in LOGSPACE.

                                    Dependency graph