Documentation

DescriptiveComplexity.Problems.FinSat.Nodes

Positions and tags of the FINSAT reduction #

The combinatorial skeleton of the RE-hardness reduction: what the elements of the encoded sentence are, and in what order they come. The reduction itself (the defining formulas) and its correctness live in the sibling files; nothing here mentions DescriptiveComplexity.FINSAT.

Positions #

The kernel φ of an ∃SO[new] definition is traversed by the subformula positions of DescriptiveComplexity.Tseitin.NodeAt, reused verbatim from the Cook–Levin reduction – as is the whole semantic layer of DescriptiveComplexity.Problems.Sat.Tseitin, whose DescriptiveComplexity.Tseitin.Gates is exactly the recursion the encoded sentence has to compute. What that layer does not carry, and this file adds, is a size: DescriptiveComplexity.FinSat.nodeSize, the size of the subformula at a position, which is what makes the parse DAG of the image descend along the order of the syntax (DescriptiveComplexity.FinSat.IsWF.child_lt).

Tags #

DescriptiveComplexity.FinSat.Tag is the tag type of the interpretation. Its elements are of three kinds:

The order. Well-formedness of the image demands a linear order in which every child comes strictly earlier, so the tags are ranked (DescriptiveComplexity.FinSat.tagRank) by the layer they sit in – leaves lowest, the prefix highest, the translated kernel ordered by the size of its subformula – and ties are broken by an arbitrary enumeration of the (finite) tag type. The resulting key DescriptiveComplexity.FinSat.tagKey is injective, so the reduction may compare two tags by trichotomy and emit ⊤, ⊥ or a comparison of the tuples. That last comparison, DescriptiveComplexity.FinSat.lexLtF / DescriptiveComplexity.FinSat.lexLeF, is the one order guard DescriptiveComplexity.OrderWalk does not carry: it walks the lexicographic order (succTupF) where a reduction defining the order of its image has to decide it. It is written here rather than there only so that this work in progress adds files instead of changing one the whole library depends on; it belongs next to succTupF.

The size of a subformula #

