Documentation

DescriptiveComplexity.Problems.Cvp.Defs

The circuit value problem: definition #

CVP asks whether a Boolean circuit, given with the values of its input gates, evaluates its designated output gate to true. It is the canonical PTIME-complete problem of the textbooks (Ladner 1975), and the natural companion of HORN-SAT one level below Cook–Levin: where HORN-SAT is the syntactic image of the Horn fragment, CVP is the syntactic image of evaluation.

The vocabulary #

FirstOrder.Language.circuit marks each element with its kind – a constant input (circIsTrue, circIsFalse), a gate (circIsAnd, circIsOr, circIsNot), the output (circOut) – and wires gates to their arguments with two binary relations circLeft and circRight, a negation using circLeft alone. Fan-in is therefore two, as in the standard statement; unbounded fan-in would put an iterated conjunction in the semantics, where this library prefers to keep it in a reduction that walks an order.

The semantics, and why nothing is assumed about the instance #

The value of a gate is defined by the least dual-rail derivation (DescriptiveComplexity.GateVal, one inductive family indexed by the value being derived): GateVal true g and GateVal false g say that the value 1, respectively 0, is derivable at g from the constant inputs by the gate rules. A yes-instance is one whose output gate derives true (DescriptiveComplexity.CircuitAccepts).

Three degeneracies are then harmless, and none needs a well-formedness hypothesis:

On a well-formed acyclic circuit the derivable value is the value, which is all the reduction of DescriptiveComplexity.Problems.Cvp.Hardness needs, since the circuit it builds is well-formed and acyclic by construction.

Folding no condition into the yes-instances is the same choice as for 3SAT's width bound and HORN-SAT's Horn condition made in reverse, and for the same reason: it keeps CVP a decision problem on arbitrary Language.circuit structures, so that it lives in the same catalog and composes with the same reductions.

source
@[reducible, inline]
abbrev FirstOrder.Language.circIsTrue :
Language.circuit.Relations 1

isTrue g: the element g is a constant input gate holding 1.

Equations
Instances For
    Dependency graph
    source
    @[reducible, inline]
    abbrev FirstOrder.Language.circIsNot :
    Language.circuit.Relations 1

    isNot g: the element g is a negation gate, its argument read off left.

    Equations
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance FirstOrder.Language.instDecidableEqCircuitRel {a✝ : ℕ} :
      DecidableEq (circuitRel a✝)
      Equations
      Dependency graph
      source
      def FirstOrder.Language.circuit :
      Language

      The relational language of Boolean circuits: one unary predicate per gate kind, one marking the output, and two binary predicates wiring a gate to its arguments.

      Equations
      Instances For
        Dependency graph
        source
        @[reducible, inline]
        abbrev FirstOrder.Language.circLeft :
        Language.circuit.Relations 2

        left g x: the gate g takes x as its first argument.

        Equations
        Instances For
          Dependency graph
          source
          inductive FirstOrder.Language.circuitRel :
          ℕ → Type

          The relation symbols of the language.

          Instances For
            Dependency graph
            source
            def FirstOrder.Language.instDecidableEqCircuitRel.decEq {a✝ : ℕ} (x✝ x✝¹ : circuitRel a✝) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              Dependency graph
              source
              @[reducible, inline]
              abbrev FirstOrder.Language.circIsFalse :
              Language.circuit.Relations 1

              isFalse g: the element g is a constant input gate holding 0.

              Equations
              Instances For
                Dependency graph
                source
                instance FirstOrder.Language.instIsRelationalCircuit :
                Language.circuit.IsRelational
                Dependency graph
                source
                @[reducible, inline]
                abbrev FirstOrder.Language.circIsAnd :
                Language.circuit.Relations 1

                isAnd g: the element g is a conjunction gate.

                Equations
                Instances For
                  Dependency graph
                  source
                  @[reducible, inline]
                  abbrev FirstOrder.Language.circOut :
                  Language.circuit.Relations 1

                  out g: the element g is an output gate.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    @[reducible, inline]
                    abbrev FirstOrder.Language.circIsOr :
                    Language.circuit.Relations 1

                    isOr g: the element g is a disjunction gate.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      @[reducible, inline]
                      abbrev FirstOrder.Language.circRight :
                      Language.circuit.Relations 2

                      right g x: the gate g takes x as its second argument.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        inductive DescriptiveComplexity.GateVal {A : Type} [FirstOrder.Language.circuit.Structure A] :
                        Bool → A → Prop

                        The value derivable at a gate, as one inductive family indexed by the value being derived: GateVal true g says that g evaluates to 1, GateVal false g that it evaluates to 0. Being an inductive predicate, it is the least pair of rails closed under the gate rules, so a gate whose arguments derive nothing – including one on a cycle – derives nothing.

                        The rules are the usual ones read in both polarities: a conjunction is true when both arguments are, false as soon as one is; a disjunction dually; a negation swaps the rails.

                        Instances For
                          Dependency graph
                          source
                          def DescriptiveComplexity.CircuitAccepts (A : Type) [FirstOrder.Language.circuit.Structure A] :
                          Prop

                          A Language.circuit-structure is a yes-instance when some output gate derives the value 1.

                          Equations
                          Instances For
                            Dependency graph

                            Isomorphism-invariance and the bundled problem #

                            source
                            theorem DescriptiveComplexity.circuitAccepts_iso {A B : Type} [FirstOrder.Language.circuit.Structure A] [FirstOrder.Language.circuit.Structure B] (e : FirstOrder.Language.circuit.Equiv A B) :
                            CircuitAccepts A ↔ CircuitAccepts B

                            Acceptance is isomorphism-invariant.

                            Dependency graph
                            source
                            def DescriptiveComplexity.CVP :
                            DecisionProblem FirstOrder.Language.circuit

                            CVP, the circuit value problem, as a problem on Language.circuit-structures: does the output gate derive the value 1?

                            Equations
                            Instances For
                              Dependency graph