Documentation

DescriptiveComplexity.EqPattern

Data read only through its equality pattern is first-order definable #

The keystone of every “write the program down as an interpretation” step, and the one a machine emitted rule by rule needs.

A transition table's attributes – when a rule applies, what state it moves to, what symbol it writes – are functions of its data, and an interpretation can only emit them if they are first-order. Asking each rule for a formula is one way; this file is the other, and the cheaper one:

a rule may read its data only through the equality pattern of that data – which coordinates hold the least element, which hold the greatest, and which two coordinates are equal – and any such reading is first-order definable, once and for all.

The pattern type DescriptiveComplexity.EqPat is finite, so a predicate that factors through it is the disjunction, over the finitely many patterns it admits, of the conjunction of equalities and disequalities that pins a pattern (DescriptiveComplexity.patSetF, DescriptiveComplexity.realize_patSetF_of_factors).

What it does and does not cover. The pattern is what a machine's own bookkeeping reads – flags, markers, which slot holds which designated element – and the whole write side of a rule, since everything a program stores is a copy, a designated element or a successor. It is not the whole guard language of a program that evaluates a logic: such a program eventually compares two of its slots in the order, or asks a relation of the source vocabulary of them, and neither is a function of the pattern. DescriptiveComplexity.Draw.UGDefinable therefore carries a formula, with the disjunction below as one way of building it.

Uniformity in the structure is the point. An interpretation carries one formula for every instance, so the factoring function must not depend on the structure: what a caller owes is a single Q : EqPat c → Prop and, for every A and every tuple, P w ↔ Q (patOf bot top w). That is a Prop about the attribute, provable where it is defined, rather than a syntax tree threaded through every abstraction the program is built from – which is what makes this affordable for a program assembled out of parameterized kits.

The two designated elements are the order's least and greatest, because those are the only elements an interpretation can name; DescriptiveComplexity.botF is Padding's and DescriptiveComplexity.topF is its mirror.

The pattern of a tuple #

source
@[reducible, inline]
abbrev DescriptiveComplexity.EqPat (c : ℕ) :
Type

The equality pattern of a tuple, against two designated elements: which coordinates hold the first, which hold the second, and which two coordinates are equal. A plain product, so that it is finite and has decidable equality without ceremony.

