Documentation

DescriptiveComplexity.Problems.Machine.HornInterp

The transcription: HORNSAT ≤ᶠᵒ[≤] DTMAccept #

The first-order half of stage 4 of the machine bridge: the defining formulas of an interpretation of Language.turing in ordered CNF instances describing the unit-propagation machine of DescriptiveComplexity.Problems.Machine.HornHardness, shown to realize exactly its predicates, and bundled as the ordered reduction DescriptiveComplexity.HornTM.hornSat_ordered_fo_reduction_dtmAccept.

The method is stage 3's (DescriptiveComplexity.Problems.Machine.Interp), one dimension up: three shape helpers – cstHF, oneHF, twoHF – for the three payload shapes of the machine's elements, each with one realization lemma taking the valuation abstractly, so that every defining formula matches on its first tag only and every characterization case discharges by rfl. The two relational destinations (tMarkEndRound/tMarkEndVer dispatch to the lowest clause, which is not in their payload) get bespoke min-clause-pinned helpers. The clause-order formulas (minClF, maxClF, nextClF, noClF) are reused from stage 3 unchanged; the element-order ones (minF, maxF, succF) come from DescriptiveComplexity.OrderWalk, with a small bridge from succF's between-form to DescriptiveComplexity.SuccElt.

Formula pieces #

source
noncomputable def DescriptiveComplexity.HornTM.succEltF {α : Type} (x y : α) :
SatOcc.satOrd.Formula α

b is the successor of a among the elements, as a formula: succF's between-form.

