Resolver ecuaciones funcionales para funciones desconocidas en cálculo lambda

¿Hay alguna técnica para resolver ecuaciones funcionales para funciones desconocidas en el cálculo lambda?

Supongamos que tengo la función de identidad definida extensivamente como tal:

$I x = x$

(es decir, escribiendo una ecuación para el comportamiento esperado de esa función) y ahora quiero resolverlo por haciendo alguna transformación algebraica para obtener la fórmula intensional para esa función:$I$

$I = \lambda x.x$

que indica cómo hace exactamente la función lo que se esperaba (es decir, cómo implementarla en el cálculo lambda).

Por supuesto, la función de identidad se usa solo como ejemplo. Estoy interesado en métodos más generales para resolver tales ecuaciones. En particular, me gustaría encontrar una función que satisfaga el siguiente requisito:$B$

$B\;f\;(\lambda x.M) = (\lambda x.f M)$

es decir, "inyecta" la función dada en la función lambda dada antes de su "cuerpo" (que es una expresión lambda arbitraria), posiblemente separándola y construyendo una nueva, para que se convierta un parámetro al que se aplica la función .( λ x . M ) M $f$$(\lambda x.M)$$M$$f$

Este es un problema conocido, conocido como unificación de orden superior .

Desafortunadamente, este problema es indecidible en general. Hay un fragmento decidible, conocido como Fragmento de Patrón de Miller. Se usa ampliamente, entre otras cosas, para la verificación de tipos de programas de tipo dependiente con metavariables o coincidencia de patrones. Este fragmento es donde las variables de unificación se aplican solo a distintas variables del programa enlazado.

Este documento proporciona un excelente tutorial sobre cómo funciona la unificación de orden superior y explica su implementación (relativamente) simple.

Desafortunadamente, no parece que su función se encuentre en este fragmento de patrón. Dicho esto, lo que estoy viendo es bastante similar a la composición de funciones. ¿La siguiente función satisface su propiedad?

$B = \lambda f\ g\ x\ \ldotp f\ (g\ x)$

Tenemos:

• $B\ f\ (\lambda x . M)$
• $= B\ f\ (\lambda y . [y/x]M)$ por -equivalencia$\alpha$
• $= \lambda x . f\ ((\lambda y. [y/x]M) x)$
• $= \lambda x . f\ ([x/y][y/x]M)$
• $= \lambda x . f\ M$

Creo que tengo una respuesta parcial, con respecto a la ecuación con la función de identidad:

$I x = x$

Queremos resolverlo encontrando la fórmula para , que tendrá la forma con alguna expresión aún desconocida como su cuerpo. Vamos a sustituirlo por en la ecuación original:( λ p . M ) M $I$$(\lambda p.M)$$M$$I$

$(\lambda p.M)\; x = x$

luego aplique la función a en el lado izquierdo:$x$

$M[p/x] = x$

¿Pero qué tenemos aquí? :> Esta ecuación es la fórmula para la expresión que estamos buscando, después de sustituir cada aparición de en ella con , y dice que después debería verse como el lado derecho :) En otras palabras, la función buscamos es:p $M$$p$$x$

$I = (\lambda x.x)$

cuál por supuesto es la respuesta correcta :)

Probemos el mismo enfoque para encontrar la fórmula del combinador de . Queremos que funcione de tal manera que, cuando se aplique a sí mismo, se produzca aplicado a sí mismo:$\omega$

$\omega\;\omega = \omega\;\omega$

Ahora vamos a encontrar la fórmula para , que es de la forma por alguna expresión aún desconocido . Sustituyendo esto en la ecuación obtenemos:( λ x . M ) $\omega$$(\lambda x.M)$$M$

$(\lambda x.M)\;\omega = \omega\;\omega$

Al aplicarlo al parámetro en el lado izquierdo se obtiene la fórmula para :$M$

$M [x/\omega] = \omega\;\omega$

Esto dice que después de sustituir cada aparición de en con , produjo , por lo que podemos deducir que la expresión original antes de la sustitución debería haber sido , por lo que la función que estábamos buscando debería se parece a esto:M ω $x$$M$$\omega$M $\omega\;\omega$$M$$x\;x$

$\omega = (\lambda x.x\;x)$

que es el caso :)

Sin embargo, tengo la sensación de que podría ser tan fácil solo porque el lado derecho ya estaba en la forma que estamos buscando.