Un cálculo Lambda para funciones invertibles (computables r-Turing)

19

Estoy interesado en el concepto de "integridad de r-Turing", según lo definido por Axelsen y Glück (2011) . Un sistema está completo en T-ruring si puede calcular el mismo conjunto de funciones que una máquina de Turing reversible, sin producir ningún dato "basura". Esto es lo mismo que poder calcular todas las funciones que son (a) computables y (b) inyectivas.

Me gustaría explorar computacionalmente el espacio de las funciones inyectables computables. Para hacer esto, estoy buscando el lenguaje de programación reversible "más mínimo", algo que pueda desempeñar el papel equivalente para la computabilidad de r-Turing que el cálculo lambda juega para la computabilidad de Turing.

Sé que hay muchos lenguajes reversibles que las personas han desarrollado y demostrado que son completos. Sin embargo, estos se están desarrollando con aplicaciones prácticas en mente, por lo que sus autores se concentran en darles características expresivas en lugar de hacerlas mínimas.

¿Alguien sabe si se ha descrito un lenguaje invertible tan mínimo, o si hay alguna investigación en esa dirección? Soy bastante nuevo en la literatura sobre este tema, por lo que fácilmente podría haberlo pasado por alto. Alternativamente, ¿alguien tiene alguna idea de cómo se podría crear dicho lenguaje?

A continuación se muestra un resumen de lo que estoy buscando. No sé si se puede crear modificando el cálculo lambda en sí, o si habría que usar un tipo de lenguaje completamente diferente.

  • Lenguaje completo de r-Turing: calcula todas las funciones invertibles computables y solo puede calcular funciones invertibles
  • Sintaxis y semántica lo más mínima posible. (Por ejemplo, el cálculo Lambda solo tiene definiciones de funciones y aplicaciones, y nada más.) No es necesario que la sintaxis o la semántica estén relacionadas con las del cálculo lambda, aunque podrían serlo.
  • Programa = datos. Es decir, los programas operan con expresiones en lugar de cualquier otro tipo de datos. Esto garantiza que la salida de un programa siempre se pueda interpretar como un programa. Esto probablemente implica que tiene que ser un estilo de lenguaje funcional más que imperativo.
  • Hay alguna forma sistemática de convertir un programa en su inverso, que no implica sustancialmente más cómputo que el involucrado en la realización del cómputo inverso. (No todos los idiomas invertibles tienen esta propiedad, pero algunos sí).

Debo enfatizar que el enfoque de Axelsen y Glück para la computación reversible es bastante diferente del enfoque conocido debido a Bennett, donde un programa (en general no invertible) se vuelve invertible al devolver cierta información sobre el historial de la computación junto con la salida. La integridad de r-Turing se trata de poder calcular funciones inyectivas sin ninguna salida adicional. Hay varias cosas llamadas variaciones del "cálculo lambda reversible" que son reversibles en el sentido de Bennet; no es lo que estoy buscando.

Nathaniel
fuente
r-Turing complete parece una definición relativamente nueva y sería útil ver una prueba de que no es lo mismo que Turing complete y las interpretaciones / análisis de otros autores que aquellos que introdujeron el concepto (y enlaces no pay-per-view si posible)
vzn

Respuestas:

4

No estoy muy familiarizado con el área, pero hay algunos trabajos recientes de la comunidad de lenguajes de programación que podrían interesarle, basados ​​en la idea de restringir a un lenguaje de isomorfismos de tipo. En particular, podrías echar un vistazo a

así como varias publicaciones relacionadas que puede encontrar en el sitio web de Amr Sabry .

Noam Zeilberger
fuente