= Linear flattening of a binary tree
{title2=`go t acc = flatten t ++ acc`}
For a <leaf-labelled binary tree>, define `go (One x) acc = x:acc` and `go (Two l r) acc = go l (go r acc)`, then apply `go t []`. The invariant in the title follows by <structural induction> and <associativity> of <list concatenation>. It proves preservation of leaf order. Each leaf supplies one output constructor and each internal node requires constant bookkeeping, giving <linear time> in the number of nodes. By contrast, flattening both subtrees and concatenating their results can copy prefixes of sizes $1,2,\ldots,n-1$ on a left-branching <tree>, taking <quadratic time>. The accumulator is the already-known suffix in a <difference list> representation.
Back to article page
