# How to check an implementation of call-by-need is correct?

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"
"echo"
> (two two id id) 1
1


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

• 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. – alim Jan 13 '18 at 6:44
• @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). – ljedrz Jan 13 '18 at 10:18
• 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. – alim Jan 13 '18 at 10:25
• @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. – ljedrz Jan 13 '18 at 10:30
• 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, – alim Jan 14 '18 at 9:54