The definition of the Church numerals in combinatory logic

295 Views Asked by At

Hindley & Seldin define ([1] Definition 4.2, p. 48) the Church numerals as follows: (I'm paraphrasing to save space. Here's the original page.)

For every $n \in \{0,1,\dots\}$, the Church numeral for $n$ is $$ \overline{n} := (SB)^n(KI) $$ where we used the abbreviations $$ \begin{align} X^nY &:= \underset{n}{\underbrace{X(X(\dots(X}}Y))) \\ B &:= S(KS)K \end{align} $$

They proceed to claim (ibid. Note 4.4, p. 48) that $\overline{n} = [x,y].x^ny$ for all $n\neq 1$.

I don't see why this claim holds. For instance, when $n=2$ we have $$ \begin{align} [x,y].x^ny &= [x].\Big([y].\big(x(xy)\big)\Big) \\ &= [x].\Big(S\big([y].x\big)\big([y].(xy)\big)\Big) \\ &= [x].\big(S(Kx)x\big) \\ &= S\Big([x].\big(S(Kx)\big)\Big)([x].x) \\ &= S\Big(S([x].S)\big([x].(Kx)\big)\Big)I \\ &= S\big(S(KS)K\big)I \\ &= SBI \\ &= (SB)^1I \\ &\neq (SB)^2(KI) \\ &= \overline{n} \end{align} $$

I checked the textbook's official errata list, but this is not listed there.

What am missing?


[1] J. Roger Hindley & Jonathan P. Seldin. (2008) Lambda-Calculus and Combinators - An Introduction. Cambridge University Press.

1

There are 1 best solutions below

5
On

The following step isn't correct:

$$(SB)^1I \ne (SB)^2(KI)$$

because $(SB)Iab = a(ab)$ and $SB(SB(KI))ab = a(ab)$ using $Bxyz = x(yz)$.

An alternative (more straightforward) check that doesn't require the deduction thm transform you are using:

$$\begin{align} % \bar{2}fx &= (SB)^2(KI)fx \\ % &= SB(SB(KI))fx \\ % &= Bf(SB(KI)f)x \\ % &= f(SB(KI)fx) \\ % &= f(Bf(KIf)x) \\ % &= f(f(KIfx)) \\ % &= f(f(Ix)) \\ % &= f(fx) \\ % \end{align}$$