λProlog , también escrito lambda Prolog , es un lenguaje de programación lógica que presenta tipado polimórfico , programación modular y programación de orden superior . Estas extensiones de Prolog se derivan de las fórmulas de Harrop hereditarias de orden superior utilizadas para justificar los fundamentos de λProlog. De orden superior cuantificación , simplemente mecanografiado lambda-términos , y de orden superior unificación da λProlog los soportes básicos necesarios para capturar el enfoque sintaxis λ-árbol de sintaxis abstracta de orden superior, un enfoque para representar la sintaxis que asigna enlaces a nivel de objeto a enlaces de lenguaje de programación. Los programadores en λProlog no necesitan lidiar con nombres de variables vinculadas: en su lugar, varios dispositivos declarativos están disponibles para lidiar con ámbitos de enlace y sus instancias.
Paradigma | Programación lógica |
---|---|
Diseñada por | Dale Miller y Gopalan Nadathur |
Apareció por primera vez | 1987 [1] |
Disciplina de mecanografía | fuertemente tipado |
Licencia | Licencia pública general GNU v3 |
Sitio web | www |
Implementaciones importantes | |
Teyjus, ELPI | |
Influenciado por | |
Prólogo | |
Influenciado | |
Makam |
Historia
Desde 1986, λProlog ha recibido numerosas implementaciones. A partir de 2013, el lenguaje y sus implementaciones aún se están desarrollando activamente.
El demostrador del teorema de Abella ha sido diseñado para proporcionar un entorno interactivo para demostrar teoremas sobre el núcleo declarativo de λProlog.
Ver también
- Paradoja de Curry # Cálculo lambda : sobre los problemas de inconsistencia causados por la combinación de lógica (proposicional) y cálculo lambda sin tipo
Referencias
- ^ "Preguntas frecuentes: ¿Qué implementaciones de lambda Prolog están disponibles?" . www.lix.polytechnique.fr . Consultado el 16 de diciembre de 2019 .
Tutoriales y textos
- Dale Miller y Gopalan Nadathur han escrito el libro Programación con lógica de orden superior , publicado por Cambridge University Press en junio de 2012.
- Amy Felty escribió en 1997 un tutorial sobre lambda Prolog y sus aplicaciones a la demostración de teoremas ([Archivado por WebCite https://www.webcitation.org/5WpO4HGEh?url=http://www.site.uottawa.ca/~afelty /dist/lprolog97.ps ]).
- John Hannan ha escrito un tutorial sobre Análisis de programas en lambda Prolog para la Conferencia PLILP de 1998.
- Olivier Ridoux ha escrito Lambda-Prolog de A à Z ... ou presque (163 páginas, francés). Está disponible como PostScript , PDF y html .
enlaces externos
- λPágina de inicio de Prolog
- Entrada en el Grupo de Preservación de Software.
Implementaciones
- El compilador Teyjus λProlog es actualmente la implementación más antigua que aún se mantiene. [1] Este proyecto de compilación está dirigido por Gopalan Nadathur y varios de sus colegas y estudiantes.
- ELPI: Enrico Tassi y Claudio Sacerdoti Coen han desarrollado un intérprete de λProlog incrustable . Está implementado en OCaml y está disponible en línea . El sistema se describe en un artículo que apareció LPAR 2015.
- El comprobador de Abella se puede utilizar para demostrar teoremas sobre los programas y especificaciones de λProlog.
- ^ Nadathur, Gopalan; Dustin Mitchell (1999). Descripción del sistema: Teyjus - Un compilador y una implementación de máquina abstracta basada en lambda Prolog . Conferencia sobre Deducción Automatizada . LNAI. 1632 . págs. 287-291. doi : 10.1007 / 3-540-48660-7_25 . ISBN 978-3-540-66222-8.