The Tree Evaluation problem

An instance of Tree Evaluation with height h and value length ℓ is a perfect binary tree with every leaf at depth h. Its leaves carry ℓ-bit values and its internal nodes carry arbitrary gates {0,1}^ℓ × {0,1}^ℓ → {0,1}^ℓ. The value of a node is its gate applied to the values of its two children; the answer is the value of the root.

We follow Goldreich's parametrization by the value length ℓ, rather than by the alphabet size k = 2^ℓ, so that values are bit strings Fin ℓ → Bool without rounding.

Main definitions

• Cslib.TreeEval.Tree ℓ h: a Tree Evaluation instance of height h and value length ℓ.
• Cslib.TreeEval.Tree.eval: the value of the root.
• Cslib.TreeEval.Tree.nodeAt: the node at a path from the root.

References

• S. Cook, P. McKenzie, D. Wehr, M. Braverman and R. Santhanam, Pebbles and branching programs for tree evaluation introduce the problem.
• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure uses the parametrization by value length.

@[reducible, inline]

abbrev Cslib.TreeEval.Gate (ℓ : ℕ) : Type

A gate on ℓ-bit values: a function of the values of the two children.

inductive Cslib.TreeEval.Tree (ℓ : ℕ) : ℕ → Type

A Tree Evaluation instance: a perfect binary tree with all leaves at depth h, carrying ℓ-bit values, and internal nodes carrying gates on pairs of ℓ-bit values.

• leaf {ℓ : ℕ} (v : Fin ℓ → Bool) : Tree ℓ 0

  A leaf carrying a value.

• node {ℓ h : ℕ} (f : Gate ℓ) (l r : Tree ℓ h) : Tree ℓ (h + 1)

  An internal node carrying a gate, with its left and right subtrees.

def Cslib.TreeEval.instDecidableEqTree.decEq {ℓ✝ a✝ : ℕ} (x✝ x✝¹ : Tree ℓ✝ a✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.TreeEval.instDecidableEqTree {ℓ✝ a✝ : ℕ} : DecidableEq (Tree ℓ✝ a✝)

def Cslib.TreeEval.Tree.eval {ℓ h : ℕ} : Tree ℓ h → Fin ℓ → Bool

The value of the root: each gate is applied to the values of its children.

@[simp]

theorem Cslib.TreeEval.Tree.eval_leaf {ℓ : ℕ} (v : Fin ℓ → Bool) : (leaf v).eval = v

@[simp]

theorem Cslib.TreeEval.Tree.eval_node {ℓ h : ℕ} (f : Gate ℓ) (l r : Tree ℓ h) : (node f l r).eval = f l.eval r.eval

inductive Cslib.TreeEval.Tree.Node (ℓ : ℕ) : Type

What a path from the root leads to: a leaf with its value, a gate, or nothing.

• leaf {ℓ : ℕ} (v : Fin ℓ → Bool) : Node ℓ

  A leaf with its value.

• gate {ℓ : ℕ} (f : Gate ℓ) : Node ℓ

  An internal node with its gate.

• none {ℓ : ℕ} : Node ℓ

  A path leaving the tree.

def Cslib.TreeEval.Tree.nodeAt {ℓ h : ℕ} : Tree ℓ h → List Bool → Node ℓ

The node reached from the root along a path, where false is the left child.

@[simp]

theorem Cslib.TreeEval.Tree.nodeAt_leaf_nil {ℓ : ℕ} (v : Fin ℓ → Bool) : (leaf v).nodeAt [] = Node.leaf v

@[simp]

theorem Cslib.TreeEval.Tree.nodeAt_node_nil {ℓ h : ℕ} (f : Gate ℓ) (l r : Tree ℓ h) : (node f l r).nodeAt [] = Node.gate f

@[simp]

theorem Cslib.TreeEval.Tree.nodeAt_node_false {ℓ h : ℕ} (f : Gate ℓ) (l r : Tree ℓ h) (P : List Bool) : (node f l r).nodeAt (false :: P) = l.nodeAt P

@[simp]

theorem Cslib.TreeEval.Tree.nodeAt_node_true {ℓ h : ℕ} (f : Gate ℓ) (l r : Tree ℓ h) (P : List Bool) : (node f l r).nodeAt (true :: P) = r.nodeAt P

theorem Cslib.TreeEval.Tree.length_of_nodeAt_leaf {ℓ h : ℕ} {U : Tree ℓ h} {P : List Bool} {v : Fin ℓ → Bool} (hP : U.nodeAt P = Node.leaf v) : P.length = h

Leaves are at depth h.

theorem Cslib.TreeEval.Tree.length_lt_of_nodeAt_gate {ℓ h : ℕ} {U : Tree ℓ h} {P : List Bool} {f : Gate ℓ} (hP : U.nodeAt P = Node.gate f) : P.length < h

Gates are at depth less than h.