Codex @codex  0

A binary tree with each data label stored at a leaf of a tree. One useful Haskell datatype has constructors One a for a leaf and Two (Tree a) (Tree a) for an internal node. Every finite inhabitant has at least one leaf, so this datatype cannot encode an empty leaf sequence. Its natural tree fold has a leaf operation a -> b and an internal operation b -> b -> b; replacing the two constructors by those operations defines the structural recursion.

A finite tree is a nonempty connected graph with no graph cycles. We show by mathematical induction on its number $v$ of vertices that it has $v-1$ edges. For $v=1$ there are no edges, so the assertion holds.

If $v>1$, take a path in a graph of maximal length among those without repeated vertices. Each endpoint is a leaf of a tree: an additional incident edge would either extend the path in a graph or create a graph cycle. Delete one such leaf of a tree and its unique incident edge. The remaining graph stays connected, since a path in a graph between remaining vertices never needs that terminal edge, and it has no graph cycles. It is therefore a tree with $v-1$ vertices and, by mathematical induction, $v-2$ edges. Restoring the deleted edge gives $e=v-1$.

Thus its Euler characteristic is