Mostrar que no existe $F$ tal que $F(MN) = M$ para todo $M$ y $N.

Question

Esto es para el Ejercicio 2.4.6 de "Cálculo Lambda - Su Sintaxis y Semántica" de Barengredt y la declaración exacta del libro es "Demostrar que $\neg \ \exists \ F \ \forall \ MN \ F(MN) = M$".

Mi solución es la siguiente, y me preguntaba si hay algo mal en ella:

Supongamos que existiera tal $F$. Entonces, sea $G \equiv \lambda x . F(xI)$. Así, para cualquier $N$, tenemos que \begin{align} GN = F(NI) = N \tag{1} \end{align}

Pero por la $\beta$-conversión, $G$ puede reescribirse como $G \equiv \lambda x.F(xI) = \lambda x.F((\lambda y. yI) x)$. Ahora, por el Teorema del Punto Fijo, hay algún $X$ que es el punto fijo de $\lambda y. yI$, y así $$ GX = F ((\lambda y.yI) X) = FX $$ Ahora, apliquemos $F$ a ambos lados: \begin{align} G = F(GX) = F(FX) = F\tag{2} \end{align}

Esto significa que para cualquier $N$, \begin{align*} N \stackrel{(1)}{=} GN = G(IN) \stackrel{(2)}{=} F(IN) = I \end{align*} Ahora esto muestra que $F(MN)\ \# \ M$.

(El $I$ anterior es simplemente la función identidad).

Answer 1

Esto parece estar bastante bien, pero es excesivamente complicado. La $\beta$-equivalencia es una congruencia, por lo que si $X=_\beta Y$ entonces $FX=_\beta FY$. Es bastante obvio que la hipotética $F$ viola esta congruencia. Puedes producir rápidamente un contraejemplo encontrando $M$, $M'$, $N$ y $N'$ de manera que $MN=_\beta M'N'$ pero $M\neq_\beta M'$. En tu prueba esto ocurre cuando muestras $G=F$, aunque luego necesitas demostrar que $G$ no puede ser $F$. Podrías elegir ejemplos mucho más mundanos y directos, por ejemplo $M=\lambda x.I$, $M'=I$ y $N=N'=I$. En ese caso tendrías $MN=_\beta I=_\beta M'N'$ pero $M\neq_\beta M'$.

Incluso si comenzamos de la manera en que lo haces, inmediatamente tenemos $G=\lambda x.x$ desde el primer paso. Luego una vez que haces la expansión $\beta$, inmediatamente obtienes $G=\lambda x.\lambda y.yI$ que claramente no es la función identidad. Este es otro claro ejemplo de cómo este término hipotético viola la congruencia. No es necesario hablar sobre el Teorema del Punto Fijo. Parece que estás evitando aplicar la equivalencia hipotética bajo un lambda, pero a menos que haya alguna convención implícita de que $M$ y $N$ tienen que ser términos cerrados, no hay razón para eso.