Equations
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.HornTM.hornF {α : Type} :
    SatOcc.satOrd.Formula α

    The instance is Horn – at most one positive literal per clause – as a sentence-shaped formula: the accept gate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      noncomputable def DescriptiveComplexity.HornTM.mLitF (b : Bool) :
      SatOcc.satOrd.Formula (Fin 2 × Fin 3)

      The literal test of the verification phase, for the statically known mark b.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.HornTM.realize_succEltF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x y : α} {a b : A} (hx : v x = a) (hy : v y = b) :
        (succEltF x y).Realize v ↔ SuccElt a b
        Dependency graph
        source
        theorem DescriptiveComplexity.HornTM.realize_hornF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} :
        hornF.Realize v ↔ AtMostOnePositive A
        Dependency graph
        source
        theorem DescriptiveComplexity.HornTM.realize_mLitF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {b : Bool} {c x : A} {v : Fin 2 × Fin 3 → A} (h0 : v (0, 0) = c) (h1 : v (0, 1) = x) :
        (mLitF b).Realize v ↔ MLit c x b
        Dependency graph

        The three shapes, as formulas #

        source
        noncomputable def DescriptiveComplexity.HornTM.cstHF (s t' : UPTag) :
        SatOcc.satOrd.Formula (Fin 2 × Fin 3)

        The second argument is the constant cstH s.

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.HornTM.oneHF (s : UPTag) (x : Fin 2 × Fin 3) (t' : UPTag) :
          SatOcc.satOrd.Formula (Fin 2 × Fin 3)

          The second argument is oneH s (v x).

          Equations
          Instances For
            Dependency graph
            source
            noncomputable def DescriptiveComplexity.HornTM.twoHF (s : UPTag) (x y : Fin 2 × Fin 3) (t' : UPTag) :
            SatOcc.satOrd.Formula (Fin 2 × Fin 3)

            The second argument is twoH s (v x) (v y).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.HornTM.roundDstF (x : Fin 2 × Fin 3) (t' : UPTag) :
              SatOcc.satOrd.Formula (Fin 2 × Fin 3)

              The second argument is a check state of the round held by x and the lowest clause: the destination of a round turn.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                noncomputable def DescriptiveComplexity.HornTM.verDstF (t' : UPTag) :
                SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                The second argument is the initial verification state of the lowest clause: the destination of the turn into verification.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HornTM.realize_cstHF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 3 → A} {s : UPTag} {q : HV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) (h2 : v (1, 2) = q.2 2) :
                  (cstHF s q.1).Realize v ↔ q = cstH s
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HornTM.realize_oneHF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 3 → A} {s : UPTag} {x : Fin 2 × Fin 3} {q : HV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) (h2 : v (1, 2) = q.2 2) :
                  (oneHF s x q.1).Realize v ↔ q = oneH s (v x)
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HornTM.realize_twoHF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 3 → A} {s : UPTag} {x y : Fin 2 × Fin 3} {q : HV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) (h2 : v (1, 2) = q.2 2) :
                  (twoHF s x y q.1).Realize v ↔ q = twoH s (v x) (v y)
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HornTM.realize_roundDstF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {x : Fin 2 × Fin 3} {q : HV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) (h2 : v (1, 2) = q.2 2) :
                  (roundDstF x q.1).Realize v ↔ q.1 = UPTag.qChk true ∧ q.2 0 = v x ∧ SatMinCl (q.2 1) ∧ ∀ (a : A), q.2 2 ≤ a
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HornTM.realize_verDstF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {q : HV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) (h2 : v (1, 2) = q.2 2) :
                  (verDstF q.1).Realize v ↔ q.1 = UPTag.qVer false true ∧ SatMinCl (q.2 0) ∧ (∀ (a : A), q.2 1 ≤ a) ∧ ∀ (a : A), q.2 2 ≤ a
                  Dependency graph

                  The defining formulas #

                  source
                  noncomputable def DescriptiveComplexity.HornTM.hPosnF :
                  UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                  Defining formula for posn.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    noncomputable def DescriptiveComplexity.HornTM.hTrF :
                    UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                    Defining formula for tr: the payload promises of HTr.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      noncomputable def DescriptiveComplexity.HornTM.hStartF :
                      UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                      Defining formula for start.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        noncomputable def DescriptiveComplexity.HornTM.hAccF :
                        UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                        Defining formula for acc.

                        Equations
                        Instances For
                          Dependency graph
                          source
                          noncomputable def DescriptiveComplexity.HornTM.hBlankF :
                          UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                          Defining formula for blank.

                          Equations
                          Instances For
                            Dependency graph
                            source
                            noncomputable def DescriptiveComplexity.HornTM.hRightF :
                            UPTag → SatOcc.satOrd.Formula (Fin 1 × Fin 3)

                            Defining formula for right.

                            Equations
                            Instances For
                              Dependency graph
                              source
                              noncomputable def DescriptiveComplexity.HornTM.hInpF :
                              UPTag → UPTag → SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                              Defining formula for inp.

                              Equations
                              Instances For
                                Dependency graph
                                source
                                noncomputable def DescriptiveComplexity.HornTM.hSrcF :
                                UPTag → UPTag → SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                                Defining formula for tsrc.

                                Equations
                                Instances For
                                  Dependency graph
                                  source
                                  noncomputable def DescriptiveComplexity.HornTM.hReadF :
                                  UPTag → UPTag → SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                                  Defining formula for tread.

                                  Equations
                                  Instances For
                                    Dependency graph
                                    source
                                    noncomputable def DescriptiveComplexity.HornTM.hDstF :
                                    UPTag → UPTag → SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                                    Defining formula for tdst.

                                    Equations
                                    Instances For
                                      Dependency graph
                                      source
                                      noncomputable def DescriptiveComplexity.HornTM.hWriteF :
                                      UPTag → UPTag → SatOcc.satOrd.Formula (Fin 2 × Fin 3)

                                      Defining formula for twrite.

                                      Equations
                                      Instances For
                                        Dependency graph
                                        source
                                        noncomputable def DescriptiveComplexity.HornTM.hornTuringInterp :
                                        FOInterpretation SatOcc.satOrd FirstOrder.Language.turing UPTag 3

                                        The interpretation of machine instances in ordered CNF instances, describing the unit-propagation machine.

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

                                          The realization lemmas #

                                          source
                                          def DescriptiveComplexity.HornTM.hornMapEquiv {A : Type} :
                                          HV A ≃ hornTuringInterp.Map A

                                          The identity equivalence between the tagged triples and the interpreted universe.

                                          Equations
                                          Instances For
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_posn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMPosn (hornMapEquiv p) ↔ HPosn p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_tr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMTr (hornMapEquiv p) ↔ HTr p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_start {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMStart (hornMapEquiv p) ↔ HStart p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_acc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMAcc (hornMapEquiv p) ↔ HAcc p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_blank {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMBlank (hornMapEquiv p) ↔ HBlank p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : HV A) :
                                            TMRight (hornMapEquiv p) ↔ HRight p
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p q : HV A) :
                                            TMLe (hornMapEquiv p) (hornMapEquiv q) ↔ tagTupleLe p q
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_inp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : HV A) :
                                            TMInp (hornMapEquiv p) (hornMapEquiv q) ↔ HInp p q
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_tsrc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : HV A) :
                                            TMSrc (hornMapEquiv p) (hornMapEquiv q) ↔ HSrc p q
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_tread {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : HV A) :
                                            TMRead (hornMapEquiv p) (hornMapEquiv q) ↔ HRead p q
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_twrite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : HV A) :
                                            TMWrite (hornMapEquiv p) (hornMapEquiv q) ↔ HWrite p q
                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.relMap_tdst {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : HV A) :
                                            TMDst (hornMapEquiv p) (hornMapEquiv q) ↔ HDst p q
                                            Dependency graph

                                            The machines agree, and the reduction #

                                            source
                                            theorem DescriptiveComplexity.HornTM.agree_hornMachine {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
                                            TMData.Agree hornMapEquiv (hornMachine A) (tmData (hornTuringInterp.Map A))

                                            The interpreted structure describes the unit-propagation machine.

                                            Dependency graph
                                            source
                                            theorem DescriptiveComplexity.HornTM.dtmAccept_map_iff_hornSatisfiable {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
                                            DTMAccept.Holds (hornTuringInterp.Map A) ↔ HornSatisfiable A

                                            Correctness of the interpretation: the interpreted structure is a yes-instance of deterministic machine acceptance exactly when the CNF instance is a yes-instance of HORN-SAT. Well-formedness and determinism hold unconditionally – they were proved for every image, Horn or not – and acceptance is DescriptiveComplexity.hornMachine_accepts_iff, transported along the agreement.

                                            Dependency graph
                                            source
                                            noncomputable def DescriptiveComplexity.HornTM.hornSat_ordered_fo_reduction_dtmAccept :
                                            OrderedFOReduction HORNSAT DTMAccept

                                            HORN-SAT reduces to deterministic machine acceptance: the ordered first-order reduction building the unit-propagation machine inside the instance.

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