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.

• dlrlc: 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.