Essential Inputs

This module defines the notion of essential (non-redundant) input variables for a Boolean function.

Main definitions

• IsEssentialInput — a function depends on a particular input variable
• essentialInputs — the set of essential input variables

def Complexity.IsEssentialInput {N M : ℕ} (f : BitString N → BitString M) (i : Fin N) : Prop

A function f depends on input variable i if flipping that bit can change some output.

Equations

• Complexity.IsEssentialInput f i = ∃ (x : Complexity.BitString N), f x ≠ f (Function.update x i !x i)

@[instance_reducible]

instance Complexity.instDecidableIsEssentialInput {N M : ℕ} {f : BitString N → BitString M} {i : Fin N} : Decidable (IsEssentialInput f i)

IsEssentialInput f i is decidable, since it is an existential over the finite type BitString N with a decidable body.

Equations

• Complexity.instDecidableIsEssentialInput = { decide := decide (∃ a ∈ Finset.univ, (fun (x : Complexity.BitString N) => f x ≠ f (Function.update x i !x i)) a), reflects_decide := ⋯ }

def Complexity.essentialInputs {N M : ℕ} (f : BitString N → BitString M) : Finset (Fin N)

The set of input variables that f depends on.

Equations

• Complexity.essentialInputs f = Finset.filter (Complexity.IsEssentialInput f) Finset.univ