Equations
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.patOf {A : Type} {c : ℕ} (bot top : A) (w : Fin c → A) :
    EqPat c

    The pattern a tuple has.

    Equations
    Instances For
      Dependency graph

      The greatest element, as a formula #

      DescriptiveComplexity.botF says a coordinate is a minimum; this is its mirror, and the two are the only elements an interpretation can name.

      source
      noncomputable def DescriptiveComplexity.topF {L : FirstOrder.Language} {γ : Type} (x : γ) :
      (L.sum FirstOrder.Language.order).Formula γ

      x is a maximum of the order, as a formula.

      Equations
      Instances For
        Dependency graph

        The successor of an element #

        The one thing a program writes that is neither a copy nor a designated element: a loop variable advanced. In a finite linear order the cover of a non-maximal element exists and is unique, so “the next element” is a total function, first-order definable and – what matters here – a function of a single coordinate, hence usable as the source of an output slot.

        source
        noncomputable def DescriptiveComplexity.ordSucc {A : Type} [Preorder A] (a : A) :
        A

        The next element: the cover, where there is one, and the element itself at the top – so that a loop variable at the end of its range simply stands still, which is what DescriptiveComplexity.Draw.tupNext does.

        Equations
        Instances For
          Dependency graph

          The formula of a pattern #

          source
          noncomputable def DescriptiveComplexity.covByF {L : FirstOrder.Language} {γ : Type} (x y : γ) :
          (L.sum FirstOrder.Language.order).Formula γ

          x is covered by y, as a formula: below it, and nothing strictly between.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.litF {L : FirstOrder.Language} {γ : Type} (b : Bool) (φ : (L.sum FirstOrder.Language.order).Formula γ) :
            (L.sum FirstOrder.Language.order).Formula γ

            A literal: a formula or its negation, by a bit.

            Equations
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.patF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (p : EqPat c) (x : Fin c → γ) :
              (L.sum FirstOrder.Language.order).Formula γ

              A pattern, as a formula: each coordinate is or is not the least element, is or is not the greatest, and each pair of coordinates is or is not equal – one literal per decision the pattern records.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                noncomputable def DescriptiveComplexity.patSetF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (Q : EqPat c → Prop) (x : Fin c → γ) :
                (L.sum FirstOrder.Language.order).Formula γ

                A predicate on patterns, as a formula: the disjunction of the patterns it admits, which is a finite disjunction because the pattern type is.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Dependency graph

                  Having a pattern #

                  Their realization #

                  Writing a tuple, slot by slot #

                  The other half of what a machine's rules do: a rule not only fires on its data, it also writes. Everything the EXPSPACE program writes is a copy of one of its input slots or one of the two designated elements, chosen by the input's pattern – so one more builder finishes the toolbox.

                  source
                  inductive DescriptiveComplexity.SlotVal (c : ℕ) :
                  Type

                  Where an output slot's value comes from: a slot of the input, one of the two designated elements, or the next element after a slot of the input – which is what a loop variable being advanced needs, and the only source that reads the order.

                  • copy {c : ℕ} : Fin c → SlotVal c

                    Copy this coordinate of the input.

                  • bot {c : ℕ} : SlotVal c

                    The clear element.

                  • top {c : ℕ} : SlotVal c

                    The set element.

                  • succ {c : ℕ} : Fin c → SlotVal c

                    The element after this coordinate of the input.

                  Instances For
                    Dependency graph
                    source
                    @[instance_reducible]
                    instance DescriptiveComplexity.instDecidableEqSlotVal {c✝ : ℕ} :
                    DecidableEq (SlotVal c✝)
                    Equations
                    Dependency graph
                    source
                    def DescriptiveComplexity.instDecidableEqSlotVal.decEq {c✝ : ℕ} (x✝ x✝¹ : SlotVal c✝) :
                    Decidable (x✝ = x✝¹)
                    Equations
                    Instances For
                      Dependency graph
                      source
                      noncomputable def DescriptiveComplexity.SlotVal.eval {A : Type} {c : ℕ} [LinearOrder A] (bot top : A) (w : Fin c → A) :
                      SlotVal c → A

                      What a source names, at a tuple.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        noncomputable def DescriptiveComplexity.slotValF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (u : Fin c → γ) (y : γ) :
                        SlotVal c → (L.sum FirstOrder.Language.order).Formula γ

                        A slot's source, as a formula: the target variable is that coordinate of the input, or a minimum, or a maximum.

                        Equations
                        Instances For
                          Dependency graph
                          source
                          noncomputable def DescriptiveComplexity.writeTupF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (G : EqPat c → Fin c → SlotVal c) (u y : Fin c → γ) :
                          (L.sum FirstOrder.Language.order).Formula γ

                          A tuple written slot by slot from another, as a formula: for the pattern the input has, each output coordinate is what that pattern's source names. A disjunction over the patterns, as everything here is.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Dependency graph
                            source
                            theorem DescriptiveComplexity.realize_patSetF_of_factors {L : FirstOrder.Language} {γ : Type} {c : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {bot top : A} (hb : IsBot bot) (ht : IsTop top) {P : (Fin c → A) → Prop} {Q : EqPat c → Prop} (hP : ∀ (w : Fin c → A), P w ↔ Q (patOf bot top w)) (x : Fin c → γ) :
                            (patSetF Q x).Realize v ↔ P fun (i : Fin c) => v (x i)

                            A predicate that reads its data only through the equality pattern is first-order definable, by one formula for every structure – which is what an interpretation needs, since it carries one formula for all of them. This is what a transition table's guard has to offer, and what a program assembled out of parameterized kits can afford to offer: a Prop about the attribute where it is defined, rather than syntax threaded through every abstraction.

                            Dependency graph