<p><code>S(C(KM)M)I ~ MM</code> suffices</p>
<p>The reduction is as follows:</p>
<pre><code>S(C(KM)M)Ix
C(KM)Mx(Ix)
C(KM)Mxx
KMxMx
MMx
</code></pre>

CC BY-SA 4.0
2021-12-06T19:11:22.137Z
2021-12-06T19:11:22.137Z
dspyz
<p>For convenience I'm using using the combinators SKIBCMTV</p>
<p>I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form:</p>
<p><code>KI ~ B(KI)(MM)</code></p>
<p>And it's possible to have a WHNF-term extensionally equivalent to one with no WHNF</p>
<p><code>BI(MM) ~ MM</code></p>
<p>But I'm having trouble finding examples of a normal form term which is extensionally equivalent to a term with no WHNF</p>
<hr />
<p>Here the combinators are:</p>
<pre><code>Sxyz = xz(yz)
Kxy = x
Ix = x
Bxyz = x(yz)
Cxyz = xzy
Mx = xx
Txy = yx
Vxyz = zxy
</code></pre>
<hr />
<p>Normal form means every combinator in the term is at most partially applied (is being passed fewer arguments than appear in its definition)</p>
<p>WHNF only means that the left-most combinator in the term is at most partially applied</p>
<p>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</p>
<p>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</p>

CC BY-SA 4.0
2021-12-06T14:33:32.860Z
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...).
Damiano Mazza
CC BY-SA 4.0
2021-12-06T16:03:11.997Z
@DamianoMazza I added some definitions. Could you take another look? Thanks
dspyz
<lambda-calculus><normalization><universal-turing-machines>
Can a normal form term be extensionally equivalent to a term with no WHNF?
dspyz
# Can a normal form term be extensionally equivalent to a term with no WHNF?

(Asked by: username_0 on 2021-12-06)

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

**Tags:** lambda-calculus, normalization, universal-turing-machines

> **Comments:**
> **username_1**: 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...).  
> **username_0**: @DamianoMazza I added some definitions. Could you take another look? Thanks  

---

## 1 answers

### Answer by username_0 on 2021-12-06. Score: 3 | Accepted answer

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


---

