I am recuperating some old posts made while I was in Sydney, this one by my then student Robbie Gates.
On Bijections between Data Types
Copyright Robbie Gates, 8th May 1996
This is a short note detailing the content of a lecture given to the third year "Categories and Computer Science" course in pure mathematics at Sydney University by Robbie Gates in which the results of the papers [
Gat] and [
Bla] were discussed.
Introduction
As previously discussed, the constructing arrows in a distributive category from a collection of basic arrows using composition and the properties of sums and products corresponds to writing straightline programs using given primitive operations. These composites can also be represented by drawing circuit diagrams, where the circuit elements represent arrows in the composite, and wires represent the objects.
To construct programs that use looping constructs (such as
for or
while loops), or circuits involving feedback requires more sophisticated notions, see [
KSW] for the theory developing these ideas.
Types as objects of a Distributive Category
Types may be described as objects of a distributive category satisfying certain equations in the distributive category.
For example, the type "binary trees of
X" may be described as an object
T together with a given isomorphism
T≅
TXT + 1 which consists of a pair of arrows
break :
T ->
TXT + 1 breaks a binary tree into (left subtree, node, right subtree) or returns * for the empty tree, and
make :
TXT + 1 ->
T which constructs a tree from its subtrees and node, or constructs the empty tree from *. Straight line programs utilising this data type are then arrows constructible from this isomorphism and the operations of a distributive category. For example, the arrow which interchanges the left and right subtrees of a given tree can be described as
make . (prj3,prj2,prj1) + 1 . break
or drawn as the following circuit,
where the wires are labelled by the object of the distributive category they represent.
We shall be mainly concerned here with a simpler example, namely trees of 1, that is to say, an object with a bijection
T≅
T^2 + 1.
The primary example we shall have in mind is indeed when
T is the set of binary trees with unlabelled nodes in the distributive category
Sets. Isomorphisms constructed between powers of
T will then corresponding to bijections between the sets of tuples of binary trees. Note that this has the form
P(T)≅
T for the polynomial
P(x) =
x^2 + 1, where
P is consider to be a polynomial with natural number coefficients. By considering polynomials with coefficients in an arbitrary distributive category, more interesting examples can be obtained (for example the paramatrized types such as trees of
X as described above).
The Generic Solution
Of particular interest is the "free" solution to the problem of finding a distributive category containing an object
T and isomorphism
P(T) ≅
T. By free here, we mean 2-initial in a suitable 2-category of distributive categories with designated object
T and isomorphism
P(T)≅
T. The object
T in this category is the generic solution to the equation, and the arrows represent generic operations on the data type, that is to say, operations that are constructed from the isomorphism using distributive operations, or alternatively, the straight line programs on the data type.
The main result of [
Gat] is to described the burnside rig (the rig of isomorphism classes of objects) of the category containing the generic solution for a large class of polynomials, including the example
P(x) =
x^2 + 1 (first studied by[
Bla]). This is done by giving a particularly tractable explicit construction of the category containing the generic object, as a category of fractions on the category of families of a particular Lawvere theory obtained from the polynomial.
In fact, the burnside rig turns out to be simply the free rig containing a solution to the equation. This is referred to by the slogan "Combinatorial equivalence is the same as Algebraic equivalence" (after a theorem from [
Bla]). By way of explanation, we note Combinatorial equivalence refers to an isomorphism between objects of the category - it is an explicit construction using the operations of the data type, where Algebraic equivalence refers to an equational deduction using rig operations.
An Interesting Bijection
Let us return again to the example
P(T) =
T^2 + 1. Here, there is an equational deduction of the fact
T^7 =
T from the equation
T^2 + 1 =
T using rig operations. Extremely informally, a suggestion of why this occurs can be obtained by solving the given quadratic over the complex numbers, and observing its roots indeed satisfy
T^7 =
T. Of course, this uses non-rig theoretic reasoning (although as we shall see, this is almost irrelevant !), an honest derivation can be given as follows:
This derivation can easily be converted to a circuit (in fact, the circuit may be easily constructed simply by thinking circuit theoretically). Such a circuit is given in the follow diagram, note that we have labelled the wires simply by the exponent of
T occurring, and all vertical juxtapositions are +. Further, labels on the circuit elements have been omitted, right-pointing triangles are instances of
break multiplied by an appropriate power of
T, whereas left-pointing triangles are instances of
make multiplied by an appropriate power of
T.
Proving Bijections don't Exist
As noted above, the circuit can indeed be constructed after some fiddling. From one point of view, the important part of the theorem is the negative part - one can show the nonexistence of straight-line programs exhibiting certain bijections. In particular, there is no bijection between the set of pairs of binary trees and the set of binary trees constructible from
make and
break using distributive operations. To see this, it suffices to show there is no equational deduction of
T^2 =
T from
T^2 + 1 =
T. This can be seen by exhibiting an element of any rig which satisfies the latter equation but not the former. Either root of
x^2 + 1 =
x in the complexes suffices.
Suppose you are given a isomorphism
U^2 +
U + 1 ≅U in a distributive category. Can you necessarily construct an isomorphism between
U^7 and
U^6 ? The answer is no, the complex number
i satisfies
x^2 +
x + 1 =
x but not
x^7 =
x^6.
Utilising the terminology of [Sch], it is shown in [Bla] that Euler characteristic and Dimension are sufficient to characterise the elements of the free rig with a solution to x^2 +1 = x. Without going into details, the net effect of this is that to determine whether or not two elements are equal, it suffices to check them at one root of the quadratic (the Euler characteristic), and to check that they either both contain an x or neither contain an x (the Dimension). This allows the existence of isomorphisms to be guaranteed merely by checking simple algebraic properties.
Further Work
The author of [
Gat] is continuing investigations in this area, with particular interest in parametrized data types (for example, the
template construct in C++)and applying the Euler characteristic and Dimension arguments to more general examples. A strong theory of data types and their behaviour in relation to straight-line programs is emerging from this work, and this connection is being vigorously explored.
Bibliography
[Bla] A. Blass, "Seven Trees in one",
Journal of Pure and Applied Algebra, 103:1-22,1995.
[Gat] R. Gates, "On the generic solution to
P(X)≅X in Distributive Categories",
Journal of Pure and Applied Algebra (to appear).
[KSW] P. Katis, N. Sabadini, R. F. C. Walters, "Bicategories of Processes",
Journal of Pure and Applied Algebra (to appear).
[Sch] S.H. Schanuel, "Negative sets have Euler characteristic and dimension",
Category Theory, Proceedings, Como 379-385, 1990.
Labels: computing, mathematics
