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:

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

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:

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

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]`:

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:

Next step, `F(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.

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:

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