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 CircuitComplexity.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

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

@[implicit_reducible]

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

Equations

• CircuitComplexity.instDecidableIsEssentialInput = CircuitComplexity.instDecidableIsEssentialInput._aux_1

def CircuitComplexity.EssentialInputs {N M : ℕ} (f : BitString N → BitString M) : Finset (Fin N)

The set of input variables that f depends on.

Equations

• CircuitComplexity.EssentialInputs f = Finset.filter (CircuitComplexity.IsEssentialInput f) Finset.univ