Lenguajes de programación con funciones canónicas.

29

¿Hay algún lenguaje de programación (funcional) donde todas las funciones tengan una forma canónica? Es decir, cualquiera de las dos funciones que devuelven los mismos valores para todo el conjunto de entrada se representa de la misma manera, por ejemplo, si f (x) devolvió x + 1 yg (x) devolvió x + 2, entonces f (f (x) )) yg (x) generarían ejecutables indistinguibles cuando se compila el programa.

Quizás lo más importante, ¿dónde / cómo podría encontrar más información sobre la representación canónica de los programas (buscar en Google "programas de representación canónica" ha sido menos que fructífero)? Parece una pregunta natural, y me temo que simplemente no sé el término apropiado para lo que estoy buscando. Tengo curiosidad por saber si es posible que dicho lenguaje sea completo, y si no, qué tan expresivo puede ser un lenguaje de programación, mientras se conserva esa propiedad.

Mi experiencia es bastante limitada, por lo que preferiría fuentes con menos requisitos previos, pero las referencias a fuentes más avanzadas también pueden ser geniales, ya que de esa manera sabré hacia lo que quiero trabajar.

math4tots
fuente

Respuestas:

38

La medida en que esto es posible es en realidad una pregunta abierta importante en la teoría del cálculo lambda. Aquí hay un resumen rápido de lo que se sabe:

  • El cálculo lambda de tipo simple con unidad, productos y espacio de funciones tiene una propiedad de formas canónicas simples. Dos términos son iguales si y solo si tienen la misma forma beta-normal, eta-larga. Calcular estas formas normales también es bastante sencillo.

  • La adición de tipos de suma complica mucho las cosas. El problema de la igualdad aún es decidible (la palabra clave para buscar es "igualdad de coproductos"), pero los algoritmos conocidos funcionan por razones extremadamente difíciles y, que yo sepa, no existe un teorema de forma normal totalmente satisfactorio. Aquí están los cuatro enfoques que conozco:

  • La adición de tipos ilimitados, como los números naturales, hace que el problema sea indecidible. Básicamente, ahora puede codificar el décimo problema de Hilbert.

  • La adición de la recursividad hace que el problema sea indecidible, porque tener formas normales hace que la igualdad sea decidible, y eso le permitiría resolver el problema de detención.

Neel Krishnaswami
fuente
Este documento extiende la equivalencia con los coproductos a la equivalencia con sumas, pero no existe una sintaxis de forma canónica "única", usted elige una "función de saturación" que es lo suficientemente inteligente como para detectar cuándo los dos términos que está comparando tienen subterms que demuestran ser falsos. Es más similar a Ahmed-Licata-Harper en que ambos usan el enfoque.
Max New
Con solo unidades, productos y funciones, la cardinalidad de cualquier cosa que puedas escribir es 1, mientras que si agregas sumas, de repente obtienes muchas cardinalidades diferentes (y puedes hacer "cálculos útiles"). ¿Están relacionados estos hechos?
glaebhoerl
1
siλX:si.λy:si.XλX:si.λy:si.yson formas normales diferentes, pero (b) no afecta a ninguno de los algoritmos que conozco.
Neel Krishnaswami