Doce

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 .

En su forma más simple, un programa Twelf (llamado "firma") es una colección de declaraciones de familias de tipos (relaciones) y constantes que habitan en esas familias de tipos. Por ejemplo, la siguiente es la definición estándar de los números naturales, con el zoperador que representa el cero y sel operador sucesor.

nat : tipo .  z : nat . s : nat -> nat .      

Aquí nathay un tipo, y zy sson términos constantes. Como sistema de tipado dependiente , los tipos se pueden indexar por términos, lo que permite la definición de familias de tipos más interesantes. Aquí hay una definición de adición:

más : nat -> nat -> nat -> tipo .        plus_zero : { M: nat } más M z M .      plus_succ : { M: nat } { N: nat } { P: nat } más M ( s N ) ( s P ) <- más M N P .               

La familia de tipos plusse lee como una relación entre tres números naturales M, Ny P, tales que M + N = P. A continuación, damos las constantes que definen la relación: la constante plus_zeroindica que M + 0 = M. El cuantificador {M:nat}se puede leer como "para todos Mlos de tipo 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 se puede entender operativamente como :-, 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 la constante plus_succ("cuando se da un término de tipo plus M N P, devuelve un término de tipo plus M (s N) (s P)").

Twelf cuenta con reconstrucción de tipos y admite parámetros implícitos, por lo que en la práctica, generalmente no es necesario escribir explícitamente {M:nat}(etc.) arriba.

Estos ejemplos simples no muestran las características de orden superior de LF ni ninguna de sus capacidades de verificación de teoremas. Consulte la distribución Twelf para ver los ejemplos incluidos.

Las firmas de Twelf se pueden ejecutar mediante un procedimiento de búsqueda. Su núcleo es más sofisticado que Prolog , ya que es de orden superior y de tipado dependiente, pero está restringido a operadores puros: no hay corte ni otros operadores extralógicos (como los que se utilizan para realizar E/S ) como los que se encuentran a menudo en las implementaciones de Prolog, lo que puede hacerlo 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 de Harrop hereditarias , que permiten nociones operativas lógicamente bien fundadas de generación de nombres nuevos y extensión con alcance de la base de datos de cláusulas.

Twelf se utiliza hoy principalmente 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 suelen desarrollarse a mano. A pesar de esto, para los dominios de problemas en los que destaca, las pruebas Twelf suelen ser más cortas y más fáciles de desarrollar que en los sistemas automatizados de propósito general.

La noción de enlace y sustitución incorporada de Twelf facilita la codificación de lenguajes de programación y lógicas, la mayoría de los cuales hacen uso de enlaces y sustitución, que a menudo se pueden codificar directamente a través de la sintaxis abstracta de orden superior (HOAS), donde los enlaces del metalenguaje representan los enlaces a nivel de objeto. Por lo tanto, los teoremas estándar como la sustitución que preserva el tipo y la conversión alfa son "gratuitos".

Twelf se ha utilizado para formalizar muchos lenguajes de programación y lógica diferentes (se incluyen ejemplos con la distribución). Entre los proyectos más grandes se encuentran una prueba de seguridad para ML estándar , ^[2] un sistema de lenguaje ensamblador tipado fundamental de CMU, ^[3] y un sistema de código portador de pruebas fundamental de Princeton.

Twelf está escrito en ML estándar y los binarios están disponibles para Linux y Windows. A partir de 2006 ^[actualizar], se encuentra en desarrollo activo, principalmente en la Universidad Carnegie Mellon. ^{[ Necesita actualización ]}

• Lista de asistentes de prueba

• Sitio web oficial , Wiki