La definición de los numerales de la Iglesia en lógica combinatoria

Question

Hindley & Seldin definen ([1] Definición 4.2, p. 48) los numerales eclesiásticos de la siguiente manera: (Parafraseo para ahorrar espacio. Aquí es la página original).

Por cada $n \in \{0,1,\dots\}$ el número de la Iglesia para $n$ i $$\overline{n} := (SB)^n(KI)$$ donde utilizamos el ab $$\begin{align} X^nY &:= \underset{n}{\underbrace{X(X(\dots(X}}Y))) \\ B &:= S(KS)K \end{align}$$

Proceden a afirmar (ibid. Nota 4.4, p. 48) que $\overline{n} = [x,y].x^ny$ para todos $n\neq 1$ .

No veo por qué se sostiene esta afirmación. Por ejemplo, cuando $n=2$ tenemos $$\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}$$

He comprobado el libro de texto oficial lista de erratas pero no aparece en la lista.

¿Qué me falta?

---

[1] J. Roger Hindley y Jonathan P. Seldin. (2008) Lambda-Calculus y combinadores - Introducción . Cambridge University Press.

Answer 1

El siguiente paso no es correcto:

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

porque $(SB)Iab = a(ab)$ et $SB(SB(KI))ab = a(ab)$ utilizando $Bxyz = x(yz)$ .

Una comprobación alternativa (más sencilla) que no requiere la deducción thm transform que está utilizando:

$$\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}$$