The problem below is interesting because it shows how you can compute with
functions (remember, functions are first-order data in SML), and also
because it shows how one can investigate the properties of programs using
theory (as opposed to just running the program, or trying to get an
intuitive, fuzzy understanding).

I wrote down many details and showed every step of the proofs. Many of
these steps are repetitive; your solution will be more than acceptable if
it follows the general approach shown here (or something similar to it),
even if it is somewhat more compact and skips the explanation of obvious
repeated steps.


Consider the following definition:

fun A f x = f x x

Also, recall the function composition operator (f o g) x = f(g(x)).

   1. Infer the type of A - clearly show and explain every step of the
      type-inference process.

   2. Consider the expression (A o A) a0 a1 ... an, where a0, a1, a2, ...,
      an are suitably chosen arguments. Determine a natural number n >= 0
      and the corresponding arguments a0, a1, a2, ..., an so that
      expression (A o A) a0 a1 ... an reduces to a non-function
      value. Describe all arguments ai in full, including their types.

   3. Show how the following expression is evaluated:

     (A o A o A) (fn a => fn b => fn c => fn d => a + b + c + d) 78

     Do not use the substitution model directly, as it would be too long
   and tedious to write out all the steps. Rather, rewrite the expression
   to reflect the action of the various functions. Obtaining the correct
   final result without showing the steps leading to it will not earn you
   points on this problem.

   4. Assuming that we denote A o A by A2, and A o A o A by A3, provide
      definitions analogous to the definition of A that show the effect of
      A2 and A3.

   5. Based on your previous answers, provide a definition for function Ak,
      where Ak is obtained by composing A with itself k > 0 times. Prove
      your statement using induction. Again, you should not use the
      substitution model directly in your proof, just rewrite the
      expression to show the effect of the various functions.


Solutions:

fun A f x = f x x

type(x) = 'a (we have no restriction on the type of x)

type(f x) = 'a -> 'c (we know that if this expression is correct, then x
must be in the domain of f)

Now, because f x x = ((f x) x), we know that the result of (f x) must also
be a function such that x is the domain of (f x). The range of this
function is not restricted. We can thus rewrite the type of (f x):

type(f x) = 'a -> ('a -> 'b) = 'a -> 'a -> 'b (i.e. 'c = 'a -> 'b)

The type of A (which is a curried function of two arguments) can be written
as

type(f) -> type(x) -> type(f x x)

By plugging in the right types for f and x we get:

('a -> 'a -> 'b) -> 'a -> 'b

You can check your solution by typing in the definition of A into SML.


Let us try evaluating A o A with one argument:

(A o A) a0 

(definition of o)
= A(A(a0))

(definition of A, first curried arg = a0)
= A(fn x => a0 x x)

(definition of A, first curried arg = fn x ...)
=  fn x => (fn x => a0 x x) x x

Note: do not get confused by the various x's; to make things clear we rewrite
= fn y => (fn x => a0 x x) y y
= fn y => (a0 y y) y

(associativity of function application)
= fn y => a0 y y y

So (A o A) a0 is a curried function of one argument. Thus (A o A) must have
been a curried function of two arguments. We repeat the derivation with two
arguments:

(A o A) a0 a1
(same as before, but all expressions have an a1 at the end)
= (fn y => a0 y y y) a1
= a0 a1 a1 a1

The type of a0 must be "curried function of three arguments of the same
type;" the type of a1 is not restricted. Thus we have:

type(a1) = 'a
type(a0) = 'a -> 'a -> 'a -> 'b
type(A o A) = ('a -> 'a -> 'a -> 'b) -> 'a -> 'b

Note: the type that you get if you type this in SML is slightly different,
because SML does not have enough information to disambiguate types. With
this limitation, the type reported by SML is the same. You could have
started with establishing the type of A o A with the help of SML, and then
just read out that A o A needs two arguments, one of type 'a -> 'a -> 'a ->
'b, the other of type 'a.

In effect, A o A takes a function of three arguments of the same type, and
"repeats" its second argument three times.

Before the next step we introduce the following notation:

F = fn a => fn b => fn c => fn d => a + b + c + d


(A o A o A) (fn a => fn b => fn c => fn d => a + b + c + d) 78

(definition of o, applied repeatedly)
= A(A(A(F))) 78

(definition of A, with first curried argument available)
= A(A(fn x => F x x)) 78

(definition of A, with first curried argument provided)
(I rename the args of anonymous functions to maintain clarity, but this 
 is not necessary.)
= A(fn y => (fn x => F x x) y y) 78

(function application)
= A(fn y => (F y y) y) 78

(remove redundant parantheses)
= A(fn y => F y y y) 78

(definition of A, with first curried argument provided)
= (fn z => (fn y => F y y y) z z) 78

(function application)
= (fn z => (F z z z) z) 78

(remove redundant parantheses)
= (fn z => F z z z z) 78

(function application)
= F 78 78 78 78

(replace definition of F)
= (fn a => fn b => fn c => fn d => a + b + c + d) 78 78 78 78

= 312


By now, it should be clear that if we compose A k times, then the resulting
function Ak "repeats" its second argument (k + 1) times, and "feeds" them
into the first argument of Ak.

fun A2 f x = f x x x
fun A3 f x = f x x x x

It is easy to come up with the guess:

fun Ak f x = f x x ... x (with k + 1 repetitions of x), for all k > 0

Proof by induction:

1. P(n) states that for n > 0, n integer, if An = A o A o .. o A (A
   composed by itself n times), then fun An f x = f x x ... x (with n + 1
   repetitions of x).

2. We do induction on integers n > 0.

3. Base case: n = 1

   We need to prove P(1): fun A f x = f x x
   This is true by the very definition of A.

4. Induction step:


Assume P(n): fun An f x = f x x ... x (n + 1 repetitions of x), n > 1
For m = n + 1, we prove
P(n + 1) = P(m): fun Am f x = f x x ... x (m + 1 repetitioins of x), n > 1

Am f x

= (A o A o ... o A) f x (A composed to itself m = n + 1 times)

= (A o (A o ... o A)) f x

(definition of o)
= A((A o A o ... o A) f) x

(we use the induction hypothesis; we rename function args for clarity)
= A((fn f => fn y => f y y ... y) f) x  (n + 1 repetitions of y)

= A(fn y => f y y ... y) x

(definition of A)
= (fn y => f y y ... y) x x

(function application)
= (f x x ... x) x  (a total of n + 2 = m + 1  repetitions of x)

(eliminate redundant parantheses)
= f x x ... x 


(Written by Tibor Janosi)