Formulas

A formula over a signature is a tree of operation symbols with inputs at its leaves, that is, a circuit in which every gate is read once. It is evaluated under an interpretation like a circuit (Formula.eval). Formulas are the free monad on the polynomial functor of the signature; a dedicated inductive type gives them readable constructors and structural induction. Equality of formulas is decidable, constructively, when equality of operation symbols is (Formula.decidableEq), so concrete formulas can be compared by decide.

The leaf size Formula.leafSize counts the input leaves, the measure of formula lower bounds Jukna, Chapter 6. Nullary operations, such as constants, are not counted: constants can be eliminated from a formula for a nonconstant function, so this changes no lower bound, and it gives constant functions leaf size zero. Formula.size counts the operation nodes, constants included. A formula of depth d with operations of arity at most r has at most r ^ d leaves (Formula.leafSize_le_pow_depth) and, for r ≥ 2, fewer than r ^ d operation nodes (Formula.size_lt_pow_depth); with s operation nodes it has at most (r - 1) s + 1 leaves (Formula.leafSize_le). The least depth of a formula computing a function, with given costs of the operations, is Formula.minDepthWith; it is ⊤ when no formula computes the function, as happens for monotone formulas. A formula is a circuit with one gate for each operation node and at most its depth (Formula.toCircuit). Counting only the leaves labelled by inputs of a set Y (Formula.leafSizeIn) splits the leaf size among disjoint blocks of inputs (Formula.sum_leafSizeIn_le_leafSize), and a formula with no leaf in Y depends only on the inputs outside Y (Formula.dependsOn_eval_of_leafSizeIn_eq_zero). An operation of arity two folds a list of k formulas into a balanced tree (Formula.balanced, by List.balancedFold) of depth ⌈log₂ k⌉ above them, the usual way to replace a gate of unbounded fan-in.

Main definitions

• Cslib.Circuits.Formula: formulas over a signature.
• Cslib.Circuits.Formula.eval, Cslib.Circuits.Formula.Computes: evaluation.
• Cslib.Circuits.Formula.leafSize, Cslib.Circuits.Formula.size, Cslib.Circuits.Formula.depth: the number of input leaves, the number of operation nodes, and the depth.
• Cslib.Circuits.Formula.leafSizeIn: the number of input leaves in a set of inputs.
• Cslib.Circuits.Formula.cost: the sum of operation weights, with input leaves free.
• Cslib.Circuits.Formula.depthWith: the depth when each operation costs a given number of levels.
• Cslib.Circuits.Formula.minDepthWith: the least depth with costs of a formula computing a function, in ℕ∞.
• Cslib.Circuits.Formula.gate₂, Cslib.Circuits.Formula.balanced: an operation of arity two applied to two formulas, and the balanced tree of such an operation over a list of formulas.
• Cslib.Circuits.Formula.bind: substitution of formulas for the inputs; Formula.rename renames the inputs, and Formula.lift and Formula.substLast add an input and substitute for it.
• Cslib.Circuits.Formula.toCircuit: a formula as a single-output circuit.

Main results

• Cslib.Circuits.Formula.map_eval: evaluation commutes with homomorphisms.
• Cslib.Circuits.Formula.minDepthWith_le, Cslib.Circuits.Formula.le_minDepthWith_iff, Cslib.Circuits.Formula.exists_depthWith_eq_minDepthWith: upper and lower bounds on the least depth, which is attained when some formula computes the function.
• Cslib.Circuits.Formula.leafSize_le_pow_depth, Cslib.Circuits.Formula.leafSize_le: leaf size under bounded fan-in.
• Cslib.Circuits.Formula.size_lt_pow_depth: size under bounded fan-in.
• Cslib.Circuits.Formula.depth_bind_le, Cslib.Circuits.Formula.size_bind_le: depth and size after substitution.
• Cslib.Circuits.Formula.size_balanced_add_one, Cslib.Circuits.Formula.depthWith_balanced_le: a balanced tree over k ≥ 1 formulas adds k - 1 nodes and ⌈log₂ k⌉ levels.
• Cslib.Circuits.Formula.Computes.toCircuit, Cslib.Circuits.Formula.size_toCircuit, Cslib.Circuits.Formula.depth_toCircuit_le: a formula is a circuit computing the same function, of the same size and at most the same depth.
• Cslib.Circuits.Formula.cost_toCircuit: compilation preserves arbitrary operation weights.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

