HR F#: Lambda Calculus - Reductions #4

The last one from reduction problems is following:

Reduce the following expression, using the beta-rule, to no more than one term. If the expression cannot be reduced, enter "CAN'T REDUCE".
(λg.((λf.((λx.(f(xx)))(λx.(f(xx)))))g))

Well, now I (and you, if you follow) understand the Lisp developers better. The number of parenthesis is quite close to critical in this expression.

The definition (λg.((λf.(...)) g)) just recalls the internal function with the same argument. It can be reduced to λf.(...).

Let's try to reduce λf.(...):

λf.(λx.(f (x x))) (λx.(f (x x))) =
  λf.(f ((λx.(f (x x))) (λx.(f (x x))))) =
  λf.(f (f ((λx.(f (x x))) (λx.(f (x x))))) =
  λf.(f (... (f ((λx.(f (x x))) (λx.(f (x x)))))...))

It grows indefinitely and similar to the expression from the problem Reduction #3. So the answer is "CAN'T REDUCE".

Just out of curiosity let's see how it will look in F#:

let f4 g =
  let f3 f =
    let f1 x = f (x x)
    let f2 x = f (x x)
    f2 f1
  f3 g

F# compiler cannot compile it with the errors:

Compilation error (line 3, col 21): Type mismatch.
Expecting a 'a but given a 'a -> 'b
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

Compilation error (line 4, col 21): Type mismatch.
Expecting a 'a but given a 'a -> 'b
The resulting type would be infinite when unifying ''a' and ''a -> 'b'