source
def DescriptiveComplexity.FinSat.fmlSize {L' : FirstOrder.Language} {n : ℕ} :
L'.BoundedFormula Empty n → ℕ

The size of a formula: one for each of its nodes.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.FinSat.fmlSize_pos {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) :
    0 < fmlSize f
    Dependency graph
    source
    def DescriptiveComplexity.FinSat.nodeSize {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) {m : ℕ} :
    Tseitin.NodeAt f m → ℕ

    The size of the subformula at a position. It is what the order of the syntax of the image is built from: a child position carries a strictly smaller subformula.

    Equations
    Instances For
      Dependency graph
      source
      @[simp]
      theorem DescriptiveComplexity.FinSat.nodeSize_rootAt {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) :
      nodeSize f (Tseitin.rootAt f) = fmlSize f
      Dependency graph
      source
      theorem DescriptiveComplexity.FinSat.nodeSize_le {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) {m : ℕ} (p : Tseitin.NodeAt f m) :
      nodeSize f p ≤ fmlSize f

      Every position of a formula carries a subformula no larger than it.

      Dependency graph

      The three descent facts the image needs: at an implication every position of either side is smaller than the implication itself, and at a quantifier so is every position of the body.

      source
      theorem DescriptiveComplexity.FinSat.nodeSize_imp_left {L' : FirstOrder.Language} {n : ℕ} (f₁ f₂ : L'.BoundedFormula Empty n) {m : ℕ} (q : Tseitin.NodeAt f₁ m) :
      nodeSize (f₁.imp f₂) (Sum.inr (Sum.inl q)) < nodeSize (f₁.imp f₂) (Sum.inl { down := ⋯ })
      Dependency graph
      source
      theorem DescriptiveComplexity.FinSat.nodeSize_imp_right {L' : FirstOrder.Language} {n : ℕ} (f₁ f₂ : L'.BoundedFormula Empty n) {m : ℕ} (q : Tseitin.NodeAt f₂ m) :
      nodeSize (f₁.imp f₂) (Sum.inr (Sum.inr q)) < nodeSize (f₁.imp f₂) (Sum.inl { down := ⋯ })
      Dependency graph
      source
      theorem DescriptiveComplexity.FinSat.nodeSize_all_body {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty (n + 1)) {m : ℕ} (q : Tseitin.NodeAt f m) :
      nodeSize f.all (Sum.inr q) < nodeSize f.all (Sum.inl { down := ⋯ })
      Dependency graph

      The arity of the atoms #

      source
      def DescriptiveComplexity.FinSat.maxArity {L' : FirstOrder.Language} {n : ℕ} :
      L'.BoundedFormula Empty n → ℕ

      A bound on the arities of the relation symbols occurring in a formula: the dimension of the reduction must be large enough to hold one element per argument of an atom of the instance's vocabulary.

      Equations
      Instances For
        Dependency graph

        Comparing two tuples lexicographically #

        source
        noncomputable def DescriptiveComplexity.FinSat.lexLtF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel sel' : Fin D → γ) :
        (L.sum FirstOrder.Language.order).Formula γ

        The tuple held by sel is lexicographically strictly below the one held by sel': the two agree before some coordinate, at which the first is strictly smaller.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.FinSat.lexLeF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel sel' : Fin D → γ) :
          (L.sum FirstOrder.Language.order).Formula γ

          The tuple held by sel is lexicographically below or equal to the one held by sel'.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.FinSat.realize_lexLtF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) :
            (lexLtF sel sel').Realize v ↔ toLex (v ∘ sel) < toLex (v ∘ sel')
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.FinSat.realize_lexLeF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) :
            (lexLeF sel sel').Realize v ↔ toLex (v ∘ sel) ≤ toLex (v ∘ sel')
            Dependency graph
            source
            theorem DescriptiveComplexity.FinSat.lexLeF_total {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) :
            (lexLeF sel sel').Realize v ∨ (lexLeF sel' sel).Realize v

            The comparison is total, so a reduction may define the order of its image by emitting DescriptiveComplexity.FinSat.lexLeF at equal tags.

            Dependency graph

            The tags #

            source
            inductive DescriptiveComplexity.FinSat.Tag (P ι : Type) (c d : ℕ) :
            Type

            The tags of the FINSAT reduction. See the module docstring for what each of them stands for; P is the type of subformula positions of the kernel, ι the index type of the second-order block, c the number of de Bruijn levels and d the dimension.

            • body {P ι : Type} {c d : ℕ} : Tag P ι c d

              The top conjunction: the diagram of the instance and the translated kernel.

            • pre {P ι : Type} {c d : ℕ} : Tag P ι c d

              An existential of the prefix, one per element of the instance; the tuple holds that element.

            • pvar {P ι : Type} {c d : ℕ} : Tag P ι c d

              The variable that existential binds, one per element of the instance.

            • neq {P ι : Type} {c d : ℕ} : Tag P ι c d

              A distinctness literal x_a ≠ x_b of the diagram; the tuple holds the pair.

            • dbvar {P ι : Type} {c d : ℕ} (l : Fin c) : Tag P ι c d

              The variable naming one de Bruijn level of the kernel.

            • sym {P ι : Type} {c d : ℕ} (i : ι) : Tag P ι c d

              A relation symbol of the encoded sentence: one per relation variable of the block.

            • apos {P ι : Type} {c d : ℕ} (j : Fin d) : Tag P ι c d

              An argument position of the relation symbols.

            • nd {P ι : Type} {c d : ℕ} (p : P) (pol : Bool) : Tag P ι c d

              The translation of the subformula at a position, at a polarity.

            • atup {P ι : Type} {c d : ℕ} (p : P) (pol : Bool) : Tag P ι c d

              One tuple of the translation of an atom of the instance's vocabulary (or of the marker old); the tuple holds the arguments.

            • alit {P ι : Type} {c d : ℕ} (p : P) (pol : Bool) (j : Fin d) : Tag P ι c d

              One equality literal inside such a tuple; the tuple holds the argument.

            Instances For
              Dependency graph
              source
              @[instance_reducible]
              instance DescriptiveComplexity.FinSat.instDecidableEqTag {P✝ ι✝ : Type} {c✝ d✝ : ℕ} [DecidableEq P✝] [DecidableEq ι✝] :
              DecidableEq (Tag P✝ ι✝ c✝ d✝)
              Equations
              Dependency graph
              source
              def DescriptiveComplexity.FinSat.instDecidableEqTag.decEq {P✝ ι✝ : Type} {c✝ d✝ : ℕ} [DecidableEq P✝] [DecidableEq ι✝] (x✝ x✝¹ : Tag P✝ ι✝ c✝ d✝) :
              Decidable (x✝ = x✝¹)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                def DescriptiveComplexity.FinSat.Tag.toSum {P ι : Type} {c d : ℕ} :
                Tag P ι c d → Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Fin c ⊕ ι ⊕ Fin d ⊕ P × Bool ⊕ P × Bool ⊕ P × Bool × Fin d

                The tags, mapped injectively into a sum of finite types: how they are seen to be finitely many.

                Equations
                Instances For
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.FinSat.Tag.toSum_injective {P ι : Type} {c d : ℕ} :
                  Function.Injective toSum
                  Dependency graph
                  source
                  instance DescriptiveComplexity.FinSat.Tag.instFinite {P ι : Type} {c d : ℕ} [Finite P] [Finite ι] :
                  Finite (Tag P ι c d)
                  Dependency graph
                  source
                  instance DescriptiveComplexity.FinSat.Tag.instNonempty {P ι : Type} {c d : ℕ} :
                  Nonempty (Tag P ι c d)
                  Dependency graph

                  The order of the syntax #

                  The parse DAG of the image has to descend along the order, so the tags are ranked by the layer they sit in. Children of a node always sit in a strictly lower layer, except among the translated kernel, where the layer is the size of the subformula – strictly decreasing from a position to its children by DescriptiveComplexity.FinSat.nodeSize_imp_left and its two companions.

                  source
                  def DescriptiveComplexity.FinSat.Tag.tagRank {P ι : Type} {c d : ℕ} (sz : P → ℕ) (S : ℕ) :
                  Tag P ι c d → ℕ

                  The layer of a tag, given the size sz of the subformula at a position and a bound S on it: the variables and symbols lowest, then the literals of an atom, the distinctness literals, the tuple nodes, the translated kernel by increasing subformula size, the top conjunction, and the prefix.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    noncomputable def DescriptiveComplexity.FinSat.Tag.enum {P ι : Type} {c d : ℕ} [Finite P] [Finite ι] :
                    Tag P ι c d ≃ Fin (Classical.choose ⋯)

                    An enumeration of the tags, used only to break ties between tags of the same layer: which of two such tags comes first is immaterial, since no two of them are ever parent and child.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      noncomputable def DescriptiveComplexity.FinSat.Tag.tagKey {P ι : Type} {c d : ℕ} [Finite P] [Finite ι] (sz : P → ℕ) (S : ℕ) (t : Tag P ι c d) :
                      Lex (ℕ × ℕ)

                      The sorting key of a tag: its layer, then its place in the enumeration.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        theorem DescriptiveComplexity.FinSat.Tag.tagKey_injective {P ι : Type} {c d : ℕ} [Finite P] [Finite ι] (sz : P → ℕ) (S : ℕ) :
                        Function.Injective (tagKey sz S)
                        Dependency graph
                        source
                        theorem DescriptiveComplexity.FinSat.Tag.tagKey_lt_of_rank_lt {P ι : Type} {c d : ℕ} [Finite P] [Finite ι] {sz : P → ℕ} {S : ℕ} {t t' : Tag P ι c d} (h : tagRank sz S t < tagRank sz S t') :
                        tagKey sz S t < tagKey sz S t'

                        A tag of a lower layer comes strictly earlier: this is what makes the parse DAG of the image descend along the order.

                        Dependency graph