Balanced folds of lists

List.balancedFold op e f l combines the images under f of the elements of l by the binary operation op along a balanced binary tree: the empty list gives e, a singleton [b] gives f b, and a list of length k ≥ 2 gives op of the folds of its first ⌊k / 2⌋ elements and of the others. The tree has depth ⌈log₂ k⌉, so a measure that grows by at most c with every application of op grows by at most c ⌈log₂ k⌉ along the fold (List.apply_balancedFold_le). For an associative operation with identity e, the fold is foldr (List.balancedFold_eq_foldr), whatever the shape of the tree.

Balanced folds give formulas of logarithmic depth: the disjunction of k formulas, and the formula saying that a branching program of length k maps one state to another.

Main definitions

• List.balancedFold: the fold of a list along a balanced binary tree.

Main results

• List.balancedFold_induction: a property preserved by concatenation holds for balanced folds.
• List.balancedFold_hom: maps commuting with the operations commute with balanced folds.
• List.balancedFold_eq_foldr: for an associative operation with an identity, the balanced fold is foldr.
• List.apply_balancedFold_le: a measure growing by at most c with each operation grows by at most c ⌈log₂ k⌉ along a balanced fold of k elements.

@[irreducible]

def List.balancedFold {α : Type u_1} {β : Type u_2} (op : α → α → α) (e : α) (f : β → α) (l : List β) : α

The fold of l along a balanced binary tree: e for the empty list, f b for [b], and for a list of length k ≥ 2, op applied to the folds of its first ⌊k / 2⌋ elements and of the others.

@[simp]

theorem List.balancedFold_nil {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} : balancedFold op e f [] = e

The balanced fold of the empty list is e.

@[simp]

theorem List.balancedFold_singleton {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} (b : β) : balancedFold op e f [b] = f b

The balanced fold of a singleton [b] is f b.

theorem List.balancedFold_of_two_le {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} {l : List β} (hl : 2 ≤ l.length) : balancedFold op e f l = op (balancedFold op e f (take (l.length / 2) l)) (balancedFold op e f (drop (l.length / 2) l))

A list of length at least two folds into op of the folds of its two halves.

theorem List.balancedFold_induction {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} {p : List β → α → Prop} (nil : p [] e) (singleton : ∀ (b : β), p [b] (f b)) (append : ∀ (l₁ l₂ : List β) (x y : α), l₁ ≠ [] → l₂ ≠ [] → p l₁ x → p l₂ y → p (l₁ ++ l₂) (op x y)) (l : List β) : p l (balancedFold op e f l)

Induction for balanced folds. A property of lists and values that holds for the empty list and e, for every singleton [b] and f b, and for l₁ ++ l₂ and op x y whenever it holds for nonempty l₁ and x and for nonempty l₂ and y, holds for every list and its balanced fold.

theorem List.balancedFold_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : α → α → α} {e : α} {f : β → α} (g : α → γ) {op' : γ → γ → γ} (hg : ∀ (x y : α), g (op x y) = op' (g x) (g y)) (l : List β) : g (balancedFold op e f l) = balancedFold op' (g e) (g ∘ f) l

A map commuting with the operations commutes with balanced folds.

theorem List.balancedFold_eq_foldr {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} [Std.Associative op] [Std.LawfulIdentity op e] (l : List β) : balancedFold op e f l = foldr op e (map f l)

For an associative operation with identity e, the balanced fold is foldr.

theorem List.apply_balancedFold_le {α : Type u_1} {β : Type u_2} {op : α → α → α} {e : α} {f : β → α} (d : α → ℕ) {c D : ℕ} (hop : ∀ (x y : α), d (op x y) ≤ max (d x) (d y) + c) {l : List β} (hf : ∀ (b : β), b ∈ l → d (f b) ≤ D) (he : l = [] → d e ≤ D) : d (balancedFold op e f l) ≤ D + c * Nat.clog 2 l.length

Depth of a balanced fold. If applying op raises a measure d by at most c above its values on the arguments, and d is at most D on the leaves, then d is at most D + c ⌈log₂ k⌉ on the balanced fold of a list of k elements; e only matters for the empty list.