= Solution
Generate every <permutation> of the tail, then insert its missing head at every possible position. The helper preserves order among the elements already present:
``
sml
fun insertEverywhere x [] = [[x]]
| insertEverywhere x (y :: ys) =
(x :: y :: ys) ::
List.map (fn zs => y :: zs) (insertEverywhere x ys);
fun permutations [] = [[]]
| permutations (x :: xs) =
List.concat
(List.map (insertEverywhere x) (permutations xs));
``
The first helper result inserts $x$ before $y$; the mapped recursive results put $y$ back at the front and insert $x$ farther along. For a list of length $k$, it yields exactly $k+1$ positions. The empty list has one <permutation>, itself, so the base result is `[[]]`, not `[]`.
For correctness, use <structural induction>. Any <permutation> of `x :: xs` has a unique position containing $x$. Removing that position leaves a <permutation> of `xs`, supplied by the induction hypothesis; reinserting $x$ at its unique position reconstructs the required output. With distinct input elements, neither the tail <permutation> nor the insertion position can be duplicated, so each output occurs once. Consequently \b[a length-$n$ input yields exactly $n!$ permutations], in an unrestricted order. The explicit output is large; this is not a polynomial-time enumeration with respect to $n$ alone.
Back to article page
