Documentation

Provenance.Circuit

Boolean circuits, read-once and d-D correctness #

This file formalises Boolean circuits over a set X of variables, together with two recursive bottom-up probability evaluators and their correctness theorems:

These are the formal counterpart of Section V-D step 1 of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data: on a read-once Boolean circuit each gate's probability is computed in O(1) from those of its two children, and on a decomposable-deterministic circuit (d-D, the structural property targeted by knowledge compilers) the same is true with simpler OR formula.

Main definitions #

Main results #

References #

source
inductive Circuit (X : Type) :
Type

Boolean circuit over a set X of variables.

Instances For
    source
    @[implicit_reducible]
    instance instReprCircuit {X✝ : Type} [Repr X✝] :
    Repr (Circuit X✝)
    Equations
    source
    def instReprCircuit.repr {X✝ : Type} [Repr X✝] :
    Circuit X✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Circuit.eval {X : Type} :
      Circuit X → (X → Bool) → Bool

      Evaluate a circuit under a Boolean valuation.

      Equations
      Instances For
        source
        def Circuit.toBoolFunc {X : Type} (c : Circuit X) :
        BoolFunc X

        A circuit's denotation as a BoolFunc.

        Equations
        Instances For
          source
          def Circuit.vars {X : Type} [DecidableEq X] :
          Circuit X → Finset X

          The variables used by a circuit, as a Finset.

          Equations
          Instances For
            source
            inductive Circuit.ReadOnce {X : Type} [DecidableEq X] :
            Circuit X → Prop

            A circuit is read-once when each gate's two children have disjoint variable supports. Constants and variables are read-once by definition; NOT is read-once if its argument is.

            Instances For
              source
              def Circuit.prob {X : Type} (P : ProbAssignment X) :
              Circuit X → ℚ

              The recursive bottom-up probability evaluator. Each gate combines the probabilities of its children in O(1), with the formula depending on the gate type.

              Equations
              Instances For
                source
                inductive Circuit.Decomposable {X : Type} [DecidableEq X] :
                Circuit X → Prop

                A circuit is decomposable when every AND gate has children with disjoint variable supports. Constants, variables, NOT, and OR are decomposable as soon as their immediate children (if any) are.

                Instances For
                  source
                  inductive Circuit.Deterministic {X : Type} :
                  Circuit X → Prop

                  A circuit is deterministic when every OR gate has mutually exclusive children: the conjunction of their BoolFunc denotations is the constant false. Constants, variables, NOT, and AND are deterministic as soon as their immediate children (if any) are. NOTE: there is no NNF restriction; not is treated semantically (Pr(¬c) = 1 - Pr(c) always).

                  Instances For
                    source
                    def Circuit.probDD {X : Type} (P : ProbAssignment X) :
                    Circuit X → ℚ

                    The d-D bottom-up probability evaluator. Differs from Circuit.prob only at OR gates, which sum the two children's probabilities directly (no inclusion-exclusion correction term). Sound on Decomposable + Deterministic circuits: see Circuit.dD_funcProb_eq_probDD.

                    Equations
                    Instances For

                      BoolFunc.DependsOn: support of a Boolean function #

                      source
                      def BoolFunc.DependsOn {X : Type} (f : BoolFunc X) (S : Finset X) :
                      Prop

                      f depends only on the variables in S: any two valuations agreeing on S produce the same value. This is the standard notion of "support".

                      Equations
                      • f.DependsOn S = ∀ (v₁ v₂ : X → Bool), (∀ x ∈ S, v₁ x = v₂ x) → f v₁ = f v₂
                      Instances For

                        Auxiliary funcProb lemmas #

                        These bridge the recursive evaluator Circuit.prob to the sum-over-valuations semantics ProbAssignment.funcProb. They are stated for arbitrary BoolFunc X, not specifically for circuit denotations, so that Circuit.readOnce_funcProb_eq_prob can be obtained by case analysis on the ReadOnce derivation.

                        source
                        theorem ProbAssignment.funcProb_var {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) (i : X) :
                        P.funcProb (BoolFunc.var i) = P.prob i

                        Pr(var i) = Pr(i): the probability of the single-variable Boolean function equals the variable's own probability. Proved by reorganising the sum ∑_v if v i then valProb v else 0 as a product ∏_y h_y(v y) and applying Fintype.prod_sum (the same swap used in sum_valProb_eq_one).

                        source
                        theorem ProbAssignment.funcProb_sub_self_const_one {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) (f : BoolFunc X) :
                        P.funcProb (1 - f) = 1 - P.funcProb f

                        Pr(¬f) = 1 - Pr(f): probability of a Boolean complement. In BoolFunc X, 1 - f is pointwise f v && !(f v)-style Boolean subtraction, which on the constant-true 1 reduces to Bool.not ∘ f. The proof splits each summand by f v and uses sum_valProb_eq_one.

                        Independence lemma #

                        The independence lemma funcProb_mul_disjoint is the technical heart of the read-once correctness theorem: Pr(f * g) = Pr(f) * Pr(g) whenever f and g depend on disjoint variable supports. The proof splits each valuation v : X → Bool into its restrictions on S and Sᶜ via Equiv.piEquivPiSubtypeProd, factors the valuation probability over the partition, and uses the marginalisation ∑_b (P̃_x b) = 1 to discard the unused half on each of the two factors.

                        source
                        theorem ProbAssignment.funcProb_mul_disjoint {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) {f g : BoolFunc X} {S T : Finset X} (hf : f.DependsOn S) (hg : g.DependsOn T) (hST : Disjoint S T) :
                        P.funcProb (f * g) = P.funcProb f * P.funcProb g

                        Independence lemma. If f, g : BoolFunc X depend on disjoint variable supports S, T, then Pr(f * g) = Pr(f) * Pr(g).

                        The proof splits each valuation v : X → Bool into (v|S, v|Sᶜ) via Equiv.piEquivPiSubtypeProd, factors valProb v as the product of the two restricted products, and uses the marginalisations ∑_{vS} (∏_{x ∈ S} P̃_x(vS x)) = 1 and ∑_{vR} (∏_{x ∉ S} P̃_x(vR x)) = 1 (both proved via Fintype.prod_sum and sum_factor_at) to collapse the unused half on each side.

                        source
                        theorem ProbAssignment.funcProb_add_eq {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) (f g : BoolFunc X) :
                        P.funcProb (f + g) = P.funcProb f + P.funcProb g - P.funcProb (f * g)

                        Pr(f + g) = Pr(f) + Pr(g) - Pr(f * g): the universal inclusion-exclusion identity for the BoolFunc disjunction (+) and conjunction (*). No disjointness hypothesis is needed; the formula holds pointwise on each summand via the Bool identity (b₁ || b₂).toℚ = b₁.toℚ + b₂.toℚ - (b₁ && b₂).toℚ.

                        source
                        theorem Circuit.toBoolFunc_dependsOn_vars {X : Type} [DecidableEq X] (c : Circuit X) :
                        c.toBoolFunc.DependsOn c.vars

                        A circuit's denotation depends only on its variables.

                        Read-once correctness #

                        source
                        theorem Circuit.readOnce_funcProb_eq_prob {X : Type} [Fintype X] [DecidableEq X] {P : ProbAssignment X} (c : Circuit X) (hc : c.ReadOnce) :
                        P.funcProb c.toBoolFunc = prob P c

                        Read-once correctness theorem. For any read-once Boolean circuit c, the recursive bottom-up probability evaluator c.prob P agrees with the sum-over-valuations semantics Pr(c.toBoolFunc). Proved by induction on the ReadOnce derivation, using:

                        d-D correctness #

                        source
                        theorem Circuit.dD_funcProb_eq_probDD {X : Type} [Fintype X] [DecidableEq X] {P : ProbAssignment X} (c : Circuit X) (hd : c.Decomposable) (hdet : c.Deterministic) :
                        P.funcProb c.toBoolFunc = probDD P c

                        d-D correctness theorem. For any decomposable + deterministic Boolean circuit c, the recursive bottom-up evaluator c.probDD P agrees with the sum-over-valuations semantics Pr(c.toBoolFunc). Proved by structural induction on c, using: