We study the set T_A of infinite binary trees with nodes labelled in a semiring A from a coalgebraic perspective. We present coinductive definition and proof principles based on the fact that T_A carries a final coalgebra structure. By viewing trees as formal power series, we develop a calculus where definitions are presented as behavioural differential equations. We present a general format for these equations that guarantees the existence and uniqueness of solutions. Although technically not very difficult, the resulting framework has surprisingly nice applications, which is illustrated by various concrete examples.
Binary trees, Coalgebra, Coinduction, Differential equations, Formal power series
DATA STRUCTURES (acm E.1), COMPUTATION BY ABSTRACT DEVICES (acm F.1)
Data structures (msc 68P05), Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
Software (theme 1)
CWI
Software Engineering [SEN]
Computer Security

Silva, A.M, & Rutten, J.J.M.M. (2007). A coinductive calculus of binary trees. Software Engineering [SEN]. CWI.