Hispanopedia WikiTwelf 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 de los lenguajes de programación .
Introducció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 pertenecen a esas familias de tipos. Por ejemplo, la siguiente es la definición estándar de los números naturales, donde zrepresenta el cero y sel operador sucesor.
nat : tipo .z : nat . s : nat -> nat .Aquí nattenemos un tipo, y zy sson términos constantes. Como sistema de tipos dependientes , los tipos pueden indexarse por términos, lo que permite definir familias de tipos más interesantes. Aquí tenemos una definición de suma:
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, tal 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}puede leerse como "para todos Mlos de tipo nat".
La constante plus_succdefine el caso en que el segundo argumento es el sucesor de algún otro número N(véase 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 operacionalmente como el de Prolog :-, o como implicación lógica ("si M + N = P, entonces M + (s N) = (s P)"), o de forma más fiel 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)").
Doce características de reconstrucción de tipo y admite parámetros implícitos, por lo que en la práctica, normalmente no es necesario escribir explícitamente {M:nat}(etc.) arriba.
Estos sencillos 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 Twelf para ver los ejemplos incluidos.
Usos
Programación lógica
Twelf puede ejecutarse mediante un procedimiento de búsqueda. Su núcleo es más sofisticado que Prolog , ya que es de orden superior y con tipado dependiente, pero se limita a operadores puros: no hay operadores de corte ni otros operadores extralógicos (como los de E/S ) 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, al igual que λProlog , Twelf generaliza las cláusulas de Horn a fórmulas de Harrop hereditarias , que permiten nociones operacionales lógicamente bien fundamentadas de generación de nombres nuevos y extensión de ámbito de la base de datos de cláusulas.
Formalización de las matemáticas
Actualmente, Twelf se utiliza principalmente como sistema para formalizar las matemáticas, en especial la metateoría de los lenguajes de programación . En este sentido, guarda una estrecha relación con Rocq e Isabelle / HOL / HOL Light . Sin embargo, a diferencia de estos sistemas, las demostraciones en Twelf suelen desarrollarse manualmente. A pesar de ello, en los ámbitos en los que destaca, las demostraciones en Twelf suelen ser más breves y fáciles de desarrollar que en los sistemas automatizados de propósito general.
La noción integrada de enlace y sustitución de Twelf facilita la codificación de lenguajes de programación y lógicas, la mayoría de las cuales utilizan estos conceptos. A menudo, esto se puede codificar directamente mediante sintaxis abstracta de orden superior (HOAS), donde los enlazadores del metalenguaje representan los enlazadores a nivel de objeto. De este modo, teoremas estándar como la sustitución que preserva el tipo y la conversión alfa se obtienen de forma automática.
Twelf se ha utilizado para formalizar diversas lógicas y lenguajes de programación (se incluyen ejemplos con la distribución). Entre los proyectos más importantes se encuentran una prueba de seguridad para Standard ML , [ 2 ] un sistema fundamental de lenguaje ensamblador tipado de CMU, [ 3 ] y un sistema fundamental de código portador de pruebas de Princeton.
Implementación
Twelf está escrito en Standard ML y existen binarios disponibles para Linux y Windows. A partir de 2006Se encuentra en fase de desarrollo activo, principalmente en la Universidad Carnegie Mellon.
Véase también
Referencias
- ↑ Pfenning, Frank; Carsten Schürmann (julio de 1999). Descripción del sistema: Twelf - un marco metalógico para sistemas deductivos (PDF) . Actas de la 16.ª Conferencia Internacional sobre Deducción Automatizada (CADE-16) . Consultado el 8 de mayo de 2019 .
- ↑ 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 .
- ↑ Crary, Karl (2003). Hacia un lenguaje ensamblador tipado fundamental (PDF) . Actas del Simposio de 2003 sobre los principios de los lenguajes de programación . Recuperado el 8 de febrero de 2007 .
Enlaces externos
- Sitio web oficial , Wiki
- Lenguajes con tipado dependiente
- Lenguajes de programación lógica
- Sistemas de software para la demostración de teoremas
- teoría de tipos
- Lógica en informática