# Can a normal form term be extensionally equivalent to a term with no WHNF?

For convenience I'm using using the combinators SKIBCMTV

I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form:

KI ~ B(KI)(MM)

And it's possible to have a WHNF-term extensionally equivalent to one with no WHNF

BI(MM) ~ MM

But I'm having trouble finding examples of a normal form term which is extensionally equivalent to a term with no WHNF

Here the combinators are:

Sxyz = xz(yz)
Kxy = x
Ix = x
Bxyz = x(yz)
Cxyz = xzy
Mx = xx
Txy = yx
Vxyz = zxy


Normal form means every combinator in the term is at most partially applied (is being passed fewer arguments than appear in its definition)

WHNF only means that the left-most combinator in the term is at most partially applied

A term can be reduced to normal form or WHNF if, by using the reduction rules above, it can be rewritten as a normal form or WHNF term respectively

Two terms are extensionally equivalent if, after tacking some number of free variables on the right side, they can both be reduced to the same thing

• Could you expand on the following points, please? 1) What do you mean by "extensionally equivalent". 2) What do you mean by weak head normal form (in the $\lambda$-calculus, usually "weak" means "not reducing under $\lambda$s", but there are no $\lambda$s in combinators, so...). Dec 6 '21 at 14:33
• @DamianoMazza I added some definitions. Could you take another look? Thanks Dec 6 '21 at 16:03

S(C(KM)M)I ~ MM suffices
S(C(KM)M)Ix