##
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