Documentation

Complexity.Computability.Circuit.Boolean.DepthTime

Computing the depths of a Boolean circuit #

The ordinary code evaluator, interpreted over depths with unit gate cost, computes one depth for every input and gate. Missing arguments and unavailable wires read zero, so the computation is total even on malformed code. Each gate increases the largest available depth by at most one; the bounds below therefore require no well-formedness premise.

The circuit depth takes the maximum only over the designated outputs. Unused gates, including ones deeper than every output, do not change it. Native polynomial-time certificates, with binary wire indices and unary computed depths, are in Boolean.DepthTime.PolyTime.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.wireDepthsCode (inputCount : ℕ) (gates : List (Op × List ℕ)) :
List ℕ

Compute every wire depth, with inputs first and gates in program order. A missing argument or unavailable wire has depth zero. Every gate, including a constant, has unit cost.

Instances For
    source
    def Cslib.Circuits.Boolean.depthCode (inputCount : ℕ) (code : List (Op × List ℕ) × List ℕ) :
    ℕ

    The maximum depth of a designated output, with maximum zero for no outputs.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.length_wireDepthsCode (inputCount : ℕ) (gates : List (Op × List ℕ)) :
      (wireDepthsCode inputCount gates).length = inputCount + gates.length

      The table has one entry for each input and gate.

      source
      theorem Cslib.Circuits.Boolean.wireDepthsCode_code {n g : ℕ} (p : Program signature n g) :
      wireDepthsCode n p.code = List.replicate n 0 ++ List.ofFn p.depths

      The raw table of a typed program lists its zero input depths and then its gate depths.

      source
      theorem Cslib.Circuits.Boolean.wireDepthsCode_getD_toNat {n g : ℕ} (p : Program signature n g) (w : Wire n g) :
      (wireDepthsCode n p.code).getD w.toNat 0 = p.wireDepths w

      Looking up a typed wire in the raw table gives its program depth.

      source
      theorem Cslib.Circuits.Boolean.depthCode_code {n m : ℕ} (c : Circuit signature n m) :
      depthCode n c.code = c.depth

      Taking the maximum over exactly the designated outputs computes Circuit.depth.

      source
      theorem Cslib.Circuits.Boolean.wireDepthsCode_le (inputCount : ℕ) (gates : List (Op × List ℕ)) (value : ℕ) :
      value ∈ wireDepthsCode inputCount gates → value ≤ gates.length

      Every computed depth is at most the number of gates. No well-formedness is required.

      source
      theorem Cslib.Circuits.Boolean.getD_wireDepthsCode_le (inputCount : ℕ) (gates : List (Op × List ℕ)) (i : ℕ) :
      (wireDepthsCode inputCount gates).getD i 0 ≤ gates.length

      The depth returned by any raw table lookup is bounded, including an unavailable wire.

      source
      theorem Cslib.Circuits.Boolean.depthCode_le (inputCount : ℕ) (code : List (Op × List ℕ) × List ℕ) :
      depthCode inputCount code ≤ code.1.length

      Even malformed output references cannot make the selected depth exceed the gate count.