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.Tag.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.Tag.tagKey is injective, so the reduction may compare two tags by trichotomy and emit ⊤, ⊥ or a comparison of the tuples. That last comparison is DescriptiveComplexity.lexSelLeF, which lives in DescriptiveComplexity.OrderWalk next to succTupF: the guard walks the lexicographic order where a reduction defining the order of its image has to decide it.

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
    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

        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
          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
            @[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.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