Marcelo Fiore
University of Cambridge

Imaginary Types


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 .


t5 = t

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

POP Seminar
October 09, 2002
1:30 p.m.
Wean Hall 8220