Finite Boolean dependency tables -- definitions

This module gives canonical restriction, extension, and table operations for a function of Boolean coordinates that depends on only a finite set. The table is indexed by assignments to exactly those coordinates, making its entry count an explicit resource rather than merely asserting that the function factors.

def Complexity.BooleanDependency.restrict {coordinate : Type u_1} (coordinates : Finset coordinate) (input : coordinate → Bool) : ↥coordinates → Bool

Restrict a total Boolean assignment to a finite set of coordinates.

Equations

• Complexity.BooleanDependency.restrict coordinates input index = input ↑index

def Complexity.BooleanDependency.mergeAssignments {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (assignments : (↥coordinates → Bool) × (↥coordinatesᶜ → Bool)) : coordinate → Bool

Merge Boolean assignments on a finite coordinate set and its complement.

Equations

• Complexity.BooleanDependency.mergeAssignments coordinates assignments index = if hindex : index ∈ coordinates then assignments.1 ⟨index, hindex⟩ else assignments.2 ⟨index, ⋯⟩

def Complexity.BooleanDependency.assignmentSplitEquiv {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) : (coordinate → Bool) ≃ (↥coordinates → Bool) × (↥coordinatesᶜ → Bool)

A total Boolean assignment is equivalently its restrictions to a finite coordinate set and its complement.

Equations

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

def Complexity.BooleanDependency.extendByFalse {coordinate : Type u_1} [DecidableEq coordinate] (coordinates : Finset coordinate) (input : ↥coordinates → Bool) : coordinate → Bool

Extend an assignment on selected coordinates by false everywhere else.

Equations

• Complexity.BooleanDependency.extendByFalse coordinates input index = if hindex : index ∈ coordinates then input ⟨index, hindex⟩ else false

def Complexity.BooleanDependency.table {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) : (↥coordinates → Bool) → result

The canonical table obtained by evaluating a function on extensions of all assignments to a selected finite coordinate set.

Equations

• Complexity.BooleanDependency.table coordinates function input = function (Complexity.BooleanDependency.extendByFalse coordinates input)