Documentation

DescriptiveComplexity.Problems.Sat.TseitinFormulas

The Tseitin encoding of a first-order kernel: defining formulas #

First-order counterpart of DescriptiveComplexity.Problems.Sat.Tseitin: formulas over the ordered expansion L.sum Language.order defining, inside an input structure, the clauses of the Tseitin ([Tseitin 1968][tseitin1968complexity]) encoding of a kernel formula and their literals – DescriptiveComplexity.Tseitin.isClauseF mirroring DescriptiveComplexity.Tseitin.IsClauseSem and DescriptiveComplexity.Tseitin.litF mirroring DescriptiveComplexity.Tseitin.LitSem, with realization lemmas (DescriptiveComplexity.Tseitin.realize_isClauseF, DescriptiveComplexity.Tseitin.realize_litF).

All builders are parameterized by maps Fin D → γ selecting the free variables holding the clause and literal tuples, so that they can be instantiated at the variable types of the defining formulas of an interpretation (Fin 1 × Fin D, Fin 2 × Fin D). The order is used in a single place: the formula DescriptiveComplexity.Tseitin.botF expressing that a coordinate is a minimum, which pins down the canonical padding of tuples.

source
noncomputable def DescriptiveComplexity.Tseitin.tTerm {L : FirstOrder.Language} {γ : Type} {D : ℕ} {B : SOBlock} {m : ℕ} (h : m ≤ D) (t : (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
(L.sum FirstOrder.Language.order).Term γ

A term of the kernel, over the ordered expansion, its variables read from the coordinates selected by c.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def DescriptiveComplexity.Tseitin.termEqF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {B : SOBlock} {m : ℕ} (h : m ≤ D) (t₁ t₂ : (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
    (L.sum FirstOrder.Language.order).Formula γ

    The equality atom of the kernel, as a formula over the ordered expansion.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev DescriptiveComplexity.Tseitin.inRelSym {L : FirstOrder.Language} {l : ℕ} (r : L.Relations l) :
      (L.sum FirstOrder.Language.order).Relations l

      An input-relation symbol, in the ordered expansion.

      Equations
      Instances For
        source
        noncomputable def DescriptiveComplexity.Tseitin.relAtF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {B : SOBlock} {m l : ℕ} (h : m ≤ D) (r : L.Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
        (L.sum FirstOrder.Language.order).Formula γ

        An input-relation atom of the kernel, as a formula over the ordered expansion.

        Equations
        Instances For
          source
          noncomputable def DescriptiveComplexity.Tseitin.atomLitF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {B : SOBlock} {m l : ℕ} (h : m ≤ D) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (u x : Fin D → γ) :
          (L.sum FirstOrder.Language.order).Formula γ

          The tuple held by x is the canonically padded tuple of values of the terms of a block-variable atom, as a formula.

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

            Realization of the builders #

            source
            theorem DescriptiveComplexity.Tseitin.realize_tTerm {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {B : SOBlock} {m : ℕ} (h : m ≤ D) (t : (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
            FirstOrder.Language.Term.realize v (tTerm h t c) = FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) fun (j : Fin m) => v (c (Fin.castLE h j))) (termToL t)
            source
            theorem DescriptiveComplexity.Tseitin.realize_termEqF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {B : SOBlock} {m : ℕ} (h : m ≤ D) (t₁ t₂ : (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
            (termEqF h t₁ t₂ c).Realize v ↔ eqGuard t₁ t₂ fun (j : Fin m) => v (c (Fin.castLE h j))
            source
            theorem DescriptiveComplexity.Tseitin.realize_relAtF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {B : SOBlock} {m l : ℕ} (h : m ≤ D) (r : L.Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (c : Fin D → γ) :
            (relAtF h r ts c).Realize v ↔ relGuard r ts fun (j : Fin m) => v (c (Fin.castLE h j))
            source
            theorem DescriptiveComplexity.Tseitin.realize_atomLitF {L : FirstOrder.Language} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {B : SOBlock} {m l : ℕ} (h : m ≤ D) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (u x : Fin D → γ) :
            (atomLitF h ts u x).Realize v ↔ atomLit ts (fun (j : Fin m) => v (u (Fin.castLE h j))) fun (j : Fin D) => v (x j)

            The clause-existence formulas #

            source
            noncomputable def DescriptiveComplexity.Tseitin.isClauseF {L : FirstOrder.Language} {B : SOBlock} {γ : Type} {D n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) :
            maxCtx f ≤ D → {m : ℕ} → NodeAt f m → Fin 3 → (Fin D → γ) → (L.sum FirstOrder.Language.order).Formula γ

            The defining formula of clause existence, mirroring DescriptiveComplexity.Tseitin.IsClauseSem: the clause tuple is read from the coordinates selected by c.

            Equations
            Instances For
              source
              theorem DescriptiveComplexity.Tseitin.realize_isClauseF {L : FirstOrder.Language} {B : SOBlock} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (hctx : maxCtx f ≤ D) {m : ℕ} (p : NodeAt f m) (k : Fin 3) (c : Fin D → γ) :
              (isClauseF f hctx p k c).Realize v ↔ IsClauseSem f hctx p k fun (j : Fin D) => v (c j)

              Realization of the clause-existence formulas.

              The literal formulas #

              source
              noncomputable def DescriptiveComplexity.Tseitin.litF {L : FirstOrder.Language} {B : SOBlock} {γ : Type} {D : ℕ} (s : Bool) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) :
              maxCtx f ≤ D → {m : ℕ} → NodeAt f m → Fin 3 → B.ι ⊕ (m' : ℕ) × NodeAt f m' → (Fin D → γ) → (Fin D → γ) → (L.sum FirstOrder.Language.order).Formula γ

              The defining formula of literal occurrence with sign s, mirroring DescriptiveComplexity.Tseitin.LitSem: the clause tuple is read from the coordinates selected by u, the literal tuple from those selected by x. Root positions of subformulas are recognized by DescriptiveComplexity.Tseitin.isRootB.

              Equations
              Instances For
                source
                theorem DescriptiveComplexity.Tseitin.realize_litF {L : FirstOrder.Language} {B : SOBlock} {γ : Type} {D : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (s : Bool) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (hctx : maxCtx f ≤ D) {m : ℕ} (p : NodeAt f m) (k : Fin 3) (vt : B.ι ⊕ (m' : ℕ) × NodeAt f m') (u x : Fin D → γ) :
                (litF s f hctx p k vt u x).Realize v ↔ LitSem s f hctx p k (fun (j : Fin D) => v (u j)) vt fun (j : Fin D) => v (x j)

                Realization of the literal formulas.