evaluador metacircular

Esta parte se basa en la Sección 3.2.4 de la tesis de Danvy. ^{[ 9 ]}

Aquí está el núcleo de un autoevaluador para el${\displaystyle \lambda }$cálculo. La sintaxis abstracta del${\displaystyle \lambda }$El cálculo se implementa de la siguiente manera en OCaml , representando las variables con su índice de De Bruijn , es decir, con su desplazamiento léxico (que comienza en 0):

término de tipo = IND de int (* índice de Bruijn *) | ABS de plazo | APP de término * término

El evaluador utiliza un entorno:

tipo valor = FUN de ( valor -> valor )let rec eval ( t : term ) ( e : value list ) : value = match t with IND n -> List . nth e n | ABS t' -> FUN ( fun v -> eval t' ( v :: e )) | APP ( t0 , t1 ) -> apply ( eval t0 e ) ( eval t1 e ) and apply ( FUN f : value ) ( a : value ) = f alet main ( t : term ) : value = eval t []

Los valores (de tipo value) combinan valores expresables (el resultado de evaluar una expresión en un entorno) y valores denotables (los valores denotados por variables en el entorno), una terminología que se debe a Christopher Strachey . ^{[ 10 ] [ 11 ]}

Los entornos se representan como listas de valores denotables.

El evaluador principal tiene tres cláusulas:

• Asigna una variable (representada con un índice de De Bruijn) al valor del entorno actual en dicho índice.
• Este proceso asigna una función sintáctica a una función semántica. (Aplicar una función semántica a un argumento se reduce a evaluar el cuerpo de la función sintáctica correspondiente en su entorno léxico, ampliado con el argumento).
• Convierte una aplicación sintáctica en una aplicación semántica.

Este evaluador es compositivo, ya que cada una de sus llamadas recursivas se realiza sobre una subparte propia del término dado. Además, es de orden superior, puesto que el dominio de valores es un espacio de funciones.

En "Intérpretes Definicionales", Reynolds respondió a la pregunta de si un auto-intérprete de este tipo está bien definido. Su respuesta fue negativa, ya que la estrategia de evaluación del lenguaje definido (el lenguaje fuente) está determinada por la estrategia de evaluación del lenguaje definitorio (el metalenguaje). Si el metalenguaje sigue el principio de paso por valor (como OCaml), el lenguaje fuente también lo sigue. Si el metalenguaje sigue el principio de paso por nombre (como Algol 60 ), el lenguaje fuente igualmente lo sigue. Y si el metalenguaje sigue el principio de paso por necesidad (como Haskell ), el lenguaje fuente igualmente lo sigue.

En "Intérpretes Definicionales", Reynolds definió con precisión un auto-intérprete al hacerlo independiente de la estrategia de evaluación de su lenguaje definitorio. Fijó la estrategia de evaluación transformando el auto-intérprete en un estilo de paso de continuaciones , que es independiente de la estrategia de evaluación, como se recoge posteriormente en los Teoremas de Independencia de Gordon Plotkin . ^{[ 12 ]}

Además, debido a que aún no se habían descubierto las relaciones lógicas , Reynolds hizo que el evaluador resultante que pasa la continuación fuera de primer orden mediante (1) la conversión a cierre y (2) la desfuncionalización de la continuación.

Señaló la «cualidad de máquina» del intérprete resultante, que es el origen de la máquina CEK ya que la transformación CPS de Reynolds era para llamada por valor. ^{[ 13 ]} Para llamada por nombre, estas transformaciones mapean el auto-intérprete a una instancia temprana de la máquina de Krivine . ^{[ 14 ]} La máquina SECD y muchas otras máquinas abstractas pueden derivarse entre sí de esta manera. ^{[ 15 ] [ 16 ]}

Es notable que las tres máquinas abstractas más famosas para la${\displaystyle \lambda }$El cálculo se corresponde funcionalmente con el mismo autointérprete.

Los lenguajes de programación totalmente funcionales que son fuertemente normalizadores no pueden ser Turing completos , de lo contrario se podría resolver el problema de la parada comprobando si el programa cumple con la verificación de tipos. Esto significa que hay funciones computables que no se pueden definir en el lenguaje total. ^{[ 17 ]} En particular, es imposible definir un autointérprete en un lenguaje de programación total, por ejemplo, en cualquiera de los cálculos lambda tipados , como el cálculo lambda simplemente tipado , el Sistema F de Jean-Yves Girard o el cálculo de construcciones de Thierry Coquand . ^{[ 18 ] [ 19 ]} Aquí, por "autointérprete" entendemos un programa que toma una representación de un 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 se cumple para otras definiciones de "autointérprete". Por ejemplo, algunos autores se han referido a funciones de tipo${\displaystyle \pi \,\tau \to \tau }$como autointérpretes, donde${\displaystyle \pi \,\tau }$es el tipo de representaciones de${\displaystyle \tau }$términos tipificados. Para evitar confusiones, nos referiremos a estas funciones como autorreconocedores . Brown y Palsberg demostraron que los autorreconocedores podían definirse en varios lenguajes fuertemente normalizadores, incluidos el Sistema F y el Sistema F _ω . ^{[ 20 ]} Esto resultó ser posible porque los tipos de términos codificados que se reflejan en los tipos de sus representaciones impiden la construcción de 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 Wikipedia como un ejemplo de la sabiduría convencional), pero lo que realmente refutan es la imposibilidad de los autorreconocedores, un concepto distinto. En su trabajo posterior, cambian a la terminología más específica de "autorreconocedor" utilizada aquí, distinguiéndolos notablemente de los "autoevaluadores", de tipo${\displaystyle \pi \,\tau \to \pi \,\tau }$. ^{[ 21 ]} 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.