En lógica matemática e informática teórica , un sistema de reescritura tiene la propiedad de normalización ( fuerte ) o está terminando si cada término se normaliza fuertemente ; es decir, si cada secuencia de reescrituras termina finalmente con un término irreductible , también llamado forma normal . Un sistema de reescritura también puede tener la propiedad de normalización débil , lo que significa que para cada término, existe al menos una secuencia particular de reescrituras que eventualmente produce una forma normal, es decir, un término irreductible.
Cálculo lambda
Cálculo lambda sin tipo
El cálculo lambda puro sin tipo no satisface la propiedad de normalización fuerte, ni siquiera la propiedad de normalización débil. Considere el término. Tiene la siguiente regla de reescritura: para cualquier término,
Pero considere lo que sucede cuando aplicamos a sí mismo:
Por lo tanto, el término no se normaliza ni fuerte ni débilmente.
Cálculo lambda tipificado
Varios sistemas de mecanografiada lambda cálculo incluyendo el cálculo simplemente mecanografiado lambda , Jean-Yves Girard 's System F , y Thierry Coquand ' s cálculo de las construcciones son fuertemente normalizadora.
Un sistema de cálculo lambda con la propiedad de normalización puede verse como un lenguaje de programación con la propiedad de que cada programa termina . Aunque esta es una propiedad muy útil, tiene un inconveniente: un lenguaje de programación con la propiedad de normalización no puede ser Turing completo . [1] Eso significa que hay funciones computables que no se pueden definir en el cálculo lambda simplemente tipado (y de manera similar hay funciones computables que no se pueden computar en el cálculo de construcciones o en el Sistema F ).
Autointerpretación en el cálculo lambda tipificado
Como ejemplo, es imposible definir un auto-intérprete en cualquiera de los cálculos citados anteriormente. [2] [3]
Aquí, por "auto-intérprete" nos referimos a un programa que toma una representación del término fuente en algún formato simple (como una cadena de caracteres) y devuelve una representación del término normalizado correspondiente. Este resultado de imposibilidad no es válido para otras definiciones de "auto-intérprete". Por ejemplo, algunos autores se han referido a funciones de tipo como auto-intérpretes, donde es el tipo de representaciones de -Términos escritos. Para evitar confusiones, nos referiremos a estas funciones como autorreconocimientos . Brown y Palsberg demostraron que los autorreconocimientos pueden definirse en varios lenguajes fuertemente normalizados, incluidos System F y System F ω . [4] Esto resultó ser posible porque los tipos de términos codificados que se reflejan en los tipos de sus representaciones impiden construir un argumento diagonal . En su artículo, Brown y Palsberg afirman refutar la "sabiduría convencional" de que la autointerpretación es imposible (y se refieren a esta misma página de Wikipedia como un ejemplo de la sabiduría convencional), pero lo que en realidad refutan es la imposibilidad de autointerpretación. reconocedores, un concepto completamente diferente. En su trabajo de seguimiento, cambian a la terminología más específica de "autorreconocimiento" que usamos aquí, distinguiéndolos notablemente de los "autoevaluadores", del tipo. [5] También reconocen que implementar la autoevaluación parece más difícil que el autorreconocimiento, y dejan la implementación de la primera en un lenguaje fuertemente normalizador como un problema abierto.
Ver también
Notas
- ^ Universidad de Rochester
- ^ Conor McBride (mayo de 2003), "sobre la terminación" (publicado en la lista de correo de Haskell-Cafe).
- ^ Andrej Bauer (junio de 2014), Respuesta a: Un lenguaje total que solo un lenguaje completo de Turing puede interpretar (publicado en el sitio Theoretical Computer Science StackExchange )
- ^ Matt Brown y Jens Palsberg. 2016. Rompiendo la barrera de la normalización: un auto-intérprete para f-omega. En Actas del 43º Simposio Anual ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación (POPL '16). Association for Computing Machinery, Nueva York, NY, EE. UU., 5–17. DOI: https://doi.org/10.1145/2837614.2837623
- ^ Matt Brown y Jens Palsberg. 2017. Autoevaluación mecanografiada mediante funciones de tipo intensional. En Actas del 44 ° Simposio ACM SIGPLAN sobre principios de lenguajes de programación (POPL 2017). Association for Computing Machinery, Nueva York, NY, EE. UU., 415–428. DOI: https://doi.org/10.1145/3009837.3009853
Referencias
- Baader, Franz ; Nipkow, Tobias (1999). Término reescrito y todo eso . Prensa de la Universidad de Cambridge. ISBN 0-521-77920-0. 316 páginas.