Cómo demostrar que una función es un combinador de punto fijo

OK, cambiemos las variables para mantener las cosas cuerdas y mostrar:

eZ = Z (eZ)

Tenga en cuenta que ninguna de las reglas reintroduce una ‘e’ o una ‘s’, por lo que tendremos que obtener alguna expresión que sea solo ‘b’, ‘w’ y ‘Z’. Comience con el lado izquierdo:

Z (eZ) = Z (s (bwb) (bwb) Z) por definición de e

Ahora con f = bwb, g = bwb, x = Z aplicamos la definición de s para obtener

Z (eZ) = Z ((bwb) Z ((bwb) Z))

y si arreglamos eso basado en la asociatividad izquierda:

Z (eZ) = Z (bwbZ (bwbZ))

Tomando el lado izquierdo, los mismos pasos nos dan

eZ = s (bwb) (bwb) Z)
eZ = bwbZ (bwbZ)

Ahora aplique la regla ‘b’ al lado izquierdo de la expresión con f = w, g = b, x = Z

eZ = w (bZ) (bwbZ)

Entonces podemos aplicar la regla ‘w’ con h = (bZ), x = (bwbZ) y obtener

eZ = (bZ) (bwbZ) (bwbZ)

Finalmente ‘b’ nuevamente con f = Z, g = (bwbZ), x = (bwbZ)

eZ = Z (bwbZ (bwbZ)) = Z (eZ)

que es lo que queríamos

La parte más dolorosa aquí es el seguimiento de la asociatividad izquierda, ya que no he hecho cálculo lambda en años. 🙂 Me pareció útil escribir sfgx = fx (gx) como ((sf) g) x = (fx) (gx) etc. para asegurarme de que el patrón coincidía correctamente.