2
$\begingroup$

My understanding of the Y-combinator is that it never terminates (Yg = g(Yg)). Its termination is only decided externally to the $\lambda$ specification when it has reached a fixed point (g(x)=x) because based on its $\lambda$ expression there is no exit from the infinite loop even when the fixed point is reached.

Am I wrong?

$\endgroup$
6
  • 1
    $\begingroup$ What reduction strategy are you considering? Call by value or call by name? $\endgroup$
    – jmite
    May 6 at 18:04
  • $\begingroup$ I'm not sure how termination is decided by the reduction strategy. Call-by-value (eager) evaluation will undoubtedly be non-terminating compared to call-by-name or call-by-need (lazy) evaluations which can often handle infinite structures (like take 10 [1..]) by discarding un-evaluated sub-expressions. Still, termination in those latter cases can only occur when the reduction strategy decides to discard i.e stop further recursion by identifying the fixed point. This is happening externally to the bare lambda formalism. Doesn't it? $\endgroup$
    – dumb0
    May 6 at 19:15
  • 1
    $\begingroup$ I seem to have misunderstood that lambda's beta reduction does not itself define an order of precedence when an expression contains multiple applications. A lambda formalism thus requires a reduction strategy to specify this precedence. $\endgroup$
    – dumb0
    May 6 at 19:36
  • 1
    $\begingroup$ Termination can occur with lazy evaluation because of how branching is formulated (e.g. $\lambda x.\lambda y.y$). The infinite sub-expression is discarded when the terminal branch is reached leaving just the normal expression. $\endgroup$
    – dumb0
    May 6 at 19:40
  • $\begingroup$ The Y-combinator would not terminate however for eager inner evaluation strategies like the Applicative Order strategy. $\endgroup$
    – dumb0
    May 6 at 19:45
4
$\begingroup$

Terms containing the Y combinator can be weakly normalizing: they can terminate for a certain order of evaluation, i.e. for a certain evaluation strategy. No term containing the Y combinator applied to another term can be strongly normalizing, i.e. no term containing Y applied to another term terminates for all evaluation strategies, since the infinite reduction chain $Y \, M \to_\beta^* M \, (Y \, M) \to_\beta^* M \, (M \, (Y \, M)) \to_\beta^* \ldots$ is possible.

There are terms $M$ such that $Y \, M$ has no normal form, i.e. such that there is no reduction strategy that reduces $Y \, M$ to a value. For example $Y (\lambda x. x) \to_\beta^* (\lambda x.x) (Y (\lambda x.x)) \to_\beta Y (\lambda x. x)$ is a recursive functions that just spins (let x = x). (The lack of another reduction chain that terminates is left as an exercise for the reader.)

Under call-by-value (only ever reducing $M \, N$ when $M$ and $N$ are values), $Y \, M$ only converges if $M$ does not use its argument, i.e. if $Y \, M$ is not “really” recursive. Under call-by-name (always reducing the outermost redex first), $Y \, M$ converges if the recursive function that it defines terminates.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.