Termination of Z combinator with call-by-value

Question

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?

Answer 1

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.