OK, I'm starting to understand all this a bit more, thank you all.

2008/2/26, Nicolas Pouillard <nicolas.pouillard@gmail.com>:
> A picture can helps...
>
>      +---------+
>   a>-|         |->c
>      |    x    |
>   b>-|         |->b
>      +---------+
>
>      +---------+
>   a>-|         |->c
>      |    y    |
>   +->-|         |->-+
>   |   +---------+   |
>   +--------b--------+
>
>  loop x = y

I saw this image before, but despite of its clarity, it hasn't solved
my problem: the chicken and egg one. See, the looping "b" in y looks
like it has to be produced out of thin air. The only solution I can
guess is that x must, for some value of "a", produce the outputs "c"
and "b" independently of the input "b". Then, the recursion in loop
must reach this particular value of "a".

Maybe I could understand this by writing a factorial function, using a
non recursive function and loop (I hope this is possible).

2008/2/27, Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>:
>  where the name "fix" suggests that we will plug in a fix-point operator
>  at the end of the day. Before reading on, you should try to write down a
>  term of type (2), given that we have fix. I will bet that your brain
>  will produce the same solution as described below.

It did :-), but it will take a bit of my time to understand the rest.

Cheers,
Loup