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

Question

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?

Answer 1

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.