# Algorithmic Problem Solving

Research Group, University of Nottingham

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.