Documentation

DescriptiveComplexity.Problems.Machine.HornTape

The tape of the unit-propagation machine #

The layout half of HORNSAT ≤ᶠᵒ[≤] DTMAccept, the deterministic machine bridge: which tagged tuples are positions, in what order, and why there are enough of them. The program that runs on this tape is in DescriptiveComplexity.Problems.Machine.HornHardness.

The layout #

As for the SAT machine: one cell per element of the instance, bracketed by two markers, followed by filler cells supplying time. The difference is the dimension: this machine does n propagation rounds of one check-and-mark pass per clause, O(n³) steps in all, so the interpreted universe is UPTag × A³ and sixteen filler tags give 16n³ positions.

A cell holds its element together with a mark – sU x unmarked, sM x marked – and the marked set is the machine's working copy of the unit propagation closure DescriptiveComplexity.Forced.

The program's tags #

All the machine's tags are declared here, as for the SAT machine: symbols, states and transitions get indices above the position tags, which leaves the order of the positions undisturbed. The states carry up to two elements – the current round and the current clause – which is what the third dimension of the payload accommodates.

The tags #

source
inductive DescriptiveComplexity.UPTag :
Type

The tags of the unit-propagation machine. Position tags first – their constructor order is the tape order – then symbols, states and transitions.

  • pStart : UPTag

    The left marker cell.

  • pCell : UPTag

    The cell of an element: one per element of the instance.

  • pEnd : UPTag

    The right marker cell.

  • pFill (i : Fin 16) : UPTag

    Filler cells, sixteen tags' worth, supplying the time budget.

  • sStart : UPTag

    The left-marker symbol ⊢.

  • sEnd : UPTag

    The right-marker symbol ⊣.

  • sBlank : UPTag

    The blank symbol.

  • sU : UPTag

    The symbol (x, unmarked).

  • sM : UPTag

    The symbol (x, marked).

  • qInit : UPTag

    The dispatch state, at the left marker.

  • qChk (f : Bool) : UPTag

    Checking the current clause, sweeping right: f says every negative literal seen so far is marked. Payload: the round and the clause.

  • qMark (m : Bool) : UPTag

    The return sweep of a clause: m says the check succeeded, so the positive literal is marked in passing. Payload: the round and the clause.

  • qVer (f d : Bool) : UPTag

    Verifying the clause of the payload against the final marks, flag f, sweeping in direction d.

  • qAcc : UPTag

    The accepting state.

  • tInitChk : UPTag

    Dispatch: a clause exists, start the first check sweep.

  • tInitAcc : UPTag

    Dispatch: no clause at all, accept.

  • tChk (m f : Bool) : UPTag

    Check sweep: read a cell with mark m under flag f.

  • tChkEnd (f : Bool) : UPTag

    Check sweep over: turn round at ⊣ into the return sweep.

  • tMark (m mk : Bool) : UPTag

    Return sweep: read a cell with mark m; if mk, mark the positive literal of the clause in passing.

  • tMarkEndNext (mk : Bool) : UPTag

    Return sweep over, another clause follows in this round.

  • tMarkEndRound (mk : Bool) : UPTag

    Return sweep over, last clause, another round follows.

  • tMarkEndVer (mk : Bool) : UPTag

    Return sweep over, last clause of the last round: verification begins.

  • tVer (m f d : Bool) : UPTag

    Verification sweep: read a cell with mark m under flag f, sweeping in direction d.

  • tVerNext (d : Bool) : UPTag

    Verified: the clause is satisfied and another one follows.

  • tVerAcc (d : Bool) : UPTag

    Verified: the last clause is satisfied, and the instance is Horn.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.instDecidableEqUPTag :
    DecidableEq UPTag
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.instDecidableEqUPTag.decEq (x✝ x✝¹ : UPTag) :
    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.instFintypeUPTag :
      Fintype UPTag
      Equations
      • One or more equations did not get rendered due to their size.
      Dependency graph
      source
      instance DescriptiveComplexity.instNonemptyUPTag :
      Nonempty UPTag
      Dependency graph
      source
      def DescriptiveComplexity.hTagIdx :
      UPTag → ℕ

      The position of a tag in the tape order.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.hTagIdx_injective :
        Function.Injective hTagIdx
        Dependency graph
        source
        @[instance_reducible]
        instance DescriptiveComplexity.instLinearOrderUPTag :
        LinearOrder UPTag

        The tape order on tags.

        Equations
        Dependency graph

        The intended positions #

        source
        def DescriptiveComplexity.IsMinTup3 {A : Type} [LinearOrder A] (w : Fin 3 → A) :
        Prop

        The tuple of minima at dimension three: what markers and constants are pinned to.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.HPosn {A : Type} [LinearOrder A] (p : UPTag × (Fin 3 → A)) :
          Prop

          The tagged tuples that are positions: the markers on the triple of minima, an element's cell that element with a minimal rest, the fillers unrestricted.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.HBlank {A : Type} [LinearOrder A] (p : UPTag × (Fin 3 → A)) :
            Prop

            The blank symbol of the machine: pinned to the triple of minima.

            Equations
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.hBlank_unique {A : Type} [LinearOrder A] {p q : UPTag × (Fin 3 → A)} (hp : HBlank p) (hq : HBlank q) :
              p = q
              Dependency graph
              source
              def DescriptiveComplexity.HInp {A : Type} [LinearOrder A] (p a : UPTag × (Fin 3 → A)) :
              Prop

              The initial tape: the markers hold their own symbols and the cell of an element holds that element, unmarked.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                theorem DescriptiveComplexity.isLinOrd_of_linearOrder {X : Type} (o : LinearOrder X) :
                IsLinOrd LE.le
                Dependency graph

                The budget #