inductive Cslib.Circuits.Formula (σ : Signature) (n : ℕ) : Type v

A formula over the signature σ with inputs Fin n: an input, or an operation applied to formulas.

• input {σ : Signature} {n : ℕ} (i : Fin n) : Formula σ n

  An input.

• gate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : Formula σ n

  An operation applied to formulas for its arguments.

@[instance_reducible]

instance Cslib.Circuits.Formula.decidableEq {σ : Signature} {n : ℕ} [DecidableEq σ.Op] : DecidableEq (Formula σ n)

Formulas have decidable equality when operation symbols do: compare the operations at the roots, then the arguments pointwise.

def Cslib.Circuits.Formula.eval {σ : Signature} {n : ℕ} {U : Type u_1} (F : Formula σ n) (I : Interpretation σ U) (x : Fin n → U) : U

Evaluate a formula under an interpretation.

@[simp]

theorem Cslib.Circuits.Formula.eval_input {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (i : Fin n) (x : Fin n → U) : (input i).eval I x = x i

An input leaf input i evaluates to x i.

@[simp]

theorem Cslib.Circuits.Formula.eval_gate {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) (x : Fin n → U) : (gate op args).eval I x = I op fun (j : Fin (σ.Arity op)) => (args j).eval I x

An operation node gate op args evaluates by applying I op to the values of its arguments.

theorem Cslib.Circuits.Formula.map_eval {σ : Signature} {n : ℕ} {U : Type u_1} {V : Type u_2} {I₁ : Interpretation σ U} {I₂ : Interpretation σ V} (h : Homomorphism I₁ I₂) (F : Formula σ n) (x : Fin n → U) : h.map (F.eval I₁ x) = F.eval I₂ (h.map ∘ x)

Evaluating a formula commutes with a homomorphism.

def Cslib.Circuits.Formula.Computes {σ : Signature} {n : ℕ} {U : Type u_1} (F : Formula σ n) (I : Interpretation σ U) (f : (Fin n → U) → U) : Prop

A formula computes f when it agrees with f on every input.

theorem Cslib.Circuits.Formula.computes_iff {σ : Signature} {n : ℕ} {U : Type u_1} {F : Formula σ n} {I : Interpretation σ U} {f : (Fin n → U) → U} : F.Computes I f ↔ F.eval I = f

A formula computes f exactly when its evaluation is f.

def Cslib.Circuits.Formula.leafSize {σ : Signature} {n : ℕ} : Formula σ n → ℕ

The leaf size: the number of input leaves. Nullary operations, such as constants, are not counted.

def Cslib.Circuits.Formula.size {σ : Signature} {n : ℕ} : Formula σ n → ℕ

The number of operation nodes, nullary ones included.

def Cslib.Circuits.Formula.cost {σ : Signature} {n : ℕ} (weight : σ.Op → ℕ) : Formula σ n → ℕ

The sum of operation weights, including nullary operations; input leaves are free.

def Cslib.Circuits.Formula.depth {σ : Signature} {n : ℕ} : Formula σ n → ℕ

The depth: inputs have depth zero, and an operation node is one deeper than its arguments, so nullary operations have depth one, as gates do in circuits.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_input {σ : Signature} {n : ℕ} (i : Fin n) : (input i).leafSize = 1

An input leaf has leaf size 1.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_gate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : (gate op args).leafSize = ∑ j : Fin (σ.Arity op), (args j).leafSize

The leaf size of an operation node is the sum of the leaf sizes of its arguments.

@[simp]

theorem Cslib.Circuits.Formula.size_input {σ : Signature} {n : ℕ} (i : Fin n) : (input i).size = 0

An input leaf has 0 operation nodes.

@[simp]

theorem Cslib.Circuits.Formula.size_gate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : (gate op args).size = ∑ j : Fin (σ.Arity op), (args j).size + 1

The size of an operation node is the sum of the sizes of its arguments plus 1.

@[simp]

theorem Cslib.Circuits.Formula.cost_input {σ : Signature} {n : ℕ} (weight : σ.Op → ℕ) (i : Fin n) : cost weight (input i) = 0

An input leaf has cost 0.

@[simp]

theorem Cslib.Circuits.Formula.cost_gate {σ : Signature} {n : ℕ} (weight : σ.Op → ℕ) (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : cost weight (gate op args) = ∑ j : Fin (σ.Arity op), cost weight (args j) + weight op

The cost of an operation node is the sum of the costs of its arguments plus weight op.

@[simp]

theorem Cslib.Circuits.Formula.cost_one {σ : Signature} {n : ℕ} (F : Formula σ n) : cost (fun (x : σ.Op) => 1) F = F.size

Unit operation weights count all operation nodes.

@[simp]

theorem Cslib.Circuits.Formula.depth_input {σ : Signature} {n : ℕ} (i : Fin n) : (input i).depth = 0

An input leaf has depth 0.

@[simp]

theorem Cslib.Circuits.Formula.depth_gate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : (gate op args).depth = (Finset.univ.sup fun (j : Fin (σ.Arity op)) => (args j).depth) + 1

The depth of an operation node is one more than the maximum depth of its arguments.

theorem Cslib.Circuits.Formula.leafSize_le_pow_depth {σ : Signature} {n r : ℕ} (hr : ∀ (op : σ.Op), σ.Arity op ≤ r) (F : Formula σ n) : F.leafSize ≤ r ^ F.depth

With operations of arity at most r, a formula of depth d has at most r ^ d leaves.

theorem Cslib.Circuits.Formula.size_lt_pow_depth {σ : Signature} {n r : ℕ} (hr : ∀ (op : σ.Op), σ.Arity op ≤ r) (hr₂ : 2 ≤ r) (F : Formula σ n) : F.size < r ^ F.depth

With operations of arity at most r, where 2 ≤ r, a formula of depth d has fewer than r ^ d operation nodes.

theorem Cslib.Circuits.Formula.leafSize_le {σ : Signature} {n r : ℕ} (hr : ∀ (op : σ.Op), σ.Arity op ≤ r) (F : Formula σ n) : F.leafSize ≤ (r - 1) * F.size + 1

With operations of arity at most r, a formula with s operation nodes has at most (r - 1) s + 1 leaves.

def Cslib.Circuits.Formula.leafSizeIn {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) : Formula σ n → ℕ

The number of input leaves labelled by inputs in Y.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_input {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) (i : Fin n) : leafSizeIn Y (input i) = if i ∈ Y then 1 else 0

An input leaf input i has 1 leaf in Y when i ∈ Y and 0 otherwise.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_gate {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : leafSizeIn Y (gate op args) = ∑ j : Fin (σ.Arity op), leafSizeIn Y (args j)

The number of leaves of gate op args in Y is the sum over its arguments.

theorem Cslib.Circuits.Formula.sum_leafSizeIn_le_leafSize {σ : Signature} {n : ℕ} {ι : Type u_3} {s : Finset ι} {Y : ι → Finset (Fin n)} (hY : (↑s).PairwiseDisjoint Y) (F : Formula σ n) : ∑ i ∈ s, leafSizeIn (Y i) F ≤ F.leafSize

Disjoint blocks of inputs share out the leaves.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_univ {σ : Signature} {n : ℕ} (F : Formula σ n) : leafSizeIn Finset.univ F = F.leafSize

Counting leaves in the set of all inputs gives the leaf size.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_empty {σ : Signature} {n : ℕ} (F : Formula σ n) : leafSizeIn ∅ F = 0

No leaves lie in the empty set of inputs.

theorem Cslib.Circuits.Formula.leafSizeIn_le_leafSize {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) (F : Formula σ n) : leafSizeIn Y F ≤ F.leafSize

The leaves in a set of inputs are at most all leaves.

theorem Cslib.Circuits.Formula.sum_leafSizeIn_singleton {σ : Signature} {n : ℕ} (S : Finset (Fin n)) (F : Formula σ n) : ∑ i ∈ S, leafSizeIn {i} F = leafSizeIn S F

The leaves in a set of inputs are the leaves at each of its inputs.

theorem Cslib.Circuits.Formula.leafSizeIn_add_leafSizeIn_compl {σ : Signature} {n : ℕ} (S : Finset (Fin n)) (F : Formula σ n) : leafSizeIn S F + leafSizeIn Sᶜ F = F.leafSize

Every leaf reads an input in a set or in its complement.

theorem Cslib.Circuits.Formula.dependsOn_eval_of_leafSizeIn_eq_zero {σ : Signature} {n : ℕ} {U : Type u_1} {Y : Finset (Fin n)} {F : Formula σ n} (hF : leafSizeIn Y F = 0) (I : Interpretation σ U) : DependsOn (F.eval I) (↑Y)ᶜ

A formula with no leaf in Y depends only on the inputs outside Y.

theorem Cslib.Circuits.Formula.eval_piecewise_eq_of_leafSizeIn_eq_zero {σ : Signature} {n : ℕ} {U : Type u_1} {Y : Finset (Fin n)} {F : Formula σ n} (hF : leafSizeIn Y F = 0) (I : Interpretation σ U) (x x' z : Fin n → U) : F.eval I (Y.piecewise x z) = F.eval I (Y.piecewise x' z)

A formula with no leaf in Y ignores the inputs in Y.

theorem Cslib.Circuits.Formula.eval_eq_of_leafSize_eq_zero {σ : Signature} {n : ℕ} {U : Type u_1} {F : Formula σ n} (hF : F.leafSize = 0) (I : Interpretation σ U) (x y : Fin n → U) : F.eval I x = F.eval I y

A formula without input leaves computes a constant.

def Cslib.Circuits.Formula.depthWith {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) : Formula σ n → ℕ

The depth when an operation node costs cost op levels instead of one: depthWith 1 is the depth, and charging nothing for negations gives the depth of formulas with free negations.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_input {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) (i : Fin n) : depthWith cost (input i) = 0

An input leaf has weighted depth 0.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_gate {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : depthWith cost (gate op args) = (Finset.univ.sup fun (j : Fin (σ.Arity op)) => depthWith cost (args j)) + cost op

The weighted depth of gate op args is the maximum weighted depth of its arguments plus cost op.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_one {σ : Signature} {n : ℕ} (F : Formula σ n) : depthWith 1 F = F.depth

With unit operation costs, depthWith is depth.

theorem Cslib.Circuits.Formula.depthWith_mono {σ : Signature} {n : ℕ} {cost cost' : σ.Op → ℕ} (h : ∀ (op : σ.Op), cost op ≤ cost' op) (F : Formula σ n) : depthWith cost F ≤ depthWith cost' F

Cheaper operations give a smaller depth.

theorem Cslib.Circuits.Formula.depthWith_le_depth {σ : Signature} {n : ℕ} {cost : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ 1) (F : Formula σ n) : depthWith cost F ≤ F.depth

Costs of at most one never make a formula deeper.

Balanced trees

def Cslib.Circuits.Formula.gate₂ {σ : Signature} {n : ℕ} (op : σ.Op) (hop : σ.Arity op = 2) (F G : Formula σ n) : Formula σ n

An operation of arity two applied to two formulas.

@[simp]

theorem Cslib.Circuits.Formula.eval_gate₂ {σ : Signature} {n : ℕ} {U : Type u_1} {op : σ.Op} {hop : σ.Arity op = 2} (I : Interpretation σ U) (F G : Formula σ n) (x : Fin n → U) : (gate₂ op hop F G).eval I x = I op fun (j : Fin (σ.Arity op)) => ![F.eval I x, G.eval I x] (Fin.cast hop j)

Evaluating gate₂ op hop F G applies I op to the values of F and G.

@[simp]

theorem Cslib.Circuits.Formula.size_gate₂ {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (F G : Formula σ n) : (gate₂ op hop F G).size = F.size + G.size + 1

The size of gate₂ op hop F G is F.size + G.size + 1.

@[simp]

theorem Cslib.Circuits.Formula.cost_gate₂ {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (weight : σ.Op → ℕ) (F G : Formula σ n) : cost weight (gate₂ op hop F G) = cost weight F + cost weight G + weight op

The cost of gate₂ op hop F G is F.cost weight + G.cost weight + weight op.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_gate₂ {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (F G : Formula σ n) : (gate₂ op hop F G).leafSize = F.leafSize + G.leafSize

The leaf size of gate₂ op hop F G is F.leafSize + G.leafSize.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_gate₂ {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (cost : σ.Op → ℕ) (F G : Formula σ n) : depthWith cost (gate₂ op hop F G) = max (depthWith cost F) (depthWith cost G) + cost op

The weighted depth of gate₂ op hop F G is the maximum of the weighted depths of F and G plus cost op.

def Cslib.Circuits.Formula.balanced {σ : Signature} {n : ℕ} (op : σ.Op) (hop : σ.Arity op = 2) (unit : Formula σ n) (l : List (Formula σ n)) : Formula σ n

The balanced tree of an operation of arity two over a list of formulas (List.balancedFold): unit for the empty list, the formula for a singleton, and for k ≥ 2 formulas the operation applied to the trees of the first ⌊k / 2⌋ formulas and of the others.

@[simp]

theorem Cslib.Circuits.Formula.balanced_nil {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (unit : Formula σ n) : balanced op hop unit [] = unit

The balanced tree over the empty list is unit.

@[simp]

theorem Cslib.Circuits.Formula.balanced_singleton {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (unit F : Formula σ n) : balanced op hop unit [F] = F

The balanced tree over a singleton list [F] is F.

theorem Cslib.Circuits.Formula.eval_balanced {σ : Signature} {n : ℕ} {U : Type u_1} {op : σ.Op} {hop : σ.Arity op = 2} (I : Interpretation σ U) (unit : Formula σ n) (l : List (Formula σ n)) (x : Fin n → U) : (balanced op hop unit l).eval I x = List.balancedFold (fun (a b : U) => I op fun (j : Fin (σ.Arity op)) => ![a, b] (Fin.cast hop j)) (unit.eval I x) (fun (x_1 : Formula σ n) => x_1.eval I x) l

A balanced tree evaluates to the balanced fold of the values of its formulas.

theorem Cslib.Circuits.Formula.size_balanced_add_one {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (unit : Formula σ n) {l : List (Formula σ n)} (hl : l ≠ []) : (balanced op hop unit l).size + 1 = (List.map size l).sum + l.length

A balanced tree over k ≥ 1 formulas has k - 1 operation nodes besides theirs.

theorem Cslib.Circuits.Formula.leafSize_balanced {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} (unit : Formula σ n) {l : List (Formula σ n)} (hl : l ≠ []) : (balanced op hop unit l).leafSize = (List.map leafSize l).sum

A balanced tree over k ≥ 1 formulas has their leaves.

theorem Cslib.Circuits.Formula.depthWith_balanced_le {σ : Signature} {n : ℕ} {op : σ.Op} {hop : σ.Arity op = 2} {cost : σ.Op → ℕ} (unit : Formula σ n) {l : List (Formula σ n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith cost F ≤ d) (hunit : l = [] → depthWith cost unit ≤ d) : depthWith cost (balanced op hop unit l) ≤ d + cost op * Nat.clog 2 l.length

A balanced tree is deeper than its formulas by ⌈log₂⌉ of their number times the cost of the operation; unit only matters for the empty list.

Least depth

noncomputable def Cslib.Circuits.Formula.minDepthWith {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (cost : σ.Op → ℕ) (f : (Fin n → U) → U) : ℕ∞

The least depth with costs cost of a formula computing f under I, or ⊤ if no formula computes f.

theorem Cslib.Circuits.Formula.minDepthWith_le {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} {F : Formula σ n} (hF : F.Computes I f) : minDepthWith I cost f ≤ ↑(depthWith cost F)

The least depth is at most the depth of every formula computing the function.

theorem Cslib.Circuits.Formula.le_minDepthWith_iff {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} {k : ℕ∞} : k ≤ minDepthWith I cost f ↔ ∀ (F : Formula σ n), F.Computes I f → k ≤ ↑(depthWith cost F)

Lower bounds on the least depth are lower bounds on the depth of every formula computing the function, including when there is none.

theorem Cslib.Circuits.Formula.minDepthWith_ne_top_iff {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} : minDepthWith I cost f ≠ ⊤ ↔ ∃ (F : Formula σ n), F.Computes I f

The least depth is finite exactly when some formula computes the function.

theorem Cslib.Circuits.Formula.exists_depthWith_eq_minDepthWith {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} (h : ∃ (F : Formula σ n), F.Computes I f) : ∃ (F : Formula σ n), F.Computes I f ∧ ↑(depthWith cost F) = minDepthWith I cost f

When some formula computes the function, the least depth is attained.

theorem Cslib.Circuits.Formula.synthesis_eval {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (F : Formula σ n) : Synthesis I (inputs n) {F.eval I} F.size

A formula is synthesized with one gate for each operation node.

Substitution

def Cslib.Circuits.Formula.bind {σ : Signature} {n m : ℕ} : Formula σ n → (Fin n → Formula σ m) → Formula σ m

Substitute the formula s i for every leaf labelled by input i: the bind of formulas as a free monad.

@[simp]

theorem Cslib.Circuits.Formula.input_bind {σ : Signature} {n m : ℕ} (i : Fin n) (s : Fin n → Formula σ m) : (input i).bind s = s i

Substituting s into an input leaf input i yields s i.

@[simp]

theorem Cslib.Circuits.Formula.gate_bind {σ : Signature} {n m : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) (s : Fin n → Formula σ m) : (gate op args).bind s = gate op fun (j : Fin (σ.Arity op)) => (args j).bind s

Substituting s into an operation node substitutes s into each argument.

@[simp]

theorem Cslib.Circuits.Formula.eval_bind {σ : Signature} {n : ℕ} {U : Type u_1} {m : ℕ} (I : Interpretation σ U) (F : Formula σ n) (s : Fin n → Formula σ m) (x : Fin m → U) : (F.bind s).eval I x = F.eval I fun (i : Fin n) => (s i).eval I x

Evaluating F.bind s on x evaluates F on the values of the substituted formulas s i.

@[simp]

theorem Cslib.Circuits.Formula.bind_input {σ : Signature} {n : ℕ} (F : Formula σ n) : F.bind input = F

Substituting each input leaf for itself leaves a formula unchanged.

@[simp]

theorem Cslib.Circuits.Formula.bind_assoc {σ : Signature} {n m k : ℕ} (F : Formula σ n) (s : Fin n → Formula σ m) (t : Fin m → Formula σ k) : (F.bind s).bind t = F.bind fun (i : Fin n) => (s i).bind t

Substitution of formulas is associative.

theorem Cslib.Circuits.Formula.leafSize_bind_le {σ : Signature} {n m : ℕ} {s : Fin n → Formula σ m} (hs : ∀ (i : Fin n), (s i).leafSize ≤ 1) (F : Formula σ n) : (F.bind s).leafSize ≤ F.leafSize

Substituting for each input a formula with at most one leaf does not raise the leaf size.

theorem Cslib.Circuits.Formula.depth_bind_le {σ : Signature} {n m : ℕ} {s : Fin n → Formula σ m} {c : ℕ} (hs : ∀ (i : Fin n), (s i).depth ≤ c) (F : Formula σ n) : (F.bind s).depth ≤ F.depth + c

Substituting formulas of depth at most c for the inputs raises the depth by at most c.

theorem Cslib.Circuits.Formula.size_bind_le {σ : Signature} {n m : ℕ} {s : Fin n → Formula σ m} {c : ℕ} (hs : ∀ (i : Fin n), (s i).size ≤ c) (F : Formula σ n) : (F.bind s).size ≤ F.size + F.leafSize * c

Substituting formulas of at most c operation nodes for the inputs adds at most c nodes for each leaf.

def Cslib.Circuits.Formula.rename {σ : Signature} {n m : ℕ} (f : Fin n → Fin m) (F : Formula σ n) : Formula σ m

The formula reading input f i where F reads input i.

@[simp]

theorem Cslib.Circuits.Formula.eval_rename {σ : Signature} {n : ℕ} {U : Type u_1} {m : ℕ} (I : Interpretation σ U) (f : Fin n → Fin m) (F : Formula σ n) (x : Fin m → U) : (rename f F).eval I x = F.eval I (x ∘ f)

Renaming the inputs of F by f evaluates F on x ∘ f.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_rename {σ : Signature} {n m : ℕ} (f : Fin n → Fin m) (F : Formula σ n) : (rename f F).leafSize = F.leafSize

Renaming the inputs keeps the leaf size.

@[simp]

theorem Cslib.Circuits.Formula.rename_rename {σ : Signature} {n m k : ℕ} (f : Fin n → Fin m) (g : Fin m → Fin k) (F : Formula σ n) : rename g (rename f F) = rename (g ∘ f) F

Renaming the inputs by f and then by g renames them by g ∘ f.

def Cslib.Circuits.Formula.lift {σ : Signature} {n : ℕ} (F : Formula σ n) : Formula σ (n + 1)

A formula on n inputs as one on n + 1 inputs that ignores the last.

def Cslib.Circuits.Formula.substLast {σ : Signature} {n : ℕ} (C : Formula σ (n + 1)) (K : Formula σ n) : Formula σ n

C with the formula K in place of its last input.

@[simp]

theorem Cslib.Circuits.Formula.eval_lift {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (F : Formula σ n) (y : Fin (n + 1) → U) : F.lift.eval I y = F.eval I fun (i : Fin n) => y i.castSucc

F.lift evaluates on y by restricting y to the first n inputs.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_lift {σ : Signature} {n : ℕ} (F : Formula σ n) : F.lift.leafSize = F.leafSize

Lifting a formula to n + 1 inputs preserves its leaf size.

@[simp]

theorem Cslib.Circuits.Formula.eval_substLast {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (C : Formula σ (n + 1)) (K : Formula σ n) (x : Fin n → U) : (C.substLast K).eval I x = C.eval I (Fin.snoc x (K.eval I x))

C.substLast K evaluates on x by extending x with K.eval I x at the last input.

@[simp]

theorem Cslib.Circuits.Formula.lift_substLast {σ : Signature} {n : ℕ} (F K : Formula σ n) : F.lift.substLast K = F

Substituting for the last input of F.lift recovers F.

@[simp]

theorem Cslib.Circuits.Formula.input_last_substLast {σ : Signature} {n : ℕ} (K : Formula σ n) : (input (Fin.last n)).substLast K = K

Substituting K for the last input in input (Fin.last n) yields K.

@[simp]

theorem Cslib.Circuits.Formula.input_castSucc_substLast {σ : Signature} {n : ℕ} (i : Fin n) (K : Formula σ n) : (input i.castSucc).substLast K = input i

Substituting for the last input leaves an earlier input leaf input i.castSucc as input i.

theorem Cslib.Circuits.Formula.gate_substLast {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ (n + 1)) (K : Formula σ n) : (gate op args).substLast K = gate op fun (j : Fin (σ.Arity op)) => (args j).substLast K

Substituting into an operation node substitutes into its arguments.

Formulas as circuits

def Cslib.Circuits.Formula.toCircuit {σ : Signature} {n : ℕ} : Formula σ n → Circuit σ n 1

A formula as a circuit: an input leaf is a wire, and an operation node is a gate on the circuits of its arguments, side by side.

@[simp]

theorem Cslib.Circuits.Formula.eval_toCircuit {σ : Signature} {n : ℕ} {U : Type u_1} (I : Interpretation σ U) (F : Formula σ n) (x : Fin n → U) (j : Fin 1) : F.toCircuit.eval I x j = F.eval I x

The single output of F.toCircuit evaluates to F.eval I x.

theorem Cslib.Circuits.Formula.Computes.toCircuit {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {F : Formula σ n} {f : (Fin n → U) → U} (hF : F.Computes I f) : F.toCircuit.Computes I (single f)

The circuit of a formula computes what the formula computes.

theorem Cslib.Circuits.Formula.cost_toCircuit {σ : Signature} {n : ℕ} (weight : σ.Op → ℕ) (F : Formula σ n) : F.toCircuit.program.cost weight = cost weight F

Compilation preserves the sum of arbitrary operation weights exactly.

@[simp]

theorem Cslib.Circuits.Formula.size_toCircuit {σ : Signature} {n : ℕ} (F : Formula σ n) : F.toCircuit.size = F.size

The circuit of a formula has one gate for each operation node.

theorem Cslib.Circuits.Formula.depthWith_toCircuit_le {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) (F : Formula σ n) : Circuit.depthWith cost F.toCircuit ≤ depthWith cost F

With costs, the circuit of a formula is no deeper than the formula.

theorem Cslib.Circuits.Formula.depth_toCircuit_le {σ : Signature} {n : ℕ} (F : Formula σ n) : F.toCircuit.depth ≤ F.depth

The circuit of a formula is no deeper than the formula.