I am trying to build my own λ-calculus interpreter. So far it supports both call-by-value and normal order.

I now want to try recursion via fixed points. The $Y$ combinator works with normal order, tested with the faculty function $$\text{fac} = \lambda f.\lambda n.\text{iszero}\,n\,1 (\text{mul}\,n\, (f(\text{pred}\,n)))\text{,}$$ and for example my interpreter yields $Y\,\text{fac}\,3 \stackrel{\text{NO}}{\rightarrow} 6$. (I'll write behaviourally equivalent Church numerals as decimal numbers)

As far as I know for call-by-value I will need the $Z$ combinator instead:

$$Z = \lambda f. (\lambda x. f (\lambda y. x x y)) (\lambda x. f (\lambda y. x x y))\text{,}$$

as $Y$ would cause an immediate infinite regression.

My problem is, I fail to understand how $Z\,\text{fac}\,0$ is supposed to terminate. It also does not terminate in my interpreter, but I want to understand it manually first.

After some steps call-by-value should arrive at: $$Z\,\text{fac}\,0 \\=\lambda f. (\lambda x. f (\lambda y. x x y)) (\lambda x. f (\lambda y. x x y))\,\text{fac}\,0 \\\stackrel{\text{CBV}}{\rightarrow}(\lambda x. \text{fac} (\lambda y. x x y)) (\lambda x. \text{fac} (\lambda y. x x y))\, 0 \\\stackrel{\text{CBV}}{\rightarrow}\text{fac} (\lambda y. (\lambda x. \text{fac} (\lambda y'. x x y')) (\lambda x. \text{fac} (\lambda y. x x y')) y) \, 0 \\\stackrel{\text{CBV}} {\rightarrow}\text{fac}\,F\,0\stackrel{\text{CBV}}{\rightarrow}\text{iszero}\,0\,1\,a\text{,}$$

where the omitted term

$$a=\text{mul}\,0\, (F\,(\text{pred}\,0))$$ contains

$$F=\lambda y.(\lambda x.\text{fac}(\lambda y'.xxy'))(\lambda x.\text{fac}(\lambda y'.xxy'))\,y$$ again.

Now, $\text{iszero}\,0\stackrel{\text{CBV}}{\rightarrow}\lambda t.\lambda f.t$, s.t.

$$\text{iszero}\,0\,1\,a\stackrel{\text{CBV}}{\rightarrow}(\lambda t.\lambda f.t)\,1\,a\stackrel{\text{CBV}}{\rightarrow} (\lambda f. 1)\,a\text{.}$$

If our language had a branching construct that would ignore the $a$ branch we'd be done, but with call-by-value we have to evaluate $a$ to a value, i.e. an abstraction.

$a=\text{mul}\,0\, (F\,(\text{pred}\,0))$ and $\text{mul}\,0$ will be another abstraction so next I have to reduce $F\,(\text{pred}\,0)$.

$\text{pred}\,0\stackrel{\text{CBV}}{\rightarrow}0$, so we reduce $F\,0$.

$$F\,0 = (\lambda y.(\lambda x.\text{fac}(\lambda y'.xxy'))(\lambda x.\text{fac}(\lambda y'.xxy'))\,y)\,0 \stackrel{\text{CBV}}{\rightarrow} (\lambda x.\text{fac}(\lambda y'.xxy'))(\lambda x.\text{fac}(\lambda y'.xxy'))\,0\stackrel{\text{CBV}}{\rightarrow}\text{fac}\,F\,0$$

And now we're back at square one. Am I doing something wrong?


I don't think you're doing the reduction wrong, but the problem isn't the Z combinator. The problem is $\text{iszero}$. Branching constructs in call-by-value cannot just take the direct terms for each branch as arguments like they can in call-by-name (or similar), because both branches will be evaluated regardless of the test. This clearly interacts poorly with recursion, but it's also undesirable in general.

Instead, branching constructs in call-by-value should take explicitly delayed arguments. So something like: $$\text{iszero}\ n\ (λ\_. 1) (λ\_. \text{mul}\ n\ (f\ (\text{pred}\ n))$$ this way the recursive evaluation can be avoided unless it is actually necessary. You could, of course, leave $\text{iszero}$ as is, always use it this way, and provide an extra argument yourself, but I think normally it would be defined to expect delayed arguments.

  • $\begingroup$ Thank you, I was under the wrong impression that $Y f$ (under normal order) and $Z f$ (under call by value) should behave the same. Your solution works in my implementation. $\endgroup$
    – dlrlc
    Mar 2 '20 at 18:54

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.