Canonical encoding of finite Boolean assignments and tables -- definitions

Coordinates are listed in their linear order. Boolean assignments to k coordinates are then indexed by the corresponding little-endian k-bit vector, giving a computable equivalence with Fin (2^k). This fixes a canonical order for serializing arbitrary Boolean dependency tables.

def Complexity.BooleanDependency.assignmentIndexEquiv {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : (↥coordinates → Bool) ≃ Fin (2 ^ coordinates.card)

Computable little-endian indexing of all Boolean assignments to an ordered finite coordinate set.

Equations

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

structure Complexity.BooleanDependency.OrderedAssignment {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Type u_1

Boolean assignments equipped with their canonical little-endian order.

• toFun : ↥coordinates → Bool

  Underlying assignment.

@[instance_reducible]

instance Complexity.BooleanDependency.OrderedAssignment.instCoeFunForallSubtypeMemFinsetBool {coordinate : Type u_1} [LinearOrder coordinate] {coordinates : Finset coordinate} : CoeFun (OrderedAssignment coordinates) fun (x : OrderedAssignment coordinates) => ↥coordinates → Bool

Equations

• Complexity.BooleanDependency.OrderedAssignment.instCoeFunForallSubtypeMemFinsetBool = { coe := Complexity.BooleanDependency.OrderedAssignment.toFun }

def Complexity.BooleanDependency.OrderedAssignment.indexEquiv {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : OrderedAssignment coordinates ≃ Fin (2 ^ coordinates.card)

Ordered assignments are canonically equivalent to their little-endian indices.

Equations

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

@[instance_reducible]

instance Complexity.BooleanDependency.OrderedAssignment.instDecidableEq {coordinate : Type u_1} [LinearOrder coordinate] {coordinates : Finset coordinate} : DecidableEq (OrderedAssignment coordinates)

Equations

• Complexity.BooleanDependency.OrderedAssignment.instDecidableEq = (Complexity.BooleanDependency.OrderedAssignment.indexEquiv coordinates).decidableEq

@[instance_reducible]

instance Complexity.BooleanDependency.OrderedAssignment.instFintype {coordinate : Type u_1} [LinearOrder coordinate] {coordinates : Finset coordinate} : Fintype (OrderedAssignment coordinates)

Equations

• Complexity.BooleanDependency.OrderedAssignment.instFintype = Fintype.ofEquiv (Fin (2 ^ coordinates.card)) (Complexity.BooleanDependency.OrderedAssignment.indexEquiv coordinates).symm

@[instance_reducible]

instance Complexity.BooleanDependency.OrderedAssignment.instLinearOrder {coordinate : Type u_1} [LinearOrder coordinate] {coordinates : Finset coordinate} : LinearOrder (OrderedAssignment coordinates)

Equations

• Complexity.BooleanDependency.OrderedAssignment.instLinearOrder = (Complexity.BooleanDependency.OrderedAssignment.indexEquiv coordinates).linearOrder

def Complexity.BooleanDependency.encodeOrderedFunction {index : Type u_1} [Fintype index] [LinearOrder index] (function : index → Bool) : List Bool

Encode a Boolean function on any finite linearly ordered domain.

Equations

• Complexity.BooleanDependency.encodeOrderedFunction function = List.ofFn fun (position : Fin (Fintype.card index)) => function ((Fintype.orderIsoFinOfCardEq index ⋯) position)

def Complexity.BooleanDependency.decodeOrderedFunction? {index : Type u_1} [Fintype index] [LinearOrder index] (bits : List Bool) : Option (index → Bool)

Decode a Boolean function on a finite linearly ordered domain only from a bit string with exactly one entry per domain element.

Equations

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

def Complexity.BooleanDependency.encodeAssignment {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (assignment : ↥coordinates → Bool) : List Bool

Encode one assignment by listing its coordinate values in increasing coordinate order.

Equations

• Complexity.BooleanDependency.encodeAssignment coordinates assignment = List.ofFn fun (position : Fin coordinates.card) => assignment ((coordinates.orderIsoOfFin ⋯) position)

def Complexity.BooleanDependency.decodeAssignment? {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : Option (↥coordinates → Bool)

Decode an assignment only from a bit string of the exact required length.

Equations

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

def Complexity.BooleanDependency.encodeTable {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (table : (↥coordinates → Bool) → Bool) : List Bool

Serialize a Boolean table in the canonical little-endian assignment order.

Equations

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

def Complexity.BooleanDependency.decodeTable? {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : Option ((↥coordinates → Bool) → Bool)

Decode a Boolean table only from a bit string with exactly one entry for every assignment.

Equations

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