Boolean-function m-semiring Bool[X]

This file defines the semiring BoolFunc X of Boolean functions over a set X of Boolean variables. Concretely, BoolFunc X = (X → Bool) → Bool: elements are functions from Boolean assignments to Booleans, with pointwise operations.

Addition is pointwise ||, multiplication is pointwise &&, and the natural order is f ≤ g ↔ ∀ a, f a → g a (pointwise implication).

BoolFunc X is absorptive, idempotent, and left-distributive.

This semiring is used in Green, Karvounarakis & Tannen, Provenance Semirings and surveyed in Senellart, Provenance and Probabilities in Relational Databases.

References

• Green, Karvounarakis & Tannen, Provenance Semirings
• Senellart, Provenance and Probabilities in Relational Databases

def BoolFunc (X : Type) : Type

The type of Boolean functions over Boolean assignments to X: (X → Bool) → Bool with pointwise operations.

Equations

• BoolFunc X = ((X → Bool) → Bool)

def BoolFunc.var {X : Type} (i : X) : BoolFunc X

The i-th variable of BoolFunc X: the Boolean function that returns the value of an assignment at i.

Equations

• BoolFunc.var i ν = ν i

@[implicit_reducible]

instance instZeroBoolFunc {X : Type} : Zero (BoolFunc X)

Equations

• instZeroBoolFunc = { zero := fun (x : X → Bool) => decide False }

@[implicit_reducible]

instance instAddBoolFunc {X : Type} : Add (BoolFunc X)

Equations

• instAddBoolFunc = { add := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν || f₂ ν }

@[implicit_reducible]

instance instOneBoolFunc {X : Type} : One (BoolFunc X)

Equations

• instOneBoolFunc = { one := fun (x : X → Bool) => decide True }

@[implicit_reducible]

instance instMulBoolFunc {X : Type} : Mul (BoolFunc X)

Equations

• instMulBoolFunc = { mul := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν && f₂ ν }

@[implicit_reducible]

instance instLEBoolFunc {X : Type} : LE (BoolFunc X)

Equations

• instLEBoolFunc = { le := fun (f₁ f₂ : BoolFunc X) => ∀ (ν : X → Bool), f₁ ν ≤ f₂ ν }

@[implicit_reducible]

instance instSubBoolFunc {X : Type} : Sub (BoolFunc X)

Equations

• instSubBoolFunc = { sub := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν && !f₂ ν }

@[implicit_reducible]

instance instCommSemiringBoolFunc {X : Type} : CommSemiring (BoolFunc X)

Equations

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

@[implicit_reducible]

instance instSemiringWithMonusBoolFunc {X : Type} : SemiringWithMonus (BoolFunc X)

BoolFunc X is a commutative m-semiring with pointwise || as addition, pointwise && as multiplication, and pointwise implication as natural order.

Equations

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

@[implicit_reducible]

instance instCommSemiringWithMonusBoolFunc {X : Type} : CommSemiringWithMonus (BoolFunc X)

Equations

• instCommSemiringWithMonusBoolFunc = { toSemiringWithMonus := instSemiringWithMonusBoolFunc, mul_comm := ⋯ }

theorem BoolFunc.absorptive {X : Type} : _root_.absorptive (BoolFunc X)

theorem BoolFunc.idempotent {X : Type} : _root_.idempotent (BoolFunc X)

theorem BoolFunc.mul_sub_left_distributive {X : Type} : _root_.mul_sub_left_distributive (BoolFunc X)

instance instNontrivialBoolFunc {X : Type} : Nontrivial (BoolFunc X)

instance BoolFunc.instCharPZero {X : Type} : CharP (BoolFunc X) 0

BoolFunc X has characteristic 0 in the CharP sense: it is idempotent and nontrivial, so every positive natural-number cast equals 1.

Universal property obstructions

The variable functions BoolFunc.var i satisfy two algebraic identities in BoolFunc X that constrain the target of any semiring homomorphism:

• 1 + var i = 1 (BoolFunc.absorptive)
• var i * var i = var i (multiplicative idempotence)

If the target K is not absorptive (there exists a : K with 1 + a ≠ 1), assigning that a to any variable makes a semiring homomorphism BoolFunc X →+* K impossible. Similarly if K's multiplication is not idempotent.

theorem BoolFunc.var_mul_self {X : Type} (i : X) : var i * var i = var i

BoolFunc.var i * BoolFunc.var i = BoolFunc.var i.

theorem BoolFunc.add_sub_self {X : Type} (f : BoolFunc X) : f + (1 - f) = 1

f + (1 - f) = 1 in BoolFunc X (Boolean complement on the join side).

theorem BoolFunc.mul_sub_self {X : Type} (f : BoolFunc X) : f * (1 - f) = 0

f * (1 - f) = 0 in BoolFunc X (Boolean complement on the meet side).

theorem BoolFunc.no_hom_of_not_absorptive {K : Type} [Semiring K] {X : Type} [Inhabited X] (hna : ¬_root_.absorptive K) : ∃ (ν : X → K), ¬∃ (φ : BoolFunc X →+* K), ∀ (i : X), φ (var i) = ν i

If the target K is not absorptive, there is no semiring homomorphism from BoolFunc X (with X inhabited) sending the variables to arbitrary values. Picking ν constant equal to a witness a of 1 + a ≠ 1 blocks any homomorphism: var i + 1 = 1 in BoolFunc X, so 1 + a = 1 is forced in K.

theorem BoolFunc.no_hom_of_not_mul_idem {K : Type} [Semiring K] {X : Type} [Inhabited X] (hna : ¬∀ (a : K), a * a = a) : ∃ (ν : X → K), ¬∃ (φ : BoolFunc X →+* K), ∀ (i : X), φ (var i) = ν i

If the target K does not have idempotent multiplication, there is no semiring homomorphism from BoolFunc X (with X inhabited) sending the variables to arbitrary values. Picking ν constant equal to a witness a of a * a ≠ a blocks any homomorphism, since var i * var i = var i in BoolFunc X.

theorem BoolFunc.homomorphism_from_BoolFunc {X Y : Type} (ν : X → BoolFunc Y) : ∃ (h : SemiringWithMonusHom (BoolFunc X) (BoolFunc Y)), ∀ (i : X), (fun (x : BoolFunc X) => h.toRingHom x) (var i) = ν i

For any assignment ν : X → BoolFunc Y, the substitution map f ↦ (τ ↦ f (fun i => ν i τ)) is an m-semiring homomorphism BoolFunc X → BoolFunc Y sending each variable BoolFunc.var i to ν i. This realizes BoolFunc X as a “free” object: variables can be sent to arbitrary Boolean functions.

Home · Documentation · Publications · Contributors · Source · Cite