Documentation

LeanPool.CircuitComplexity.Internal.AON

Internal: AND/OR/NOT Completeness Proof #

This internal module proves functional completeness of Basis.unboundedAON via DNF (disjunctive normal form) construction. The basis definitions are in Circ.AON.Defs; this module is re-exported through Circ.AON.

source
def CircuitComplexity.AONIndicator {N : ℕ} [NeZero N] (s : BitString N) :
Circuit Basis.unboundedAON N 1 0

Indicator circuit: outputs true iff the input equals s.

A single N-input AND gate where input i is wired to primary input i, negated when s i = false. No internal gates needed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CircuitComplexity.AONFor {N : ℕ} [NeZero N] (f : BitString N → Bool) :
    Circuit Basis.unboundedAON N 1 (2 ^ N)

    Single-output DNF circuit computing f : BitString N → Bool.

    For each of the 2^N possible inputs s, internal gate i is the indicator AND for s when f s = true, or a trivially-false 0-input OR otherwise. The single output OR gate disjoins all internal gates.

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

      Helper lemmas for AONFor correctness #

      source
      theorem CircuitComplexity.AONFor_is_Correct {N : ℕ} [NeZero N] (f : BitString N → Bool) :
      (fun (x : BitString 1) => x 0) ∘ (AONFor f).eval = f

      The single-output DNF circuit correctly computes f.

      Multi-output DNF circuit: AONForM #

      source
      def CircuitComplexity.AONForM {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) :
      Circuit Basis.unboundedAON N M (M * 2 ^ N)

      Multi-output DNF circuit computing f : BitString N → BitString M.

      For each output bit j and each of the 2^N possible inputs, there is an indicator AND gate (or a trivially-false gate). Each output OR gate disjoins the 2^N gates for its output bit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CircuitComplexity.AONForM_is_Correct {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) :
        (AONForM f).eval = f

        The multi-output DNF circuit correctly computes f.

        source
        instance CircuitComplexity.instCompleteBasisUnboundedAON :
        CompleteBasis Basis.unboundedAON