Marcelo Fiore
University of Cambridge

Imaginary Types

Abstract:

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

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