The algorithmic problem solving group conducts research into mathematical method, in particular the problem-solving skills involved in the formulation and solution of algorithmic problems.  Our goal is to articulate these skills primarily by way of concrete examples, but also by the development of appropriate mathematical theory.

A Field of Type Isomorphisms

Written by Wei Chen.


Lawvere is credited with the famous remark that “seven trees are one”.
More formally, the property is that the set of shapes of seven binary
trees is isomorphic to the set of shapes of single binary trees. The
strategy used to prove this property has been modelled as a game with
coins, called nuclear pennies. We briefly mention how we have exploited
our understanding of the theory in order to invent a novel class of
“replacement-set games” of which nuclear pennies is an instance. The
main part of the presentation concerns a subsequent remark made by
Lawvere in 2004 [1], namely that he was unable to establish certain
isomorphisms between tree structures, and Blass has proved that it is
indeed impossible. We show, nevertheless, that the isomorphisms he
mentioned can be proven by the introduction of lists. In particular, we
show that the set of shapes of a single binary tree is isomorphic to the
disjoint sum of the unit type and the set of shapes of three binary
trees, from which many other isomorphisms follow. (Note that the
statement of this property does not involve lists, but the proof
necessarily does.) Algebraically, Fiore has shown that the proof of
Lawvere’s remark is based on constructing a ring from a rig; our proof
takes the construction one step further to constructing a field from a
ring — lists provide a mechanism for constructing a pseudo-inverse
operator. The isomorphisms have been implemented in Haskell.

[1] Left and right adjoint operations on spaces and data types, F.W.F.
William Lawvere, Theoretical Computer Science 316 (2004) 105  111.