The number of nodes of a formula

The node count of a formula is the number of nodes of its syntax tree: the operation nodes, nullary ones such as constants included (Cslib.Circuits.Formula.size), together with the input leaves (Cslib.Circuits.Formula.leafSize). It is the size of a formula in the usual sense of algebraic complexity, where leaves labelled by variables and by constants both count.

Main definitions

• Cslib.Circuits.Formula.nodeCount: the number of syntax-tree nodes.

Main results

• Cslib.Circuits.Formula.nodeCount_input, Cslib.Circuits.Formula.nodeCount_gate: an input is one node, and an operation node adds one to the nodes of its arguments.
• Cslib.Circuits.Formula.nodeCount_pos: every formula has a node.

def Cslib.Circuits.Formula.nodeCount {σ : Signature} {n : ℕ} (F : Formula σ n) : ℕ

The number of syntax-tree nodes, counting input leaves, constants and operations alike: the operation nodes Formula.size together with the input leaves Formula.leafSize.

@[simp]

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

An input is one node.

@[simp]

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

An operation node adds one node to those of its arguments.

theorem Cslib.Circuits.Formula.nodeCount_pos {σ : Signature} {n : ℕ} (F : Formula σ n) : 0 < F.nodeCount

Every formula has a node.