Came across this particular implementation of permutation, and spent some effort trying to understand why it works. For permutation, the usually algorithm I have in mind is the following:

1
2
perm [] = [[]]
perm xs = [x:rest | x <- xs, rest <- perm (delete x xs)]

For [1..3], the result would be:

1
2
3
4
5
6
[1,2,3]
[1,3,2]
[2,1,3]
[2,3,1]
[3,1,2]
[3,2,1]

I can make sense of the ordering by focusing the x <- xs part, that the ordering should follow the original list element order, and it does.

Now, let’s try to decipher the seemingly odd implementation. The most interesting (or confusing) part is this P function:

1
2
3
4
5
6
7
8
9
10
static void P( int n )
{
    if (n > 1) {
        for ( int j = n-1; j != 0; --j ) {
            P( n-1 );
            F( n );
        }
        P( n-1 );
    }
}

It’s not obvious what this function does, but according to its name, we could guess that it’s doing permutation. Some other information that is relevant but not very essential:

  • the list is captured in a static field
  • the actual result is kept in a static field, perms as a list, for P has void as its return type.
  • F reverses the first n elements of the list
1
2
3
4
5
6
7
8
private static Perm perms;    /* local to these functions */
private static Pair x;        /* local to these functions */

static void F( int n )
{
    x = revloop( x, n, tail( x, n ) );
    perms = Perm.cons ( x, perms );
}

Let’s start with a bold hypothesis that P performs permutation for a list of length n, and the first (top) element of perms is the reverse of the original list, e.g. [1..3]:

1
2
3
4
5
6
[3,2,1] -----
[X,X,X]      |
[X,X,X]      |
[X,X,X]      6
[X,X,X]      |
[1,2,3] -----

If you compile the original code, and try a few inputs to see the permutations, you would find that it does return the correct result, so probably our hypothesis holds. Let’s prove it using mathematical induction.

The base case would be a list of length 2, [1..2]. Because P(1) is no-op, the only meaningful call is F(2), which reverses the first 2 elements of the list, which is the whole list. Therefore, the result, perms, is [[2,1],[1,2]].

Given P(n-1) calculates the permutations of the first n-1 elements of the list, after P(n-1) in the first iteration, the perms should look something like:

1
2
3
[n-1 ..    1, n]
...                     // omitted permutations of [1..n-1]
[ 1   .. n-1, n]

Next step, F(n):

1
2
3
4
[n, 1 ..    n-1]
[n-1 ..    1, n]
...                     // omitted permutations of [1..n-1]
[ 1   .. n-1, n]

Now, the last element is n-1, and we are ready to do another round of permutation for the first n-1 elements. Pay close attention to the order of the top list that it’s the actual shift-one version of the original list. We would use this property later. The same pattern repeats for n-1 times.

1
2
3
4
5
6
[2   ..  n,   1]
[   ..    ,   2]        // permutations end with 2
...
[   ..    , n-2]        // permutations end with n-2
[   ..    , n-1]        // permutations end with n-1
[   ..    ,   n]        // permutations end with n

Using the “shifting” property, we know that the top one is shift-n-1 version, namely [2..n, 1]. Then, the last P(n-1) would get perms to be:

1
2
3
4
5
6
[   ..    ,   1]        // permutations end with 1
[   ..    ,   2]        // permutations end with 2
...
[   ..    , n-2]        // permutations end with n-2
[   ..    , n-1]        // permutations end with n-1
[   ..    ,   n]        // permutations end with n

Finally, the perms contains all the permutations of [1..n]. Q.E.D.