Title: How to Create a Doubly-Linked Dodecahedron
Author: Christian Sattler
Draft Version: Fri Apr  6 20:15:49 UTC 2012

Abstract:

This document was originally created in response to a challenge
from Richard Bird in his talk "How to Link a List" at FITA 2012.
He proposed a method for constructing not only a doubly-linked list,
but also a "doubly-linked" torus. Jesting, he ended his talk with
the challenge of constructing a doubly-linked dodecahedron.

Here, we take up his challenge seriously, presenting a general
elegant method for constructing doubly-linked structures of
symmetric objects based on two well-known notions,
memoization and (representations of) symmetry groups.

This method is sufficiently abstract to not only solve the above
specific challenge within the character limit of a Twitter message,
as Richard Bird joked in his talk, but also generalize to other
graph structures with nicely representable local automorphisms.


Executive Summary (Twitter message, 138 characters [with line breaks]):

import Data.Function.Memoize
data N=N[Integer]N N
c u=(.flip map u.(!!))
t f=memoFix(\s x->N(f x)(c[1,0,2,4,3]s x)$c[0,4,1,3,2]s x)[0..4]


Short Explanation:

One problem is that there is no canonical way of assigning names for
the three directions to the neighbours of each vertex in the
dodecahedron as exists for the torus (left, right, up, down). The
canonical solution is to include direction information in each node,
representing each vertex three times, yielding 60 nodes represented by
even permutations of size 5. Now, given a node  n = N pi x y, let
address n = pi  represent the "address" of n (with equality of
"addresses" implying "identity"), let  swap n = x  represent the next
node in the implicit direction, with the new direction pointing back
to the old vertex, and  rot n = y  represent the same vertex with the
implicit direction rotated by 120 degrees. It is clear that this
yields complete navigability of the dodecahedron. For example, we have
"identities"  swap (swap n) = n  and  rot (rot (rot n)) = n. Less
trivially, we for example have an "identity"  iter 5 (rot . swap) n = n.


Detailed Explanation:

Let us look at the type [Nat] = nu X. 1 + Nat x X where Nat = nu T. 1 + T.
Unfortunately, the difference between inductive and coinductive types is
not expressible in Haskell, so we make clear that we are interested only in
finite lists and natural numbers. Then, given any type A, there is a
canonical isomorphism between [Nat] -> A and the coinductive type mu Y. A x
Stream(Y) where Stream(Y) = mu Z. Y x Z. Let f and g be the mediating
arrows, i.e. f o g = id and g o f = id. Now, with lazy evaluation, even
though g o f is extensionally equal to the identity, it acts as a
"memoization" operator on [Nat] -> A, transforming any function into an
equivalent function which evaluates each function value only ever once.

Obviously, we can construct memoization operators for many more types, and
that is precicely what the Memoize library does for us. For example, let
Z/(m) denote the integers modulo m : Nat with the usual additive structure.
The torus from your talk can be seen as Z/(m) x Z/(n). Given a function f :
Z/(m) x Z/(n) -> A on it, we can create a doubly-linked structure from it
by defining

  record TorusNode A where
    element : A,
    left  : TorusNode A,
    right : TorusNode A,
    up    : TorusNode A,
    down  : TorusNode A

  g = memoize g' where g' z = TorusNode {
    element = f z,
    left  = g (z + (-1,  0)),
    right = g (z + ( 1,  0)),
    up    = g (z + ( 0, -1)),
    down  = g (z + ( 0,  1))
  }

or simply

  g = memoize (liftA5 TorusNode
    f
    (g . (+(-1,  0)))
    (g . (+( 1,  0)))
    (g . (+( 0, -1)))
    (g . (+( 0,  1)))
  )

where we exploited that X. Z/(m) x Z/(n) -> X is an applicative functor.

Now, with memoization, the problem of constructing a doubly-linked
structure on a given graph is not so much a problem of backlinking any more
but more a problem of how to represent the local structure of the graph
globally using appropriate automorphisms. For the torus, this was quite
easy because of the naturally given additive structure. For the regular
dodecahedron, it is helpful to know that the symmetry group of
orientation-preserving Euclidean transformations (i.e., rotations) is
isomorphic to A_5, the group of even permutations on five elements [0..4].
This isomorphism can be constructed as follows:

There is a canonical way (up to isomorphism, up to renumbering there are
two choices) to color the vertices of a dodecahedron with five colors
[0..4] such that no two adjacent vertices have the same color. One sees
easily that this coloring must also have the property that each face is
incident to exactly one vertex of each color. A less trivial insight is
that, given a face and an indident starting vertex, each even permutation
appears exactly once as the permutation corresponding to the list of colors
of the vertices of the face, counting in counter-clockwise direction. Given
an orientation-preserving Euclidean transformation, we can now identify
this transformation with the permutation of colors it induces one the
vertices of some fixed face (or, inversely, the permutation of colors it
induces between the vertices of some fixed face and the face it is mapped
to). An amazing fact of naturality is that this permutation does not depend
on the choice of the face. This permutation is always even, so this
correspondence induces an isomorphism between the group of
orientation-preserving symmetries and A_5.

