Problem 9

For notational simplicity, let us denote the array of function arguments that we want to permute circularly by 1 2 3 ... n-1 n. The circular permutation that we want to implement transforms 1 2 3 ... n-1 n into n 1 2 3 ... n-1. In fact, there is a functional arguments before the list of "real" arguments. In our discussion we will mostly ignore this function, and number the rest of the arguments from 1. The problem provides a solution for three arguments, and asks you to provide a solution for n = 4.

The circular permutation of n arguments can be achieved by using the solution for circularly permuting n-1 arguments in two ways:

(1) 1 2 3 ... n-1 n        flip last two arguments
    1 2 3 ... n   n-1      circularly permute first n-1 elements
    n 1 2 ... n-2 n-1


(2) 1 2 3 ... n-1 n        circularly permute last n-1 elements
    1 n 2 ... n-2 n-1      flip first two arguments
    n 1 2 ... n-2 n-1

Let us study the solution provided for n = 3:

(B (B C) C) f 1 2 3
  = (B C) (C f) 1 2 3      [apply definition of B]
  = B C (C f) 1 2 3        [eliminate redundant parantheses]
  = (B C (C f) 1) 2 3      [show the arguments B takes]
  = C ((C f) 1) 2 3        [apply definition of B]
  = ((C f) 1) 3 2          [C flips first and second argument]
  = C f 1 3 2              [eliminate redundant parantheses]
  = (C f 1 3) 2            [show the arguments C takes]
  = (f 3 1) 2              [C flips first and second argument]
  = f 3 1 2                [eliminate redundant parantheses]

This solution flips the last two arguments, then circulary permutes the first two. Of course, circular permutation of two arguments, is equivalent to flipping them. So this is a solution in the second family.

Which part of the solution flips the last pair of arguments? Well, it is the application of (B C). So C flips the (last two) arguments of two arguments, and (B C) flips the last two of three arguments. Could it be that (B (B (... (B C) ...)) flips the last two of a list of n+2 arguments, when it contains n instances of B? It turns out that this is true, and can easily be proven formally (do it!).

Now, what is the role of the first B in the solution? By studying its definition and by examining its action in the sample solution, we realize that B combines the effect of (B C) and C. More generally, B is the function composition operator.

We now know enough to write down solutions from family (1) for the general case of n arguments:

(B (* flip last two of n args *)  (* solution for n-1 *))

Note that the solution for n-1 arguments can be *any* solution that permutes the first n-1 arguments; in particular it can be a solution that belongs to family (2).

We instantiate the general solution for n = 4 as follows:

(B (B (B C)) (B (B C) C))

Here is an informal proof that the solution is correct:

val Y1 = B (B C)
val Y2 = B (B C) C

(B (B (B C)) (B (B C) C)) f 1 2 3 4 1
  = (B Y1 Y2) f 1 2 3 4  [use shorthand notation]
  = B Y1 Y2 f 1 2 3 4    [eliminate redundant parantheses]
  = (B Y1 Y2 f) 1 2 3 4  [show the arguments B takes]
  = Y1 (Y2 f) 1 2 3 4    [apply definition of B]
  = (Y2 f) 1 2 4 3       [Y1 flips third and fourth argument]
  = Y2 f 1 2 4 3         [eliminate redundant parantheses]
  = (Y2 f 1 2 4) 3       [show the arguments Y2 takes]
  = (f 4 1 2) 3          [Y2 circularly permutes the three arguments]
  = f 4 1 2 3            [eliminate redundant parantheses]

Try to give a more detailed proof for this solution! If you do, you will see that the solution reduces to always flipping adjacent arguments, starting at the right end of the argument list and advancing toward the left end: 1 2 3 4 -> 1 2 4 3 -> 1 4 2 3 -> 4 1 2 3. This is a characteristic of the general solution as well.

Now let us focus on the second family of solutions. Flipping the first two arguments is easy, as this is accomplished directly by C. We immediately get the following idea (also using the fact that B performs function composition):

(B (* solution for n-1 *) C)

Let us denote the solution for n - 1 arguments with X:

(B X C) f 1 2 3 ... n            [apply definition of B]
  = X (C f) 1 2 3 ... n          [X circularly permutes the first n-1 arguments]
  = (C f) (n-1) 1 2 ... (n-2) n  [eliminate redundant parantheses]
  = C f (n-1) 1 2 ... (n-2) n    [apply C's definition]
  = f 1 (n-1) 2 ... (n-2) n

Well, this does not work. Why? Notice that when X is applied, it is applied to 1, 2, ..., n-1, rather than to 2, 3, ..., n. We should somehow "shield" 1 from the effect of X. But how? Well, take a look at the first two lines of the derivation: the effect of B is to "package" f together with C, and thus combine them into one unit (argument) for X. But this is exactly what we want to do! We refine our initial idea, and this time we get it right (prove!):

(B (B (* solution for n-1 *)) C)

Interestingly enough, the solution for n = 3 is the same for both family of solutions: B (B C) C! Can you tell why?

Again, the solution for n-1 might belong to the other family of solutions, or be of a type we did not consider here.

Here is the solution for n = 4:

(B (B (B (B C) C)) C)

Prove, using the informal proof style given above, that this solution is correct!

In general, one can generate solutions for this problem by composing other permutations that lead to the same result. Another approach is to introduce the identity permutation into the formulas we develop. For example, (B C C) f 1 2 = f 1 2. Consider (B (B (B (B C*) C)) C) and assume that we want to replace the C marked with a star with an equivalent formula using the identity permutation above. We immediately note that C = (B (B C C) C). By replacing this into the original formula, we get: (B (B (B (B (B (B C C) C)) C)) C). Of course, we can push this much farther: (B (B (B (B (B (B C C) C)) (B (B C C) C))) (B (B (B (B C C) C) C) C)).

To practice your understanding of B and C, try to determine what the functions below do, and especially how they achieve their result:

(B (B (C B C (B C))) C)
(B (B (B C (B (B C (B (B (B C) C) C)) C)))  C)

Prepared by Tibor Jánosi, Fall 2002.

CS312 home  © 2002 Cornell University Computer Science