λProlog, natively in Lean 4
LeanElpi is a clean-room Lean 4 implementation of ELPI, the extended λProlog. Write logic programs over higher-order terms, run them from the command line or inside Lean, and have the Lean kernel check the proofs they find.
What it is
A λProlog engine
Typed clauses, backtracking search, pi and => goals, and higher-order pattern unification. The dialect is ELPI 1.18, and the answers are compared against the real ELPI on a shared test corpus.
A Lean metaprogramming tool
Declare programs with elpi_program, run them with #elpi, and write tactics and commands in λProlog. Lean expressions are reflected as higher-order terms.
A certified proof search
An opt-in LF layer records a proof term for every answer, exports the signature to Lean inductives, and lets the kernel check the result as a theorem with no extra axioms.
How the solution works
#lf signatureThe engine is a small interpreter with its state in persistent data structures, so backtracking is just keeping an older version of the state. Unification variables are scoped by de Bruijn levels, which keeps unification inside the decidable pattern fragment. Everything above the engine is optional: use the engine as a library, as a command-line tool, or inside Lean. Read the architecture article for the details.
A first taste
A type checker for the simply typed λ-calculus is four lines of λProlog. Binders are handled by the logic, not by hand-written substitution:
kind tm type. kind ty type.
type app tm -> tm -> tm. type lam (tm -> tm) -> tm.
type arr ty -> ty -> ty. type nat ty.
pred of i:tm, o:ty.
of (app M N) B :- of M (arr A B), of N A.
of (lam F) (arr A B) :- pi x\ of x A => of (F x) B.Run it with lean-elpi, or inside Lean with #elpi. The getting-started chapter shows both.
Ways to use it
| Mode | You write | You get |
|---|---|---|
| Standalone | lean-elpi program.elpi -test | A λProlog interpreter and REPL |
| Library | Program.load, solve | Logic queries from ordinary Lean code |
| Inside Lean | elpi_program, #elpi, elpi_tactic | Tactics and commands written in λProlog |
| Python, Node.js, Rust | pip install leanelpi, npm install @lean-elpi/leanelpi | Load a program once and query it from your own application |
| LF layer | lf_signature, lf_certify | Proof search whose results the kernel checks |
From your own application
ctypes, koffi, extern "C"Load a program once, add clauses, and run as many queries as you like. Programs are immutable values, so adding a clause never disturbs a program that other threads are using. Install with pip install leanelpi or npm install @lean-elpi/leanelpi; Rust users add the crate and the native library. Read how it works and see the examples.
from leanelpi import Program
p = Program("pred n o:int.\nn 1.\nn 2.")
[s["X"] for s in p.solve("n X")] # ['1', '2']Why higher-order logic
Programs, proofs and formulas have binders. A logic language that understands binders can manipulate them safely, and a system that records its derivations can hand them to a trusted checker. That combination is useful whenever a learned component proposes and a symbolic one must verify. The book chapter Higher-order logic and neuro-symbolic systems makes the case.