5
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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...). $\endgroup$ Dec 6 '21 at 14:33
  • $\begingroup$ @DamianoMazza I added some definitions. Could you take another look? Thanks $\endgroup$
    – dspyz
    Dec 6 '21 at 16:03
3
$\begingroup$

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

The reduction is as follows:

S(C(KM)M)Ix
C(KM)Mx(Ix)
C(KM)Mxx
KMxMx
MMx
$\endgroup$

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.