Twelf es una implementación del marco lógico LF desarrollado por Frank Pfenning y Carsten Schürmann en la Universidad Carnegie Mellon . [1] Se utiliza para la programación lógica y para la formalización de la teoría del lenguaje de programación.
Introducción [ editar ]
En su forma más simple, un programa Twelf (llamado "firma") es una colección de declaraciones de familias de tipos y constantes que habitan esas familias de tipos. Por ejemplo, la siguiente es la definición estándar de los números naturales , con el zcero y sel operador sucesor.
nat : tipo . z : nat . s : nat -> nat .Aquí nathay un tipo, y zy sson términos constantes. Como sistema de tipificación dependiente , los tipos se pueden indexar por términos, lo que permite la definición de familias de tipos más interesantes (relaciones). Aquí hay una definición de suma:
más : nat -> nat -> nat -> tipo . plus_zero : { M: nat } plus M z M . plus_succ : { M: nat } { N: nat } { P: nat } plus M ( s N ) ( s P ) <- plus M N P .La familia de tipos plusse lee como una relación entre tres números naturales M, Ny P, tal que M + N = P. Luego damos las constantes que definen la relación: plus_zeroindica que cualquier número natural Mmás cero es todavía M. El cuantificador {M:nat}se puede leer como "para todo Mtipo nat".
La constante plus_succdefine el caso en el que el segundo argumento es el sucesor de algún otro número N(ver coincidencia de patrones ). El resultado es el sucesor de P, donde Pes la suma de My N. Esta llamada recursiva se realiza a través del subobjetivo plus M N P, introducido con <-. La flecha puede entenderse operativamente como Prolog's :-, o como implicación lógica ("si M + N = P, entonces M + (s N) = (s P)"), o más fielmente a la teoría de tipos, como el tipo de constante plus_succ("cuando se le da un término de tipo plus M N P, devuelve un término de tipo plus M (s N) (s P)").
Twelf presenta la reconstrucción de tipos y admite parámetros implícitos, por lo que en la práctica no es necesario escribir explícitamente {M:nat}(etc.) arriba.
Estos simples ejemplos no muestran las características de orden superior de LF, ni ninguna de sus capacidades de verificación de teoremas. Consulte la distribución de Twelf para ver los ejemplos incluidos.
Usos [ editar ]
Twelf se usa de varias formas diferentes.
Programación lógica [ editar ]
Las firmas Twelf se pueden ejecutar mediante un procedimiento de búsqueda, por lo que Twelf se puede utilizar como lenguaje de programación lógica . Su núcleo es más sofisticado que Prolog , ya que es de orden superior y se escribe de forma dependiente, pero está restringido a operadores puros: no hay cortes ni otros operadores extralógicos (como los que se utilizan para realizar E / S ) como se encuentran a menudo en Prolog implementaciones, lo que puede hacer que sea menos adecuado para aplicaciones prácticas de programación lógica. Algunos usos de la regla de corte de Prolog se pueden obtener declarando que ciertos operadores pertenecen a familias de tipos deterministas, lo que evita el recálculo. Además, como λProlog , Twelf generaliza las cláusulas de Horn a fórmulas hereditarias de Harrop., que permiten nociones operativas lógicamente bien fundamentadas de generación de nombres nuevos y extensión de alcance de la base de datos de cláusulas.
Formalización de las matemáticas [ editar ]
Twelf se utiliza principalmente hoy en día como un sistema para formalizar las matemáticas (especialmente la metateoría de los lenguajes de programación ). Como tal, está estrechamente relacionado con Coq e Isabelle / HOL / HOL Light . Sin embargo, a diferencia de esos sistemas, las pruebas Twelf se desarrollan típicamente a mano. A pesar de esto, para los dominios de problemas en los que sobresale, las pruebas de Twelf son a menudo más breves y fáciles de desarrollar que en los sistemas automatizados de propósito general.
Twelf se adapta particularmente bien a la codificación de lenguajes de programación y lógicas, porque tiene una noción incorporada de enlace y sustitución. La mayoría de los lenguajes de programación y lógicas de interés utilizan la vinculación y la sustitución. Cuando se implementan en Twelf, los aglutinantes a menudo se pueden codificar directamente utilizando la técnica de sintaxis abstracta de orden superior (HOAS), en la que los aglutinantes del metalenguaje (Twelf) se utilizan para representar los aglutinantes a nivel de objeto. Como consecuencia, los teoremas estándar como la sustitución con conservación de tipos y la conversión alfa vienen "gratis".
Twelf se ha utilizado para formalizar muchas lógicas y lenguajes de programación diferentes (se incluyen ejemplos con la distribución). Entre los proyectos más grandes se encuentran una prueba de seguridad para el lenguaje de programación ML estándar , [2] un sistema de lenguaje ensamblador mecanografiado fundamental de CMU, [3] y un sistema de código portador de prueba fundamental de Princeton.
Implementación [ editar ]
Twelf está escrito en ML estándar y hay binarios disponibles para Linux y Microsoft Windows . A partir de 2006, [actualizar]se encuentra en desarrollo activo (principalmente en la Universidad Carnegie Mellon ).
Referencias [ editar ]
- ^ Pfenning, Frank; Carsten Schürmann (julio de 1999). Descripción del sistema: Twelf - un marco meta-lógico para sistemas deductivos (PDF) . Actas de la XVI Conferencia Internacional sobre Deducción Automatizada (CADE-16) . Consultado el 8 de mayo de 2019 . CS1 maint: parámetro desalentado ( enlace )
- ^ Lee, Daniel; Karl Crary; Robert Harper (enero de 2007). Hacia una metateoría mecanizada del ML estándar (PDF) . Actas del Simposio de 2007 sobre los principios de los lenguajes de programación . Niza , Francia . Consultado el 8 de febrero de 2007 . CS1 maint: parámetro desalentado ( enlace )
- ^ Crary, Karl (2003). Hacia un lenguaje ensamblador mecanografiado fundamental (PDF) . Actas del Simposio de 2003 sobre los principios de los lenguajes de programación . Consultado el 8 de febrero de 2007 . CS1 maint: parámetro desalentado ( enlace )
Enlaces externos [ editar ]
- Wiki el Proyecto Twelf
