A little book of higher-order logic
The Little Elpier
Higher-Order Logic, Types and λProlog, One Question at a Time
Volodymyr Pavlyshyn
Most programs are recipes. Do this, then this, then loop until that. A logic program is something else: a list of things that are true, and a way to ask what follows from them. You do not tell the computer how to find the answer. You tell it what you know, and you ask.
Open access The PDF and EPUB are free under CC BY 4.0. Read it, share it, and buy a copy if it helps you.
What eats a fly? Ask the pond.
A logic program is a list of things that are true, and running it is asking a question. This small book teaches that idea from zero, in the question-and-answer style of The Little Schemer: short questions on the left, short answers on the right, one idea at a time.
- Facts, questions, rules and recursion, with a pond of eight critters and who eats whom.
- What the engine really does: unification and search, drawn as trees.
- Lists, Peano numbers, and relations that run backwards.
- Types, predicates passed as values, and lambdas.
- The two ideas that make λProlog higher-order: pi and =>.
- A finale: a type checker for a little language in seven clauses, which also infers types.
Every chapter ends with graded exercises, with room to write in the paperback, and a dot-grid notes page for drawing search trees. Every example runs on lean-elpi, from Python with one pip install, and every solution is in the book.
Written for students who have never taken a logic course. No mathematics or prior Prolog needed.
9 chapters, 541 questions, 11 Maxims, and four graded exercises at the end of every chapter, each with a worked solution that runs.
A gate to neurosymbolic AI
Neurosymbolic AI joins two kinds of system. A neural model, such as a large language model, is fluent and fast, and it guesses. A symbolic system reasons from facts and rules: it can say why an answer follows, and it can say no. Together, the model proposes and the logic checks.
The symbolic half is a logic program, and this book teaches it from zero. Each idea in it is one that half is built from:
- Facts and rules
Knowledge written down, so an answer comes from what is stated, not from a guess. - Unification and search
How an answer is derived, step by step, so it can be explained. - Types
A checker that turns away ill-formed input before it runs, such as a malformed fact a model proposes. - Predicates as values and lambdas
Rules and queries as data that a program can build and pass around. piand=>
Reasoning under assumptions, "suppose this were true", without changing what is known.- A type checker as a logic program
The shape of a verifier: a set of rules that says yes or no, and runs both ways.
The book itself stays in the pond: there is no language model in it, and it asks for nothing but some programming. It is the gate. Beyond it are lean-elpi's chapter on higher-order logic and neuro-symbolic systems, and the author's other books: Logic for Agents gives an AI agent a logic layer that checks what a language model proposes, and Bulletproof Knowledge goes into Lean 4, where facts come with proofs.
Free to read. Worth buying.
The Little Elpier is open access. The PDF and the EPUB are free under the Creative Commons Attribution 4.0 license: read them, share them, print them for a class, as long as you credit the author.
A book like this takes months to write. If it helps you, please buy a copy. It pays for the work, and for the next book.
Buy it and support the work
Leanpub: PDF and EPUB, with every future update free.
Amazon: the Kindle edition.
Pavlyshyn, V. (2026).
The Little Elpier: Higher-Order Logic, Types and λProlog, One Question at a Time. Zenodo.
https://doi.org/10.5281/zenodo.23864702
Read it the way the book reads
Each page is two columns: a question on the left, its answer on the right. Cover the answers, try each question, then look. Here are two sections of Chapter 1.
Facts
What is eats frog fly?
A fact. It says that the frog eats flies.
How do we know it is a fact?
It ends with a dot and has no conditions. It does not say "if" anything. It is true because the file says so.
What are frog and fly?
Constants. Each one is the name of one thing in the pond.
And eats?
A predicate: the name of a relation between things. eats relates an eater to its food.
Is eats fly frog the same fact as eats frog fly?
No. Order matters. The first place is the eater, the second is the food. eats fly frog would say the fly eats the frog, which would be news to the frog.
Is eats fly frog in the pond?
No.
Where are the parentheses?
There are none. Many languages would write eats(frog, fly). λProlog writes the predicate, then its arguments, separated by spaces. Parentheses are only for grouping, as we will see in Chapter 3.
How many arguments does eats take?
Two.
Are there predicates with one argument?
Yes:
pred swims o:critter.
swims frog.
swims fish.
swims duck.
swims otter.
pred flies o:critter.
flies fly.
flies heron.
flies duck.
pred plant o:critter.
plant algae.A one-argument predicate says something about one thing: the frog swims, the heron flies.
How many eats facts are in the pond?
Eleven. Here they are as a picture.
eats X Y; the arrow points at the food.What eats nothing?
The algae. No fact starts with eats algae.
What does nothing eat?
The heron and the otter. No fact ends with heron or otter. They are at the top.
The file is a list of things we say are true. That is all a fact is. Nothing in the program checks that frogs really eat flies; the program believes the file. If we wrote eats fly heron, it would believe that too.
Questions
How do we ask a question?
Start lean-elpi without -test. The file ask.elpi only loads the pond:
lean-elpi ask.elpi -I ../libIt prints ?- and waits. Type a question, end it with a dot, and press Enter.
What do we get if we ask eats frog fly.?
We typed the question, then n:
eats frog fly.
nand lean-elpi answered:
?- Success:
More? (y/N) ?-Success means yes: the pond says so.
What is More? (y/N)?
The engine offering to look for another answer. For a yes-or-no question there is nothing more to find, so we said n, and it gave us a new ?-.
What do we get if we ask eats otter algae.?
?- Failure
?-Does that mean otters never eat algae?
No. It means the pond does not say they do. Failure is "I cannot show this from the facts I have", not "this is false in the real world". In our pond the two happen to agree, because we wrote down everything we know.
Contents
- 1
Facts and Questions
There is a small pond. Algae grow in it. Snails and flies eat the algae. Frogs and fish eat the snails and the flies, a duck eats whatever it can reach, and a heron and an otter stand at the top and eat the frogs and the fish.
- 2
Rules and Recursion
Is the heron above the algae? Look at the food web from Chapter 1 and you will say yes at once: the heron eats the frog, the frog eats the fly, and the fly eats the algae. But no line in the pond says
eats heron algae, and the engine knows only what the lines say. Ask it, and it answersFailure. - 3
Terms and Unification
The frog has been busy. It ate three flies this morning, and the pond wants to remember how many. Chapter 1's facts can say that the frog eats flies. They cannot say how many.
- 4
Lists
The heron eats frogs and fish. Ask the pond what the heron eats and it answers twice, one critter at a time. But a menu is one thing: a card with two names on it. We want to hold both names at once, count them, turn them around, and ask questions about the card itself.
- 5
Types
Someone at the pond wants to note that the frog had three flies for lunch. They add a line to the file:
eats 3 fly.The pond refuses to load. Not one question gets an answer.lean-elpireads the line, says what is wrong with it, and stops. - 6
Predicates as Values
In Chapter 2 we taught the pond to answer "Is the heron above the algae?" with two clauses. Now a stream runs through the pond, and the critters have ages. "Is the spring upstream of the sea?" "Is the otter older than the fish?" Each question wants the same two clauses again, with one name changed.
- 7
Lambdas
In Chapter 6 we handed
swimsandeats herontostd.filter. Now we want the critters that eat flies.eats heronfixes the first place, and we need the second place fixed. We could writeflyeater X :- eats X fly.and use it once. A name for something used once is clutter. - 8
Pi and Implication
The heron is above the algae, and the frog is above the flies. The duck is not above the flies. It eats snails and algae, and neither of those eats a fly.
- 9
The Little Type Checker
Here is a small expression:
add tt (num 1). It asks us to add true to the number one. That is nonsense, and most of us see it at once. But who decides that it is nonsense, and how?
The eleven Maxims
Short rules, each earned by the questions of one chapter.
- The First Maxim
A fact says what is true. A question asks whether it follows.
- The Second Maxim
A capital letter is a hole. The answer fills the holes.
- The Third Maxim
Read
:-as "if" and the comma as "and". Two clauses mean "or". - The Fourth Maxim
Every recursion needs a way out, and every step must move toward it.
- The Fifth Maxim
Unification makes two terms the same, or it fails. There is no halfway.
- The Sixth Maxim
A relation has no inputs and outputs until you ask it something. Ask it backwards.
- The Seventh Maxim
Give every name a type. The checker reads the program before it runs.
- The Eighth Maxim
A predicate is a value. Pass it where you would pass a number.
- The Ninth Maxim
A lambda is a term with a hole in it. Applying it fills the hole.
- The Tenth Maxim
pimakes a name nobody has used.=>adds a fact for one goal only. - The Eleventh Maxim
A typing rule is a clause. A type checker is a logic program, and it runs both ways.
Get the code
Every program in the book comes from the companion repository, and every output printed in the book is a golden file there that a test checks. It runs on macOS, Linux and Windows with WSL.
git clone https://github.com/Volland/little-elpier
cd little-elpierPython only
Python 3.10 or later. The leanelpi package
carries its own copy of the engine, so there is nothing to compile.
python3 -m venv .venv
source .venv/bin/activate
pip install -e .
cd ch01
elpier hello.elpi -I ../lib -testDocker
Nothing to install but Docker. The image has
lean-elpi and elpier in it.
docker build -t little-elpier .
docker run --rm -it \
-v "$PWD":/book little-elpierFrom source
If you already use Lean 4, build
lean-elpi v0.4.1 with lake build and put
lean-elpi on your PATH.
Runs on lean-elpi
Every example runs on lean-elpi, an implementation of the ELPI dialect of λProlog written in Lean 4. It runs as a command-line program and as a Python package, so you do not need Lean to read this book. When you finish the pond, its site goes further: Python, Node.js and Rust bindings, tactics written in λProlog, and proof search whose results Lean's kernel checks.