Sintaxis abstracta de orden superior - Higher-order abstract syntax

En informática , la sintaxis abstracta de orden superior (abreviado HOAS ) es una técnica para la representación de árboles de sintaxis abstracta para lenguajes con carpetas variables .

Relación con la sintaxis abstracta de primer orden

Un árbol de sintaxis abstracta es abstracto porque es un objeto matemático que tiene cierta estructura por su propia naturaleza. Por ejemplo, en los árboles de sintaxis abstracta de primer orden ( FOAS ), como se usa comúnmente en los compiladores , la estructura de árbol implica la relación de subexpresión, lo que significa que no se requieren paréntesis para eliminar la ambigüedad de los programas (como están, en la sintaxis concreta ). HOAS expone una estructura adicional: la relación entre las variables y sus sitios de unión. En las representaciones de FOAS, una variable se representa típicamente con un identificador, y la relación entre el sitio de unión y el uso se indica utilizando el mismo identificador. Con HOAS, no hay nombre para la variable; cada uso de la variable se refiere directamente al sitio de unión.

Hay varias razones por las que esta técnica es útil. Primero, hace que la estructura de enlace de un programa sea explícita: así como no hay necesidad de explicar la precedencia del operador en una representación de FOAS, no es necesario tener a mano las reglas de enlace y alcance para interpretar una representación de HOAS. En segundo lugar, los programas que son alfa-equivalentes (que solo difieren en los nombres de las variables vinculadas) tienen representaciones idénticas en HOAS, lo que puede hacer que la verificación de equivalencia sea más eficiente.

Implementación

Un objeto matemático que podría usarse para implementar HOAS es un gráfico donde las variables están asociadas con sus sitios de unión a través de bordes . Otra forma popular de implementar HOAS (en, por ejemplo, compiladores) es con índices de Bruijn .

Uso en programación lógica

El primer lenguaje de programación que soportó directamente enlaces λ en la sintaxis fue el lenguaje de programación lógica de orden superior λProlog . El artículo que introdujo el término HOAS utilizó el código λProlog para ilustrarlo. Desafortunadamente, cuando se transfiere el término HOAS de la programación lógica al ajuste de programación funcional, ese término implica la identificación de enlaces en sintaxis con funciones sobre expresiones. En este último escenario, HOAS tiene un sentido diferente y problemático. El término sintaxis de árbol λ se ha introducido para referirse específicamente al estilo de representación disponible en la configuración de programación lógica. Si bien es diferente en detalle, el tratamiento de las vinculaciones en λProlog es similar a su tratamiento en los marcos lógicos, elaborado en la siguiente sección.

Uso en marcos lógicos

En el dominio de los marcos lógicos , el término sintaxis abstracta de orden superior se utiliza generalmente para referirse a una representación específica que utiliza los enlaces del metalenguaje para codificar la estructura de enlace del lenguaje objeto .

Por ejemplo, el marco lógico LF tiene una construcción λ, que tiene el tipo de flecha (→). Como ejemplo, considere que queríamos formalizar un lenguaje muy primitivo con expresiones sin tipo, un conjunto de variables incorporado y una construcción let ( let <var> = <exp> in <exp'>), que permite vincular variables varcon definición expen expresiones exp'. En la sintaxis de Twelf , podríamos hacer lo siguiente: 

exp : type.
var : type.
v : var -> exp.
let : var -> exp -> exp -> exp.

Aquí expestá el tipo de todas las expresiones y varel tipo de todas las variables integradas (implementadas quizás como números naturales, que no se muestran). La constante vactúa como una función de conversión y atestigua el hecho de que las variables son expresiones. Finalmente, la constante letrepresenta las construcciones let de la forma let <var> = <exp> in <exp>: acepta una variable, una expresión (que está vinculada por la variable) y otra expresión (dentro de la cual está vinculada la variable).

La representación HOAS canónica del mismo lenguaje de objeto sería: 

exp : type.
let : exp -> (exp -> exp) -> exp.

En esta representación, las variables a nivel de objeto no aparecen explícitamente. La constante lettoma una expresión (que se está vinculando) y una función de meta-nivel exp→ exp (el cuerpo del let). Esta función es la parte de orden superior : una expresión con una variable libre se representa como una expresión con huecos que se rellenan con la función de metanivel cuando se aplica. Como ejemplo concreto, construiríamos la expresión a nivel de objeto 

let x = 1 + 2
in x + 3

(asumiendo los constructores naturales para números y suma) usando la firma HOAS anterior como 

let (plus 1 2) ([y] plus y 3)

donde [y] ees la sintaxis de Twelf para la función .

Esta representación específica tiene ventajas más allá de las anteriores: por un lado, al reutilizar la noción de enlace de meta-nivel, la codificación disfruta de propiedades como la sustitución de conservación de tipos sin la necesidad de definirlas / probarlas. De esta manera, el uso de HOAS puede reducir drásticamente la cantidad de código repetitivo que tiene que ver con el enlace en una codificación.

La sintaxis abstracta de orden superior generalmente solo es aplicable cuando las variables del lenguaje de objetos pueden entenderse como variables en el sentido matemático (es decir, como sustitutos de miembros arbitrarios de algún dominio). Este es a menudo, pero no siempre, el caso: por ejemplo, no se pueden obtener ventajas de una codificación HOAS de alcance dinámico como aparece en algunos dialectos de Lisp porque las variables de alcance dinámico no actúan como variables matemáticas.

Ver también

Referencias

Otras lecturas