Skip to main content

Proving the unique fixed−point principle correct: an adventure with category theory

Ralf Hinze and Daniel W.H. James

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.

Address
New York‚ NY‚ USA
Book Title
Proceeding of the 16th ACM SIGPLAN international conference on Functional programming
ISBN
978−1−4503−0865−6
Location
Tokyo‚ Japan
Month
September
Pages
359–371
Publisher
ACM
Series
ICFP '11
Year
2011