TRANSPOSITION FOR THREE-BY-THREE MATRICES

Jeremy Gibbons
29th November 2005


Transposition is easy enough to write on matrices represented as
(let's say, non-empty) lists of lists, either as a fold

> trans = foldr1 (zipWith (++)) . map (map (:[]))

or as an unfold

> trans' = unfold (any null) (map head) (map tail)
> unfold p f g x = if p x then [] else f x : unfold p f g (g x)

However, nearly all reasoning about transposition revolves around
showing that is its own inverse. In fact, in general it is not: on a
non-rectangular list of lists, transposition necessarily loses
information. As you might expect, transposition turns out to be its
own inverse on rectangular lists of lists. Since rectangular lists of
lists are all and only those results returned by trans, this is
equivalent to

  trans . trans . trans = trans

Sadly, this fact turns out to be a real pig to prove. I'm sure this is
because it - in a sense I will not try to make precise - only
"accidentally" rather than "naturally" true. 

My suspicion is that it would be much easier to prove if it were
"naturally" true; for example, if the rectangularity side-condition
were expressed and enforced in the type. This script considers the
case of three-by-three matrices.


A triple has three elements of the same type.

> data Trip a = Trip a a a deriving Eq

> fst3, snd3, thd3 :: Trip a -> a
> fst3 (Trip a b c) = a
> snd3 (Trip a b c) = b
> thd3 (Trip a b c) = c

> contents :: Trip a -> [a]
> contents (Trip a b c) = [a,b,c]

> fill :: [a] -> Trip a
> fill [a,b,c] = Trip a b c

> instance Show a => Show (Trip a) where
>   show = show . contents


Various combinators on triples - triplication:

> trip :: a -> Trip a
> trip a = Trip a a a

"zip with apply":

> zap3 :: Trip (a->b) -> Trip a -> Trip b
> zap3 (Trip f g h) (Trip a b c) = Trip (f a) (g b) (h c)

and in terms of these, map:

> instance Functor Trip where
>   fmap f abc = zap3 (trip f) abc

...and fork:

> fork3 :: Trip (a->b) -> a -> Trip b
> fork3 fgh a = zap3 fgh (trip a)


Here is an example three-by-three matrix.

> m :: Trip (Trip Int)
> m = fill $ map fill $ [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]


Here is a kind of coinductive definition of transposition (in the
sense that the computation is structured after the output, like the
unfold version - even though it is not actually recursive).

> tr3 :: Trip (Trip a) -> Trip (Trip a)
> tr3 = fork3 (Trip (fmap fst3) (fmap snd3) (fmap thd3))


Now, the proof that transposition is its own inverse turns out to be
entirely straightforward. (I use some simple properties of fork3.)

  tr3 . tr3
=   { definition of tr3 }
  fork3 (Trip (fmap fst3) (fmap snd3) (fmap thd3)) . tr3
=   { fork fusion }
  fork3 (Trip (fmap fst3 . tr3) (fmap snd3 . tr3) (fmap thd3 . tr3))
=   { naturality of fst3, snd3, thd3 - see below }
  fork3 (Trip fst3 snd3 thd3)
=   { fork identity }
  id

The intermediate lemma mentioned above is that if k is a natural
transformation from Trip to Id (as fst3, snd3 and thd3 all are), then

  fmap k . tr3
=   { definition of tr3 }
  fmap k . fork3 (Trip (fmap fst3) (fmap snd3) (fmap thd3))
=   { fork-map fusion: 
      fmap k . fork3 (Trip f g h) = fork3 (Trip (k . f) (k . g) (k . h)) }
  fork3 (Trip (k . fmap fst3) (k . fmap snd3) (k . fmap thd3))
=   { naturality of k }
  fork3 (Trip (fst3 . k) (snd3 . k) (thd3 . k))
=   { fork fusion }
  fork3 (Trip fst3 snd3 thd3) . fst3
=   { fork identity }
  k


As an application, consider Richard Bird's sudoku problem. He wanted
to extract the rows, columns and boxes from a sudoku board, manipulate
them, and reassemble them to reconstruct the board. We model the board
as a nonet of nonets, where a nonet is a triple of triples.

> type Nine a = Trip (Trip a)
> type Mat a = Nine (Nine a)

We might consider each row as a list, so rows should yield a list of
lists; but then it will of course require a different function (of the
converse type) as its inverse. Richard saw that if each of rows, cols
and boxs was an endofunction, then at least the type is right for them
to be their own inverses.

> rows, cols, boxs :: Mat a -> Mat a

Now, it so happens that each extraction is simply some combination of
transpositions of various of the four dimensions of this
three-to-the-fourth hypergrid. Precisely which transpositions you need
depend on precisely how you represent the nine-by-nine sudoku square
in this hypercube; but with the interpretation I chose, I get:

> rows = id
> cols = fmap tr3 . tr3 . fmap (fmap tr3) . fmap tr3
> boxs = fmap tr3

Happily, the fact that each of these is its own inverse is a corollary
of the same holding for tr3 (together with naturality of tr3), as can
easily be shown. My question for Problem-Solving Club was: can we
generalize this definition of transposition and the result that it is
its own inverse to fixed-size lists of arbitrary size?


Here is a sudoku-sized board to play with, and the results of
computing its rows, columns and boxes.

> triples :: [a] -> [Trip a] -- better have length divisible by 3!
> triples = unfold null (fill . take 3) (drop 3)

> lay :: Show a => Nine a -> IO ()
> lay = putStrLn . unlines . map show . concat . map contents . contents 

> m' :: Trip (Trip (Trip (Trip Int)))
> m' = head $ triples $ triples $ triples $ triples $ [1..81]

*Main> lay $ m'
[[1,2,3],[4,5,6],[7,8,9]]
[[10,11,12],[13,14,15],[16,17,18]]
[[19,20,21],[22,23,24],[25,26,27]]
[[28,29,30],[31,32,33],[34,35,36]]
[[37,38,39],[40,41,42],[43,44,45]]
[[46,47,48],[49,50,51],[52,53,54]]
[[55,56,57],[58,59,60],[61,62,63]]
[[64,65,66],[67,68,69],[70,71,72]]
[[73,74,75],[76,77,78],[79,80,81]]

*Main> lay $ rows m'
[[1,2,3],[4,5,6],[7,8,9]]
[[10,11,12],[13,14,15],[16,17,18]]
[[19,20,21],[22,23,24],[25,26,27]]
[[28,29,30],[31,32,33],[34,35,36]]
[[37,38,39],[40,41,42],[43,44,45]]
[[46,47,48],[49,50,51],[52,53,54]]
[[55,56,57],[58,59,60],[61,62,63]]
[[64,65,66],[67,68,69],[70,71,72]]
[[73,74,75],[76,77,78],[79,80,81]]

*Main> lay $ cols m'
[[1,10,19],[28,37,46],[55,64,73]]
[[2,11,20],[29,38,47],[56,65,74]]
[[3,12,21],[30,39,48],[57,66,75]]
[[4,13,22],[31,40,49],[58,67,76]]
[[5,14,23],[32,41,50],[59,68,77]]
[[6,15,24],[33,42,51],[60,69,78]]
[[7,16,25],[34,43,52],[61,70,79]]
[[8,17,26],[35,44,53],[62,71,80]]
[[9,18,27],[36,45,54],[63,72,81]]

*Main> lay $ boxs m'
[[1,2,3],[10,11,12],[19,20,21]]
[[4,5,6],[13,14,15],[22,23,24]]
[[7,8,9],[16,17,18],[25,26,27]]
[[28,29,30],[37,38,39],[46,47,48]]
[[31,32,33],[40,41,42],[49,50,51]]
[[34,35,36],[43,44,45],[52,53,54]]
[[55,56,57],[64,65,66],[73,74,75]]
[[58,59,60],[67,68,69],[76,77,78]]
[[61,62,63],[70,71,72],[79,80,81]]