λProlog

λProlog , también escrito lambda Prolog , es un lenguaje de programación lógica que incluye tipado polimórfico , programación modular y programación de orden superior . Estas extensiones de Prolog se derivan de las fórmulas hereditarias de Harrop de orden superior utilizadas para justificar los fundamentos de λProlog. La cuantificación de orden superior , los términos λ simplemente tipados y la unificación de orden superior proporcionan a λProlog el soporte básico necesario para capturar el enfoque de sintaxis de árbol λ para la 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, hay varios mecanismos declarativos disponibles para manejar ámbitos de vinculación y sus instanciaciones.

Desde 1986, λProlog ha recibido numerosas implementaciones. A fecha de 2023, el lenguaje y sus implementaciones siguen en desarrollo activo.

El demostrador de teoremas Abella ha sido diseñado para proporcionar un entorno interactivo para demostrar teoremas sobre el núcleo declarativo de λProlog.

Dos características únicas de λProlog son las implicaciones y la cuantificación universal. La implicación se utiliza para el alcance local de las definiciones de predicados, mientras que la cuantificación universal se utiliza para el alcance local de las variables, como en la siguiente implementación de `reverse` que depende de un predicado auxiliar `rev`:

revertir L K :- pi revertir \ ( revertir nil K & ( pi H \ pi T \ pi S \ revertir ( H :: T ) S :- revertir T ( H :: S ))) => revertir L nil .?- inverso [ 1 , 2 , 3 ] L .Éxito : L = 3 :: 2 :: 1 :: nil 

Un uso común de estas construcciones de alcance es simular el alcance que se observa a menudo en una presentación de una lógica mediante reglas de inferencia. Por ejemplo, la búsqueda de pruebas (y la verificación de pruebas) en la deducción natural se puede codificar de la siguiente manera:

pv Pf P :- hyp Pf P . pv ( andI P1 P2 ) ( and A B ) :- pv P1 A , pv P2 B . pv ( impI P ) ( imp A B ) :- pi p \ ( hyp p A ) => ( pv ( P p ) B ) . pv ( andE1 P ) A :- sigma B \ hyp P ( and A B ) . pv ( andE2 P ) B :- sigma A \ hyp P ( and A B ) . pv ( impE P1 P2 ) B :- sigma A \ hyp P1 ( imp A B ) , pv P2 A .?- pi p qr \ pv ( Pf p q r ) ( imp p ( imp ( y q r ) ( y ( y p q ) r ))) .Éxito : Pf = W1 \ W2 \ W3 \ impI ( W4 \ impI ( W5 \ yI ( yI W4 ( yE1 W5 )) ( yE2 W5 )))

• La paradoja de Curry#Cálculo lambda : sobre los problemas de inconsistencia causados ​​por la combinación de la lógica (proposicional) y el cálculo lambda sin tipos .
• Comparación de implementaciones de Prolog
• Sintaxis y semántica de Prolog

• Página principal de λProlog
• Entrada en el Grupo de Preservación de Software.