λProlog and LeanElpi: a short book

A hands-on introduction to λProlog, to its implementation in Lean 4, and to why higher-order logic matters for neuro-symbolic systems. Read it in order, or jump to the chapter you need.

1. Why λProlog
   What λProlog adds to Prolog, and where ELPI and LeanElpi fit.
2. Getting started
   Install LeanElpi and run a first program, standalone and inside Lean.
3. Terms, clauses and search
   Facts, rules, unification, backtracking, cut and arithmetic.
4. Higher-order programming
   Binders as data, pi and implication goals, and pattern unification.
5. Types and modes
   Declaring kinds, types and predicates, and what input and output modes mean.
6. Constraints and CHR
   Delayed goals, suspended unification, and constraint handling rules.
7. Using it standalone
   The lean-elpi command, the REPL, include paths, fuel, and ELPI source files.
8. Using it inside Lean
   Programs, queries, quotations, tactics and commands written in λProlog.
9. Sharing types between Lean and λProlog
   Declare a data type, a function or an inductive type on one side and use it on the other, and what Coq-Elpi taught us about doing so.
10. Certified proof search with LF
    The LF layer: signatures, proof terms, export to Lean, and kernel-checked certificates.
11. Higher-order logic and neuro-symbolic systems
    Why binders, hypotheses and checkable derivations matter when learned and symbolic parts meet.
12. From Python, Node.js and Rust
    Load ELPI programs and run queries from Python, Node.js or Rust through one native library. How it works, how to install it, how to use it.