Sintaxis abstracta de orden superior

Este artículo incluye una lista de referencias generales , pero carece de suficientes citas en línea correspondientes . Por favor, ayude a mejorar este artículo introduciendo citas más precisas. ( Agosto de 2010 ) ( Aprenda cómo y cuándo eliminar este mensaje )

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

Una sintaxis abstracta es abstracta porque está representada por objetos matemáticos que tienen cierta estructura por su propia naturaleza. Por ejemplo, en los árboles de sintaxis abstracta de primer orden ( FOAS ), como se usan comúnmente en los compiladores , la estructura del árbol implica la relación de subexpresión, lo que significa que no se requieren paréntesis para desambiguar los programas (como lo son, en la sintaxis concreta ). HOAS expone una estructura adicional: la relación entre las variables y sus sitios de enlace. En las representaciones FOAS, una variable generalmente se representa con un identificador, y la relación entre el sitio de enlace y el uso se indica mediante el uso del mismo identificador. Con HOAS, no hay un nombre para la variable; cada uso de la variable se refiere directamente al sitio de enlace.

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

Un objeto matemático que podría utilizarse para implementar HOAS es un gráfico en el que las variables se asocian con sus sitios de enlace mediante aristas . Otra forma popular de implementar HOAS (en, por ejemplo, compiladores) es con índices de De Bruijn .

El primer lenguaje de programación que admitió directamente enlaces λ en la sintaxis fue el lenguaje de programación lógica de orden superior λProlog . ^[1] El artículo que introdujo el término HOAS ^[2] utilizó el código λProlog para ilustrarlo. Desafortunadamente, cuando uno transfiere el término HOAS del entorno de programación lógica al de programación funcional , ese término implica la identificación de enlaces en la sintaxis con funciones sobre expresiones. En este último entorno, 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 el entorno de programación lógica. ^{[3] [4]} Si bien es diferente en detalle, el tratamiento de los enlaces en λProlog es similar a su tratamiento en los marcos lógicos, que se detalla en la siguiente sección.

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

Por ejemplo, el marco lógico LF tiene una construcción λ, que tiene un tipo de flecha (→). Como ejemplo, supongamos que queremos 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 : tipo . var : tipo . v : var -> exp . let : var -> exp -> exp -> exp .                   

Aquí, expse muestra el tipo de todas las expresiones y varel tipo de todas las variables integradas (implementadas quizás como números naturales , lo cual no se muestra). 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 construcciones let de la forma let <var> = <exp> in <exp>: acepta una variable, una expresión (que está limitada por la variable) y otra expresión (dentro de la cual está limitada la variable).

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

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

En esta representación, las variables de nivel de objeto no aparecen explícitamente. La constante lettoma una expresión (que se está vinculando) y una función de nivel meta 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 nivel meta cuando se aplica. Como ejemplo concreto, construiríamos la expresión de nivel de objeto

 Sea x = 1 + 2 en x + 3         

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

 sea ​​( más 1 2 ) ([ y ] más y 3 )       

¿Dónde [y] eestá la sintaxis de Twelf para la función ?${\displaystyle \lambda ye}$

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

La sintaxis abstracta de orden superior generalmente solo es aplicable cuando las variables del lenguaje objeto pueden entenderse como variables en el sentido matemático (es decir, como sustitutos de miembros arbitrarios de algún dominio). Esto sucede a menudo, pero no siempre: por ejemplo, no hay ventajas que se puedan obtener 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.

• Tipo de datos algebraicos generalizados
• Sintaxis abstracta paramétrica de orden superior (PHOAS)

• J. Despeyroux; A. Felty; A. Hirschowitz (1995). "Sintaxis abstracta de orden superior en Coq". Cálculos Lambda tipificados y aplicaciones. Apuntes de clase en informática. Vol. 902. págs. 124–138. doi :10.1007/BFb0014049. ISBN. 978-3-540-59048-4. Archivado desde el original el 30 de agosto de 2006.
• Martin Hofmann (1999). Análisis semántico de la sintaxis abstracta de orden superior. 14.º Simposio anual IEEE sobre lógica en informática . pág. 204. ISBN 0-7695-0158-3.
• Eli Barzilay; Stuart Allen (2002). Reflexión de la sintaxis abstracta de orden superior en Nuprl (PDF) . Demostración de teoremas en lógica de orden superior 2002. págs. 23–32. ISBN 3-540-44039-9. Archivado desde el original (PDF) el 11 de octubre de 2006.
• Eli Barzilay (2006). Un evaluador autohospedado que utiliza HOAS (PDF) . Taller ICFP sobre Scheme y programación funcional 2006.