By relating problems in programming-language theory and computational algebra, we elucidate the general character of the following argument in the style of eighteenth-century analysis.
The data type
datatype t = nil | succ of t | bin of t * t ;
of finite unary or binary unlabelled trees satisfies the equation
t = 1 + t + t2
from which it follows that
t = 1i .
Thus
and hence
t * t * t * t * t and t
are isomorphic types, in that there are mutually inverse conversion programs between them.
This is joint work with Tom Leinster (Institut des Hautes Itudes Scientifiques, Bures-sur-Yvette), following work of Bill Lawvere and Steve Schanuel, Andreas Blass, and Robbie Gates.
Host: Stephen Brookes
Appointments: Deb Cavlovich
Principles
of Programming Seminars