λProlog

λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. These extensions to Prolog are derived from the higher-order hereditary Harrop formulas used to justify the foundations of λProlog. Higher-order quantification, simply typed λ-terms, and higher-order unification gives λProlog the basic supports needed to capture the λ-tree syntax approach to ''higher-order abstract syntax'', an approach to representing syntax that maps object-level bindings to programming language bindings. Programmers in λProlog need not deal with bound variable names: instead various declarative devices are available to deal with binder scopes and their instantiations.

History

Since 1986, λProlog has received numerous implementations. As of 2023, the language and its implementations are still actively being developed.

The Abella theorem prover has been designed to provide an interactive environment for proving theorems about the declarative core of λProlog.

Programming in λProlog

Two unique features of λProlog include implications and universal quantification. Implication is used for local scoping of predicate definitions while universal quantification is used for local scoping of variables, as in the following implementation of reverse depending on an auxiliary rev predicate:

reverse L K :- pi rev \
(rev nil K &
(pi H\ pi T\ pi S\ rev (H::T) S :- rev T (H::S)))
=> rev L nil.

?- reverse , 2, 3L.

Success:
L = 3 :: 2 :: 1 :: nil

A common use of these scoping constructs is to simulate scope often seen in an inference-rule presentation of a logic. For example, proof search (and proof checking) in natural deduction may be encoded as follows:

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 q r \ pv (Pf p q r) (imp p (imp (and q r) (and (and p q) r))).

Success:
Pf = W1\ W2\ W3\ impI (W4\ impI (W5\ andI (andI W4 (andE1 W5)) (andE2 W5)))

See also

* Curry's paradox#Lambda calculus — about inconsistency problems caused by combining (propositional) logic and ''untyped'' lambda calculus
* Comparison of Prolog implementations
* Prolog syntax and semantics

References

Tutorials and texts

Dale Miller
an
Gopalan Nadathur
have written the boo
''Programming with higher-order logic''
published by Cambridge University Press in June 2012.

Amy Felty
has written in a 1997 tutorial o
lambda Prolog and its Applications to Theorem Proving


John Hannan
has written a tutorial o
Program Analysis in lambda Prolog
for the 1998 PLILP Conference.

Olivier Ridoux
has written ''Lambda-Prolog de A à Z... ou presque'' (163 pages, French). It is available as tp://ftp.irisa.fr/techreports/habilitations/ridoux.ps.gz PostScriptbr>PDF
an

External links

λProlog homepage


at the Software Preservation Group.

Implementations

The Teyjus λProlog compiler
is currently the oldest implementation still being maintained. This compiler project is led b
Gopalan Nadathur
and various of his colleagues and students.

ELPI: an Embeddable λProlog Interpreter
has been developed b
Enrico Tassi
an
Claudio Sacerdoti Coen
It is implemented in OCaml and is availabl
online
The system is described in
paper
that appeared LPAR 2015. ELPI is also available as
Coq plugin
see Enrico Tassi'

on this plugin.
* Th
Abella
prover can be used to prove theorems about λProlog programs and specifications.

Prolog programming language family
Logic in computer science

{{Compu-lang-stub