I implemented call-by-need evaluation of untyped $\lambda$-terms. I run it with the following inputs

$ (((2 \, 2) \lambda x.x) \lambda x.x )$

$ (((3 \, 3) \lambda x.x) \lambda x.x )$

$ (((4 \, 4) \lambda x.x) \lambda x.x )$

All these reduced to $\lambda x.x$, so I believe it works correctly. However, I want to make sure of it.

I also tried terms like $(2 \, 2)$, but such terms are not reduced completely, so not easy to see if the result is correct. Also, I could not find any $\lambda$-evolution tool with call-by-need to make a comparison.

Is there a way that I can produce a completely reduced church numeral? By applying some terms to (3 3) thus it forces 3 3 to completely reduced under call-by-need?

When (3 3) is computed, it ends up with a term which has redex under an abstraction. So, what I am asking is how can I force it to reduce all redex?

I tried $\lambda x.x ( 3 \, 3)$, that still end up with a term redex under an abstraction.

Any idea?


In a pure setting, call-by-need should produce the same results as call-by-name.

I'm assuming in your notation e.g. $(2\, 2)$ describes two Church numerals applied to each other. In that case yes, your term is equivalent to $2\, 2\, I\, I$ (where $I$ is the identity combinator), since lambda calculus application is left-associative, and should reduce with call-by-need order to $λx.x$.

You can verify this e.g. with the following Haskell (which is call-by-need) code e.g. under GHCI or some other Haskell REPL:

> two = \f -> \x -> f (f x)
> (((two two) id) id) "echo"
> (two two id id) 1

The same applies to $(3\, 3)$, $(4\, 4)$ etc.

  • $\begingroup$ In my encoding, call-by-name and call-by-need did not end up at the same for inputs such as (2 2). Call-by-name stopped with not evaluating some redex under abstraction, call-by-need also stopped with un-evaluated redex under abstractions and there are thunks shared. So, the results are not the same syntactically, but as I check they are the same terms actually. I tried (2 2 id id) n, (3 3 id id) n ...., all produced n. It seems these are best example to show it computes correctly. I was hoping there are different inputs with certain results. $\endgroup$ – alim Jan 13 '18 at 6:44
  • 1
    $\begingroup$ @alim I have tested these terms with my own reductor and with call-by-name order they also reduce to $id$. The final result will be the same, but call-by-need should have less reduction steps (depending on the kind of memoization you implemented). $\endgroup$ – ljedrz Jan 13 '18 at 10:18
  • $\begingroup$ These inputs should be reduced to identify function are also reduced correctly to identify functions in my implementation, both call-by-name, and call-by-value. but these such as (2 2) or (3 3) have different outputs. $\endgroup$ – alim Jan 13 '18 at 10:25
  • $\begingroup$ @alim ah, you mean (2 2) or (3 3) as the whole expression? Those will not fully reduce: (2 2) will end up with λa.(λb.λc.b (b c)) ((λb.λc.b (b c)) a), (3 3) with λa.(λb.λc.b (b (b c))) ((λb.λc.b (b (b c))) ((λb.λc.b (b (b c))) a)) etc. You need a different reduction strategy to be able to reduce them further. $\endgroup$ – ljedrz Jan 13 '18 at 10:30
  • 2
    $\begingroup$ Thanks for the discussion. I think since arguments are shared in call-by-need, it is natural to have a different result from call-by-name because these shared parts are not exactly $\lambda$-terms. In call-by-name, it is pure lambda terms, not other constructions. At least, in my implementation, that is the case, $\endgroup$ – alim Jan 14 '18 at 9: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.