Monotone circuits constructing sets

The existing monotone signature acts on sets by intersection and union. Its constants denote the empty and full sets. Native Program and Circuit supply the syntax, evaluation and costs; the interpretation does not require decidable membership or a finite ambient type.

Mathlib's Boolean characteristic functions turn pointwise membership into an interpretation homomorphism. Constructing a tuple of sets is equivalent to computing its membership functions from those of the supplied sets, using exactly the same circuit. Thus arbitrary operation weights, sharing, unused gates and all designated outputs are preserved. The characteristic functions are noncomputable for arbitrary sets; this is a semantic correspondence.

Main definitions

• Cslib.Circuits.Monotone.setInterpretation: sets as an interpretation of the monotone basis.
• Cslib.Circuits.Monotone.membershipHomomorphism: pointwise Boolean membership.

Main results

• Cslib.Circuits.Monotone.eval_set_iff_computesFrom: set construction is pointwise computation.
• Cslib.Circuits.Monotone.eval_setOf_iff_computesFrom: the interface for Boolean source families.
• Cslib.Circuits.Monotone.ecomplexityFrom_boolIndicator: equality of weighted complexities.

References

• Adapted from Basis/AndOr.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib, extending its binary AND/OR interpretation to the existing basis with constants. The pointwise interface adapts LowerBound/Fusion/Boolean.lean from the same source.

def Cslib.Circuits.Monotone.setInterpretation (U : Type u_2) : Interpretation signature (Set U)

Interpret conjunction and disjunction as intersection and union, with empty/full constants.

@[simp]

theorem Cslib.Circuits.Monotone.setInterpretation_false (U : Type u_2) (args : Fin 0 → Set U) : setInterpretation U (Op.const false) args = ∅

@[simp]

theorem Cslib.Circuits.Monotone.setInterpretation_true (U : Type u_2) (args : Fin 0 → Set U) : setInterpretation U (Op.const true) args = Set.univ

@[simp]

theorem Cslib.Circuits.Monotone.setInterpretation_and {U : Type u_2} (args : Fin 2 → Set U) : setInterpretation U Op.and args = args 0 ∩ args 1

@[simp]

theorem Cslib.Circuits.Monotone.setInterpretation_or {U : Type u_2} (args : Fin 2 → Set U) : setInterpretation U Op.or args = args 0 ∪ args 1

theorem Cslib.Circuits.Monotone.setInterpretation_mono {U : Type u_1} (op : Op) : Monotone (setInterpretation U op)

Every set operation is monotone in its arguments.

noncomputable def Cslib.Circuits.Monotone.membershipHomomorphism {U : Type u_1} (x : U) : Homomorphism (setInterpretation U) interpretation

Membership at a point commutes with all operations, including the empty/full constants.

@[simp]

theorem Cslib.Circuits.Monotone.membershipHomomorphism_map {U : Type u_1} (x : U) (s : Set U) : (membershipHomomorphism x).map s = s.boolIndicator x

theorem Cslib.Circuits.Monotone.eval_set_iff_computesFrom {U : Type u_1} {n m : ℕ} (c : Circuit signature n m) (input : Fin n → Set U) (target : Fin m → Set U) : c.eval (setInterpretation U) input = target ↔ c.ComputesFrom interpretation (fun (x : U) (o : Fin m) => (target o).boolIndicator x) fun (x : U) (i : Fin n) => (input i).boolIndicator x

Constructing all target sets is equivalent to computing their characteristic functions from those of the supplied sets. This retains the circuit and every designated output.

theorem Cslib.Circuits.Monotone.eval_setOf_iff_computesFrom {U : Type u_1} {n m : ℕ} (c : Circuit signature n m) (sources : U → Fin n → Bool) (target : U → Fin m → Bool) : ((c.eval (setInterpretation U) fun (i : Fin n) => {x : U | sources x i = true}) = fun (o : Fin m) => {x : U | target x o = true}) ↔ c.ComputesFrom interpretation target sources

Boolean source families may be given directly as ordinary functions, with their true sets as the set-valued inputs. In particular, sources may include positive and negative literals.

theorem Cslib.Circuits.Monotone.ecomplexityFrom_boolIndicator {U : Type u_1} {n m : ℕ} (weight : Op → ℕ) (input : Fin n → Set U) (target : Fin m → Set U) : (ecomplexityFrom interpretation weight (fun (x : U) (o : Fin m) => (target o).boolIndicator x) fun (x : U) (i : Fin n) => (input i).boolIndicator x) = ecomplexityFrom (setInterpretation U) weight (fun (x : Unit) => target) fun (x : Unit) => input

Pointwise Boolean computation and constructing the fixed tuple of sets have equal minimum cost for every operation weight, including infinity when no circuit exists.