Algoritmos de inversión de programas para programas de orden superior.

El término inversión de programa tiene múltiples matices de significado, pero probablemente comenzó con el trabajo de J. McCarthy de 1956 La inversión de las funciones definidas por las máquinas de Turing en el contexto de la IA. Hasta ahora se han descubierto muchas conexiones entre la inversión del programa y otros campos, por ejemplo, programación reversible (física y lógica), evaluación parcial, verificación, programación bidireccional, programación lógica y aprendizaje automático.

¿Qué es la inversión del programa? En primera aproximación es algo como esto: Dado un programa tomar argumentos de tipo A y devolver resultados de tipo B , producir un programa de P - 1 que es "de alguna manera" el inverso de P . Estoy deliberadamente siendo vago aquí, ya que el concepto se puede (y se) aclara de varias maneras: por ejemplo, ¿se requiere que P sea ​​inyectable? En caso de que P - 1 ( b ) devuelva todo o solo algo a tal que P ( a ) = $P : A \rightarrow B$$A$$B$$P^{-1}$$P$$P$$P^{-1}(b)$$a$$P(a) = b$?

Hay formas genéricas de invertir un programa, por ejemplo, utilizando la diagonalización como ya señaló McCarthy, o utilizando una evaluación parcial, pero tienden a no ser eficientes. Además, la mayoría del trabajo sobre inversión de programas con el que estoy familiarizado no parece tratar con lenguajes de programación completos de orden superior (es decir, cálculos ).$\lambda$

Solicitud de referencia. ¿Cuál es el estado de la técnica en algoritmos explícitos para la inversión de programas decálculos λ (sin restricción en el orden superior)?$\lambda$

No ha habido una gran cantidad de trabajo en este espacio, pero lo que hay es bastante interesante.

1. Torben Mogensen ha trabajado en este problema. Aquí hay dos documentos suyos.

   El primer documento proporciona un algoritmo para programas funcionales de primer orden, y el segundo lo extiende a un orden superior. La caracterización precisa de cuándo este algoritmo tendrá éxito se deja para el trabajo futuro.

   • Semi-inversión de ecuaciones guardadas
   • Semiinversión de parámetros funcionales

2. Tetsuo Yokoyama, Holger Bock Axelsen y Robert Glück.

   Esto describe el lenguaje de programación RFun, que invierte los programas funcionales de primer orden, pero impone restricciones de inyectividad y determinismo hacia atrás que aseguran que la evaluación hacia atrás sea tan rápida como hacia adelante. (Han escrito una serie de otros documentos sobre este tema, que he tenido problemas para conseguir).

   • Hacia un lenguaje funcional reversible.

3. Stefan Bohne y Baltasar Trancón Widemann.

   ¡Este es un papel realmente bueno! Observa que (a) puede construir una categoría donde los morfismos son funciones emparejadas con su inversa (para cualquier noción particular de inversa que esté usando), y (b) esta categoría tiene una estructura compacta de daga. Esto significa que puede escribir un programa con una disciplina de tipo lineal ligeramente funky, y luego leer las interpretaciones hacia adelante y hacia atrás de la semántica.

   Dan un lenguaje funcional con una sintaxis bastante salvaje: las expresiones casi arbitrarias se pueden usar como patrones, y la reversibilidad lo hace sensible.

   • Un enfoque para la programación funcional reversible generalizada

4. Francesco Tiezzia, Nobuko Yoshida

   No he leído este, pero solo lo descubrí cuando busqué en Google los otros documentos. Teniendo en cuenta los autores y el tema, ¡sospecho que esto está en tu callejón!

   • Cálculo reversible basado en sesiones