# Termination of Z combinator with call-by-value

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.
• 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. Mar 2 '20 at 18:54