Substituting variables and constants for inputs

A substitution ρ : Fin N → Fin n ⊕ Bool feeds every input of a Boolean function of N variables from one of n new variables or from a constant; several inputs may receive the same variable, so this is a projection in Valiant's sense rather than a restriction, which would leave the remaining inputs free. A substitution does not make a function harder to compute: a circuit for f with its inputs rewired, and two gates for the constants, computes f ∘ ρ.

The substitution appendInputs r fixes the last p inputs of a function of n + p variables to the bits r: substituting it computes x ↦ f (Fin.append x r); prependInputs r fixes the first p inputs instead. A restriction (partial assignment) is the substitution that replaces each bit by itself or by a constant (BitString.PartialAssignment.substitute_toSubstitution).

Fixing inputs that a target function ignores keeps the agreement on average: if g agrees with a function of its first n inputs on a δ fraction of all inputs, then for some fixing of the other inputs the resulting function, two gates larger, agrees with it on a δ fraction of the inputs (Cslib.Circuits.Boolean.exists_complexity_le_of_agree_prefix).

Main definitions

• Cslib.Circuits.Boolean.substitute, Cslib.Circuits.Boolean.appendInputs, Cslib.Circuits.Boolean.prependInputs.
• Cslib.Circuits.Boolean.substituteCircuit: executable substitution with two shared constants.
• Cslib.BitString.PartialAssignment.toSubstitution: a partial assignment as a substitution.

Main results

• Cslib.Circuits.Boolean.complexity_substitute_le: a substitution costs at most two gates.
• Cslib.Circuits.Boolean.exists_complexity_le_of_agree_prefix: fixing ignored inputs.

def Cslib.Circuits.Boolean.substitute {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) (x : Fin n → Bool) : Fin N → Bool

The inputs of a function of N variables fed by ρ from the variables x: input j is x i when ρ j = .inl i, and the constant b when ρ j = .inr b.

@[simp]

theorem Cslib.Circuits.Boolean.substitute_inl {n N : ℕ} {ρ : Fin N → Fin n ⊕ Bool} {x : Fin n → Bool} {j : Fin N} {i : Fin n} (h : ρ j = Sum.inl i) : substitute ρ x j = x i

@[simp]

theorem Cslib.Circuits.Boolean.substitute_inr {n N : ℕ} {ρ : Fin N → Fin n ⊕ Bool} {x : Fin n → Bool} {j : Fin N} {b : Bool} (h : ρ j = Sum.inr b) : substitute ρ x j = b

def Cslib.Circuits.Boolean.substituteCircuit {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) : Circuit signature n N

Implement a substitution using one shared gate for each Boolean constant. Both gates are included even when unused or when the output is empty.

@[simp]

theorem Cslib.Circuits.Boolean.eval_substituteCircuit {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) (x : BitString n) : (substituteCircuit ρ).eval interpretation x = substitute ρ x

The shared-constant circuit implements its input substitution.

theorem Cslib.Circuits.Boolean.cost_program_substituteCircuit {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) (cost : signature.Op → ℕ) : (substituteCircuit ρ).program.cost cost = cost (Op.const false) + cost (Op.const true)

Substitution charges each of the two shared constant gates once.

@[simp]

theorem Cslib.Circuits.Boolean.size_substituteCircuit {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) : (substituteCircuit ρ).size = 2

The substitution circuit has exactly two gates, regardless of the output width.

theorem Cslib.Circuits.Boolean.depth_substituteCircuit_le {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) : (substituteCircuit ρ).depth ≤ 1

The shared-constant substitution circuit has depth at most one.

theorem Cslib.Circuits.Boolean.complexity_substitute_le_two {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) : complexity interpretation (substitute ρ) ≤ 2

A substitution costs at most two gates, one for each constant.

theorem Cslib.Circuits.Boolean.complexity_substitute_le {n N : ℕ} (ρ : Fin N → Fin n ⊕ Bool) (f : BooleanFunction N) : complexity interpretation (single fun (x : Fin n → Bool) => f (substitute ρ x)) ≤ complexity interpretation (single f) + 2

Substitutions do not make functions harder. Feeding the inputs of f from variables and constants costs at most two more gates than f.

def Cslib.Circuits.Boolean.appendInputs {n p : ℕ} (r : Fin p → Bool) : Fin (n + p) → Fin n ⊕ Bool

The substitution fixing the last p inputs of a function of n + p variables to r.

@[simp]

theorem Cslib.Circuits.Boolean.substitute_appendInputs {n p : ℕ} (r : Fin p → Bool) (x : Fin n → Bool) : substitute (appendInputs r) x = Fin.append x r

def Cslib.Circuits.Boolean.prependInputs {n p : ℕ} (r : Fin p → Bool) : Fin (p + n) → Fin n ⊕ Bool

The substitution fixing the first p inputs of a function of p + n variables to r.

@[simp]

theorem Cslib.Circuits.Boolean.substitute_prependInputs {n p : ℕ} (r : Fin p → Bool) (x : Fin n → Bool) : substitute (prependInputs r) x = Fin.append r x

theorem Cslib.Circuits.Boolean.exists_complexity_le_of_agree_prefix {n N : ℕ} (hle : n ≤ N) (E : BooleanFunction n) (g : BooleanFunction N) {δ : ℝ} (hagree : δ * 2 ^ N < ↑{y : BitString N | g y = E fun (i : Fin n) => y (Fin.castLE hle i)}.card) : ∃ (C : BooleanFunction n), complexity interpretation (single C) ≤ complexity interpretation (single g) + 2 ∧ δ * 2 ^ n < ↑{x : BitString n | C x = E x}.card

Fixing ignored inputs. If g on N inputs agrees with a function E of its first n inputs on more than δ * 2 ^ N inputs, then fixing the other N - n inputs suitably (appendInputs) gives a function on n inputs, of complexity at most two more, that agrees with E on more than δ * 2 ^ n inputs: some fixing does at least as well as the average.

def Cslib.BitString.PartialAssignment.toSubstitution {n : ℕ} (ρ : PartialAssignment (Fin n)) : Fin n → Fin n ⊕ Bool

The substitution replacing each fixed bit by its value and each free bit by itself.

theorem Cslib.BitString.PartialAssignment.substitute_toSubstitution {n : ℕ} (ρ : PartialAssignment (Fin n)) : Circuits.Boolean.substitute ρ.toSubstitution = ρ.fill

Restricting is substituting constants for the fixed bits.