[Note that the full symmetry group of the regular dodecahedron is not
isomorphic to S_5, but a different semidirect product A_5 with Z/(2). The
reason for this is that counting the colors of the vertices of a face in
clockwise direction instead still does not yield an odd permutation,
because it corresponds to composition of the counter-clockwise permutation
with (\x -> 4 - x) = (04)(13), an even permutation. This is an artifact of
the number five and "the reason" the full symmetry group of the regular
tetrahedron is S_4, since (02) is an odd permutation.]

Now, let us try to define a node type for the dodecahedral graph.
Obviously, we cannot make use of directions like left/right/up/down for the
torus. Instead we invent something like

  record DodecahedronNode A where
    element A,
    back  : DodecahedronNode A,
    left  : DodecahedronNode A,
    right : DodecahedronNode A

where each vertex comes with a direction 'back' indicating the edge we came
from. 'left' and 'right' then correspond to the other two edges, in the
obvious order. Effectively, we represent each vertex as three different
nodes, but this is necessary for this approach. By the above, each element
of pi : A_5 induces an orientation-preserving transformation of the
dodecahedron and hence a permutation pi^{(Node)} of nodes, but this is a
transitive action (in the sense of actions in group theory), so we can
break this symmetry by associating a specific arbitrary node x_id to the
identity element of A_5 and then associating pi : A_5 with x_pi :=
pi^{(Node)}(x_id).

Now, there is exactly one pi_back : A_5 such that x_{pi_back} is the node
we arrive at when choosing the 'back' link from x_id, i.e. x_{pi_back} =
back(x_id), and similar permutations pi_left, pi_right : A_5. Given any
other node x_pi with pi : A_5, pi^{(Node)} maps x_id to x_pi and hence also
should map

  back (x_id) to back (x_pi),
  left (x_id) to back (x_pi),
  right(x_id) to right(x_pi)

because it corresponds to an orientation-preserving symmetry of the
dodecahedron. This means we must define

  back(x_pi) = pi^{(Node)}(back(x_id))
             = pi^{(Node)}(pi_back^{(Node)}(x_id))
             = (pi o pi_back)^{(Node)}(x_id)
             = x_{pi o pi_back}

and similarly for 'left' and 'right'. In other words, given a function f :
A_5 -> B for some arbitrary type B representing the data to be attached to
each node, we can create a "doubly-linked" dodecahedron out of it by
defining

  g = memoize g' where g' pi = DodecahedronNode {
    element = f pi,
    back  = g (pi . pi_back ),
    left  = g (pi . pi_left ),
    right = g (pi . pi_right)
  }

or simply

  g = memoize (liftA4 DodecahedronNode
    f
    (g . (. pi_back ))
    (g . (. pi_left ))
    (g . (. pi_right))
  )

in complete analogy to the torus, now that we have exploited the symmetry
of the dodecahedron. Trying to fit this into a twitter post, we arrive

  import Data.Function.Memoize
  data N a=N a(N a)(N a)
  c u=(.flip map u.(!!))
  t f=memoFix(\s x->N(f x)(c[1,0,2,4,3]s x)$c[0,4,1,3,2]s x)[0..4]

which is exactly 140 character and would work were it not for the obstacle
that the type of the permutations defaults to [Int] instead of [Integer]
and the Memoize library does not seem to work correctly on [Int] -> a at
the moment (resulting in the topmost version). The only major difference to
the above explanation is that we chose a different representation of
dodecahedral nodes using operators 'swap' and 'rot' and an (arbitrarily)
inverted semantics of direction, with the understanding that this still
yields complete navigability of the dodecahedron, for example by defining

  back  = conjugate_swap(swap) = swap,
  left  = conjugate_swap(rot) = swap . rot . swap,
  right = conjugate_swap(rot . rot) = swap . rot . rot . swap

In particular, we have pi_swap = [1,0,2,4,3] (0 maps to 1, 1 to 0, 2 to 2,
3 to 4, 4 to 3), pi_rot = [0,4,1,3,2], map (v !!) u is composition v o u
(so c u s v = s (v o u)), x_id = t f, and the rest should fall into place.
It might be more elegant to represent permutations as Integer -> Integer
instead of [Integer] (because composition of permutations is then just
composition of functions), but the brevity of the list notation made the
latter the only choice for meeting the character limit.