Parenthesized reductions

ReductionTree records a nonempty reduction without choosing an arithmetic implementation. Unlike mathlib's BinaryTree, values occur at leaves, not internal nodes. An empty reduction needs a separately chosen identity and is deliberately not represented here.

inductive FloatLib.Numerics.ReductionTree (α : Type u_1) : Type u_1

A nonempty collection of inputs together with a binary evaluation schedule.

• leaf {α : Type u_1} (value : α) : ReductionTree α
• node {α : Type u_1} (left right : ReductionTree α) : ReductionTree α

def FloatLib.Numerics.instReprReductionTree.repr {α✝ : Type u_1} [Repr α✝] : ReductionTree α✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprReductionTree {α✝ : Type u_1} [Repr α✝] : Repr (ReductionTree α✝)

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqReductionTree {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ReductionTree α✝)

def FloatLib.Numerics.instDecidableEqReductionTree.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : ReductionTree α✝) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.ReductionTree.leaves {α : Type u_1} : ReductionTree α → List α

Input occurrences in left-to-right order, including repetitions.

def FloatLib.Numerics.ReductionTree.eval {α : Type u_1} {β : Type u_2} (combine : β → β → β) (value : α → β) : ReductionTree α → β

Evaluate the chosen schedule; the combining operation need not be associative.

def FloatLib.Numerics.ReductionTree.map {α : Type u_1} {β : Type u_2} (f : α → β) : ReductionTree α → ReductionTree β

Change leaf values without changing the evaluation schedule.

@[simp]

theorem FloatLib.Numerics.ReductionTree.eval_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : ReductionTree α) (f : α → β) (combine : γ → γ → γ) (value : β → γ) : eval combine value (map f t) = eval combine (value ∘ f) t

Mapping leaves commutes with evaluation.

@[simp]

theorem FloatLib.Numerics.ReductionTree.leaves_map {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (f : α → β) : (map f t).leaves = List.map f t.leaves

Mapping preserves the order and multiplicity of leaf occurrences.

def FloatLib.Numerics.ReductionTree.nodeCount {α : Type u_1} : ReductionTree α → ℕ

Number of combining operations in the schedule.

theorem FloatLib.Numerics.ReductionTree.length_leaves {α : Type u_1} (t : ReductionTree α) : t.leaves.length = t.nodeCount + 1

A full binary reduction performs one fewer addition than it has inputs.

theorem FloatLib.Numerics.ReductionTree.nodeCount_eq_of_perm {α : Type u_1} {a b : ReductionTree α} (h : a.leaves.Perm b.leaves) : a.nodeCount = b.nodeCount

A permutation of inputs cannot change the number of combining operations.

def FloatLib.Numerics.ReductionTree.AllNodes {α : Type u_1} {β : Type u_2} (combine : β → β → β) (value : α → β) (p : β → β → Prop) : ReductionTree α → Prop

A predicate on the two evaluated operands holds at every internal node of this tree.

theorem FloatLib.Numerics.ReductionTree.map_eval {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → γ) (combine' : γ → γ → γ) (h : AllNodes combine value (fun (x y : β) => interpret (combine x y) = combine' (interpret x) (interpret y)) t) : interpret (eval combine value t) = eval combine' (interpret ∘ value) t

Interpretation commutes with evaluation when it preserves the actual operations used.

theorem FloatLib.Numerics.ReductionTree.eval_add_eq_sum {α : Type u_1} {β : Type u_2} [AddMonoid β] (t : ReductionTree α) (value : α → β) : eval (fun (x1 x2 : β) => x1 + x2) value t = (List.map value t.leaves).sum

Exact additive evaluation agrees with the ordinary list sum.

theorem FloatLib.Numerics.ReductionTree.eval_add_eq_of_perm {α : Type u_1} {β : Type u_2} [AddCommMonoid β] {a b : ReductionTree α} (h : a.leaves.Perm b.leaves) (value : α → β) : eval (fun (x1 x2 : β) => x1 + x2) value a = eval (fun (x1 x2 : β) => x1 + x2) value b

Reordering leaves or changing parentheses preserves an exact commutative sum.