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.