Proving the Unique Fixed-Point Principle Correct
An Adventure with Category Theory
International Conference on Functional Programming, Sept. 19–21, 2011, Tokyo, Japan.
PDF
|
DOI
|
BibTEX
Technical Report
PDF
|
BibTEX
Source Code
Zip
Abstract
Say you want to prove something about an infinite data-structure, such
as a stream or an infinite tree, but you would rather not subject
yourself to coinduction.
The unique fixed-point principle is an easy-to-use, calculational
alternative. The proof technique rests on the fact that certain
recursion equations have unique solutions; if two elements of a
coinductive type satisfy the same equation of this kind, then they are
equal.
In this paper we precisely characterize the conditions that guarantee
a unique solution. Significantly, we do so not with a syntactic
criterion, but with a semantic one that stems from the categorical
notion of naturality.
Our development is based on distributive laws and bialgebras, and
draws heavily on Turi and Plotkin’s pioneering work on mathematical
operational semantics.
Along the way, we break down the design space in two dimensions,
leading to a total of nine points. Each gives rise to varying
degrees of expressiveness, and we will discuss three in depth.
Furthermore, our development is generic in the syntax of equations and
in the behaviour they encode—we are not caged in the world of
streams.
Keywords
streams, infinite trees, unique fixed-points, initial algebras,
final coalgebras, bialgebras, distributive laws, free pointed functor,
free monad, cofree copointed functor, cofree comonad