A New View of Binary Trees
We present a new formalism of labelled binary trees, using two partial binary constructors instead of the usual total ternary constructor. This formalism is complemented by some higher-order operators, encapsulating common patterns of computation on trees. We explore their use by deriving solutions to a couple of algorithmic problems on trees. \par The work proceeds in the Bird-Meertens style. This is a calculus for programs, closely related to applicative programming languages. Expressions are written at the function level, avoiding the use of unnecessary names and being as concise as possible. Derivations are performed by program transformation — the application of correctness-preserving transformations to an initial specification, with the intention of improving its efficiency without changing its meaning.