Tree Evaluation with fan-in d

An instance of d-ary Tree Evaluation with height h and value length ℓ is a perfect d-ary tree with every leaf at depth h. Its leaves carry ℓ-bit values and its internal nodes carry arbitrary gates ({0,1}^ℓ)^d → {0,1}^ℓ. The value of a node is its gate applied to the values of its children; the answer is the value of the root. Fan-in 2 is the binary problem Cslib.TreeEval.Tree, which embeds by Cslib.TreeEval.Ary.Tree.ofBinary.

Fan-in larger than two arises when Tree Evaluation is used to simulate time-bounded multi-tape machines, where a block of the computation depends on one earlier block per tape.

Main definitions

• Cslib.TreeEval.Ary.Tree d ℓ h: a d-ary instance of height h and value length ℓ.
• Cslib.TreeEval.Ary.Tree.eval: the value of the root.
• Cslib.TreeEval.Ary.Tree.nodeAt: the node at a path from the root.
• Cslib.TreeEval.Ary.Tree.ofBinary: a binary instance as an instance of fan-in 2.

Main results

• Cslib.TreeEval.Ary.Tree.eval_ofBinary: the embedding preserves the value.

References

• S. Cook, P. McKenzie, D. Wehr, M. Braverman and R. Santhanam, Pebbles and branching programs for tree evaluation introduce the problem for arbitrary fan-in.
• J. Cook and I. Mertz, Tree Evaluation is in Space O(log n · log log n) treat fan-in d.

@[reducible, inline]

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

A gate of fan-in d on ℓ-bit values: a function of the values of the d children.

def Cslib.TreeEval.Ary.Gate.ofBinary {ℓ : ℕ} (f : TreeEval.Gate ℓ) : Gate 2 ℓ

A binary gate as a gate of fan-in 2, reading child 0 as the left one.

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

A d-ary Tree Evaluation instance: a perfect d-ary tree with all leaves at depth h, carrying ℓ-bit values, and internal nodes carrying gates of fan-in d.

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

  A leaf carrying a value.

• node {d ℓ h : ℕ} (f : Gate d ℓ) (c : Fin d → Tree d ℓ h) : Tree d ℓ (h + 1)

  An internal node carrying a gate, with its d subtrees.

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

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

@[simp]

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

@[simp]

theorem Cslib.TreeEval.Ary.Tree.eval_node {d ℓ h : ℕ} (f : Gate d ℓ) (c : Fin d → Tree d ℓ h) : (node f c).eval = f fun (j : Fin d) => (c j).eval

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

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

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

  A leaf with its value.

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

  An internal node with its gate.

• none {d ℓ : ℕ} : Node d ℓ

  A path leaving the tree.

def Cslib.TreeEval.Ary.Tree.nodeAt {d ℓ h : ℕ} : Tree d ℓ h → List (Fin d) → Node d ℓ

The node reached from the root along a path, where j selects the j-th child.

@[simp]

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

@[simp]

theorem Cslib.TreeEval.Ary.Tree.nodeAt_node_nil {d ℓ h : ℕ} (f : Gate d ℓ) (c : Fin d → Tree d ℓ h) : (node f c).nodeAt [] = Node.gate f

@[simp]

theorem Cslib.TreeEval.Ary.Tree.nodeAt_node_cons {d ℓ h : ℕ} (f : Gate d ℓ) (c : Fin d → Tree d ℓ h) (j : Fin d) (P : List (Fin d)) : (node f c).nodeAt (j :: P) = (c j).nodeAt P

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

Leaves are at depth h.

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

Gates are at depth less than h.

def Cslib.TreeEval.Ary.Tree.ofBinary {ℓ h : ℕ} : TreeEval.Tree ℓ h → Tree 2 ℓ h

A binary instance as an instance of fan-in 2, with child 0 on the left.

@[simp]

theorem Cslib.TreeEval.Ary.Tree.eval_ofBinary {ℓ h : ℕ} (T : TreeEval.Tree ℓ h) : (ofBinary T).eval = T.eval

The embedding of binary instances preserves the value.