Documentation

Complexitylib.Circuits.Internal.AndOrNot

Internal: AND/OR/NOT Completeness Proof #

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

source
def Complexity.AONIndicator {N : ℕ} [NeZero N] (s : BitString N) :
Circuit Basis.unboundedAndOr 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 Complexity.andOrNotFor {N : ℕ} [NeZero N] (f : BitString N → Bool) :
    Circuit Basis.unboundedAndOr 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 andOrNotFor correctness #

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

      The single-output DNF circuit correctly computes f.

      Multi-output DNF circuit: andOrNotForM #

      source
      def Complexity.andOrNotForM {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) :
      Circuit Basis.unboundedAndOr 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 Complexity.andOrNotForM_eval {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) :
        (andOrNotForM f).eval = f

        The multi-output DNF circuit correctly computes f.

        source
        instance Complexity.instCompleteBasisUnboundedAndOr :
        CompleteBasis Basis.unboundedAndOr

        Basis.unboundedAndOr is functionally complete: every finite Boolean function f : BitString N → BitString M is computed by some circuit over it, witnessed by the DNF construction andOrNotForM.