ΛProlog

{{Short description|Computer programming language}} {{Lowercase title}} {{More citations needed|date=November 2025}} {{Infobox programming language | name = λProlog | logo =  | logo caption = | screenshot =  | screenshot caption = | paradigm = [[Logic programming]] | family = | designers = Dale Miller and Gopalan Nadathur | developer =  | released = 1987<ref>{{Cite web|url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/faq/implementations.html|title=FAQ: What implementations of lambda Prolog are available?|website=www.lix.polytechnique.fr|access-date=2019-12-16}}</ref> | latest release version = | latest release date =  | latest preview version = | latest preview date =  | typing = strongly typed | scope = | programming language = | discontinued = | platform = | operating system = | license = [[GPL|GNU General Public License]] v3 | file ext = | file format =  | website = {{url|http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/}} | implementations = Teyjus, ELPI | dialects = | influenced by = [[Prolog]] | influenced = Makam }}

'''λ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 formula]]s used to justify the foundations of λProlog. [[Higher-order logic|Higher-order quantification]], [[Typed lambda calculus|simply typed λ-term]]s, and [[Unification (computing)#Higher-order unification|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: <syntaxhighlight lang="elpi"> 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 [1, 2, 3] L.

Success: L = 3 :: 2 :: 1 :: nil </syntaxhighlight> 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: <syntaxhighlight lang="elpi"> 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))) </syntaxhighlight>

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

==References== {{Reflist}} ===Tutorials and texts=== *[http://www.lix.polytechnique.fr/Labo/Dale.Miller/ Dale Miller] and [http://www-users.cs.umn.edu/~gopalan/ Gopalan Nadathur] have written the book [https://sites.google.com/site/proghol/ ''Programming with higher-order logic''], published by Cambridge University Press in June 2012. * [http://www.site.uottawa.ca/~afelty/ Amy Felty] has written in a 1997 tutorial on [http://www.site.uottawa.ca/~afelty/dist/lprolog97.pdf lambda Prolog and its Applications to Theorem Proving]. * [http://www.cse.psu.edu/~hannan/ John Hannan] has written a tutorial on [http://www.cse.psu.edu/~hannan/papers/plilp-tutorial.ps.gz Program Analysis in lambda Prolog] for the 1998 PLILP Conference. * [http://www.irisa.fr/prive/ridoux/ Olivier Ridoux] has written ''Lambda-Prolog de A à Z... ou presque'' (163 pages, French). It is available as [ftp://ftp.irisa.fr/techreports/habilitations/ridoux.ps.gz PostScript], [https://web.archive.org/web/20220108003853/ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf PDF], and [http://www.irisa.fr/lande/ridoux/LPAZ/lpaz_html.html html].

==External links== * [http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/ λProlog homepage] * [http://www.softwarepreservation.org/projects/prolog/index.html#Lambda Entry] at the Software Preservation Group.

===Implementations=== * [http://teyjus.cs.umn.edu/ The Teyjus λProlog compiler] is currently the oldest implementation still being maintained.<ref>{{cite book|last=Nadathur|first=Gopalan|author2=Dustin Mitchell|title=System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda Prolog|journal=Conference on Automated Deduction|year=1999|volume=1632|series=LNAI|pages=287–291|doi=10.1007/3-540-48660-7_25|isbn=978-3-540-66222-8}}</ref> This compiler project is led by [http://www-users.cs.umn.edu/~gopalan/ Gopalan Nadathur] and various of his colleagues and students. * [https://github.com/LPCIC/elpi ELPI: an Embeddable λProlog Interpreter] has been developed by [http://www-sop.inria.fr/members/Enrico.Tassi/ Enrico Tassi] and [http://www.cs.unibo.it/~sacerdot/ Claudio Sacerdoti Coen]. It is implemented in OCaml and is available [https://github.com/LPCIC/elpi online]. The system is described in a [https://hal.inria.fr/hal-01176856/ paper] that appeared LPAR 2015. ELPI is also available as a [https://github.com/LPCIC/coq-elpi Coq plugin]: see Enrico Tassi's [https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html tutorial] on this plugin. * The [http://abella-prover.org/ Abella] prover can be used to prove theorems about λProlog programs and specifications.

{{DEFAULTSORT:Lambda prolog}} [[Category:Prolog programming language family]] [[Category:Logic in computer science]]