Andrew Coppin andrewcoppin at btinternet.com
Sun Aug 31 12:29:54 EDT 2008

```Ryan Ingram wrote:
> On Sun, Aug 31, 2008 at 12:46 AM, Andrew Coppin
> <andrewcoppin at btinternet.com> wrote:
>
>> Right. So if I have, say, the factorial function defined using the Y
>> combinator, there's no way to stop the interpretter expanding an infinite
>> number of copies of Y, even though in theory the factorial function should
>> terminate?
>>
>
> Well, this is exactly what ghci is doing; you just have to choose an
> evaluation order that makes sense.
>
> Lets consider a simple translation for recursive lets:
>
>> let x = exp1 in exp2
>>
> (where x may be free in exp1 and/or exp2)
>
> Here's a simple translation into lambda-calculus:
>
>> (\x. exp2) (y (\x. exp1))
>>
>
> (Of course, this representation for let can lose sharing; without
> knowing what you have or your goals I don't know if you care).
>
> Now, you just have to choose a y-combinator that makes sense for your
> evaluation order.  If you do normal-order evaluation like Haskell
> ("non-strict"), this Y should work for you:
>
> y = \f. (\x. f (x x)) (\x. f (x x))
>
>
>> Oh well, I guess I'll just have to live with that one. Maybe I can make the
>> binding to expand user-selectable or something...
>>
>
> Now, if you are eagerly-expanding the entire expression, trying to get
> to head normal form, then any expression that ends up with "y" in it
> won't terminate.  But if you use normal form evaluation order, then if
> a normal form exists, you will find it and terminate.
>
> So evaluating "fact" to normal form won't terminate, but evaluating
> "fact 5" should.
>

All of this strongly suggests that if you execute things in the correct
order, you can arrange it so that expressions that have a normal form
will be evaluated to it. But how to decide the correct evaluation order?
For the plain lambda calculus, IIRC you just have to execute the
left-most, outer-most redex every time and it'll work. For a language
with let-binds, it is unclear to me how to proceed...

```