eyeprolog

Front page for The Art of EyeProlog, presenting ISO Prolog rules and inspectable proofs.

This book is licensed under Creative Commons Attribution 4.0 International. You may copy, share, and adapt it for any purpose, including commercially; please give appropriate credit, link to the licence, and indicate changes.

EyeProlog turns facts and rules into answers and inspectable proofs. This book is an original introduction to the habits of logic programming: describe a world, state the relationships that hold in it, and let unification and search connect the two.

This book is also the reference for the EyeProlog implementation. EyeProlog is a standards-based reasoning system: programs use the documented and tested ISO Prolog profile. Chapters 38–40 define the supported ISO Prolog profile, built-ins, and execution interface, describe every supported built-in predicate, and document the command-line interface. The explanatory chapters give the reasoning and operational context needed to use those details correctly.

Its subject is not syntax alone. A logic program has two inseparable aspects: the relation described by its clauses and the procedure induced when goals are selected and clauses are tried. The first tells us what answers are justified; the second tells us whether and how the machine will find them. Learning to program with EyeProlog means learning to move comfortably between these views.

EyeProlog implements a broad ISO Prolog profile with facts, clauses, terms, lists, control, arithmetic, dynamic predicates, operators, streams, and standard built-ins. Automatic tabling, explicit integrity checks, and proof output are implementation capabilities around that standards-based foundation. EyeProlog does not attempt to claim formal certification of every ISO processor edge case.

Standards are crucial because knowledge and rules often outlive the software that first processes them. Using ISO Prolog keeps programs teachable, inspectable, and portable across processors. EyeProlog aims to provide a compact implementation of that standard with explanations and practical host integration, not another proprietary rule language.

This places EyeProlog in a tradition that joins automated deduction, database querying, and programming. Jacques Herbrand’s doctoral work made ground terms and ground instances central to proof theory; Robinson’s later resolution principle turned unification and refutation into a general proof procedure; early Prolog showed that Horn clauses could also be executable programs; deductive databases emphasized finite relations and fixed points. EyeProlog borrows from all three traditions without pretending that they are identical. Its clauses are logical statements, its query execution is an ordered computation, and its proof terms make the connection between the two available for inspection.

That history explains a recurring theme of the book. Logic programming is not the claim that control disappears. It is the discipline of stating the relation clearly enough that control can be studied and improved separately. Robert Kowalski’s phrase “algorithm = logic + control” names this separation; EyeProlog’s focused surface makes it unusually easy to see in running examples.

Complete EyeProlog code displays from the book are also available as files under examples/book/, grouped by chapter. From a source checkout with Node.js 18 or newer, run the CLI directly:

node bin/eyeprolog.js examples/socrates.pl

The EyeProlog command should print:

type(socrates, mortal).
holds_result(test, true).

Then ask for the derivations:

node bin/eyeprolog.js --proof examples/socrates.pl

To use the published package, first verify that node --version reports Node.js 18 or newer. Upgrade an older runtime through a Node version manager or the official Node.js download. A current Linux distribution can still expose an older Node.js package.

The package can be launched without a global installation:

npx --yes eyeprolog

For a persistent command without administrator access, install into a user-owned prefix:

npm install --global --prefix "$HOME/.local" eyeprolog
export PATH="$HOME/.local/bin:$PATH"

Persist the PATH export in the appropriate shell startup file. Do not use sudo npm install; npm’s EACCES guidance recommends a Node version manager or a user-owned npm prefix.

Readers who do not want to install anything can begin in the browser playground. Paste the source of examples/socrates.pl into the editor and run it. The playground and local CLI accept the same in-memory Prolog source and resolve the same standard modules. A program imports relations such as append/3 and member/2 with use_module(library(lists)). The page starts src/playground-worker.js as a dedicated ES-module worker for each run. Serve a local checkout over HTTP(S), rather than opening the page as a file: URL. Filesystem predicates and include/1 are Node-only; URL and embedding examples require their documented host environment.

The best way to read is beside a running interpreter. Before each run, predict the answer; after it, change one fact or query and explain the difference. Use npm run generate after editing the book to refresh the extracted examples/book/ files.

Reading conventions

Code displays serve three different purposes:

Top-level programs under examples/ are the complete runnable cases. Their exact outputs live under examples/output/; selected proof outputs live under examples/proof/. Use the chapter extractions for copying a particular display and the top-level corpus for end-to-end experiments.

The promise of this book

This book treats logic programming as a craft, not a collection of clever tricks. By the end, a reader should be able to:

  1. state a domain as relations whose ground instances have an unambiguous meaning;
  2. read every clause both as a logical sentence and as a computation;
  3. design finite searches, justify termination, and recognize when a calling mode is unsafe;
  4. construct programs from examples and invariants, then improve their control without quietly changing their meaning;
  5. test conclusions, detect inconsistent inputs explicitly, and inspect proofs as evidence; and
  6. connect a Prolog rule set to JavaScript without hiding the host boundary.

That is the stake in the ground: a focused implementation of standard Prolog is enough to teach the large ideas when semantics, execution, and evidence remain visible together. The implementation is therefore part of the argument. The examples are programs, the reference chapters are the reference for the running system, and npm test checks the complete code displays, local references, and built-in index against the source tree.

A working discipline

Approach each example through the same six moves:

  1. Sentence. Say what one ground instance means.
  2. Question. Choose the bindings with which the relation will be called.
  3. Prediction. Write the expected answers before running the program.
  4. Search. Trace the first choice, the bindings it adds, and the next goal.
  5. Evidence. Inspect a proof and distinguish it from the failed search branches that were explored.
  6. Revision. Change one fact, query, goal order, or representation and explain what should remain invariant.

This rhythm deliberately joins declarative reading, operational reading, and program construction. Readers new to logic programming can follow Parts I–III in order. Experienced Prolog programmers can begin with Chapters 3, 13, and 17 to see where EyeProlog’s hybrid execution and proof-oriented design differ. Chapter 41 gives further routes through the material.

When a run surprises you

Do not change several clauses at once. Use this recovery loop:

  1. reduce the issue to the smallest ground question whose answer you dispute;
  2. confirm that every predicate in that question has one clear sentence;
  3. write the bindings available before each body goal from left to right;
  4. run with --proof if an unexpected answer succeeds;
  5. run with --stats or hand-trace the first branch if an expected answer is missing or slow;
  6. preserve the discovery as a test before repairing the program.

No output can mean a legitimate absence, suppression of a queried source fact, an unready built-in, or an unfinished search. Chapter 1 introduces source-fact suppression, Chapters 7 and 11 distinguish failure from printed output, and Chapter 32 develops the full debugging method.

Choose a route

The book supports several paths; reading every chapter in order is not a test of seriousness.

Reader Suggested route What to postpone
New to programming Chapters 1–10, 11–12, 18–20, then Laboratories 1–4 The formal parts of Chapter 3, embedding, and Parts V–VI
Programmer new to logic Parts I–II, Chapters 11–13 and 17–25, then Part VII Detailed history and mathematical foundations on the first pass
Experienced Prolog programmer Chapters 3, 7, 11–13, 16–17, and 31–33 Introductory syntax and list material
Knowledge engineer Chapters 7, 11–16, 25, 31–33, then Laboratories 9–12 Symbolic mathematics unless it serves the domain
Mathematics reader Chapters 1–5, 19, and 26–30 Embedding until an application needs it
Instructor or study group Parts I–III, one route through Part V or VI, then selected laboratories Reference chapters until reference work begins

On a first pass, treat sections marked Deeper foundations as optional. They make the semantics precise but are not prerequisites for writing and running the next program.

The construction order

The sequence follows the teaching architecture associated with The Art of Prolog: begin with the meaning of a relation, make the relation executable, study the control it induces, and then return to the same ideas at a larger scale through transformation, search, interpreters, and applications. Each part therefore ends by asking the reader to construct, test, or improve a program rather than merely recognize syntax. Reference material follows practice, laboratories turn the methods into work, and checkpoint notes close the loop with retrieval and diagnosis.

Balance here does not mean that every chapter has the same length or the same number of pictures. A language catalog should be searchable; a construction chapter should be argumentative; a laboratory should leave an artifact. The recurring balance is instead between four readings of a program:

Reading Question carried through the book Typical evidence
Meaning What does each ground relation claim? a domain sentence and examples
Computation How are answers actually found? a trace, finite bound, or termination measure
Construction Why is the program shaped this way? a worked refinement and rejected alternative
Judgment What has been established, and what remains assumed? tests, proofs, counterexamples, and a trust boundary

Diagrams follow the same rule. Scenes introduce an intuition; structural diagrams expose a term, proof, or dependency; process diagrams guide a piece of work; maps help navigate reference and review. A diagram earns its place by making a relationship visible that prose alone would make easy to miss.

Contents

Chapters are numbered continuously across the twelve parts, from Chapter 1 to Chapter 46.

Part I — Relations

Chapters 1–5

Part II — Search

Chapters 6–10

Part III — Trustworthy reasoning

Chapters 11–16

Part IV — The craft of logic programming

Chapters 17–20

Part V — Advanced relational design

Chapters 21–25

Part VI — Mathematics made executable

Chapters 26–30

Part VII — The reasoning laboratory

Chapters 31–33

Part VIII — Standard Prolog in practice

Chapters 34–37

Part IX — Reference as practice

Chapters 38–43

Part X — Laboratories

Chapter 44

Part XI — Review

Chapter 45

Part XII — Development note

Chapter 46

Part I — Relations

People, homes, a school, and a bicycle connected by named relations in a small town.
One ordinary scene contains many relations: who lives where, who is a parent, who attends school, and who owns the bicycle.

We begin with connection rather than calculation. Facts place points in a relational world; variables draw threads between them; rules make one pattern follow from another.

1. A program is a little theory

Logic programming begins with a change of emphasis. Instead of listing the steps that calculate an answer, write sentences that are true in the problem domain.

parent(ada, byron).
parent(byron, clara).
parent(clara, diego).

Each line is a fact. parent/2 is a relation: the name is parent and the arity is two. Arity matters. parent/2 and parent/3 are different predicates.

A host-supplied query selects the relation whose ground answers EyeProlog prints:

child(Child, Parent) :- parent(Parent, Child).

eyeprolog --goal 'child(X, Y)' program.pl

The answers are:

child(byron, ada).
child(clara, byron).
child(diego, clara).

EyeProlog distinguishes solutions found by the solver from answers printed by the CLI. A query such as eyeprolog --goal 'parent(X, Y)' program.pl can find the three source facts internally, but the normal CLI output suppresses answers that merely repeat source facts. Derived child/2 answers are printed. Chapter 11 explains this output policy; it does not change what calls inside rules can prove.

The program did not copy values through named slots. It found substitutions for Child and Parent that made the rule body true, then applied those same substitutions to the head.

Before writing a relation, ask:

  1. What does one ground fact mean as a sentence?
  2. Which arguments are normally known when it is called?
  3. Is the relation finite in that calling pattern?

For parent(Parent, Child), a ground fact reads naturally from left to right. Calling it with a parent enumerates children; calling it with a child enumerates parents; calling it open enumerates the finite database. A good relation has a clear sentence and useful modes.

Facts are data, not commands. Clause order can affect search order, but a fact does not mean “do this now.”

Learning to see relations

The shift from functions to relations takes practice. A function is normally introduced with a direction: put an input in one side and receive an output from the other. A relation begins with a set of tuples. Direction enters only when somebody asks a question.

Take parent/2. The program does not store a procedure named “find children.” It stores pairs for which the relation holds. From that single relation, one may ask for a child’s parents, a parent’s children, whether two named people stand in the relation, or every known pair. The source text stays fixed while the binding pattern changes.

This is why the wording of a predicate matters. Before adding a rule, read a ground instance aloud:

parent(ada, byron) means that Ada is a parent of Byron.

Now replace one name at a time with a question:

For which Child is Ada a parent?

Who is a Parent of Byron?

Which Parent–Child pairs are known?

If those questions feel like natural uses of one statement, the relation is probably well shaped. If each reading requires a different interpretation of an argument, split the concept before the ambiguity spreads into later rules.

Exercise. Add grandparent/2 using two calls to parent/2. Query all grandparents, then only the grandparents of diego.

Checkpoint. Before continuing, make sure you can (1) read parent(ada, byron) as a sentence, (2) explain what the two variables in eyeprolog --goal 'child(X, Y)' program.pl ask for, and (3) predict which output changes after adding parent(diego, elena).

2. Terms, variables, and substitution

Prolog programs accepted by EyeProlog are built from terms:

Plain atom constants begin with a lowercase ASCII letter. Variables begin with an uppercase letter or underscore. The bare _ is anonymous and every occurrence is fresh. _Name is a named variable; repeated occurrences refer to the same variable within its clause. Variables are local to a clause.

Unification

Unification asks whether two terms can be made identical by binding variables.

reading(Sensor, 91)
reading(temp, Value)

They unify with Sensor = temp and Value = 91. Structure must agree recursively. point(X, X) unifies with point(2, 2) but not point(2, 3). Functor and arity must agree.

Two reading term trees align to produce bindings for Sensor and Value.
Unification walks corresponding branches of two term trees and records the bindings needed to make them identical.

The picture is worth lingering over. Unification does not assign values in a one-way parameter list. It aligns two structures. A variable on either side may receive a binding; a nested pair of compounds causes the same comparison to continue recursively. The result shown is the most general substitution: it commits to exactly what structural agreement requires and nothing more.

EyeProlog exposes unification as =/2:

same_shape(Pair) :- (Pair = pair(X, X)).

eyeprolog --goal 'same_shape(pair(red, red))' program.pl
eyeprolog --goal 'same_shape(pair(red, blue))' program.pl

Only the first query succeeds. \=/2 succeeds when two resolved terms are not structurally equal.

Compound terms retain domain structure:


:- use_module(library(lists)).

measurement(battery_1, sample(17, volts(28.4), amps(12.1))).
route(a, d, path([a, b, d], cost(9))).

As a fact head, measurement(...) is an atomic formula. Nested terms are data. The same surface form serves both roles; context decides which.

ready is an atom constant and "ready" is, by default, a proper list of one-character atoms. Keep symbolic vocabulary as atoms and use character lists when text must be inspected relationally. Quoted atoms remain atoms:

label(sensor_1, "Cabin temperature").
web_name(sensor_1, '<https://example.org/sensor/1>').

Exercise. Write diagonal/1, which succeeds for point(X, X). Then write same_ends/1 for a three-element list whose first and last values agree.

Checkpoint. Without running EyeProlog, decide whether each pair unifies: point(X, X) with point(red, red), point(X, X) with point(red, blue), and [Head | Tail] with [a, b, c]. Then run a small =/2 query to check each prediction.

3. Rules and their two readings

The executable-clause idea emerged from work on automated theorem proving. Robinson’s resolution principle supplied a general proof rule, while the development of Prolog specialized proof search around clauses that could be read as procedures. EyeProlog begins further downstream: it offers a compact definite-clause language rather than a general first-order theorem prover. The restriction buys a direct correspondence between a rule body and the subquestions used to establish its head.

A rule has a head and a comma-separated body:


:- use_module(library(lists)).

eligible(Person) :-
  age(Person, Years),
  (Years >= 18),
  registered(Person).

Read it declaratively: a person is eligible if the person has an age of at least 18 and is registered. Read it operationally: to solve the head, solve the body goals in their written dependency order, carrying bindings into later goals. EyeProlog normally selects from left to right. As a safe optimization, it may run a ready deterministic built-in filter early; such a filter cannot add alternative answers and already has the inputs its registered mode requires.

Both readings matter. The declarative reading checks the model. The operational reading helps make search finite and selective. Put a generator before a built-in that needs its input:

One recursive path rule points to its logical and operational readings.
A clause is both a sentence in a theory and a recipe for reducing a question to subquestions.

The two readings are not rivals. The logical reading prevents an efficient program from quietly answering the wrong question. The operational reading prevents a beautiful specification from wandering forever without producing an answer. Much of the craft in this book consists of keeping one reading steady while improving the other.


:- use_module(library(lists)).

adult(Person) :-
  age(Person, Years),
  (Years >= 18).

Multiple clauses express alternatives:

can_enter(Person) :- staff(Person).
can_enter(Person) :- visitor(Person), escorted(Person).

Helper predicates reveal the model and improve explanations:

high_score(Case) :-
  score(Case, Score),
  threshold(Threshold),
  (Score >= Threshold).

status(Case, accepted) :- high_score(Case).
reason(Case, "score meets threshold") :- high_score(Case).

Deeper foundations: Herbrand’s move

This section through “Meaning is not the search strategy” supplies the formal model behind the earlier examples. On a first practical reading, it is safe to continue at Chapter 4 and return here after writing a recursive relation.

The terminology in the next section honors a remarkably early source. Jacques Herbrand developed the relevant ideas in his 1930 doctoral thesis, Recherches sur la théorie de la démonstration (“Investigations in proof theory”). His fundamental theorem connected first-order derivability with propositional reasoning over suitably chosen ground instances. In broad terms, quantified proof obligations could be studied through formulas obtained by substituting constructed terms for variables.

That move supplied more than names. It made syntax usable as a mathematical universe: constants and function symbols generate ground terms, and atomic formulas over those terms provide a concrete space in which proofs can be analyzed. This viewpoint became foundational for automated theorem proving. Unification can be understood as finding substitutions that bring symbolic formulas together, while later proof procedures can search among clause instances without first assigning terms to an unrelated external domain.

The historical distinctions matter. Herbrand did not invent Robinson’s 1965 resolution calculus, nor did his thesis state the later least-model semantics of logic programs in its modern form. Rather, his proof theory laid essential groundwork. Resolution supplied a powerful subsequent inference mechanism, and van Emden and Kowalski later gave definite logic programs their fixed-point and least-Herbrand-model account. EyeProlog sits downstream of this sequence:

Herbrand: ground terms and instances as a proof-theoretic foundation
  -> Robinson: resolution and unification as a proof procedure
  -> logic programming: executable clauses and least-model semantics
  -> EyeProlog: a focused Prolog implementation with inspectable derivations

Herbrand completed this work while still in his early twenties and died in

  1. The scale of its later influence—in proof theory, automated deduction, and logic programming—is one reason the word Herbrand recurs throughout this book rather than appearing only as historical attribution.

The Herbrand world

The declarative reading needs a precise answer to a deceptively simple question: what can a term denote? EyeProlog uses Herbrand semantics. Its universe contains exactly the ground terms that can be constructed from the program’s atom constants, numbers, list constructors, and compound functors. There are no unnamed elements hiding behind the notation. A ground term denotes itself.

This separates the Herbrand universe, whose members are terms such as pat, 3, [red, blue], and ticket(alice), from the Herbrand base, whose members are ground atomic formulas such as person(pat) and owns(alice, ticket(17)). A term is not true or false merely by existing: pat is a possible argument, whereas person(pat) is a proposition that an interpretation may make true.

Ground terms form the Herbrand universe, ground formulas form the base, and justified formulas form the least model.
Terms provide the vocabulary; atomic formulas provide the possible claims; facts and rules select the least model.

This three-level distinction answers several recurring questions. A newly constructed term does not automatically assert anything. A formula that can be written is not automatically true. And the model is not an arbitrary collection of convenient formulas: it is the smallest collection forced by the program. Keeping those levels separate makes symbolic data safe to inspect without confusing mention with assertion.

A Herbrand interpretation is a set of ground atomic formulas regarded as true. A source fact contributes one such formula:

parent(pat, jan).

A rule stands for all of its ground instances. Thus:

ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).

says that for every substitution of X, Y, and Z by Herbrand terms, truth of both body formulas entails truth of the head formula. Variables in rules are implicitly universally quantified.

The declarative meaning of a pure Prolog program is its least Herbrand model: the smallest interpretation containing every fact and closed under every rule. One mathematical way to obtain it is the immediate-consequence operation. Begin with the facts; add each ground rule head whose ground body is already true; repeat until reaching the least fixed point. This construction defines meaning. It does not prescribe that the implementation enumerate the model from the bottom up.

Why terms denote themselves

Herbrand semantics is a particular form of ordinary model theory, chosen because logic programs inspect and construct symbolic terms. Consider:

different(alice, bob) :- (alice \= bob).
different(ticket(alice), ticket(bob)) :-
  (ticket(alice) \= ticket(bob)).

In an unrestricted first-order interpretation, alice and bob could denote the same object unless a unique-name axiom forbids it. Even if they denote different objects, the interpretation of ticket need not be injective. Additional axioms would be required to show that ticket(alice) and ticket(bob) differ.

In the Herbrand universe those terms differ by construction. Different atom constants are different terms; compound terms are free constructors and are identical only when functor, arity, and corresponding arguments are identical. Lists follow the same rule through [] and the internal ./2 constructor. Unification, read-back, witness construction, and proof explanations therefore share one predictable notion of identity.

This is a property of the representation, not a claim that two names can never refer to one real-world entity. If robert and bob name the same person, say so with same_as(robert, bob) or normalize them to one canonical term. The Herbrand layer keeps names unambiguous; domain rules express equivalence.

The runnable examples/herbrand-semantics.pl example and its normal and proof outputs make this distinction concrete.

Quantification and visible witnesses

Variables range over Herbrand terms, not external records, pointers, or host-language objects. Variables in a selected goal are existential in the logic-programming sense: EyeProlog searches for substitutions that make the goal follow from the program.

EyeProlog has no blank nodes or existential variables in rule heads. When a rule needs to name a consequent object, construct an explicit witness:

has_parent(Child, parent_of(Child)) :-
  person(Child).

registration(Student, Course, registration_of(Student, Course)) :-
  takes(Student, Course).

The same inputs construct the same witness term; different inputs construct different terms. The witness is printable, queryable, and visible in a proof, rather than being an anonymous object created behind the program’s back.

Equality, unification, and the occurs check

Equality in the pure Herbrand reading is syntactic identity after substitution. Operationally, unification discovers a substitution that makes terms identical. EyeProlog performs an occurs check whenever unification would bind a variable. It therefore uses finite-tree unification and rejects a binding when the variable occurs anywhere in the proposed value. For example, this call fails rather than constructing a cyclic term:

(X = wrapper(X)).

ISO classifies unifications whose outcome depends on an occurs check as subject-to-occurs-check (STO). EyeProlog’s default remains the sound finite-tree behavior above. For diagnosis, EyeProlog additionally provides the implementation-specific flag occurs_check; setting it to error turns a normal unification that would otherwise fail because of the occurs check into a representation error:

:- set_prolog_flag(occurs_check, error).

sto_example :- X = wrapper(X).
% error(representation_error(term), [])

The ISO error mechanism wraps an error term together with an implementation-defined context term. For this implementation-specific STO diagnostic EyeProlog uses representation_error(term) and currently uses the empty list [] as that context. This reports that the cyclic result of a succeeding STO unification cannot be represented by EyeProlog’s finite-tree term model, without exposing a non-standard occurs_check/2 error term.

The supported values are true (the default finite-tree behavior) and error (STO detection). EyeProlog deliberately does not provide occurs_check=false, because its term model does not construct cyclic terms. The ISO predicate unify_with_occurs_check/2 is independent of the diagnostic flag: it continues to perform finite-tree unification and fails on unify_with_occurs_check(X, wrapper(X)) even when occurs_check is error.

Meaning is not the search strategy

EyeProlog’s evaluator is goal-directed. It resolves selected goals against facts, rules, and built-ins using ordered conjunction, clause selection, indexing, tabling, and deterministic host operations. Written order defines the normal dataflow; a mode-ready deterministic built-in may be selected early as a pure filter. For the pure Horn-clause fragment, the answers it finds are intended to belong to the least Herbrand model. The evaluator is not, however, a complete bottom-up enumerator. Infinite generation or nonterminating recursion can prevent it from reaching a true answer.

Built-ins extend the pure core. Relational built-ins such as =/2, append/3, and member/2 are readily understood over Herbrand terms. Arithmetic, date handling, regular expressions, aggregation, once/1, and negation have additional operational definitions. They still consume and produce Prolog terms: X is 2 + 3 binds X to the Herbrand number term 5, not to an invisible host value.

\+ Goal succeeds when the current finite search finds no solution for Goal; it does not insert a negative formula into the Herbrand model. User-defined negative dependencies should be stratified. In a stratified program, positive dependencies may remain in the same or a lower layer, while every negative dependency points strictly downward:

closed(X) :- blocked(X).
open(X) :- candidate(X), \+ closed(X).

A cycle containing a negative edge is not stratified:

p(X) :- q(X).
q(X) :- \+ p(X).

The CLI reports such portability problems with --warnings. JavaScript embedders can inspect stratifiedNegation, negationStratificationErrors, negationDependencies, and per-group negationStratum; request eager analysis with analyzeNegation, reject it with strictNegation, or call program.assertStratifiedNegation().

Checkpoint. Read one rule twice: first as a sentence about all its ground instances, then as a left-to-right sequence of subquestions. Identify which body goal first binds each variable. If you took the practical route, defer Herbrand bases and interpretations without guilt; recursion is next.

4. Recursion: describing reachability

Recursive rules define an unbounded family of finite proofs. An ancestor is a parent, or a parent of an ancestor:

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).

eyeprolog --goal 'ancestor(X, Y)' program.pl

The first clause is the base case. The second reduces an ancestor question to a subquestion one edge farther through the graph. To design recursion, draw one proof, find the repeated subquestion, and ensure some path reaches a base case.

Constructing the recursive argument

A recursive program should expose the same argument that would justify its result on paper. For ancestor/2, that argument has four parts:

Design obligation ancestor/2 answer
Smallest supported case one known parent/2 edge
Repeated question whether the intermediate parent is an ancestor
Progress advance from X to the next vertex Y
Finite reason a finite graph gives finitely many endpoint pairs to table

The progress column is deliberately not “the term gets smaller.” Structural recursion over a list usually consumes a tail; graph recursion moves through a finite relation; arithmetic recursion may decrease a number. State the actual well-founded argument for the intended mode instead of borrowing the language of a different recursion pattern.

Clause order then expresses a control preference. Trying the direct edge first finds short proofs early, but it does not change which ancestor pairs the two clauses mean. Reversing the recursive clause’s body is different: it asks an open recursive question before selecting an edge and may destroy the useful mode. Meaning and control must be reviewed separately.

Real graphs contain cycles. Naive depth-first recursion can revisit a call forever. EyeProlog analyzes predicate dependencies and automatically tables suitable positive recursive groups. A table records answers for a recursive call, iterates cyclic calls to a fixed point, and reuses results. Authors describe path/2; the engine chooses the recursive strategy.

A railway network with a cycle and a ledger of routes already reached.
Recursive route questions may return to the same station. A table acts like a route ledger: new destinations are recorded and recurring questions reuse them.

Tabling does not make every open relation finite. A rule that constructs ever-larger terms can still produce infinitely many distinct calls or answers. Keep the selected query and its generators finite.

A relation can construct a witness:


:- use_module(library(lists)).

path(X, Y, [X, Y]) :- edge(X, Y).
path(X, Z, [X | Rest]) :-
  edge(X, Y),
  path(Y, Z, Rest).

On cyclic graphs, track visited vertices and use ISO negation as \+ member(Next, Visited) to obtain finite simple paths rather than arbitrary walks.

Notice that ancestor/2 and path/3 make different promises. Endpoint reachability has at most one logical pair for each pair of vertices, whereas path construction may have many witnesses for the same endpoints. Table the finite relation you need; bound or simplify the richer witness relation. This distinction reappears in grammars, planning, proof search, and program analysis.

Checkpoint. In the three-edge family from Chapter 1, predict the direct and indirect ancestor/2 answers. Point to the base clause and recursive clause, then say what becomes smaller or moves closer to a known fact in one successful derivation.

5. Lists as relations

[a, b, c] abbreviates nested cons cells. [Head | Tail] exposes one cell; [] is empty.

Three railway carriages illustrate a list head and tail.
A list resembles a train: expose the first carriage as the head, pass the remaining train as the tail, or join two trains with an append relation.
first([Head | _], Head).

contains_item(X, [X | _]).
contains_item(X, [_ | Rest]) :- contains_item(X, Rest).

joins([], Ys, Ys).
joins([X | Xs], Ys, [X | Zs]) :- joins(Xs, Ys, Zs).

Different modes give joins/3 different uses. It can construct a concatenated list, enumerate every prefix/suffix split, or find a missing part. This is the practical meaning of a relational definition.

Some algorithms carry explicit state through an accumulator:

reverse_acc(List, Reversed) :- reverse_go(List, [], Reversed).
reverse_go([], Acc, Acc).
reverse_go([X | Xs], Acc, Reversed) :-
  reverse_go(Xs, [X | Acc], Reversed).

No mutation occurs; every call receives a new term. EyeProlog also includes member/2, append/3, select/3, nth0/3, reverse/2, length/2, ISO sort/2, slicing helpers, and numeric summaries. Improper lists such as [a | Tail] are valid terms, but operations requiring a proper finite list fail unless the tail is [].

Checkpoint. Trace joins([a], [b, c], Whole) by hand. Then reverse the question: bind Whole to [a, b, c] and predict all prefix/suffix splits. Finally explain why [a | Tail] is not yet known to be a proper finite list.

Part I summary

Part I established the relational eye:

You should now be able to read a program aloud, predict a unifier, write base and recursive clauses, and explain why a list relation may construct as well as inspect its arguments. Carry forward one habit: begin with a meaningful ground instance, then ask which variables may safely replace which parts.

Historical note: clauses become a programming medium

The ingredients of Part I were assembled across several traditions. First-order logic supplied variables, substitution, and quantified formulas. Herbrand made ground terms and ground instances central to proof theory. Robinson’s 1965 resolution principle gave automated deduction a uniform, machine-oriented inference rule whose practical force depended on unification.

Prolog emerged when these ideas met a natural-language project in Marseille in the early 1970s. Colmerauer and Roussel stress that the project did not begin as an abstract attempt to invent a programming language: the need to analyze French drove the development of executable clauses and their control. Lists then became more than containers. They naturally represented sentences, syntax, proof states, and sequences of goals. The familiar two-clause list program condenses a much older mathematical pattern—definition by constructors and structural induction—into executable form.

Part II — Search

A traveler chooses among mountain paths leading toward a cabin.
A route is found by exploring alternatives, recognizing dead ends and cycles, and carrying a productive choice toward the destination.

A theory may justify many conclusions, but an evaluator must still find them. This Part studies the finite domains, constraints, failure, and choice that turn a field of possibilities into a productive computation.

6. Arithmetic and finite generation

Arithmetic uses the standard is/2 predicate, conventionally written with infix operator syntax:

A finite generator binds a number before arithmetic computes a result and a comparison filters it.
Arithmetic goals consume bindings rather than inventing them: generate a finite candidate, compute from ready inputs, then filter the ground result.

:- use_module(library(lists)).

next(X, Y) :- (Y is X + 1).
area_rectangle(W, H, Area) :- (Area is W * H).

hypotenuse(A, B, C) :-
  (A2 is A * A),
  (B2 is B * B),
  (C2 is A2 + B2),
  (C is sqrt(C2)).

Inputs must be bound to suitable numbers before a numeric function runs. Comparisons filter generated solutions:

safe_reading(Sensor, Value) :-
  reading(Sensor, Value),
  (Value >= 0),
  (Value =< 80).

between(Low, High, Value) enumerates an inclusive integer range or checks an already-bound value:

:- use_module(library(lists)).

square(N, Square) :-
  between(1, 10, N),
  (Square is N * N).

Finite generators turn loops into searches. Recurrences need intended modes:

factorial(0, 1).
factorial(N, F) :-
  (N > 0),
  (Previous is N - 1),
  factorial(Previous, PF),
  (F is N * PF).

The intended call direction belongs in the predicate’s tests and surrounding documentation; it does not require executable metadata.

Checkpoint. For every arithmetic goal above, mark which arguments must be numbers before the goal can run. Explain why between/3 is a generator in square/2 but merely a check when its third argument is already bound.

7. Failure, negation, and quantification

A goal fails when no clause or built-in proves it under current bindings. Failure prunes that branch and search tries another choice.

Failure is an operational event, not automatically a statement about the world. Turning failure into \+ Goal is justified only relative to the program and the current bindings. This is the closed-world move familiar from databases: for some bounded relation, what cannot be derived is treated as absent. It differs from the open-world stance common on the Web, where a missing claim may simply be unknown. Neither stance is universally right; the modeler must say which knowledge boundary is complete.

\+ Goal succeeds when Goal has no solution:

allowed(User) :-
  user(User),
  \+ blocked(User).

This means “blocked cannot be proved from this program,” not classical negation. Bind variables before negating. Putting \+ blocked(User) before user(User) asks whether there is no blocked user at all, not whether this particular user is unblocked.

A receptionist checks a complete guest registry against a blocked list.
Absence becomes informative only inside a declared complete boundary: Clara is allowed because the event registry is complete and she is not on its blocked list.

For ordinary \+/1, negative dependencies should normally be stratified: compute a lower relation, then negate it from a higher layer. Use --warnings to report negative recursion:

eyeprolog --warnings program.pl

Some finite rule systems intentionally contain recursion through negation. In normal mode, EyeProlog provides explicit tnot/1 for that case. When the reachable component is finite, function-free, and range-restricted Datalog, cycles through tnot/1 are evaluated with the well-founded semantics (WFS) rather than ordinary negation-as-failure. WFS has three truth states: true, false, and undefined. A negative cycle may therefore produce a conditional answer instead of forcing an arbitrary true/false choice.

move(a, b).
move(b, a).
win(X) :- move(X, Y), tnot(win(Y)).

Here neither win(a) nor win(b) is unconditionally established; both belong to the undefined part of the well-founded model. EyeProlog exposes undefined WFS answers as conditional successes, including inside finite collectors. Direct calls to tnot/1 must be ground. In WFS rules, variables occurring in the head or a negated literal must be range-restricted by positive body literals. Ordinary \+/1 is unchanged, and strict ISO mode does not provide tnot/1.

Universal checking needs no extension predicate: define the counterexample and negate it.

all_tests_pass(Suite) :-
  \+ failing_test(Suite).

failing_test(Suite) :-
  test_in(Suite, Test),
  \+ passed(Test).

Use negation where the knowledge boundary is closed: a complete roster, configuration, or finite result set. In open-world data, model explicit states such as confirmed_absent instead of deriving absence from silence.

Checkpoint. Compare user(User), \+ blocked(User) with \+ blocked(User), user(User). State the question each ordering asks and the completeness assumption needed before calling either result “allowed.”

8. Collecting and choosing answers

Finite aggregation asks about a solution set:

:- use_module(library(aggregate)).
:- use_module(library(lists)).
:- use_module(library(iso_ext)).

findall(Template, Goal, List).
countall(Goal, Count).
sumall(Value, Goal, Sum).

:- use_module(library(aggregate)).
:- use_module(library(lists)).

outgoing_costs(Node, Costs) :-
  findall(Cost, edge(Node, _, Cost), Costs).

total_outgoing(Node, Total) :-
  sumall(Cost, edge(Node, _, Cost), Total).

findall/3 returns [] for no answers; counts and sums return zero.

Choose a collector from the question, not from convenience:

Question Result shape Empty search
Which witnesses were found? findall/3 returns a list []
How many derivations succeeded? countall/2 returns an integer 0
What is their numeric total? sumall/3 returns a number 0
Which candidate has the least or greatest key? aggregate_min/5 or aggregate_max/5 returns one candidate failure

Counting solutions is not necessarily counting distinct domain objects: two proofs may resolve the visible value in the same way. When identity matters, collect the identifying template and deliberately canonicalize it with ISO sort/2; when derivation multiplicity matters, retain the duplicates. Making that decision explicit prevents a database-style summary from silently changing the question.

Market baskets with weights flow into count, sum, minimum, and maximum results.
Aggregation temporarily treats a finite family of solutions as a collection: the same baskets can be counted, summed, or compared.

Optimization can retain only a best solution:

:- use_module(library(aggregate)).
:- use_module(library(lists)).

best_route(From, To, Route, Cost) :-
  aggregate_min(
    [CandidateCost, CandidateRoute],
    CandidateRoute,
    route(From, To, CandidateRoute, CandidateCost),
    [Cost, Route],
    Route
  ).

The key [Cost, Route] supplies deterministic tie-breaking through term order. aggregate_min/5 and aggregate_max/5 fail when their goal has no answers. An aggregate opens a smaller query scope inside the surrounding proof, and its inner search must be finite.

Keep candidate generation separate from choice. A relation such as route/4 should explain which routes exist and how their costs arise; best_route/4 states a policy over that finite relation. This separation lets the same candidates be inspected, counted, tested, or optimized without burying their meaning in a single committed search. It also makes an empty candidate set visible: “there is no route” is different from inventing a sentinel route with an artificial cost.

Checkpoint. For an empty route relation, predict the behavior of findall/3, countall/2, sumall/3, and aggregate_min/5. Then identify the finite generator that bounds each aggregate in a program of your own.

9. Structured data, text, and contexts

Term predicates decompose or construct general terms:

Raw text becomes structured members inside one message context, which ordinary term traversal inspects without asserting those members globally.
Normalize text into explicit structure at the boundary; inspecting a member inside one context does not turn it into an ambient fact.
functor(Term, Name, Arity).
arg(Index, Term, Value).
(Term =.. [Name | Arguments]).

arg/3 uses one-based indexes. Prefer direct pattern matching when the shape is known; use inspection for generic transformations.

Text is best normalized at the model boundary. The library(strings) module uses ISO-friendly atoms or proper lists of one-character atoms for its text arguments; newly produced text is an atom:

:- use_module(library(strings)).
:- use_module(library(lists)).

normalized(Input, Words) :-
  trim(Input, Trimmed),
  lowercase(Trimmed, Lower),
  split(Lower, ' ', Words).

Conversions include number_string/2, atom_string/2, and term_string/2. Pattern operations include contains/2, matches/2, and named-capture matches/3. Turn text into structured terms early and keep central rules relational. Double-quoted source notation follows the ISO double_quotes flag; it does not create a separate Prolog string type.

Parenthesized comma terms can serve as context data:


:- use_module(library(lists)).

message(event_17, (severity(high), source(sensor_3), reading(temp, 91))).

context_member((Left, _right), Member) :- context_member(Left, Member).
context_member((_left, Right), Member) :- context_member(Right, Member).
context_member(Member, Member) :- Member \= (_left, _right).

hot_event(Id) :-
  message(Id, Context),
  context_member(Context, severity(high)),
  context_member(Context, reading(temp, Value)),
  (Value > 80).

context_member/2 is an ordinary program relation: it walks a comma-context from left to right. When the member’s shape is not known in advance, decompose it with (Member =.. [Name | Arguments]). Context members remain quoted data; inspecting them does not assert them as ambient facts.

Checkpoint. Distinguish the atomic formula message(...) from the nested data term (severity(high), source(sensor_3), reading(temp, 91)). Explain why context_member/2 can inspect the latter without asserting severity(high) globally.

10. From puzzles to models

A robust finite search has three layers: generate candidates, constrain them, and present a concise answer.

color(red).
color(green).
color(blue).

coloring(A, B, C) :-
  color(A),
  color(B),
  (A \= B),
  color(C),
  (B \= C),
  (A \= C).

answer(colors(A, B, C)) :- coloring(A, B, C).

eyeprolog --goal 'answer(X)' program.pl

Place cheap, selective constraints as soon as their inputs are bound. For state-transition problems, represent state and moves explicitly:


:- use_module(library(lists)).

plan(State, State, _, []).
plan(State, Goal, Seen, [Move | Moves]) :-
  transition(State, Move, Next),
  \+ member(Next, Seen),
  plan(Next, Goal, [Next | Seen], Moves).

The visited list makes a finite state space explicit. EyeProlog is strongest when the result is a logical consequence with a compact witness: a path, matching, classification, schedule, proof, or bounded model. Mutable arrays and large numerical kernels generally belong in a host, with EyeProlog as the decision layer.

For the coloring program, the six printed answers are the permutations of red, green, and blue:

answer(colors(red, green, blue)).
answer(colors(red, blue, green)).
answer(colors(green, red, blue)).
answer(colors(green, blue, red)).
answer(colors(blue, red, green)).
answer(colors(blue, green, red)).

Checkpoint. Label the generator, each constraint, and the final witness in the coloring program. Before changing it, predict how many answers remain if A \= C is removed; then run the program and account for every additional answer.

Part II summary

Part II turned relations into finite computations:

You should now be able to justify a query’s finiteness, order goals by binding dependency, distinguish negation as failure from classical negation, and explain why optimization is search plus an ordering.

Historical note: control, databases, and finite failure

Early Prolog made a decisive engineering choice: clauses would be tried in an order and subgoals would normally be selected left to right. That choice made logic executable, but also made control visible. A logically symmetric conjunction could behave asymmetrically when one order supplied a value and another asked arithmetic to run too soon.

The meeting of logic programming and database research in the 1970s sharpened questions about finite relations, closed-world reasoning, and query evaluation. Keith Clark’s 1978 account did not identify failure with unrestricted logical negation; it related negation as failure to a completed database reading. Later work on stratification disciplined negative dependencies. Aggregation continued the database lineage: a set of solutions could itself become data, provided the nested search was finite.

These distinctions explain EyeProlog’s conservative treatment. Negation and aggregation are powerful because they expose a bounded subcomputation. Their safety comes not from punctuation but from a mathematical argument about scope and termination.

Part III — Trustworthy reasoning

A spacecraft engineer reviews sensor evidence leading to a battery safety action.
Current, resistance, and temperature readings remain visible as independent premises for a thermal warning and safety action.

An answer becomes useful when its grounds remain visible. Here reasoning is treated as an accountable structure: queries define the question, proofs retain support, integrity checks expose invalid states, and knowledge boundaries stay explicit.

11. Queries, answers, and proofs

EyeProlog goals are supplied by the host, for example eyeprolog --goal 'child(X, Y)' program.pl. EyeProlog prints ground answers, removes duplicates, and suppresses answers that merely repeat source facts. Answers are not inserted back into the running program.

An answer and a derivation serve different audiences. An answer records what the theory supports; a derivation records how this run supported it. In mathematics that distinction resembles theorem versus proof. In data systems it resembles result versus provenance. The proof is not a substitute for valid source data or sound domain rules, but it makes both reviewable: a user can trace a decision to clauses, facts, bindings, and built-in operations instead of trusting an opaque status code.

Use --proof or -p to add a machine-readable why/2 fact after every answer:

eyeprolog --proof examples/socrates.pl


:- use_module(library(lists)).

why(
  type(socrates, mortal),
  proof(
    goal(type(socrates, mortal)),
    by(rule("socrates.pl", clause(4))),
    bindings([binding("X", socrates)]),
    uses([
      proof(
        goal(type(socrates, man)),
        by(fact("socrates.pl", clause(3)))
      )
    ])
  )
).

Proof output is valid EyeProlog input:

eyeprolog --proof examples/socrates.pl > socrates.why.pl

A normal answer is one resolved ground term followed by a period. Strings, quoted atoms, lists, and compounds are rendered in supported source syntax so the output can be read back. Enabling --proof, --warnings, or --stats must not change which answers are found.

The second argument of why/2 is an abstract proof term of the general shape proof(goal(G), by(Method), bindings(Bindings), uses(Proofs)). User clauses are identified as fact(Filename, clause(N)) or rule(Filename, clause(N)), with one-based source clause numbers. Built-ins are identified as builtin(Name, Arity). Explanation data is outside the logical semantics of the input program: it describes the derivation but does not participate in finding it.

A second program can query why/2. Read a proof as an argument. If it contains irrelevant detours, improve the helpers. If a key premise is hidden inside an opaque value, model it as a fact. Designing for a good explanation often produces a better theory.

Checkpoint. Run examples/socrates.pl once normally and once with --proof. Confirm that the ground answers are unchanged. In one proof, identify the queried goal, the rule that derived it, the source fact used, and the binding carried between them.

12. Integrity checks as ordinary predicates

Integrity conditions are ordinary relations that describe invalid input states:

invalid_probability(Disease, Probability) :-
  probability(Disease, Probability),
  (Probability > 1).

A host that requires validated input queries the integrity relation explicitly before it asks for domain decisions. This keeps the policy visible: the host may reject the input, report every defect, or continue in a diagnostic mode.

false/0 keeps its ISO meaning: it is a built-in goal that always fails. It is a protected static procedure, so false. and clauses of the form false :- Body. are rejected with permission_error(modify, static_procedure) rather than acquiring special pre-query behavior.

An explicit invalid-state query identifies conflicting engineering limits before operation.
An integrity relation reports the invalid state; the host decides whether that state blocks later decisions.
invalid_assignment(Person, Role, Other) :-
  assigned(Person, Role),
  incompatible_roles(Role, Other),
  assigned(Person, Other).

The logical reading is that the program can derive witnesses for an inadmissible combination. The operational response is outside the relation itself and remains an explicit host decision.

Designing an integrity relation

Start with a sentence that must never be accepted, then translate its witnesses into positive, finite goals. “No person has two incompatible roles” becomes the relation above. A useful integrity check is:

Four outcomes that can look like “failure” at a shell prompt have different meanings:

Outcome Interpretation Appropriate response
query has no answer this theory did not derive the selected goal inspect data, rules, and closed-world assumptions
integrity query has an answer the supplied input contains a forbidden combination repair, reject, or report the input
resource ceiling is reached the computation exceeded an operational budget bound or redesign the search
parser or type error the program or call violates the language contract correct the source or interface

Do not treat every undesirable business result as invalid input. A declined application, unavailable route, or negative test may be a perfectly valid answer of the theory. Reserve integrity relations for states whose witnesses must be handled before trusted downstream decisions.

To see the explicit validation path, run:

node bin/eyeprolog.js examples/integrity-check.pl

It prints the invalid-state witness and the resulting diagnostic status. Nothing runs implicitly before the supplied goals.

Checkpoint. Explain the difference between an ordinary query with no answer and an integrity query that returns a defect. Write one invalid-state relation and one ordinary negative result that should remain query failure.

13. Termination, tabling, and performance

Declarative clarity and operational care reinforce each other. Bind selective arguments early, keep generators finite, and make decreasing structure visible.

Three recursive call patterns: decreasing lists, finite tabled graph answers, and terms that grow without bound.
Termination needs a specific argument: a decreasing measure or a finite tabled call-and-answer space; ever-growing terms satisfy neither.

Naive depth-first search can revisit the same recursive question indefinitely. Tabling changes the unit of work: a call pattern becomes a shared subproblem, its answers are remembered, and consumers reuse answers rather than expanding the same call again. This idea connects logic programming to memoization and dynamic programming, but tabling also has a semantic role: over a finite positive recursive domain, repeated rounds can compute the least fixed point. It is therefore especially natural for reachability, grammars, dependency analysis, and other recursive relations with overlapping subproblems.

Ordinary goals use indexed depth-first resolution. Positive recursive groups are tabled automatically. Bound recursive calls reuse answers and cyclic calls iterate toward a fixed point. For sufficiently large finite, function-free Datalog dependency cones, EyeProlog may share one most-general relation table across call variants. This turns an open closure such as tc(X, Y) into one finite relation computation rather than many overlapping bound subcomputations; bound consumers can then use indexes over the stored answers. The exact admission policy is an engine optimization, not part of the language contract. Fully open or structurally unbounded recursive programs may retain ordinary resolution.

Recursive components with negative dependencies are not positive least-fixed- point problems. When such a component uses explicit tnot/1 and satisfies the finite, range-restricted, function-free Datalog restrictions, EyeProlog instead computes the alternating fixed point of the well-founded semantics. Existing \+/1 code remains ordinary negation-as-failure.

Deeper implementation: how clause indexing stays semantic

This section explains why an optimization does not change clause meaning. Readers focused on modeling may skip to the statistics command and return when performance or implementation portability becomes relevant.

Every predicate group keeps compact indexes for scalar values in each argument position. Index keys include the scalar type, so 7, '7', and "7" remain distinct even though their printed payload is the same. A clause whose indexed head argument is a variable or structured term stays in a fallback set, and the selected candidates are merged back into source order before unification. An index narrows where to look; it never decides whether a clause matches.

For groups of at least ten clauses, a call with several bound scalar arguments may cause a wider combined index to be built on demand. The admission policy rejects indexes with too many variable fallbacks or too little expected speedup, and requires a combined index to improve substantially over the best single-argument index. These choices are performance details: removing every index should change running time, not answers or clause order.

Authors choose query modes, finite domains, visited-state representations, negation strata, and witness size. They normally do not choose the engine’s search strategy.

Inspect counters without changing answer output:

eyeprolog --stats examples/observability-log-correlation.pl

The reported counters include completed goal lists, calls to the goal solver and single-goal solver, unification attempts, maximum depth and goal-list size, deterministic built-in successes and failures, and table fixed-point rounds. WFS execution additionally reports wfs_fixpoint_rounds and wfs_undefined_answers. The latter counts undefined-answer observations made while producing query results; it is an execution statistic, not a declaration that those atoms are true. All statistics describe work performed, not logical truth. Compare counters only across equivalent queries and the same implementation version.

Common sources of nontermination are recursive calls made before constraints, ever-growing terms, infinite open mathematical queries, negative cycles, and path enumeration without a visited set. Repair the model by strengthening the query, adding a finite domain, tracking states, or exposing a decreasing argument.

Checkpoint. Classify three recursive calls: one justified by a decreasing list, one by finitely many tabled graph answers, and one that constructs terms without bound. State why the first two may terminate and why tabling does not repair the third.

14. Knowledge engineering

A maintainable theory separates:

Source facts pass through normalization and domain concepts into a decision and proof.
A maintainable theory moves in visible layers from observations to decisions, while the proof preserves the route back to evidence.

Prefer positive domain concepts. Use negation only across a closed boundary. Represent confidence, alternative worlds, and provenance explicitly rather than hiding them in rule order.

An evidence-backed diagnosis can separate physics from policy:

heating(Battery, Watts) :-
  current(Battery, Amps),
  resistance(Battery, Ohms),
  (I2 is Amps * Amps),
  (Watts is I2 * Ohms).

thermal_warning(Battery) :-
  heating(Battery, Watts),
  heating_limit(Limit),
  (Watts > Limit),
  temperature(Battery, Celsius),
  temperature_limit(TLimit),
  (Celsius > TLimit).

action(Battery, isolate_and_cool) :- thermal_warning(Battery).

Physics, limits, redundant sensing, and policy become distinct proof steps. See examples/spacecraft-battery-diagnosis.pl for a complete case.

Test theories with successful derivations, expected failures, boundary values, duplicate paths, contradictory inputs, and proof premises. The repository’s conformance cases, example goldens, and proof goldens demonstrate these levels.

Checkpoint. Draw four columns for the battery example: source, physical concept, decision, and integrity. Place each predicate in a column, then list the measurements and policy thresholds that a proof cannot authenticate by itself.

15. Explicit data boundaries

EyeProlog deliberately keeps external integration outside the reasoning core. An embedder validates input, converts it to ordinary Prolog terms and clauses, and then asks the solver a focused goal. This keeps parsing a business format, authenticating a source, and deriving a conclusion as three separate jobs.

A boundary should make four decisions visible:

A boundary in four steps

Suppose a host receives one JSON temperature record. The host, not the logic program, owns the JSON syntax and the decision to trust that record. A narrow adapter can validate the record, map its values into a deliberately small Prolog vocabulary, construct the theory, and ask one bounded question:

import { run } from 'eyeprolog';

const inputText = '{"sensor":"sensor_1","celsius":91}';
const allowedSensors = new Set(['sensor_1', 'sensor_2']);

function reasoningSource(record) {
  if (!record || typeof record !== 'object') throw new TypeError('record');
  if (!allowedSensors.has(record.sensor)) throw new TypeError('sensor');
  if (!Number.isFinite(record.celsius)) throw new TypeError('celsius');
  if (record.celsius < -100 || record.celsius > 200) {
    throw new RangeError('celsius');
  }

  return `
reading(${record.sensor}, ${record.celsius}).
thermal_alert(Sensor) :-
  reading(Sensor, Celsius),
  (Celsius >= 80).
`;
}

const record = JSON.parse(inputText);
const result = run(reasoningSource(record), {
  goal: `thermal_alert(${record.sensor})`,
  proof: true,
  maxDepth: 10_000,
  maxInferences: 100_000,
  maxMemoryBytes: 256 * 1024 * 1024,
  solutionLimit: 10
});

console.log(result.stdout);

The allow-list makes interpolation safe here: the external sensor identifier can become only one of two known Prolog atoms, and the temperature must be a finite number in an accepted range. General text must be encoded with a well-tested term constructor or serializer rather than inserted into source. The generated program defines only reading/2 and the fixed domain rule; the host supplies the goal and ceilings explicitly.

This small example exposes four different claims:

Stage Claim and owner
Parse the bytes are valid JSON — host parser
Validate the record has an accepted sensor and temperature — adapter
Convert the accepted values denote these exact Prolog terms — adapter
Derive the supplied reading satisfies thermal_alert/1 — EyeProlog proof

The proof procedure can explain how supplied clauses support an answer. It cannot prove that a file, database, sensor, or remote service was trustworthy. That responsibility stays with the host application.

Checkpoint. Choose one external record used by an application. State what the host validates, the Prolog term it constructs, the goal it asks, and the resource limit that prevents an untrusted input from consuming unbounded work.

16. Embedding EyeProlog

The JavaScript API exposes a convenience runner and lower-level types:

import { run, Program, Solver, parseGoalText } from 'eyeprolog';

const result = run(`
answer(ok) :- ok = ok.
`, { goal: 'answer(X)' });
console.log(result.stdout);
console.log(result.stats);

The first console.log prints answer(ok). followed by a newline. The second prints numeric work counters; those counters describe this run rather than an additional logical answer.

run/2 accepts source text or an already parsed Program. Its options include proof (with why and explain as aliases), maxDepth, maxInferences, maxMemoryBytes, solutionLimit, a custom registry, and strictNegation or analyzeNegation. It returns stdout, the solver’s numeric stats, and a nullable haltCode; it does not write to the process streams.

When run receives an already parsed Program, canonical interop imports needed only by its host-supplied goals are added to that Program before solving, just as they are while source text is parsed. Pass autoload: false when the Program must retain only explicitly imported predicates.

For applications that inspect or prepare a theory before running it, use Program directly:

const source = `
edge(a, b).
edge(b, c).
path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).
`;

const program = Program.parse(source, { analyzeNegation: true });
const goal = parseGoalText('path(a, X)');
const path = program.findGroup('path', 2);

console.log(goal);
console.log(program.stratifiedNegation);
console.log(path?.recursive, path?.tabled, path?.tableInputPositions);

const solver = new Solver(program, {
  maxDepth: 50_000,
  maxInferences: 1_000_000,
  maxMemoryBytes: 256 * 1024 * 1024,
  solutionLimit: 100_000
});

The limits are safety ceilings, not logical declarations. Reaching the depth, inference, or solution ceiling may truncate search; it does not prove that no further answer exists. Reaching maxMemoryBytes instead raises resource_error(memory), because continuing until the JavaScript engine’s hard heap limit would let the host abort before Prolog could report an exception. At the Solver API boundary, solutionLimit is opt-in: if it is omitted, ordinary solving and child searches that inherit the solver limit do not stop after a fixed number of solutions. This matters for re-executable goals such as repeat/0 and for library relations such as call_nth/2; an implementation safety threshold must not turn a still re-executable search into logical failure. Embedders that need a finite answer budget should pass solutionLimit explicitly.

Variable term order is deliberately scoped rather than stored as a permanent property of a variable. ISO 13211-1 section 7.2.1 leaves the order of two distinct variables implementation dependent and requires constancy only while a sorted list is being created. EyeProlog therefore chooses a local variable ranking for an ordinary term comparison, while sort/2, keysort/2, and the sorting step of setof/3 share one ranking for the duration of that single sorted-list operation. No process-global variable registry or creation ordinal is retained or exposed through later comparisons.

EyeProlog periodically checks detectable JavaScript heap use and keeps a quarter of the applicable host heap ceiling in reserve so the solver can unwind and report resource_error(memory) before a fatal host out-of-memory abort. When Node is started with --max-old-space-size, the guard compares that old-generation ceiling with V8’s non-young heap spaces; short-lived new-generation allocations therefore do not cause a false resource error. Embedders may replace that automatically derived soft ceiling with maxMemoryBytes; setting it to Infinity disables the proactive check. Environments that do not expose heap use cannot provide the proactive check. Host capacity failures that V8 reports as Map maximum size exceeded or Set maximum size exceeded are also normalized at the solver boundary instead of leaking a JavaScript RangeError. ISO 13211-1 leaves the resource atom implementation dependent. EyeProlog uses memory for a finite host allocation/capacity ceiling and reserves the finite_memory spelling for the distinct convention where no finite amount of memory could complete the computation. After a recoverable memory error, the solver keeps a bounded recovery window while the failed search unwinds so the host can collect released query terms. The same solver can then run later queries; this recovery does not resume the query that exhausted its limit.

The iterative solver keeps active-call frames only where they are semantically needed for cut scope or recursive variant guards. Bundled-library helpers whose callable dependency region is cut-free and which need no recursive variant guard therefore do not copy a growing active-call sequence at every step. Under the normal EyeProlog registry, the bundled Prologue length/2 also has a scoped iterative execution path: named lists are counted or constructed without recursive interpreter frames, and an anonymous list is not materialized because its binding cannot be observed. A newly constructed fixed-length suffix starts as a lazy compact skeleton and expands one ordinary ./2 cell at a time when unification, another list predicate, or answer readback inspects it. This is a storage optimization, not a distinct Prolog term or list semantics. Embedders that inspect the JavaScript term model can recognize this representation with CompactListTerm, isCompactList, and compactListLength, or construct one with compactVariableList. For open-ended length(List, N) generation, each generated spine is known not to contain the caller’s dereferenced tail variable. The bundled path passes that proof through the normal unifier, sharing the same proven-nonoccurrence mechanism as first-use clause variables instead of maintaining a predicate-specific raw binding shortcut. It still reserves recovery headroom proportional to the retained spine, so a finite heap limit is raised inside the length/2 search as a catchable resource_error(memory) rather than allowing an outer solver frame to encounter the limit first.

The same proven-nonoccurrence mechanism has a conservative source-level form for freshly renamed clauses. A singleton variable in the clause head, or a variable that has not appeared in the head or any earlier body goal and occurs exactly once in a direct =/2 goal, cannot already be a subterm of the value it is about to receive. EyeProlog marks only that binding as locally fresh and skips its occurs traversal. A repeated variable such as the X in X = f(X), a variable already seen earlier in the clause, and unify_with_occurs_check/2 all keep the normal finite-tree check. The solver also treats such a first-use equality as a source-order barrier for its deterministic-goal scheduling, so the freshness proof cannot be invalidated by moving a later goal ahead of it. This recovers much of the classic WAM-family “local variable” optimization for DCG tail variables without introducing a WAM local/global stack distinction into the JavaScript term model.

For grammar execution, phrase/2 passes its fixed final remainder [] directly into the expanded grammar. Besides matching the two-argument contract, this avoids repeatedly trying an empty production against a temporary output variable. phrase/3 still uses a private final-output variable and delays its last unification, preserving the existing steadfast treatment of its explicit third argument. The ordinary length/2 clauses remain the authoritative module definition and are used unchanged by the ISO-only registry and whenever delays or finite-domain constraints require their normal wake-up points.

Implementation boundary

The source layout mirrors the language boundary while keeping the JavaScript runtime flat under src/. src/iso.js remains the stable ISO facade and built-in registry; arithmetic evaluation lives in src/iso-arithmetic.js, and processor control/error classes live in src/errors.js. src/dcg.js implements the shared Part 3-oriented grammar-rule and dynamic-body expansion without depending back on the ISO registry. This keeps the low-level syntax and error layers acyclic while preserving the existing src/iso.js exports.

src/cleanup.js is an execution-layer sibling of the solver. It installs lifecycle-aware closing of protected builtin iterators from the supported API and CLI entry paths and registers call_cleanup/2 and setup_call_cleanup/3 for the normal EyeProlog profile. The standard-library layer does not import the solver back through this module, preserving the acyclic source graph.

Program preparation follows the same pattern. src/program.js remains the Program facade and source/module loader. Static recursion, Datalog, WFS, and negation-stratification analysis is isolated in src/program-analysis.js, while compact-clause representation and conservative candidate indexes live in src/program-indexing.js. The solver consumes those same indexes directly; large execution fast paths deliberately remain in src/solver.js rather than being split through extra strategy objects or callbacks. Architectural cleanup is required to preserve benchmark performance as well as semantics.

Focused files under src/lib/ contain the portable extensions, with src/lib/lists.pl supplying common list relations. They are ordinary Prolog modules using EyeProlog’s documented module compatibility surface, organized like Trealla’s library/ and registered for library(Name) by src/standard-library.js in Node and the browser. The browser entry point src/playground-worker.js uses that same program and module-loading path in a dedicated worker. src/ARCHITECTURE.md records the layering and dependency rules, and the architecture regression rejects JavaScript import cycles.

Normal CLI, JavaScript, Solver, proof replay, and the browser playground use the same module loader. A library is added to a Program only when its source uses use_module/1 or use_module/2; exported predicates are imported into the calling module and private predicates remain module-local. Advanced embedders and conformance tests can select getStrictIsoRegistry() together with isoStrict: true for the Part 1 + Corrigenda strict surface. All paths share the parser, term representation, solver, streams, and proof machinery.

Extending the built-in registry

An embedder can start from the default EyeProlog registry and add a host relation. A handler is a generator over environments. It should clone before binding and yield only environments in which its result unifies:

import {
  atom,
  createEyePrologRegistry,
  run,
  unify
} from 'eyeprolog';

const registry = createEyePrologRegistry();

registry.add(
  'host_status',
  2,
  function* ({ goal, env }) {
    const next = env.clone();
    if (
      unify(goal.args[0], atom('service'), next) &&
      unify(goal.args[1], atom('ready'), next)
    ) {
      yield next;
    }
  },
  { deterministic: true }
);

const result = run(`
answer(X) :- host_status(service, X).
`, { registry, goal: 'answer(X)' });

Only mark a built-in deterministic when it can produce at most one environment for a call. An unmarked suspended iterator is conservatively an untried continuation: the solver never resumes it merely to discover whether a later answer will succeed. An iterator that knows its remaining search positions may provide hasPendingAlternatives(), updated before each yield, to remove its resume frame exactly when no position remains. This method reports pending search, not the existence of a future successful answer. A mode-sensitive extension can additionally provide ready, fallbackWhenNotReady, and shouldUse metadata. This metadata affects dispatch and safe early filtering, so it belongs to the extension’s contract.

The ISO false/0 built-in always fails, and source clauses that attempt to define it raise permission_error(modify, static_procedure). Programs expose stratification diagnostics through stratifiedNegation, negationStratificationErrors, and assertStratifiedNegation().

Treat remote source as executable logic. Although EyeProlog has no arbitrary host call primitive, search can consume CPU and memory. Embedders should impose appropriate depth, solution, input-size, and time limits.

Those ceilings are operational safeguards. If one is reached, report an incomplete computation rather than turning truncation into a negative domain conclusion.

Part III summary

Part III moved from obtaining answers to trusting them:

You should now be able to distinguish proof trees from search trees, state what an integrity query establishes, explain the finite-answer argument behind tabling, and name which trust duties remain outside the solver.

Historical note: from answers to accountable inference

The least-model semantics developed by van Emden and Kowalski in 1976 connected definite programs to a mathematical fixed point: repeatedly add supported ground consequences until nothing new appears. Tabled logic programming later turned fixed-point ideas into a goal-directed technique that shares recursive calls and accumulates answers. EyeProlog’s automatic positive tabling is smaller than the general systems in that literature, but inherits their central insight: remembering a recursive question can change termination without changing what the relation says. For finite Datalog with recursion through explicit tnot/1, EyeProlog also uses the alternating-fixed-point account of the well-founded semantics so a negative cycle may remain undefined instead of being collapsed into ordinary negation-as-failure.

In parallel, deductive databases asked where facts come from and how derived claims retain provenance. EyeProlog adopts the expectation that conclusions should be inspectable while implementing a focused ISO Prolog profile.

The historical lesson is architectural. A proof procedure can attest that a conclusion follows from supplied clauses. It cannot authenticate a database, calibrate a sensor, or authorize a request. Systems became more trustworthy when those boundaries became named rather than implicit.

Part IV — The craft of logic programming

A logic programmer works between domain sketches, design questions, and tested EyeProlog clauses.
Craft moves repeatedly between the real domain, the relations on paper, executable clauses, answers, and proofs.

This Part turns from implementation features to habits of construction. A good program rarely arrives whole; it is discovered through examples, corrected by invariants, and refined without losing sight of the relation it means.

17. Logic and control

The central pleasure—and central difficulty—of logic programming is that a short definition plays two roles. Consider:

This distinction is one of logic programming’s oldest and most durable design ideas. The logical component describes admissible answers; the control component determines which consequences are explored, in what order, and with what resource cost. A change in indexing, goal order, or tabling policy should ideally preserve the first while improving the second. In practice, modeful built-ins and incomplete searches mean that programmers must reason about both.


:- use_module(library(lists)).

path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

As logic, the clauses say that every edge is a path and that an edge followed by a path is a path. As control, they tell the solver to try a direct edge first, then choose an outgoing edge and continue from its endpoint.

It is useful to write the relation first as a sentence:

path(X, Y) holds when there is a finite sequence of edges from X to Y.

That sentence is independent of clause order. It is the specification against which examples and counterexamples can be judged. Only then ask procedural questions: which argument will normally be known, which goal generates a finite set, and which recursive call is smaller or already tabled?

The same relation, a different computation

Conjunction is logically commutative, but its textual order guides search. These two rules have the same intended ground consequences:


:- use_module(library(lists)).

adult(Person) :- person(Person), age(Person, Age), (Age >= 18).

adult(Person) :- (Age >= 18), age(Person, Age), person(Person).

The first is executable in the natural open mode because person/1 and age/2 bind values before >=/2 inspects them. The second asks a comparison to operate on unbound variables and fails. Logical equivalence therefore does not imply equivalent behavior for a goal-directed interpreter with modeful built-ins.

Clause order also gives a search order. Put simple and common proofs where they can be found cheaply, provided doing so does not starve a necessary base case. A recursive clause that calls itself before consuming input is a warning:


:- use_module(library(lists)).

% Poor control: recursion starts before one list cell is exposed.
bad_member(X, List) :- bad_member(X, Rest), (List = [_ | Rest]).

The usual definition exposes the decreasing structure first:

item(X, [X | _]).
item(X, [_ | Rest]) :- item(X, Rest).

Modes are part of the design

A predicate has one logical meaning but may support several useful calling patterns. append(Prefix, Suffix, Whole) can:

It is not a useful generator when all three arguments are free: there are infinitely many lists. Before accepting a predicate design, make a small mode table:

Call Intended use Finite?
append(+,+,-) concatenate yes
append(-,-,+) enumerate splits yes
append(-,-,-) generate all triples no

The + and - marks are documentation, not supported Prolog syntax.

A mode is a promise about calls, not a replacement for the relation’s meaning. When a rule calls a helper outside its promised mode, the program may remain logically plausible while becoming operationally useless.

Search trees and proof trees

A proof tree contains only the successful choices supporting one answer. A search tree also contains failed alternatives and repeated attempts. Proof output shows the former; performance counters give clues about the latter. Confusing the two leads to a common surprise: a tiny proof may have required a large search.

A compact successful proof tree beside a larger search tree containing failures and repeated branches.
The proof explains why an answer holds; the search tree explains the work needed to discover that proof.

The distinction also explains why explanations are not performance profiles. Removing a failed branch can make a program dramatically faster without changing the final why/2 term. Conversely, introducing a well-named helper may make a proof longer on paper while making it far clearer to a reader.

When a program is slow, sketch the first few levels of its search tree. Mark:

  1. the selected leftmost goal;
  2. the clauses or built-ins that can solve it;
  3. bindings produced by each choice;
  4. the next selected goal;
  5. branches that repeat a previous call.

This exercise often reveals that the model is sound but a generator is too broad, a constraint is too late, or a witness carries needless alternatives.

Checkpoint. Take one clause and write two notes beside it: its ground meaning and its intended mode. Reorder two body goals, predict whether the answer set, termination, first answer, or proof shape changes, and only then run the variant.

18. Constructing a program

A good logic program is rarely discovered by typing clauses from top to bottom. It is constructed by moving between examples, relations, and invariants.

A program is constructed by cycling from a ground sentence through examples, representation, invariants, clauses, answers, and proofs.
Construction begins with meaning and examples, chooses a representation that exposes an invariant, and lets surprising answers send the design back to the right layer.

Begin with ground sentences

Suppose packages must be routed through compatible hubs. Start with sentences that contain no variables:


:- use_module(library(lists)).

routeable(parcel_7, hub_north).

Decide exactly what that sentence claims. Does it mean the parcel can enter the hub, can leave it, or can complete an entire route through it? Ambiguity in a ground sentence becomes ambiguity in every rule built on it.

Now name the evidence:


:- use_module(library(lists)).

routeable(Parcel, Hub) :-
  destination_zone(Parcel, Zone),
  serves(Hub, Zone),
  package_class(Parcel, Class),
  accepts(Hub, Class).

The variables express the joins already present in the English explanation. No variable should appear merely because “a value might be needed later.” Every repeated variable asserts identity; every distinct variable permits difference.

Invent examples before recursion

For a recursive relation, write the smallest positive example, the next larger positive example, and a near miss. For list prefixes:

prefix([], [a,b])          true
prefix([a], [a,b])         true
prefix([b], [a,b])         false

The empty example suggests the base clause. Comparing the second example with a smaller one suggests removing a matching head from both lists:

prefix([], _).
prefix([X | Xs], [X | Ys]) :- prefix(Xs, Ys).

This is a general construction method: find a measure that becomes smaller, preserve the invariant while reducing it, and state directly the case where no reduction is needed.

Separate generate, test, and describe

Finite combinatorial programs become easier to read when their jobs are separate:

candidate_pair(A, B) :-
  person(A),
  person(B).

compatible_pair(A, B) :-
  candidate_pair(A, B),
  (A \= B),
  \+ conflict(A, B).

answer(pair(A, B)) :- compatible_pair(A, B).

candidate_pair/2 states the domain. compatible_pair/2 states the constraints. answer/1 controls presentation. The split is not bureaucratic: it makes the closed domain visible, gives negation bound arguments, and makes proofs say whether a step generated or rejected a choice.

For performance, tests may be interleaved as soon as their inputs are ready:

compatible_pair(A, B) :-
  person(A),
  person(B),
  (A \= B),
  \+ conflict(A, B).

The conceptual separation remains even when the final clause is compact.

Choose representations by the operations they support

The same domain can be represented in many ways. A graph may be edge facts, a list of edge terms, or a context. Ask which questions dominate:

Do not encode structure into strings and then recover it throughout the theory. Parse once at the boundary. A term such as address(City, PostalCode) can be unified, inspected, and explained; a string containing the same data needs repeated procedural parsing.

Grow a theory through layers

Large rule sets benefit from a dependency direction:

source facts → normalized facts → domain concepts → decisions → answers

Negation should normally point in the same direction, from a higher layer to a complete lower layer. Cycles among positive domain concepts may be tabled; cycles through negation usually signal that the concepts have not been given a stable meaning.

At every layer, add one representative query. Do not wait for the final decision predicate to discover that normalization silently failed. Small queries are the logic-programming counterpart of inspecting intermediate values, but they retain the declarative vocabulary of the model.

Checkpoint. Before writing rules for a small domain of your own, record three positive ground examples, one near miss, the intended query mode, and a candidate finite generator. If the ground sentences are ambiguous, revise the predicate names before introducing variables.

19. Correctness and termination

Testing examples is necessary, but a reusable relation deserves a stronger argument. Two questions should be asked separately:

Overlapping circles for soundness, completeness, and termination meet at a dependable operational contract.
Soundness, completeness, and termination are independent promises; a dependable intended call needs all three.
  1. Partial correctness: if the program returns an answer, is it justified?
  2. Completeness: for the intended finite calls, can it find every answer required by the specification?

For prefix/2, partial correctness follows by the clauses. The base clause returns only the empty prefix. The recursive clause adds the same head to a smaller valid prefix, so the result remains a prefix. Completeness follows in the opposite direction: every nonempty prefix shares its first element with the whole list, and removing that element yields a smaller prefix problem covered by the recursive clause.

This informal induction is often enough. State the property, justify each base clause, assume recursive calls satisfy it, and show that each recursive clause preserves it.

Termination needs its own argument

A correct relation may still fail to return. For ordinary structural recursion, identify a well-founded measure:

The measure must decrease before the recursive call in the intended mode. For factorial, N decreases while remaining a nonnegative integer:

factorial(0, 1).
factorial(N, F) :-
  (N > 0),
  (Previous is N - 1),
  factorial(Previous, PF),
  (F is N * PF).

Reordering the subtraction after the recursive call preserves a mathematical equation but destroys the termination argument.

Tabling changes the argument for graph recursion. A cyclic path/2 call can terminate when the program has only finitely many distinct tabled calls and answers. The measure is then not necessarily smaller at each edge; finiteness comes from exhausting a finite answer space. Tabling cannot rescue a rule that constructs s(s(s(...))) without bound.

Negation and aggregation require bounded subsearch

\+ Goal and aggregates ask the engine to settle a nested search. Their meaning is usable only when that search can finish. Before writing:

\+ disqualified(Person)

check that Person is bound and that disqualified/1 has a finite search for that value. Before collecting routes, decide whether only simple routes, only routes below a cost, or some other finite family is intended.

Integrity is not merely failure

Ordinary failure says that one attempted proof did not work. An explicit integrity relation can instead return the evidence for an invalid state:

invalid_limits(Name, Low, High) :-
  lower_limit(Name, Low),
  upper_limit(Name, High),
  (Low > High).

This distinction matters operationally and socially. A failed eligibility query may be a legitimate negative result. A successful invalid_limits/3 query identifies contradictory limits; the host can then stop decisions until the input is repaired.

Checkpoint. For one recursive relation, state three claims separately: partial correctness, completeness in one intended mode, and termination in that mode. Give the invariant supporting the first two and the decreasing measure or finite table supporting the third.

20. Improving a program

Program improvement begins with observation, not cleverness. Preserve a set of representative answers and proofs, collect solver statistics, and change one structural choice at a time.

Strengthen calls before adding machinery

The most effective improvement is often a better question. Prefer route(brussels, Destination) to a completely open enumeration if the application already knows its origin. Put selective, indexed relations early enough to bind arguments for later work. Avoid constructing a large witness when the caller needs only existence.

Compare:

connected(X, Y) :- path_with_nodes(X, Y, _).

with a direct reachability relation that tables pairs. The first may enumerate many distinct paths to establish one fact; the second records the fact itself. Keep the witness-producing relation for callers that truly need a path.

Introduce helpers that express invariants

Inlining every condition creates wide clauses with repeated work. A helper can name a stable concept:

within_thermal_limits(Battery) :-
  temperature(Battery, T),
  temperature_limit(Max),
  (T =< Max).

The gain is not just reuse. Proofs now contain a domain statement, and later changes to the limit policy have one home. Choose helpers that add vocabulary; avoid names such as step2/3 that merely expose an implementation sequence.

Move invariant work outward

If a recursive call repeatedly computes a value that does not change, compute it once and pass the result:

search(Request, Answer) :-
  normalized_request(Request, Normalized),
  search_normalized(Normalized, initial_state, Answer).

This resembles loop-invariant code motion in procedural programming, but the relational formulation is explicit: the helper’s arguments show exactly which values vary from step to step.

Preserve meaning while changing control

Reordering goals, adding a helper, or specializing a predicate should preserve the intended ground answers. Verify that with:

An optimization that changes which proof is found first may affect once/1, tie-breaking aggregates, and explanation shape even when the answer set is unchanged. Treat those observable choices as part of the calling contract whenever users depend on them.

Know when to stop

Not every relation should be made maximally general. A three-mode predicate can be harder to terminate, explain, and index than two simple predicates with clear contracts. Generalize when a real second use appears. The art lies in keeping the logical idea visible while giving it enough control to run well.

Checkpoint. Save representative answers, one proof, and solver statistics for a program. Make exactly one control change, rerun all three views, and classify every difference as intended, harmless but observable, or a regression.

Part IV summary

Part IV treated logic programming as a discipline of construction:

You should now be able to construct a theory from examples, state a termination measure, refactor a helper without losing meaning, and recognize when greater relational generality has no practical use.

Historical note: logic plus control

Kowalski’s 1979 formulation “algorithm = logic + control” gave a durable name to the dual reading developed here. The logic component specifies knowledge; control determines how it is used. The slogan did not claim that control was unimportant. It argued that control can often be improved while meaning stays steady, and that programs become easier to reason about when the two are distinguished.

The craft tradition of Prolog grew around this tension. Goal ordering, accumulators, generate-and-test, and representation change were never merely interpreter tricks. At their best they were transformations justified by invariants and modes. Sterling and Shapiro made construction and improvement central to The Art of Prolog, showing that declarative clarity and procedural competence mature together.

EyeProlog removes several classic Prolog control devices, especially cut. The smaller surface changes the techniques but not the problem: authors must still turn a true relation into a productive computation and say what was preserved.

Part V — Advanced relational design

A central relation connects a search tree, a syntax tree, a transformed program, and an auditable decision.
Advanced design keeps meaning at the center while search is inspected, syntax is represented, control is transformed, and decisions remain auditable.

The earlier parts introduced the supported Prolog profile and the habits needed to use it safely. This part stays longer with whole computations. It asks how to inspect a search tree, represent languages and evaluators as relations, transform a correct program without losing its meaning, and organize a decision system whose conclusions remain auditable.

EyeProlog supplies the Part 1 control, dynamic-database, operator, and I/O facilities together with its normal-profile module forms module/2, use_module/1, use_module/2, and Module:Goal. These forms are treated as a module compatibility surface, not as a claim of complete ISO/IEC 13211-2:2000 conformance. Definite-clause grammar notation remains outside this profile. The examples still prefer explicit domain relations, state, and syntax trees where that makes assumptions easier to inspect.

21. Reading the computation

A query is not solved in one leap. It is reduced to goals, each goal is matched against candidate clauses, and each successful match contributes bindings and new subgoals. The computation has two kinds of branching:

This and–or structure is the operational counterpart of the program’s logical structure. A conjunction asks for several supporting claims; multiple clauses offer alternative justifications.

parent(ada, byron).
parent(byron, clara).
parent(clara, diego).

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).

eyeprolog --goal 'ancestor(ada, Who)' program.pl

For ancestor(ada, Who), the first clause asks parent(ada, Who) and produces Who = byron. The second clause asks two questions in sequence. parent(ada, Y) first binds Y = byron; the remaining call is therefore ancestor(byron, Who). That call repeats the choice between a direct-parent proof and a longer proof.

The three answers occupy increasing depths of one proof family:

ancestor(ada, byron)
  parent(ada, byron)

ancestor(ada, clara)
  parent(ada, byron)
  ancestor(byron, clara)
    parent(byron, clara)

ancestor(ada, diego)
  parent(ada, byron)
  ancestor(byron, diego)
    parent(byron, clara)
    ancestor(clara, diego)
      parent(clara, diego)

Drawing even a partial tree exposes errors that are hard to see in source alone: a variable that should have been shared, a recursive call that did not consume input, or a generator placed after the test that needs its output.

An ancestor query branches between clauses while a binding ledger shows Y becoming byron and flowing into the remaining recursive goal.
Search alternates between choices and conjunctions; substitutions flow forward, while failure returns to the latest unfinished choice.

Substitutions accumulate

A substitution is a set of bindings carried through the remaining goals. Bindings are not local return values. If the first goal binds a variable, every later occurrence of that variable sees the same term:

grandparent(X, Z) :-
  parent(X, Y),
  parent(Y, Z).

Solving grandparent(ada, Z) begins with parent(ada, Y). Once that goal binds Y to byron, the second goal is the selective parent(byron, Z).

Repeated variables impose equality through unification:


:- use_module(library(lists)).

loop_edge(Node) :- edge(Node, Node).

This does not find an arbitrary edge and compare its endpoints later. The shared variable makes equal endpoints part of the pattern being matched.

Failure rewinds choices, not facts

Suppose a later goal fails:


:- use_module(library(lists)).

eligible(Person) :-
  applicant(Person),
  age(Person, Age),
  (Age >= 18),
  verified(Person).

Failure of verified(Person) rejects the current combination of bindings. Search may return to another age/2 fact or another applicant clause. It does not retract source facts or erase answers already printed. Backtracking is better understood as exploring alternatives than as undoing the world.

Variants, cycles, and tables

Recursive graph search can encounter the same logical subquestion through different paths. Calls that differ only in variable names are variants: path(a, X) and path(a, Y) pose the same pattern. Positive recursive groups can table such patterns, share their answers, and stop a cycle from expanding the same question forever.

The table does not prove termination for every recursive program. If each call constructs a larger pattern, then the calls are not variants:

grows(X) :- grows(wrapper(X)).

grows(A), grows(wrapper(A)), and grows(wrapper(wrapper(A))) are distinct calls. Remembering them does not make their number finite.

A practical tracing discipline

When a query surprises you, write down:

  1. the selected goal;
  2. its current resolved arguments;
  3. the candidate clause;
  4. the unifier produced by the head;
  5. the new body goals;
  6. the point to which failure would return.

Compare that hand trace with --proof for a successful answer and --stats for the amount of search. Proofs explain one successful derivation; statistics summarize work across successful and failed branches. Neither is a complete trace, but together they usually locate the modeling issue.

Exercises.

  1. Draw the and–or tree for ancestor(byron, Who).
  2. Add a second parent of clara and identify where the tree branches.
  3. Write a cyclic edge/2 graph and compare reachability answers with the table rounds reported by --stats.
  4. Construct a recursive rule whose call grows a list on every step. Explain why variant tabling does not make its call space finite.

Checkpoint. Hand-trace one successful answer and one failed branch using the six-item tracing discipline. Compare the successful trace with --proof and the total work with --stats; state one fact that each view omits.

22. Trees, languages, and symbolic evaluation

Compound terms are finite trees. A functor labels an internal node and its arguments are the children. Lists are one familiar tree encoding, but syntax, plans, types, circuits, formulas, and organizational structures can all be represented directly.

tree(
  oak,
  tree(birch, empty, empty),
  tree(pine, empty, empty)
).

A structural relation follows the representation:


:- use_module(library(lists)).

tree_member(X, tree(X, _, _)).
tree_member(X, tree(_, Left, _)) :- tree_member(X, Left).
tree_member(X, tree(_, _, Right)) :- tree_member(X, Right).

The clauses say where a member may occur. They also define a search order: root, then left subtree, then right subtree. If only membership matters, that order is an implementation choice. If a caller uses once/1, it becomes observable.

One expression tree is inspected as data, evaluated to a value, and rewritten to another syntax tree with an explicit environment.
A compound term remains persistent data; different relations inspect, evaluate, or rewrite it according to the question being asked.

Transforming a tree

mirror(empty, empty).
mirror(
  tree(Value, Left, Right),
  tree(Value, MirroredRight, MirroredLeft)
) :-
  mirror(Left, MirroredLeft),
  mirror(Right, MirroredRight).

Read forward, mirror/2 constructs a mirror. With both trees ground, it verifies the relationship. In some partially bound modes it can fill missing structure. The rule does not mutate a tree; it relates two persistent terms.

The representation exposes an invariant: mirroring preserves every node value and exchanges left and right at every level. It also suggests a structural induction. The empty tree is its own mirror; if both recursive calls are correct, the constructed parent is correct.

A standard definite clause grammar

ISO/IEC TS 13211-3 definite clause grammar rules describe a sequence while the processor supplies the pair of difference-list arguments used for execution:

sentence --> noun_phrase, verb_phrase.

noun_phrase --> [the], noun.
noun_phrase --> [a], noun.

noun --> [robot].
noun --> [scientist].

verb_phrase --> verb, noun_phrase.

verb --> [helps].
verb --> [observes].

complete_sentence(Words) :- phrase(sentence, Words).

eyeprolog --goal 'complete_sentence([the, robot, helps, a, scientist])' program.pl

The expansion of sentence//0 is an ordinary sentence/2 relation: its first extra argument is the sequence before parsing and its second is the suffix. Composition shares the suffix from noun_phrase//0 with the input to verb_phrase//0. phrase/2 requires complete consumption; phrase/3 exposes the remaining sequence.

The same relation can be a bounded generator when vocabulary and output length are constrained by surrounding relations. An unconstrained complete_sentence(Words) call can generate sentences of unbounded length if the grammar is recursive. A grammar is also a search program, so its intended modes need the same termination analysis as other recursive relations.

Interpreting an expression

Syntax trees separate the expression from the act of evaluating it:

evaluate(number(N), N).

evaluate(add(Left, Right), Value) :-
  evaluate(Left, L),
  evaluate(Right, R),
  (Value is L + R).

evaluate(multiply(Left, Right), Value) :-
  evaluate(Left, L),
  evaluate(Right, R),
  (Value is L * R).

eyeprolog --goal 'evaluate(
    add(number(2), multiply(number(3), number(4))),
    Value
  )' program.pl

The value is 14. More importantly, the proof follows the syntax tree: two literal evaluations support one multiplication and one addition.

An extension can add variables and an explicit environment:


:- use_module(library(lists)).

lookup(Name, [binding(Name, Value) | _], Value).
lookup(Name, [_ | Rest], Value) :- lookup(Name, Rest, Value).

evaluate(variable(Name), Environment, Value) :-
  lookup(Name, Environment, Value).

Passing the environment as data avoids hidden global state. Shadowing is determined by list order and should be documented as part of lookup/3.

Rewriting symbolic expressions

Evaluation collapses syntax to a value. Rewriting preserves syntax while replacing one form with an equivalent or preferred form:

simplify(add(number(0), X), X).
simplify(add(X, number(0)), X).
simplify(multiply(number(1), X), X).
simplify(multiply(X, number(1)), X).

simplify(add(A, B), add(SA, SB)) :-
  simplify(A, SA),
  simplify(B, SB).

Overlapping rules can produce several answers. That may be desirable when exploring equivalent forms, but a normalizer needs a strategy and termination measure. A rule that expands X to add(X, number(0)) reverses the first simplification and permits unbounded rewriting.

Exercises.

  1. Define tree_size/2 and tree_height/2.
  2. Extend the grammar with adjectives while preserving the input/suffix contract.
  3. Add subtraction to the evaluator and state which arguments must be ground.
  4. Define constant folding for add(number(A), number(B)).
  5. Explain why individually sensible rewrite rules may fail to terminate when repeatedly combined.

Checkpoint. For one compound term, label the object-language syntax, the EyeProlog relation that inspects it, and the environment or state used to interpret it. Then identify a rewrite pair that would create a cycle if both directions were enabled.

23. Transforming programs

Program transformation changes clauses while attempting to preserve an intended relation. The useful question is not merely “does the new version run?” but “for which calls does it preserve answers, termination, answer order, and explanations?”

Four transformations recur in logic programs:

Each can improve control or reveal structure. Each can also change modes, duplicate work, or alter proof shape.

An original relation branches into unfolding, folding, specialization, and accumulation, then all four return to a shared contract comparison.
Transformation is a controlled experiment: change the clauses, then compare meaning, supported modes, termination, proof shape, and cost.

Unfolding and folding

Start with:


:- use_module(library(lists)).

adult(Person) :-
  recorded_age(Person, Age),
  adult_age(Age).

adult_age(Age) :- (Age >= 18).

Unfolding adult_age/1 gives:


:- use_module(library(lists)).

adult(Person) :-
  recorded_age(Person, Age),
  (Age >= 18).

For this deterministic helper, the ground answers are unchanged. The shorter proof loses the named concept adult_age/1, however. That loss may be undesirable in an auditable policy even if execution becomes slightly cheaper. If a helper has several clauses, unfolding produces one caller clause for each alternative. If it is recursive, unrestricted unfolding may never finish.

Folding moves in the other direction. Suppose decisions repeat:


:- use_module(library(lists)).

can_board(Person) :-
  registered(Person),
  identity_checked(Person),
  \+ suspended(Person),
  has_ticket(Person).

can_enter_lounge(Person) :-
  registered(Person),
  identity_checked(Person),
  \+ suspended(Person),
  lounge_pass(Person).

Name the shared concept:


:- use_module(library(lists)).

traveler_in_good_standing(Person) :-
  registered(Person),
  identity_checked(Person),
  \+ suspended(Person).

can_board(Person) :-
  traveler_in_good_standing(Person),
  has_ticket(Person).

can_enter_lounge(Person) :-
  traveler_in_good_standing(Person),
  lounge_pass(Person).

The helper is valuable because it has a stable meaning, not merely because three lines became one. It creates one place to state and test the closed-world assumption behind \+ suspended(Person).

Specializing a relation

A general transport database may use:

connection(Mode, From, To, Cost).

An application that only plans rail journeys can define:

rail_connection(From, To, Cost) :-
  connection(rail, From, To, Cost).

This wrapper establishes a stronger contract and gives indexing a bound first argument. Deeper specialization can precompute invariant classifications or remove irrelevant branches. Keep the general relation as the specification against which specialized answers are compared.

Accumulators and modes

A direct list sum performs work after recursion:

sum_numbers([], 0).
sum_numbers([X | Xs], Sum) :-
  sum_numbers(Xs, Rest),
  (Sum is X + Rest).

An accumulator makes the partial sum explicit:

sum_numbers_acc(List, Sum) :- sum_from(List, 0, Sum).

sum_from([], Accumulator, Accumulator).
sum_from([X | Xs], Accumulator, Sum) :-
  (Next is Accumulator + X),
  sum_from(Xs, Next, Sum).

For a ground numeric list, both versions return the same sum. They do not have identical relational behavior in every mode. The accumulator version requires each intermediate addition to be ready on the way down. State the intended mode instead of claiming unconditional equivalence.

A transformation checklist

Before replacing one definition with another, record:

  1. the intended ground relation;
  2. supported binding patterns;
  3. a termination measure for each supported pattern;
  4. whether duplicates and answer order matter;
  5. whether callers inspect proof structure;
  6. representative positive, negative, and boundary queries.

Then compare both versions. --stats can show fewer calls or unifications, but performance evidence comes after semantic evidence. A faster program that silently drops a mode is a different program.

Exercises.

  1. Unfold a two-clause helper and count the resulting caller clauses.
  2. Fold repeated validation conditions in two rules of your own.
  3. Specialize a generic graph relation for one edge type.
  4. Compare direct and accumulator-based length relations in several modes.
  5. Find a transformation that preserves answers but changes the first proof selected by once/1.

Checkpoint. Choose one original and transformed relation. Compare their answer sets in both directions over a finite domain, then separately compare termination, answer order, duplicates, proof shape, and solver statistics.

Nondeterminism is not randomness. A nondeterministic relation defines several legitimate continuations, and search systematically explores them. The design problem is to make useful alternatives complete while keeping their number finite and their order productive.

A funnel narrows six generated worker-task candidates through ready constraints into four witnesses before ordering the survivors.
Finite search is designed from the top down: bound generation, prune with ready constraints, preserve the witness, then order only the survivors.

Generate, constrain, describe

A clear search program often has three layers:

  1. generate a candidate from a finite domain;
  2. constrain the candidate;
  3. describe or score the surviving witness.
worker(ada).
worker(byron).
worker(clara).

task(inspect).
task(repair).

qualified(ada, inspect).
qualified(byron, repair).
qualified(clara, inspect).
qualified(clara, repair).

assignment(Worker, Task) :-
  worker(Worker),
  task(Task),
  qualified(Worker, Task).

eyeprolog --goal 'assignment(Worker, Task)' program.pl

worker/1 and task/1 make the search space explicit. qualified/2 is both a constraint and a selective relation. If the application knows the task, calling assignment(Worker, repair) avoids generating irrelevant task values.

Search over states

A state-space problem needs a state term, a finite move relation, a goal test, a policy for repeated states, and a witness representation. A simple graph path carries visited nodes:


:- use_module(library(lists)).

simple_path(From, To, Path) :-
  walk(From, To, [From], Reversed),
  reverse(Reversed, Path).

walk(To, To, Visited, Visited).
walk(From, To, Visited, Path) :-
  edge(From, Next),
  \+ member(Next, Visited),
  walk(Next, To, [Next | Visited], Path).

The visited list makes the witness finite on a finite graph. It also changes the question from arbitrary walks to simple paths. That is a modeling choice, not merely an optimization. A caller asking for repeated stops needs another bound, such as maximum steps or cost.

Existence, one witness, and all witnesses

These questions have very different costs:


:- use_module(library(lists)).

reachable(From, To).
once(simple_path(From, To, Path)).
findall(Path, simple_path(From, To, Path), Paths).

Reachability needs only a pair and is a good candidate for tabling. One path may stop after the first witness. All simple paths may be exponentially numerous even though the graph is finite. Choose the weakest result that meets the caller’s need.

Optimization is search plus an order

An optimal answer requires a finite candidate relation and a comparison key:

:- use_module(library(aggregate)).
:- use_module(library(lists)).

best_plan(Request, Plan, Cost) :-
  aggregate_min(
    [CandidateCost, CandidatePlan],
    CandidatePlan,
    candidate_plan(Request, CandidatePlan, CandidateCost),
    [Cost, Plan],
    Plan
  ).

The structured key makes ties deterministic. It does not reduce the candidate space: aggregate_min/5 must settle the nested search before knowing the minimum. For a large problem, strengthen candidate_plan/3 or use a domain-specific dynamic program instead of assuming aggregation performs branch-and-bound.

Depth-first clause search can become trapped in an infinite branch before reaching a later finite proof. Base cases should be reachable before recursive expansion, and recursive steps should consume a finite resource or enter a finite table. When neither is possible, the query is outside the practical contract of the relation.

Multiple clauses normally mean that any or all may yield legitimate answers. once/1 turns the first success into a don’t-care choice: later alternatives are intentionally discarded. Use it only when selection order is an accepted part of the specification.

Exercises.

  1. Add skills and time slots to the assignment example.
  2. Modify simple_path/3 to return accumulated cost.
  3. Compare reachability, one path, and all paths on a diamond-shaped graph.
  4. Give a finite candidate relation for which aggregate_min/5 still performs an impractically large search.
  5. Construct a recursive first clause that starves a valid later base clause, then repair its control.

Checkpoint. Write down the size of a candidate space before running its search. Name the generator, the earliest ready constraint, the witness, and the ordering used for optimization. If the size cannot be bounded, the design is not yet ready for aggregation.

25. Case study: an auditable decision service

This case study develops a small access decision from prose to an executable, explainable theory. The purpose is the sequence of design decisions that turns informal requirements into maintainable relations.

Versioned source facts and policy pass integrity checks and reasoning to produce a decision with a replayable proof bundle.
An auditable service keeps source and theory versions attached to the premises, blocks invalid input at an integrity gate, and returns the decision with replayable provenance.

Requirements and questions

A research facility says:

Before coding, identify ambiguities. Is the badge registry complete? Is missing training evidence a denial or unknown? Can a person have several active badges? Which clock determines “current”? A rule engine cannot remove these choices; it can only make the chosen answers precise.

Source and concept layers

Represent observations without embedding decisions:


:- use_module(library(lists)).

person(ada).
badge(b17, ada).
badge_status(b17, active).
badge_clearance(b17, laboratory).
zone_requires(clean_room, laboratory).
training_valid(ada, clean_room).

The badge identifier remains explicit. Collapsing it into active_badge(ada) would hide the record used as evidence and make conflicting records harder to detect.

Build vocabulary that reads like the policy:


:- use_module(library(lists)).

active_badge(Person, Badge) :-
  badge(Badge, Person),
  badge_status(Badge, active).

cleared_for(Badge, Zone) :-
  badge_clearance(Badge, Clearance),
  zone_requires(Zone, Clearance).

prepared_for(Person, Zone) :-
  training_valid(Person, Zone).

Each helper has one responsibility. A proof of cleared_for/2 names both the badge clearance and zone requirement rather than burying their join in a wide decision clause.

Closed-world choice

If the suspension list is authoritative and complete, absence can be used:

in_good_standing(Person) :-
  person(Person),
  \+ suspended(Person).

If it is incomplete, this rule is unsound as policy. Replace it with a positive source claim such as standing(Person, good). The difference is an agreement about the knowledge boundary, not a matter of syntax.

Decision, reasons, and proof


:- use_module(library(lists)).

permit(Person, Zone) :-
  active_badge(Person, Badge),
  cleared_for(Badge, Zone),
  prepared_for(Person, Zone),
  in_good_standing(Person).

reason(Person, Zone, badge_and_training_verified) :-
  permit(Person, Zone).

eyeprolog --goal 'permit(Person, Zone)' program.pl
eyeprolog --goal 'reason(Person, Zone, Reason)' program.pl

reason/3 supplies a stable user-facing summary. With --proof, the same answer carries its detailed derivation. These are complementary: the reason is domain vocabulary, while the proof records actual clauses and bindings.

Integrity before decisions

Contradictory badge states are exposed by an explicit validation relation:

incompatible_status(active, revoked).
incompatible_status(revoked, active).

invalid_badge_status(Badge, Status, Other) :-
  badge_status(Badge, Status),
  incompatible_status(Status, Other),
  badge_status(Badge, Other).

This result does not say that one permit failed. It identifies input that is unfit for a trusted decision. The host can query invalid_badge_status/3 before permit goals, alongside checks for a badge assigned to two people or a zone with incompatible clearance definitions.

Tests are policy examples

A useful test set includes an ordinary permit, missing training, suspension, insufficient clearance, duplicate derivations, contradictory status, and a proof showing the exact badge and training facts.

Boundary examples reveal requirements. If a person has two valid badges, should there be one permit with two derivations or two permit terms containing the badge? permit(Person, Zone) chooses one ground decision with potentially several proofs. If badge identity belongs in the answer, define permit(Person, Zone, Badge).

Embedding and audit

Authenticate source systems in the host, convert records to EyeProlog facts, run the theory, and store the answer with its proof and input version. The solver can explain logical support; it cannot attest that a badge database was current or a training provider trustworthy.

authenticated source snapshot
  -> normalized EyeProlog facts
  -> checked theory
  -> permit and reason
  -> proof referencing clauses and facts

When policy changes, preserve old inputs, theory versions, and proofs so a past decision can be reconstructed under the rules that actually governed it.

Exercises.

  1. Add time-bounded training using explicit dates and difference/3.
  2. Model denial/3 without assuming every failed permit has the same reason.
  3. Add a two-person escort rule and identify duplicate-proof cases.
  4. Write an integrity relation for badges assigned to multiple people.
  5. Define the validation the host must perform before supplying badge facts.
  6. Run the case with --proof and decide which helpers improve the explanation.

Checkpoint. Reconstruct one permit decision from a preserved source snapshot, theory version, answer, and proof. Mark which step authenticates the source, which checks integrity, which derives the decision, and which merely stores evidence for later audit.

Part V summary

Part V followed whole computations rather than isolated features:

You should now be able to trace substitutions through several goals, represent an object language without confusing it with the surrounding Prolog syntax, justify a bounded program transformation, and design a reconstructable decision theory.

Historical note: interpreters, transformation, and the art tradition

Logic programming became a laboratory for symbolic programming because its principal data—terms, clauses, substitutions, and proof trees—could be represented with the same structures used for ordinary domains. Meta-interpreters made resolution itself a program topic; grammar rules made language recognition relational; partial evaluation showed how a general relation could be specialized when part of its input was known.

Futamura’s work in the 1970s gave partial evaluation a striking interpretation: specializing an interpreter with respect to a source program can produce a compiled form. Logic-program transformation developed related practices of unfolding, folding, and specialization. The inheritance for EyeProlog is not a promise that every classic transformation is built in. It is the demand that a transformation name its invariant and preserve a stated answer contract.

The Art of Prolog joined computation, construction, nondeterminism, grammars, interpreters, transformation, and applications into a sustained account of craft. Part V pays tribute to that breadth through EyeProlog’s explicit subset: syntax is data, state is an argument, and audit evidence remains visible.

Part VI — Mathematics made executable

A bridge carries mathematical definitions and proof into executable clauses, witnesses, counterexamples, and derivations.
Formal clauses form a bridge: definitions and invariants become computations that return witnesses, counterexamples, and inspectable proofs.

This Part is a route, not a prerequisite for the reasoning laboratory. For a short practical path, read Chapters 26, 27, and 29, then continue at Chapter

  1. Read Chapters 28 and 30 as well when representation, formal scope, and the limits of computation are central to your purpose.

Mathematics appears throughout this book as subject matter: arithmetic, combinatorics, graphs, geometry, algebra, statistics, and physical models. But its deeper presence is structural. A logic program is possible because parts of mathematical reasoning can be represented as finite symbols, transformed by explicit rules, and checked step by step.

In that qualified sense, the history of logic programming belongs inside the history of mathematics. It inherits the mathematician’s old practices of definition, proof, construction, abstraction, and counterexample. It also inherits the twentieth century’s harder questions. What counts as a formal proof? What is an effective procedure? Which truths follow from a finite set of axioms? Which questions cannot be decided by any uniform mechanical method?

EyeProlog inherits a small, practical fragment of that tradition. It is not a foundation for all mathematics, a computer algebra system, or an interactive theorem prover. Its definite clauses cover only a disciplined fragment of logic. Precisely because the fragment is small, however, one can see the ancient mathematical acts inside the running machine:

Mathematical act EyeProlog form Operational consequence
Define a class facts and clauses enumerate its instances
Introduce an unknown a variable seek a substitution
Use a lemma call a helper relation open a subgoal
Split into cases multiple clauses create alternatives
Perform induction base and recursive clauses reduce to smaller calls
Construct a witness bind an output term return evidence, not only truth
Refute a universal guess search for a counterexample one answer is enough
Check consistency an explicit integrity query let the host reject or report invalid input
Explain a conclusion a proof term expose the successful derivation

The table is a correspondence, not an identity. A mathematical proof and an EyeProlog execution answer different questions unless the encoding between them is itself justified. This Part develops both the power and the limit of the correspondence.

26. A proof can be a computation

For most of mathematical history, an algorithm and a proof could live close together without being regarded as the same kind of object. Euclid’s algorithm computes a greatest common divisor, while Euclid’s propositions justify why the procedure works. A geometrical construction produces an object, while an argument establishes that it has the required properties. The distinction remains useful, but modern logic revealed increasingly exact connections among a proposition, its proof, and the construction carried by that proof.

An existential query passes through theory and proof search, producing both a ground object witness and a derivation witness.
A successful existential query returns an object that satisfies the claim and a derivation that explains why the theory licenses that object.

Logic programming enters through one particular connection. A definite clause

mortal(X) :- human(X).

is at once an implication-like statement and an instruction for reducing the question mortal(socrates) to the subquestion human(socrates). A successful derivation does not merely return true; it records a sequence of justified reductions and the substitutions that made them fit.

From axioms to effective procedure

The route was neither straight nor inevitable. A compact historical spine is:

  1. Axiomatization. Nineteenth- and early-twentieth-century mathematics sharpened the demand that assumptions and inference rules be stated explicitly. Hilbert’s program made formal proof and consistency central mathematical subjects.
  2. Limits of formal systems. Gödel showed that sufficiently expressive, effectively axiomatized consistent systems cannot capture every arithmetical truth within themselves. Formalization acquired proven limits, not merely engineering difficulties.
  3. Effective calculability. Church and Turing gave exact, extensionally equivalent accounts of effective computation and established that some decision problems have no general algorithm.
  4. Ground instances. Herbrand connected quantified first-order statements to finite combinations of ground instances. The terms used to instantiate variables became central proof objects.
  5. Machine-oriented inference. Robinson’s resolution principle combined clauses and unification into a small general proof mechanism.
  6. Logic as a programming language. Prolog specialized these ideas into an executable discipline, and the least-model and fixed-point semantics of van Emden and Kowalski explained how definite programs denote their ground consequences.

Each step narrowed one ambiguity while uncovering another. Formal syntax made proofs mechanically inspectable, but Gödel marked the boundary of formal completeness. Models of computation made “algorithm” exact, but Church and Turing marked the boundary of decidability. Resolution made inference uniform, but a proof procedure still needed control: selection order, clause order, termination discipline, and eventually tabling.

Logic programming is therefore not the historical triumph of machinery over mathematics. It is one result of mathematics becoming reflective about its own methods.

Answers are existential witnesses

Consider a relation for a Pythagorean triple:

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

triple(A, B, C) :-
  between(1, 20, A),
  between(A, 20, B),
  between(B, 20, C),
  (AA is A * A),
  (BB is B * B),
  (Sum is AA + BB),
  (Sum is C * C).

eyeprolog --goal 'triple(A, B, C)' program.pl

The open query asks an existential question over a finite domain: find values for which the equation holds. Each printed ground answer is a witness. The substitution is not an incidental side effect; it is the computational content of the existential claim.

A verifier and a generator are logically close but operationally different. If A, B, and C are already known, the arithmetic goals check a candidate. If they are unknown, the bounded between/3 calls create candidates first. The equation alone does not tell a mode-sensitive evaluator where numbers should come from.

This is an important distinction between mathematical existence and executable witness production. A classical proof may establish that something exists without furnishing an efficient construction. An EyeProlog query produces a witness only when its clauses and control actually reach one.

Proof objects and proof checking

The normal answer


:- use_module(library(lists)).

triple(3, 4, 5).

states the result. Proof output adds the successful chain of facts, rule uses, built-ins, and bindings. That evidence supports three different activities:

These activities must not be conflated. A derivation can be mechanically valid but pedagogically obscure. It can be clear but depend on an untrustworthy source fact. It can be valid in the implemented arithmetic but fail to express the intended physical quantity. Proof output makes scrutiny possible; it does not perform all scrutiny on the reader’s behalf.

The least model as mathematical closure

For a definite program, begin with its ground facts. Repeatedly add every ground rule head whose ground body is already satisfied. The least fixed point of this operation is the least Herbrand model.

For


:- use_module(library(lists)).

edge(a, b).
edge(b, c).

path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

the closure first contains the two edges, then the corresponding direct paths, then path(a, c). No unsupported path is added. Bottom-up closure and goal-directed proof search approach the same declarative meaning from opposite directions: one asks what follows globally, the other asks what is needed for this goal.

Automatic tabling makes the connection visible. A table for a recursive component grows monotonically with newly discovered answers until no rule adds another. The implementation is performing a local, demand-driven fixed-point calculation.

There is an important lifetime distinction between a table that is needed to finish one fixed point and a cache of tables retained for possible later reuse. For recursive grammars invoked through phrase/2-3, EyeProlog uses a separate invocation-keyed table scope rather than the caller’s general table map. Static analysis also recognizes the normalized DCG form of strict list-tail recursion (for example ... --> [_], ...). On a new input, such a grammar runs directly without automatic tabling because every recursive call consumes the input and there is no fixed-point cycle to close. This prevents a stream of distinct sequences from constructing a useless suffix-table family for every input.

The optimization is deliberately asymmetric. If the same phrase/2-3 invocation repeats, normal tabling is allowed again so the compact completed table from that invocation can serve subsequent repetitions. That is useful for workloads that probe one grammar/input many thousands of times. Only one invocation signature is retained in the phrase scope, completed entries are still subject to a bound, and active fixed points are never evicted. Thus the policy limits cross-call retention without turning each distinct input into an O(cache-size) eviction pass or changing the declarative answers.

Exercises.

  1. Run the triple program with one, two, and three arguments bound. Compare the logical question, answer set, and search size.
  2. Add a primitive-triple test by rejecting triples whose three values share a divisor. State exactly which finite generators make the negation safe.
  3. Inspect examples/fundamental-theorem-arithmetic.pl. Separate the witness it constructs from the property it verifies.
  4. Draw the fixed-point stages for a four-edge graph containing one cycle.
  5. Find a proof whose machine form is correct but whose helper names make it a poor human explanation.

Checkpoint. For one printed mathematical answer, state the existential claim witnessed by its bindings, the finite domain that made search effective, and the separate argument—if any—that justifies a universal theorem.

27. Recursion is induction in motion

Recursion and mathematical induction are not identical, but they are natural partners. Induction justifies a statement for every object generated by a finite construction. Recursion defines a result by following that same construction toward smaller objects.

For natural numbers represented as z, s(z), s(s(z)), and so on:

natural(z).
natural(s(N)) :- natural(N).

plus(z, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).

The clauses for plus/3 say:

Operationally, the first argument decreases by one constructor until it reaches z. Mathematically, the clauses mirror a recursive definition. To prove a property of plus/3 for all Peano naturals, induction on that first argument is the obvious proof shape.

Parallel ladders align a base clause with an induction base case, a recursive call with the induction hypothesis, and the rule head with the preserved conclusion; a separate box states the decreasing termination measure.
Recursion and induction can share a structural skeleton, but termination still requires its own well-founded decreasing measure.

Three obligations, not one

A recursive mathematical program invites three separate arguments:

  1. Partial correctness: if the relation returns an answer, does the answer satisfy the intended specification?
  2. Completeness for the intended mode: if an answer satisfies the specification, will this program find it?
  3. Termination: will search finish for calls in the intended mode?

They are logically independent. A program can terminate and return the wrong answer. It can return only correct answers while missing some. It can describe the correct relation and still diverge before producing it.

For plus(+,+,-), a termination measure is the number of s/1 constructors in the first argument. Every recursive call strictly decreases that natural number. The measure is well-founded: there is no infinite descending sequence of natural numbers.

That last sentence is the mathematical heart of a termination proof. “It seems to get smaller” is not enough. Name a set with no infinite descent, give a measure into that set, and show strict decrease on every recursive branch.

Structural induction and data design

Lists carry their induction principle in their syntax:

A relation following that structure is easy to reason about:


:- use_module(library(lists)).

list_length([], 0).
list_length([_ | Tail], N) :-
  list_length(Tail, M),
  (N is M + 1).

To prove that list_length(List, N) returns the number of cells in a finite proper list, prove the empty case, then assume the claim for Tail and prove it for [Head | Tail]. The recursive program and inductive proof share a skeleton because both respect the same constructors.

Representation can either expose or obscure this skeleton. A syntax tree built from number/1, plus/2, and times/2 supports structural recursion directly. A flat token string requires parsing before the same argument becomes visible. Good representations do not merely save code; they make invariants and proof principles available.

Accumulators and strengthened invariants

An accumulator often improves control but makes the induction hypothesis more subtle:

reverse_acc(List, Reversed) :-
  reverse_go(List, [], Reversed).

reverse_go([], Acc, Acc).
reverse_go([X | Xs], Acc, Reversed) :-
  reverse_go(Xs, [X | Acc], Reversed).

The useful invariant is not merely “Reversed is the reverse of Xs.” It is:

reverse_go(Xs, Acc, Reversed) holds when Reversed is the reverse of Xs placed before Acc.

Strengthening the statement makes the recursive step provable. This is a classic mathematical move: a theorem that is too weak to support induction is generalized until the induction hypothesis contains what the next step needs. Program transformation and proof discovery meet at the invariant.

Tabling changes the termination argument

Ordinary structural recursion terminates by decreasing a term. Graph reachability on a cyclic finite graph has no such simple decrease: following an edge can return to an earlier vertex. Tabling supplies a different well-founded argument.

If the graph has finitely many vertices, then there are finitely many possible ground path/2 answers. A table only grows; each productive iteration adds a previously unseen answer; therefore only finitely many productive iterations are possible. Termination follows from finiteness of the answer space rather than structural descent of each call.

The proof also states its boundary. If rules construct terms of unbounded depth, the set of possible calls or answers may be infinite, and tabling no longer supplies a finite bound.

Exercises.

  1. State partial correctness, completeness, and termination claims for plus(+,+,-) separately.
  2. Define multiplication over Peano naturals and give its decreasing measure.
  3. Prove the strengthened reverse_go/3 invariant on paper.
  4. Compare the termination arguments for list membership and cyclic graph reachability.
  5. Study examples/peano-calculus.pl and identify where the data constructors determine the available induction.

Checkpoint. Align one recursive program with an inductive argument: base clause with base case, recursive call with induction hypothesis, and rule head with the preserved conclusion. Then give the independent termination measure.

28. Algebra, symmetry, and representation

Algebra studies operations by the laws they satisfy rather than by the material of the objects being operated on. Logic programming has a similar appetite for structure. Unification ignores the private identity of a variable name and asks whether two terms have a common instance. A relational program often works over lists, trees, graphs, substitutions, or group elements because the clauses depend only on their constructors and laws.

Unification is structural equation solving

The goal

(pair(X, f(Y)) = pair(g(a), f(b))).

decomposes into structural equations. The outer functors and arities agree, so corresponding arguments must agree; the resulting substitution is X = g(a) and Y = b.

This resembles algebraic equation solving, but unification is more specific. It operates in the free term algebra: different constructors are distinct, and two constructed terms agree only when their outer symbols and corresponding arguments agree. It does not know, unless clauses or built-ins say so, that X is 2 + 3 and X is 3 + 2 express a commutative operation.

The distinction prevents a common conceptual error:

For polynomials, matrices, groups, or sets, choosing a canonical representation can turn some domain equalities into syntactic equalities. But the normalization algorithm then carries a proof obligation: equivalent objects must normalize alike, and normalization must not identify inequivalent ones.

Suppose a triangle is represented by three side lengths. Searching all permutations repeats the same geometric object six times. Ordering the sides removes the symmetry:

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

triangle(A, B, C) :-
  between(1, 20, A),
  between(A, 20, B),
  between(B, 20, C),
  (Sum is A + B),
  (Sum > C).

The constraints A =< B =< C select one representative from each permutation class. This is more than a performance trick. It is a quotient-like move: identify descriptions related by a symmetry, then search canonical representatives.

Mathematics repeatedly advances by finding the right equivalence relation. Fractions are identified when cross-products agree; graphs may be identified up to renaming; group presentations may denote isomorphic structures; logical formulas may be identified up to variable renaming. Logic programs must decide which distinctions belong to the problem and which are artifacts of notation.

Relations reveal inverse problems

A function privileges one direction. An equation or relation contains several:


:- use_module(library(lists)).

rectangle(W, H, Area) :- (Area is W * H).

In a supported arithmetic mode, this relation may verify an area or calculate it from width and height. With a finite generator it can also search for factorizations:

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

integer_rectangle(Area, W, H) :-
  between(1, Area, W),
  between(W, Area, H),
  (Area is W * H).

eyeprolog --goal 'integer_rectangle(24, W, H)' program.pl

The relational view makes inverse questions conceptually ordinary, even when the implementation still needs an explicit finite direction. Mathematics has long moved between direct and inverse problems: multiply versus factor, evaluate versus interpolate, evolve a system versus infer its initial state. A relational vocabulary lets both questions share a specification where their common structure genuinely permits it.

Composition, homomorphism, and reusable laws

Well-designed relations compose because variables carry outputs from one statement into another. Mathematical structure tells us what composition should preserve.

If a mapping is claimed to preserve an operation, write the preservation law as a testable relation. For a symbolic mapping image/2 and operation combine/3:


:- use_module(library(lists)).

preserves_combine(X, Y) :-
  combine(X, Y, XY),
  image(X, IX),
  image(Y, IY),
  image(XY, IXY),
  combine(IX, IY, CombinedImages),
  (IXY = CombinedImages).

Over a finite carrier, define a relation for a violating pair and use ISO \+/1 to ask whether that counterexample relation has any answer. Over an infinite carrier, finite testing is evidence, not proof. The algebraic law must instead follow from definitions or a stronger proof system.

The examples d3-group.pl, matrix-noncommutativity.pl, group-inverse-uniqueness.pl, and composition-of-injective-functions-is-injective.pl show different roles: computing a finite operation table, finding a counterexample to commutativity, proving uniqueness from axioms, and composing preserved properties.

Representation is a mathematical commitment

Representing a rational number as fraction(N, D) raises immediate questions: may D be zero, must signs be normalized, and are fraction(1, 2) and fraction(2, 4) identical or merely equivalent? These are not serialization details. They determine the equality relation, the search space, and the meaning of every later proof.

Before selecting a representation, state:

  1. its valid inhabitants;
  2. its equivalence relation;
  3. whether it has a canonical form;
  4. the operations that must be efficient;
  5. the induction or decomposition principle it exposes.

That checklist joins abstract algebra, data modeling, and program design.

Exercises.

  1. Modify the triangle generator to enumerate only primitive Pythagorean triples and explain every removed symmetry.
  2. Give two representations of an undirected edge. Compare their equality and indexing behavior.
  3. Design a normalized rational representation and write integrity relations for invalid denominators and noncanonical zero.
  4. Use examples/d3-group.pl to test identity, inverses, and associativity. Which checks are exhaustive, and why?
  5. Find a matrix counterexample showing that multiplication is not commutative. Explain why one witness refutes a universal law.

Checkpoint. Pick a domain value with two possible representations. State whether EyeProlog regards them as structurally equal, whether the domain regards them as equivalent, and which normalization or explicit relation connects the two notions.

29. Search as experimental mathematics

Mathematicians do not prove only by moving forward from axioms. They calculate small cases, draw figures, search for patterns, try extreme examples, and hunt for counterexamples. Computation greatly enlarges this experimental practice. Logic programming contributes a particularly transparent form: generate a finite mathematical world, state the property relationally, and ask for witnesses or failures.

A universal conjecture is tested over a declared finite box; a found counterexample refutes it globally, while exhaustion gives only bounded evidence.
Finite search is asymmetric: one valid counterexample defeats a universal claim, while finding none establishes only the explicitly bounded statement.

Examples suggest; proofs compel

The first values of a sequence can suggest a recurrence. Exhaustive search up to a bound can destroy a false conjecture. Neither establishes a universal theorem over an unbounded domain.

This boundary can be written directly:

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

counterexample_to_odd_square(N) :-
  between(1, 100, N),
  (1 is N mod 2),
  (Square is N * N),
  (Remainder is Square mod 2),
  (Remainder \= 1).

eyeprolog --goal 'counterexample_to_odd_square(N)' program.pl

No answer means only that no counterexample was found in the generated range under the implemented arithmetic. The theorem that every odd integer has an odd square needs an algebraic argument valid for an arbitrary integer: (2k+1)^2 = 2(2k^2+2k)+1.

By contrast, if the claim concerns exactly the integers from 1 through 10,000, the finite exhaustive search can be a proof—provided the generator is complete, the predicate expresses the property correctly, and the arithmetic implementation is trusted.

One counterexample has asymmetric power

A universal statement falls to one valid counterexample. This makes finite search especially valuable for criticism. Testing associativity over random inputs offers evidence; finding one triple where associativity fails settles the negative question.

noncommuting_pair(A, B) :-
  matrix(A),
  matrix(B),
  matrix_multiply(A, B, AB),
  matrix_multiply(B, A, BA),
  (AB \= BA).

The example need not explain every failure of commutativity. Its existence is enough to refute the universal claim. This asymmetry between confirmation and refutation is one reason constraint solving, model finding, and property-based testing are so productive.

Finite model exploration

A finite structure consists of a finite carrier and interpretations of its operations and relations. EyeProlog can enumerate candidates, apply axioms as filters, and return models or countermodels. The method is mathematically serious because the scope is explicit.

For a carrier of three named elements, a binary operation table has nine entries. Searching all possible tables is finite but large. Algebraic laws can prune partial or complete candidates:

The order of these constraints is operational mathematics. A strong law applied early may collapse the search space; the same law applied after full generation merely rejects enormous numbers of candidates.

Search complexity is often a counting problem before it is a programming problem. If a choice has n alternatives at each of k positions, naive generation contains n^k leaves. If order does not matter, permutations may be redundant. If partial choices already violate a constraint, pruning saves an entire subtree.

This is why combinatorial examples are not toys. clpz-n-queens.pl exposes the classic eight-queens search through finite-domain constraints. Together with send-more-money.pl, integer-partitions.pl, stirling-bell-numbers.pl, and weighted-interval-scheduling.pl, they show different geometries of choice: permutations, digit assignments, recursive decompositions, set partitions, and ordered optimization.

For each search program, ask a mathematical question before a performance question:

What objects are being counted, and when do two execution branches denote the same mathematical object?

Only after answering that should one add indexing, reorder goals, or introduce an accumulator. Otherwise the program may optimize accidental multiplicity.

Numerical models and epistemic humility

The scientific examples combine logical rules with floating-point calculations. beam-deflection.pl, orbital-transfer-design.pl, competitive-enzyme-kinetics.pl, and least-squares-regression.pl encode mathematical models of physical or statistical relationships.

A correct derivation inside such a model establishes a conditional:

given these measurements, equations, units, approximations, and thresholds, this conclusion follows under the implementation’s numeric semantics.

It does not establish that the sensor was calibrated, the model applies in this regime, omitted variables are negligible, or a floating-point result is an exact real number. The proof boundary should name these conditions rather than conceal them.

Exercises.

  1. Turn a familiar universal conjecture into a bounded counterexample search. State what a failure to find an answer does and does not prove.
  2. Estimate the naive search space of send-more-money.pl, then identify each constraint that removes branches.
  3. Use examples/stirling-bell-numbers.pl to connect a recurrence with the combinatorial objects it counts.
  4. Design a finite carrier and search for a noncommutative operation with an identity.
  5. Choose one scientific example and list every premise outside pure logic: measurements, units, empirical law, approximation, and numeric behavior.

Checkpoint. Label a computation as one of: witness construction, counterexample, exhaustive finite-model check, bounded evidence, or numerical model evaluation. Write one sentence stating exactly what its success proves and what its failure leaves open.

30. What mathematics promises

Mathematics earns unusual trust because it makes its conditions inspectable. Once definitions, axioms, and inference rules are fixed, a valid proof does not negotiate with status, rhetoric, fashion, or desire. The conclusion either follows by the accepted rules or it does not.

That is perhaps the precise sense in which mathematics does not cheat us. It does not promise that our premises describe the world. It promises that we can ask whether the conclusion follows from them.

Conditional certainty

Every theorem is conditional, even when the conditions have become culturally invisible:

axioms + definitions + inference rules
  -> theorem

Every trustworthy EyeProlog conclusion has the same broad shape:

source facts + clauses + built-in semantics + execution assumptions
  -> ground answer + proof

The arrows are where rigor lives. A proof disciplines the transition from premises to conclusion. It cannot authenticate the premises merely by using them.

This yields four layers of trust:

  1. Source trust: are facts authentic, current, complete enough, and represented with the correct units and identity?
  2. Model trust: do the predicates and rules express the intended domain?
  3. Engine trust: do parsing, unification, built-ins, tabling, and proof generation implement the stated standards profile?
  4. Derivation trust: does this answer have a valid proof from this exact theory?

Explicit integrity relations expose contradictions and invalid states inside the supplied theory. Conformance tests address the implementation. Proof output addresses the derivation. Provenance, signatures, calibration, peer review, and domain validation address other layers. No single mechanism replaces the rest.

The dignity of a counterexample

Mathematics corrects itself through definitions and counterexamples. A false conjecture is not rescued by the beauty of its statement. One legitimate counterexample has standing against a thousand confirming cases.

Logic programming should preserve this culture. Write negative tests before the theory becomes emotionally expensive. Search boundary cases. Ask for forbidden states. Turn domain invariants into queryable integrity relations. Keep the failed model that forced a redesign.

A knowledge system becomes trustworthy not when it never changes, but when it can say:

This is mathematical honesty translated into engineering practice.

The limits are part of the truth

Gödel, Church, and Turing did not diminish mathematics by proving limits. They made informal hopes precise enough to refute. There is no complete effective method that settles every sufficiently expressive mathematical question. No amount of faster hardware turns an undecidable general problem into a decidable one.

EyeProlog has smaller, immediate limits:

Naming these limits is not an apology. A trustworthy formal tool states the edge of its guarantee.

Mathematics as a style of care

The deepest lesson is methodological. Mathematics asks us to separate:

Those separations are exactly what good logic programming requires. A predicate must have a sentence. A recursive clause must have an invariant and a termination argument. A finite search must declare its domain. An aggregate must have a bounded subsearch. A decision must retain its premises. A proof must remain attached to the theory version that licensed it.

The result is not certainty about everything. It is something more useful: certainty whose boundary is visible.

A final program-reading ritual

Before trusting an EyeProlog conclusion, ask:

  1. What does the ground answer say in the domain?
  2. Which facts and rules support it?
  3. Which facts came from outside the theory?
  4. Which built-ins contribute extra semantics?
  5. Was the search domain finite, and why?
  6. Could goal or clause order hide an answer?
  7. Does negation mean absence of proof or an explicit opposite?
  8. What invariant justifies each recursive relation?
  9. What counterexample would overturn the model?
  10. Can the result be reconstructed under the same source and theory version?

That ritual is the book in miniature. State a small theory. Ask a precise question. Let the machine search. Inspect the witness. Challenge the premises. Preserve the proof.

Exercises.

  1. Take one policy example and classify every dependency under the four layers of trust.
  2. Write a conclusion that is logically valid from false premises. Explain why proof checking alone cannot repair it.
  3. Add version and provenance facts to a scientific example and make them visible in its explanation.
  4. Find one claim in your own program for which tests provide evidence but not proof. State the missing universal argument.
  5. Write a one-page “trust contract” for an embedded EyeProlog service: accepted sources, model scope, numeric assumptions, resource bounds, proof retention, and known limits.

Checkpoint. Take one strong conclusion and prefix it with every condition on which it depends: source authenticity, model scope, built-in semantics, finite search, theory version, and derivation validity. If the qualified claim still matters, the model has earned its confidence honestly.

Part VI summary

Part VI placed logic programming inside the longer history of mathematics:

You should now be able to distinguish computation from proof, bounded evidence from a universal theorem, syntactic equality from mathematical equivalence, and valid derivation from trustworthy premises.

Historical note: mathematics examines its own methods

This arc begins before electronic computing. Hilbert’s program made formal proof and consistency mathematical objects. Gödel established limits for sufficiently expressive effective axiomatic systems. Church and Turing made effective calculability precise enough to prove that some general decision problems have no algorithm. Herbrand and Robinson supplied ideas that became central to automated first-order deduction.

Logic programming belongs to this history because it operationalizes a restricted proof discipline. It does not erase the limit results or turn every existence proof into an efficient witness generator. It gives a small region where propositions, substitutions, proof steps, and computations can be inspected together.

The deeper inheritance is a style of honesty. Mathematics advanced by proving not only more statements but also where methods fail, separating truth, provability, decidability, and computation. EyeProlog’s finite bounds, mode restrictions, search risks, and trust boundaries belong inside its account for the same reason: limits are part of the result, not fine print.

Part VII — The reasoning laboratory

A reasoning laboratory bench connects a small theory to predictions, tests, search statistics, proofs, and revisions.
A theory becomes dependable through a repeated laboratory cycle: predict, test, inspect the search and proof, then revise one assumption at a time.

The final craft is experimental without being careless. A logic programmer works like a mathematician at a blackboard and an engineer at a test bench: state a claim precisely, derive consequences, seek counterexamples, measure the computation, and preserve enough evidence for another person to repeat the work.

This Part turns the book’s ideas into a daily discipline. It does not add a new language feature. It shows how to make theories survive change.

31. Testing a theory

A conventional unit test often presents an input to a function and compares one returned value with an expected value. A relational program needs a wider test vocabulary. One call may have several answers, no answer, duplicate proofs, or different useful modes. Correctness includes the answer set, the absence of forbidden answers, the shape of witnesses, and the finiteness of the intended search.

A public relation is surrounded by tests for meaning, supported modes, finite properties, metamorphic changes, integrity, proofs, and scale.
A relational contract has several observable surfaces; examples, mode tests, bounded properties, metamorphic checks, integrity cases, proofs, and scale checks protect different promises.

Begin with a semantic test table

Before writing test code, make a table in domain language:

Case Given Question Expected Why this case matters
direct edge(a,b) path from a to b? yes base clause
composed a→b→c path from a to c? yes recursive clause
absent disconnected d path from a to d? no false positive
cycle c→a all destinations from a? finite set tabling or visited state
reflexive no explicit loop path from a to a? design choice relation boundary

The last row is especially valuable. Many bugs are not implementation mistakes but unresolved meanings. Does a path require at least one edge, or may it be empty? No test framework can choose the definition for you.

Positive and negative observers

Queries naturally record positive expectations:


:- use_module(library(lists)).

edge(a, b).
edge(b, c).

path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

eyeprolog --goal 'path(a, b)' program.pl
eyeprolog --goal 'path(a, c)' program.pl

To make an expected absence visible, define a finite observer:

unexpected_path :-
  path(a, d).

expected_absence :-
  \+ unexpected_path.

eyeprolog --goal 'expected_absence' program.pl

This is a test over a ground, terminating goal. It does not turn negation as failure into classical negation; it records that this finite theory derives no such path.

For a reusable package, prefer a dedicated test program that loads or repeats the relevant theory and declares only test queries. For a small example, the golden answer file is an executable specification of the expected answer set.

Test the relation from more than one mode

Suppose append/3 is intended both to concatenate and to split:

eyeprolog --goal 'append([a, b], [c], Whole)' program.pl
eyeprolog --goal 'append(Prefix, Suffix, [a, b])' program.pl

The first call should construct one list. The second should enumerate three splits. Testing only the first mode would miss a regression in relational generality; testing the completely open mode would request an infinite relation and prove little beyond the absence of a useful bound.

For every public predicate, record:

  1. the principal mode;
  2. any secondary supported modes;
  3. modes that are meaningful but intentionally unsupported;
  4. calls expected to be finite;
  5. calls whose answer order is part of the observable contract.

Keep this design close to the clauses in comments or tests, and exercise each supported call pattern directly.

Properties over finite domains

Examples test selected points. A finite generated property tests every point in a declared scope:

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

double(N, D) :- (D is N + N).

double_is_even(N) :-
  double(N, D),
  (0 is D mod 2).

bounded_double_law :-
  \+ bounded_double_counterexample.

bounded_double_counterexample :-
  between(-100, 100, N),
  \+ double_is_even(N).

eyeprolog --goal 'bounded_double_law' program.pl

This is exhaustive for the 201 generated integers, not for all integers. Naming the predicate bounded_double_law/0 keeps the scope honest.

Useful finite properties include:

Metamorphic tests

Sometimes the correct answer is hard to list, but a controlled change has a predictable effect. These are metamorphic tests.

If an isolated graph vertex is added, existing reachability answers should not change. If every edge cost is multiplied by a positive constant, the cheapest route should retain the same vertices. If the order of source facts changes, the set of logical answers should remain unchanged even if their discovery order changes.

A metamorphic test states a relation between runs. It is particularly useful for optimizations because it checks a preserved invariant rather than one frozen implementation trace.

Proof regression and answer regression

An answer golden asks, “Did the public conclusions change?” A proof golden asks, “Did their supporting derivations change?”

Proof changes may be desirable after introducing a clearer helper. They may also reveal that a decision now depends on an unintended fact. Treat proof goldens as reviewed evidence, not snapshots updated automatically whenever a test fails.

Use answer regression broadly. Use proof regression selectively where provenance, explanation, or policy accountability is part of the product.

Test failures, integrity results, and warnings

Three outcomes carry different meanings:

A mature suite covers all three. Include malformed source in parser tests, inconsistent source in integrity-query tests, and semantically dubious dependency cycles in warning tests.

A release-quality test matrix

Before releasing a theory or embedded service, cover:

Dimension Minimum evidence
Meaning one positive, one absent, and one boundary case per public relation
Modes every documented mode; explicit rejection or warning for unsafe uses
Recursion base case, multi-step case, cycle, and termination argument
Search smallest witness, competing witnesses, ties, and empty domain
Negation ground success, ground failure, and stratification check
Aggregation empty, singleton, duplicates, and deterministic tie handling
Integrity each invalid state is detected and valid input is not misclassified
Proof representative derivation with source premises visible
Scale a case large enough to expose indexing or table behavior
Reproducibility fixed time, source version, stable fixtures, and clean output

Exercises.

  1. Build the semantic test table for ancestor/2, including a cycle and a disputed reflexive case.
  2. Write bounded commutativity and associativity tests for a finite operation table. Explain why one is cheaper.
  3. Create a metamorphic test for a route planner.
  4. Choose one proof golden and identify changes that should be accepted versus changes that should block a release.
  5. Design a test that distinguishes “no answer” from “invalid input theory.”

Checkpoint. Assemble a minimum release matrix for one public relation: positive, absent, boundary, alternate mode, recursive or cyclic, integrity, proof, and scale cases. State which expected outputs should be exact goldens.

32. Debugging by meaning, search, and proof

Debugging a logic program is difficult when every symptom is described as “the query failed.” Failure can mean the fact is absent, a variable was bound too early, a built-in ran outside its mode, a negative goal saw an unintended answer, recursion did not reach its base case, or the original relation was misstated.

Use four views in a fixed order:

  1. meaning: what should a ground instance say?
  2. bindings: what is known before each goal?
  3. search: which alternatives are explored, repeated, or pruned?
  4. proof: which successful premises support the observed answer?
A disputed ground query passes through four diagnostic lenses—meaning, bindings, search, and proof—before the repaired invariant is preserved as a regression.
Each debugging lens answers a different question; begin with meaning, move outward only as needed, and preserve the lesson as an executable check.

Reduce to the smallest disputed ground question

Do not begin with an open query that prints hundreds of answers. Name one conclusion that is missing or surprising:

eyeprolog --goal 'eligible(alex)' program.pl

Then expand only the clause intended to prove it. Replace broad generators with the relevant ground facts. A small ground question removes accidental branching and makes every failed subgoal discussable.

If the ground question is itself ambiguous, stop debugging the implementation. Rewrite the domain sentence first.

Follow bindings from left to right

Consider:


:- use_module(library(lists)).

eligible(Person) :-
  (Age >= 18),
  age(Person, Age).

The intended mathematics is easy to recognize, but >=/2 sees an unbound Age. Write a binding ledger:

Before goal Goal Bindings produced
none Age >= 18 none; not ready
— age(Person,Age) never productively reached

Reordering the goals repairs the operational mode:


:- use_module(library(lists)).

eligible(Person) :-
  age(Person, Age),
  (Age >= 18).

For a clause with five goals, the ledger is often more revealing than staring at the source. Record structures as well as scalar bindings: a variable may be bound to an improper list or a compound term whose inner variables remain open.

Use a symptom atlas

No answers

Too many answers

Right answers, wrong order

Nontermination or explosive search

A surprising proof

Create diagnostic relations

Temporary helpers can expose intermediate concepts:


:- use_module(library(lists)).

candidate_debug(Person, Age) :-
  age(Person, Age).

adult_debug(Person, Age) :-
  candidate_debug(Person, Age),
  (Age >= 18).

eyeprolog --goal 'candidate_debug(Person, Age)' program.pl
eyeprolog --goal 'adult_debug(Person, Age)' program.pl

Once the fault is understood, either remove the helper or rename it as a permanent domain concept. Do not leave debug2/3 archaeology in a theory whose proofs people must read.

Compare specification and implementation

For a bounded domain, write a deliberately simple reference relation and compare it with the optimized one. The reference may be slow; its purpose is clarity.

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

reference_square(N, S) :-
  between(0, 20, N),
  (S is N * N).

optimized_square(N, S) :-
  between(0, 20, N),
  (S is N * N).

disagreement(N, S) :-
  reference_square(N, S),
  \+ optimized_square(N, S).

eyeprolog --goal 'disagreement(N, S)' program.pl

A complete equivalence check needs both directions and must account for duplicates if proof multiplicity matters. Within a finite domain, differential testing is a powerful guard during program transformation.

Read statistics as questions

--stats reports work, not meaning. A high solution count may be necessary or may indicate a generator that should be constrained. Many table hits may show effective reuse; many distinct table entries may reveal an argument that prevents calls from sharing. On the Node CLI it also reports current heap use, non-young/old-generation use, the amount currently compared with the memory guard, resident-set size, and the soft and hard memory ceilings in bytes. These memory figures are printed even when execution ends by raising a Prolog error.

--stats is an end-of-run summary. For a deliberately non-terminating or very long computation, call the EyeProlog extension statistics/0 at the points where a live snapshot is useful. For example, a long-running loop can include statistics as one of its goals, as in loop :- work, statistics, loop.

statistics/0 writes the current solver counters and memory figures immediately to the current output stream. statistics/2 makes an individual value available to the program, for example statistics(memory_guard_used_bytes, Used). With an unbound first argument it enumerates the available statistic keys and values. An atom that is not an available key raises domain_error(statistics_key, Key) rather than silently failing. These predicates are EyeProlog observability extensions and are not available under --iso-strict.

Compare statistics only between runs with the same query, data, and observable answer contract. A faster program that silently loses answers is not an optimization.

Preserve the failure that taught you

Every repaired defect should leave behind one of:

Otherwise the repository remembers the repair but forgets the reason.

Exercises.

  1. Deliberately misorder a numeric filter and diagnose it with a binding ledger.
  2. Introduce a missing-variable join into a two-relation rule. Use the proof of one false positive to locate it.
  3. Create a recursive term-growing rule, then state why tabling cannot make its answer space finite.
  4. Compare statistics before and after moving an invariant calculation out of recursion.
  5. Write a bidirectional bounded equivalence check for two list relations.

Checkpoint. Preserve one defect as a regression. Record the smallest disputed ground question, expected answer, first incorrect binding or search choice, repaired invariant, and test that would fail if the defect returned.

33. A pattern catalog for reasoning

A pattern is not a copied code fragment. It is a recurring arrangement of meaning, representation, and control that solves a named design problem. The following patterns summarize the strongest constructions in this book.

Six recurring design symptoms point to patterns for meaning, tabling, closed boundaries, finite search, proof-carrying answers, and canonical representation.
Choose a pattern by the design problem and its consequence, not by superficial code shape; each pattern coordinates meaning, representation, modes, and control.

Pattern 1: Ground sentence first

Problem: a predicate’s argument order and meaning drift while rules are being written.

Form: write one representative ground fact and read it aloud before adding variables.


:- use_module(library(lists)).

assigned_badge(alex, badge_17).

Consequence: argument roles become reviewable; modes and indexes can be discussed against a stable sentence.

Pattern 2: Normalize at the boundary

Problem: spelling, aliases, units, or source-specific terms leak into every domain rule.

Form: retain source facts, derive one canonical vocabulary, and make core rules depend only on the normalized layer.

:- use_module(library(strings)).
:- use_module(library(lists)).

source_role(person_7, 'Doctor').

canonical_role(Person, clinician) :-
  source_role(Person, Text),
  lowercase(Text, doctor).

Consequence: adapters change independently from policy; proofs still trace back to source data.

Pattern 3: Generate, constrain, describe

Problem: a search relation mixes candidate production, pruning, and explanation until none can be reasoned about separately.

Form: generate a finite candidate, apply the cheapest selective constraints in dependency order, then construct a witness or reason.

:- use_module(library(between), [between/3]).
:- use_module(library(lists)).

chosen_pair(pair(X, Y), reason(sum_is_ten)) :-
  between(0, 10, X),
  between(X, 10, Y),
  (10 is X + Y).

Consequence: the search domain and each pruning step are visible.

Pattern 4: Carry the witness

Problem: a Boolean-like conclusion proves existence but loses the object needed for explanation or later computation.

Form: add a structured output containing the path, assignment, schedule, or evidence summary.


:- use_module(library(lists)).

path(X, Y, [X, Y]) :- edge(X, Y).
path(X, Z, [X | Rest]) :-
  edge(X, Y),
  path(Y, Z, Rest).

Consequence: answers become constructive; witness size and duplicate paths become explicit design concerns.

Pattern 5: Bound absence

Problem: the domain needs a negative conclusion, but absence is meaningful only after a complete finite search.

Form: bind the subject and finite scope before \+/1; isolate the closed-world step behind a clearly named predicate.

unregistered(Person) :-
  person(Person),
  \+ registered(Person).

Consequence: the closed-world assumption has one reviewable home. It must not be mistaken for an explicit fact that the person is not registered.

Pattern 6: Explicit state transition

Problem: planning or interpretation appears to require mutable state.

Form: represent the old and new states as terms related by an action.

step(state(Room, outside), enter(Room), state(Room, inside)).

Consequence: histories are ordinary lists, transitions can be queried, and the state representation exposes invariants.

Pattern 7: Fixed-point closure

Problem: reachability, inheritance, or dataflow revisits the same finite subquestions.

Form: state the positive recursive relation directly and let eligible components be tabled.

depends(X, Y) :- direct_dependency(X, Y).
depends(X, Z) :- direct_dependency(X, Y), depends(Y, Z).

Consequence: termination rests on a finite call and answer space, not on pretending the graph is acyclic.

Pattern 8: Proof façade

Problem: low-level helper clauses produce technically correct but unreadable explanations.

Form: introduce stable domain concepts and a small public decision relation whose premises are meaningful reasons.

within_limit(Device) :-
  reading(Device, Value),
  maximum(Max),
  (Value =< Max).

status(Device, safe) :-
  within_limit(Device).

Consequence: internal calculations remain available, while the successful proof reads in domain vocabulary.

Pattern 9: Integrity before inference

Problem: contradictory or impossible input would make ordinary conclusions misleading.

Form: encode forbidden combinations as ordinary relations with diagnostic arguments.


:- use_module(library(lists)).

invalid_badge_assignment(Badge, PersonA, PersonB) :-
  assigned_badge(PersonA, Badge),
  assigned_badge(PersonB, Badge),
  (PersonA \= PersonB).

Consequence: callers can collect every defect, and a host that requires validated input can query this relation before it requests trusted decisions. The rejection policy remains explicit rather than being hidden in clause-head syntax.

Pattern 10: Version the evidence boundary

Problem: an answer can be reproduced only if its facts, rules, and external semantics are known.

Form: retain source snapshot, theory version, adapter version, and relevant clock or numeric assumptions beside the proof.

theory_version("2026-07-24").
source_snapshot("telemetry-0042").
numeric_model(ieee_754_double).

Consequence: an old decision can be reconstructed under the system that actually made it rather than silently rerun under today’s theory.

Anti-patterns

The unbounded open generator. A relation is queried with every argument free even though its mathematical extension is infinite.

The premature test. A mode-sensitive built-in or negative goal appears before the goals that bind its inputs.

The accidental Cartesian product. Two goals use different variables for what should be the same entity.

The opaque mega-clause. One rule performs normalization, search, policy, and explanation with no named intermediate concepts.

The Boolean witness eraser. A relation returns only yes after doing the work needed to construct a useful path or reason.

The silent closed world. Failure to derive a fact is used as its opposite without documenting finite scope and completeness assumptions.

The proof-hostile helper. Names such as step3/2 or tmp/4 expose an implementation sequence instead of a domain idea.

The optimization by answer loss. once/1, early aggregation, or reordered search makes a benchmark faster by changing the public answer contract.

The floating theorem. A numerical result is described as mathematically exact without naming units, approximation, or host floating-point behavior.

The timeless decision. Sources and rules change, but conclusions retain no snapshot or theory version.

Selecting patterns

Patterns compose. A robust decision service often uses:

normalize at the boundary
  -> generate, constrain, describe
  -> carry the witness
  -> proof façade
  -> integrity before inference
  -> version the evidence boundary

Do not apply every pattern mechanically. A three-fact teaching example does not need six architectural layers. Introduce a pattern when its named problem is present, and keep the smallest theory that makes meaning and control clear.

Exercises.

  1. Find three patterns and two anti-patterns in an existing large example.
  2. Refactor an opaque rule into boundary, concept, and decision layers; compare proofs before and after.
  3. Add witness carrying to a Boolean reachability relation and analyze the new duplicate-answer behavior.
  4. Replace a silent closed-world decision with a named bounded-absence helper.
  5. Write a versioned evidence envelope for the Chapter 25 decision service.

Checkpoint. Select the smallest set of patterns that solves a real problem in one theory. For every selected pattern, name the pressure that justifies it; remove any layer that exists only because the catalog made it available.

Part VII summary

Part VII made theory development repeatable:

You should now be able to design a release-quality test matrix, reduce a surprising result to one ground question, compare a reference relation with an optimized relation, and recognize productive patterns and anti-patterns.

Historical note: executable specifications learn to remember

Logic programs have long stood between specification and implementation. That made testing both easier and subtler: a ground clause could serve as an example, yet a relation might have several modes and an answer set rather than one returned value. Testing practice absorbed ideas from theorem proving, database validation, software regression, and property-oriented testing.

The repository form of this practice is historically significant in its quiet way. A theory, exact answer file, proof file, conformance corpus, and version tag preserve not only a program but expectations about its meaning. Regression tests make old decisions reviewable; property tests seek counterexamples; metamorphic tests state what remains invariant across controlled change.

Patterns complete the cycle by naming recurring design knowledge. Sterling and Shapiro’s craft-oriented presentation helped establish that expertise lives in constructions and transformations, not syntax alone. The reasoning laboratory extends that attitude into maintenance: prediction, execution, evidence, and revision form one method, and the failure that taught a lesson becomes executable memory.

Part VIII — Standard Prolog in practice

A standards workbench connects an ISO Prolog manual to control, term, state, operator, and stream instruments.
The broader ISO profile is a practical workbench: relational term operations remain at its center while control, mutable state, and I/O are introduced at explicit boundaries.

The supported ISO Prolog profile includes processor-facing facilities that become important in reusable libraries, language tools, long-running applications, and file boundaries. Earlier chapters use its relational core; this part makes control, reflection, state, operators, and streams explicit. For Part 1 portability work, EyeProlog also provides a strict core mode: --iso-strict on the CLI or isoStrict: true in the JavaScript API restricts the language/runtime surface to ISO/IEC 13211-1:1995 plus Technical Corrigenda 1–3. The processor character set is an implementation-defined choice shared by normal and strict profiles: EyeProlog uses Unicode scalar values U+0000..U+10FFFF excluding surrogates, with the scalar value as the collating-sequence integer. Strict mode restricts implementation-specific language facilities, but it does not narrow this processor-defined character repertoire. Isolated mode and error cases live in test/conformance/cases/iso/. The examples here compose those operations into programs worth changing and rerunning.

These facilities do not all have the same declarative character. Term inspection and atomic conversion are relations. Cut commits to an operational choice. Dynamic updates and stream operations change solver-owned state. Use the pure relation when it expresses the problem; introduce control or effects at a named boundary.

34. Control, exceptions, and grouped solutions

The control predicates accept goals as arguments. call/1 invokes a callable term, and call/2-8 appends arguments to a callable closure. The expanded goal runs in the current search continuation, so a direct goal and its meta-called form expose the same remaining alternatives; the meta-call still establishes its own cut boundary. once/1 keeps its first solution, and !/0 commits within the clause that contains it. If-then-else commits to the first successful condition:

A goal passes through choice and exception recovery before finite solutions enter findall, bagof, and setof collectors.
Control narrows or redirects search; collection then gives a finite solution stream a deliberate list or grouping shape.
travel_status(From, To, Status) :-
  (route(From, To) -> Status = connected ; Status = disconnected).

once(Goal) is a local request for one solution. Cut is lower level: it discards alternatives created since entry into the current predicate call. The two can produce the same first answer without expressing the same control boundary. Keep cut close to the choice it documents and test the complete answer set before and after introducing it. A cut executed inside a predicate called by one disjunction branch remains local to that predicate: if the branch later fails, Left ; Right must still try Right. This remains true for cut-bearing validation helpers used by generators such as between/3.

Exceptions separate an exceptional call from ordinary logical failure:

require_route(From, To) :-
  (route(From, To) -> true ; throw(no_route(From, To))).

checked_route(From, To, Result) :-
  catch(
    (require_route(From, To), Result = accepted),
    no_route(From, To),
    Result = rejected
  ).

The catcher is unified with the thrown term. A matching recovery goal runs in the environment at the catch/3 boundary; unrelated exceptions continue outward. Prefer failure for an expected negative answer, such as a route that does not exist. Throw when a caller cannot safely interpret the computation, for example malformed input or an unavailable required resource. ISO instantiation, type, domain, permission, representation, and evaluation errors follow this same exception path.

Normal EyeProlog also provides call_cleanup(Goal, Cleanup) and setup_call_cleanup(Setup, Goal, Cleanup). Cleanup is run exactly once when the protected search completes deterministically, is exhausted, is cut or otherwise pruned, top-level answer enumeration is abandoned, or an exception unwinds the search. setup_call_cleanup/3 runs Setup once and installs Cleanup only after Setup succeeds. On cut or ordinary pruning Cleanup sees the current Goal bindings; on exception unwind the Goal bindings have been removed and Cleanup sees the Setup environment. When a deterministic protected goal runs Cleanup before yielding, substitutions produced by a successful Cleanup are included in that answer. Cleanup failure is ignored, and an exception already being propagated takes precedence over a cleanup exception. Nested cleanups run inside-out. These two controls are EyeProlog extensions and are absent from --iso-strict.

Collection also makes search boundaries explicit. findall/3 returns one list and existentially closes variables that occur only in its goal. bagof/3 instead creates a group for each binding of a free variable and fails when there are no solutions. setof/3 has the same grouping rule, then sorts and deduplicates each group. The ^/2 notation marks a goal variable existential:


:- use_module(library(lists)).

regional_total(Region, Total) :-
  bagof(Amount, Seller^sale(Region, Seller, Amount), Amounts),
  sum_amounts(Amounts, Total).

Here Region deliberately remains free and produces one answer per region; Seller is hidden from grouping. This distinction matters whenever a collection unexpectedly arrives as several answers.

Integer arithmetic has similarly precise choices. // truncates the quotient toward zero, while Corrigendum 2’s div takes the mathematical floor. With a positive divisor, mod returns a nonnegative modulo while rem keeps the dividend’s sign. For -7 and 3, // is -2, div is -3, and the two remainders are 2 and -1. Bitwise conjunction, disjunction, exclusive-or, complement, and shifts require integers.

Run the focused examples:

Checkpoint. Explain why bagof(Amount, sale(Region, Seller, Amount), X) groups on both Region and Seller, then write the existential qualification that groups only on Region. Name one expected absence that should fail and one broken precondition that should throw.

35. Reflective terms and atomic conversion

Ordinary pattern matching should remain the first choice when term shape is known. Reflective predicates are valuable when the shape itself is input: generic walkers, schema checkers, interpreters, and source transformations.

One structured event term fans out into functor, argument, univ-list, variable, ordering, character, and code views.
A term is not mutated by reflection: standard relations expose its structure, ordering, or lexical representation for a particular question.

functor/3 relates a term to its name and arity. arg/3 selects a one-based argument. =../2—traditionally called univ—relates a term to a list whose head is the functor and whose tail contains the arguments:

term_shape(Term, shape(Name, Arity, Arguments)) :-
  functor(Term, Name, Arity),
  (Term =.. [Name | Arguments]).

In a construction mode, functor/3 creates a term with fresh arguments and =../2 rebuilds a term from a proper list. Their ISO errors are useful guardrails: an unknown functor name, negative arity, partial univ list, or uninstantiated required argument is not silently treated as failure.

copy_term/2 preserves sharing inside a term while replacing its variables with fresh ones. term_variables/2 returns each distinct variable in first-occurrence order. Identity predicates make the distinction observable: ==/2 tests whether two resolved terms are identical without binding them; \==/2 is its negation. =/2 still performs unification, while unify_with_occurs_check/2 explicitly rejects cyclic bindings.

The standard term-order family—compare/3, @</2, @=</2, @>/2, and @>=/2—compares terms without evaluating arithmetic. Do not replace 3 + 4 < 8 with 3 + 4 @< 8: the former evaluates numbers and the latter orders syntax.

Atomic conversion predicates expose reversible representations:

These are atom relations, distinct from the EyeProlog library predicates whose historical names contain string. Quoted atoms such as 'λ' remain atoms; with the default flag, "λ" denotes the character list ['λ'].

iso-reflective-terms.pl walks through shape, rebuilding, fresh copying, variables, and order. iso-atomic-conversion.pl demonstrates both conversion directions and every three-character sub-atom of eyeprolog.

Checkpoint. Given pair(X, X), predict the variable list before and after copy_term/2. Then explain why atom_codes/2 belongs at a text boundary rather than throughout a domain theory.

36. Dynamic predicates, directives, and operators

A dynamic predicate is a mutable clause store owned by one solver run. Declare it before updates:

Initialization and assertions establish an ordered dynamic task queue beside an operator declaration that parses readable syntax into an ordinary reports term.
Dynamic predicates change solver-local clause order; operator declarations change how subsequent source is parsed. Both effects are explicit and ordered.
:- dynamic(task/2).

prepare_queue :-
  asserta(task(check_power, urgent)),
  assertz(task(check_network, normal)).

asserta/1 inserts at the beginning and assertz/1 at the end. retract/1 removes the first unifying clause and can be retried for later matches. abolish/1 removes a dynamic procedure. clause/2 inspects accessible clauses, while current_predicate/1 enumerates or tests predicate indicators. Static and private built-in procedures are protected by permission errors.

Updates are ordered effects, not pure logical conclusions, and they are not undone by ordinary backtracking: later goals observe a changed database. Each update invalidates cached tabled and ground-chain answers, and rule changes refresh recursion and negation analysis before later goals continue. Keep them in a narrow lifecycle layer. The queue example performs setup in initialization/1, so query order does not determine its state:

:- initialization(prepare_queue).

Initialization runs after preparation and before host queries. include/1 expands a source file in place; ensure_loaded/1 loads the same designation at most once. multifile/1 and discontiguous/1 document permitted clause layout. Prolog flags and character conversions are also solver-scoped and should be set deliberately near the boundary that relies on them.

Operators offer readable syntax without adding a new data model:

:- op(600, xfx, reports).

sensor_7 reports temperature.

The fact is exactly reports(sensor_7, temperature). Priority determines binding strength, and fx, fy, xf, yf, xfx, xfy, and yfx determine position and associativity. current_op/3 inspects the table; op(0, Specifier, Name) removes a definition. Because declarations affect parsing of subsequent text, place them before their first use. ISO argument syntax also permits an atom that is currently an operator to appear directly as a functional argument or list element, so forms such as current_op(Priority, Specifier, :-) and [:-,-] are valid without quoting or parenthesizing those operator atoms. A current operator atom may likewise be the complete content of parentheses or curly brackets: (+) denotes the atom +, and {*} denotes the curly term {}(*). Term output observes the same context rules: with quoted(true), an operator atom is not quoted merely because it occurs as a functional argument, list element, or sole curly-bracket content. Thus writeq({*}) emits {*}, writeq([:-,-]) emits [:-,-], and writeq(f(;,'|',';;')) emits f(;,'|',';;'); the bar stays quoted because ISO treats the unquoted | token as a list separator rather than an atom. The ISO initial operator table also contains ?- at priority 1200 with specifier fx, so current_op(1200, fx, ?-) succeeds. EyeProlog’s embedded quad syntax permits an optional label before the query marker (Label ?- Query.), so while quad syntax is supported it additionally exposes ?- at priority 1200 with specifier xfx as an implementation-specific operator. Consequently current_op(Priority, Specifier, ?-) enumerates both definitions. At top level in the normal EyeProlog profile, the quad marker is recognized from the parsed ?-/1 or ?-/2 term rather than from one privileged surface spelling. Thus Label ?- Query., ?-(Label, Query)., mixed forms such as ?-((Label), Query)., quoted-functor notation, and a parenthesized whole (?-(Label, Query)). denote the same quad when followed by indented answer descriptions. Label itself is parsed with the ordinary Prolog term grammar: there is no quad-specific comma or metadata syntax. The runner requires the resulting first argument to be ground; if it is not, that quad is reported as BAD_ID and later quads are still processed. In --iso-strict mode this quad interpretation is disabled, and ?-/2 remains ordinary Prolog term syntax.

Run iso-dynamic-database.pl for an explicitly stateful queue and iso-operators.pl to see custom notation decomposed back into an ordinary term.

Checkpoint. State the final clause order after one asserta/1 and two assertz/1 calls. Then rewrite one custom-operator fact in canonical functor notation and verify it with =../2.

37. Streams and term I/O

Streams are handles to ordered input or output. open/4 adds options to the basic open/3: text or binary type, alias, repositioning, and end-of-file action. Always close a nonstandard stream, including exceptional paths in application code.

A structured event is written with a terminating period to a text stream, read back as a term, and followed to end of file.
A term round trip has visible lifecycle obligations: open the right stream type, write readable syntax with a period, read in order, observe end state, and close.
write_event(Path, Event) :-
  setup_call_cleanup(
    open(Path, write, Stream, [type(text)]),
    ( write_canonical(Stream, Event),
      put_char(Stream, '.'),
      nl(Stream)
    ),
    close(Stream)
  ).

In normal mode, setup_call_cleanup/3 is the preferred lifecycle boundary for resources such as streams: close(Stream) still runs if the protected work fails, throws, is cut, or its remaining alternatives are abandoned. Strict ISO mode does not provide this EyeProlog extension.

The period is essential when another Prolog processor will read the result as a term. write/1-2 uses readable conventional syntax, writeq/1-2 quotes where needed, and write_canonical/1-2 exposes canonical structure. Dotted graphic atoms do not need quotes merely because they contain a period: writeq(./*), writeq(.*), and writeq(...*) output ./*, .*, and ...* respectively. ISO term output uses only the separator characters needed by the syntax, so functional arguments, list elements, and operator applications are emitted compactly when no lexical ambiguity would arise. For example, writeq([a,b]) outputs [a,b] and writeq(1+2) outputs 1+2; a separator is still retained where adjacent graphic tokens would otherwise merge, as in a+ -b. write_term/2-3 supports quoted/1, ignore_ops/1, numbervars/1, and variable_names/1. Normal mode additionally accepts the EyeProlog extension double_quotes(true|false): true lets eligible character/code lists use the current double_quotes representation, while strict ISO mode rejects this implementation-specific write option. Normal mode also accepts the implementation-specific boolean spacing(true|false) option: false emits only separators required to avoid lexical ambiguity, while true adds conventional layout around operators. For example, write_term(1+1,[spacing(false)]) emits 1+1 and write_term(1+1,[spacing(true)]) emits 1 + 1. The REPL always follows the minimal-separator rule, so X=1*1 is displayed as X = 1*1, while a separator is retained in X = a+ -b because the adjacent graphic tokens would otherwise merge. Strict ISO mode rejects both extension options.

Character operations are get_char, peek_char, put_char, get_code, peek_code, and put_code; byte streams use the corresponding byte predicates. Peeking does not advance the position. Mixing byte operations with a text stream, or text operations with a binary stream, raises a permission error rather than guessing an encoding.

read/1-2 reads the next term. read_term/2-3 can also return all variables, source variable names, and singletons. The metadata contains variables, so a program normally validates or transforms it before placing it in a ground query answer. Every read operation creates a fresh variable set: a source name such as X in two separately read terms does not alias either the caller’s X or the variable named X by the other read. Within one read term, repeated occurrences and the variables returned through its metadata still share as written. stream_property/2 exposes mode, type, alias, position, and end state. current_input/1, current_output/1, set_input/1, and set_output/1 manage defaults shared by nested goals.

End of file is a state transition, not merely a character. With eof_action(eof_code), term input yields end_of_file, character input yields end_of_file, and code or byte input yields -1; at_end_of_stream/1 tests the position. Repeated input after the end follows the selected eof_action.

iso-term-io.pl writes a temporary fixture, reads its terms in order, checks variable metadata, and observes end of stream. The file lives under /tmp; running the example does not modify the checkout.

Checkpoint. Write a term round trip and name where quoting, the terminating period, stream type, and close operation matter. Explain why a stream side effect belongs outside the central relation that decides what the term means.

Part VIII summary

The supported ISO facilities make EyeProlog suitable for more than closed rule files:

Chapters 38–40 state the supported profile, list every registered predicate, and document the command line; the conformance corpus fixes success, failure, mode, and error behavior. Use this part for working practice and those chapters for exact reference.

Part IX — Reference as practice

Reference is useful only when the route into it is clear. Begin with the task in hand: Chapter 38 answers what source means, Chapter 39 helps select a predicate, and Chapter 40 turns a file into observable evidence. Chapters 41–43 then support study design, boundary decisions, and precise vocabulary. The long catalogs are meant to be entered locally, not memorized linearly.

A task map routes language, predicate, and execution questions into Chapters 38 to 40, then onward to study paths, boundaries, and vocabulary in Chapters 41 to 43.
Enter the reference through a concrete question. The first three chapters answer how to read, choose, and run; the next three help place that answer in a course, a boundary, and a shared vocabulary.

38. Language and ISO profile

The normative strict-core baseline is ISO/IEC 13211-1:1995, as corrected by Technical Corrigenda 1:2007, 2:2012, and 3:2017. The post-N289 WG17/STC working draft is used as defect-discovery input, not as an unpublished fourth Corrigendum. The 2026-08-23 draft through items #73-#76 is tracked by test/conformance/STC-DRAFT-STATUS.md; where a proposal changes published semantics, such as #75’s conditional power-underflow proposal, strict mode keeps the licensed baseline until the change is standardized or explicitly adopted as a compatibility extension. Normal EyeProlog additionally provides a practical module interface aligned with later WG17 module amendment work and a definite-clause-grammar profile following ISO/IEC TS 13211-3. Those normal-mode profiles are documented and tested compatibility surfaces; they are not currently claimed as complete clause-by-clause certifications of Part 2 or Part 3.

Normal-mode Prolog source accepted by EyeProlog is UTF-8. % starts a line comment and /* ... */ delimits a block comment. Plain atoms begin with a lowercase ASCII letter. Variables begin with uppercase or underscore. The bare _ is fresh each time. Single quotes delimit quoted atoms; double quotes use ISO double-quoted-list notation. Integers, decimals, scientific notation, binary/octal/hexadecimal integers, and character-code constants are accepted.

The processor character set is shared by normal and --iso-strict modes because Part 1 makes it implementation defined rather than an extension boundary. EyeProlog’s PCS is the Unicode scalar repertoire. Printable ASCII keeps the Part 1 lexical classes; Unicode letters extend alphanumeric name syntax, Unicode white-space characters are layout, and remaining non-ASCII symbols/punctuation are extended graphic characters. Character-code and collation values are the corresponding Unicode scalar integers. Quoting remains available for any atom spelling that should not depend on an extended lexical class:


:- use_module(library(lists)).

city('München').
message("café").

Inside a quoted atom, a single quote is doubled: 'don''t'. EyeProlog follows the ISO quoted-character grammar rather than accepting arbitrary backslash escapes. The symbolic control escapes are \a, \b, \r, \f, \t, \n, and \v; the meta characters backslash, single quote, double quote, and back quote may be escaped after a backslash; and numeric octal or hexadecimal escapes are terminated by a backslash. For example, '\7\' and '\x7\' both denote the alert character. Forms such as \c, \d, \e, \u, \. and \ are not ISO quoted-character escapes and are syntax errors.

A literal layout character other than ordinary space is not a quoted character. In particular, a literal tab or newline inside quotes is a syntax error. A quoted token can cross a line boundary only through a continuation escape: a backslash immediately followed by the newline, which contributes no character to the atom. The NUL character is written readably as '\0\'; digits 8 and 9 are not octal digits, so forms such as '\8\' are syntax errors. writeq/1 uses octal escapes for other non-symbolic control characters, for example ESC is written as '\33\'. Double-quoted lists use the same quoted-character rules. Whitespace is insignificant between tokens, and a % comment continues to the end of its line. Doubling the active delimiter is also accepted inside either quoted form, so "" inside double-quoted notation denotes one literal double quote character.

Graphic tokens use the characters #$&*+-./<=>?@^~\; ! and ; are solo atoms. A colon is the Part 2 module qualification operator in Module:Goal; quote an atom whose name itself contains a colon. Unquoted angle-bracket IRIs are not syntax.

A /* sequence opens a block comment only when it begins a token; inside a maximal graphic token the slash and star remain atom characters. Graphic tokens are formed maximally before a period can be recognized as the terminating full stop. Consequently, interactive input *. or ./*. is not yet a complete term: the period is part of the graphic atom and the reader waits for a separate terminating full stop. Thus ./*. . reads the atom ./*. and consumes the second period as the terminator.

In the grammar below, { x } means zero or more repetitions of x, [ x ] means that x is optional, and parentheses group alternatives. These marks describe the grammar; they are not characters written in EyeProlog source.

program             ::= { clause }
clause              ::= head "."
                      | head ":-" goal-list "."
head                ::= term
goal-list           ::= term { "," term }
term                ::= variable | atom-constant | double-quoted-list | number
                      | compound | list | curly-term | parenthesized-term
compound            ::= atom-constant "(" term { "," term } ")"
list                ::= "[" "]"
                      | "[" term { "," term } [ "|" term ] "]"
double-quoted-list  ::= '"' { quoted-character } '"'
curly-term          ::= "{}" | "{" term "}"
parenthesized-term  ::= "(" term [ "," term { "," term } ] ")"
variable            ::= "_"
                      | variable-start { name-continue }
atom-constant       ::= plain-atom | quoted-atom | graphic-atom
plain-atom          ::= lowercase-letter { name-continue }
number              ::= [ "-" ] digits [ "." digits ] [ exponent ]
exponent            ::= ( "e" | "E" ) [ "+" | "-" ] digits
variable-start      ::= uppercase-letter | "_"
name-continue       ::= uppercase-letter | lowercase-letter | digit | "_"

Zero-arity compounds such as ready() are unsupported; use ready. Every clause ends in a period. The grammar above gives the canonical term shapes. The initial operator table contains the following ISO-style operators, all lowered to ordinary compound terms:

op/3 directives and runtime calls define or remove prefix, infix, and postfix operators using the ISO fx, fy, xf, yf, xfx, xfy, and yfx specifier classes. Variables cannot occur in functor or predicate position. Parentheses around one term denote that term; parentheses around two or more comma-separated terms construct a right-associated ','/2 term. In goal position it is conjunction; in data position it remains inspectable data.

The pure definite-clause fragment has a Herbrand reading: ground terms denote themselves, predicates denote sets of ground atomic formulas, variables have clause scope, and unification is structural. The implementation performs first-order finite-tree unification with an occurs check. An attempt to bind a variable to a term containing that same variable fails.

An atom constant such as pat is a term. An atomic formula such as parent(pat, jan) is a proposition that may be a fact, rule head, or goal. The surface form pair(pat, jan) may also be compound data when nested inside another term; its role comes from context. Predicate identity includes arity, so edge/2 and edge/3 are different predicates.

Execution is goal-directed rather than complete bottom-up saturation. Goals in a body normally run from left to right; the solver may select a ready deterministic built-in early as a pure filter. Ordinary user-defined calls use depth-first resolution, while eligible positive recursive groups are tabled automatically. \+/1 is stratified negation as failure, not classical negation.

EyeProlog supports cut, operator declarations, dynamic database updates, grouped solutions, exceptions, flags, initialization and inclusion directives, and standard stream and term I/O. Normal mode additionally provides lifecycle-aware call_cleanup/2 and setup_call_cleanup/3; these cleanup controls are EyeProlog extensions and are excluded by --iso-strict. Normal mode also adds the documented module compatibility surface and a Part 3-oriented DCG profile.

Module compatibility profile

A module gives predicate identity one more component: module name, predicate name, and arity. The first directive in a module source names the module and lists its public predicates:

% colors.pl
:- module(colors, [tone/1]).

tone(blue).
hidden(module_private).

Another source can import all exports or select particular indicators. An unqualified call first uses a predicate local to the calling module and then an import; a local definition therefore stays distinct from a same-named private predicate elsewhere.

:- use_module('colors.pl', [tone/1]).

hidden(user_local).
answer(Tone, Hidden) :- tone(Tone), hidden(Hidden).
qualified(ok) :- colors:tone(blue).

Imports such as use_module(library(lists)) and use_module(library(strings)) resolve the bundled modules in Node and the browser. Atom source designations such as 'colors.pl' resolve relative to the importing file in Node. use_module/1 imports every export; use_module/2 imports only its indicator list, including an empty list when only qualified calls are wanted. Module:Goal selects a module explicitly. Repeated module loads are idempotent, while conflicting imports and requests for predicates that a module does not export are errors.

Part 3-oriented definite clause grammars

A grammar rule Head --> Body. is prepared as an ordinary predicate with two additional difference-list arguments. Parameterized nonterminals retain their written arguments, so token(Type)//1 is implemented by token/3. Nonterminal indicators can be exported and imported through modules:

:- module(vocabulary, [word//1]).

word(noun) --> [robot] | [scientist].

The supported grammar constructs include terminal lists, [], sequencing with comma, alternatives with ; or |, if-then-else, embedded goals {Goal}, call//1, phrase//1, and !//0. Semicontexts provide look-ahead by restoring terminals to the remaining sequence:

look_ahead(X), [X] --> [X].

phrase(+Body,?Sequence) accepts or generates a complete sequence. phrase(+Body,?Sequence,?Rest) leaves Rest unconsumed and is steadfast in that argument. A variable body raises instantiation_error; a non-callable body raises type_error(callable). EyeProlog performs terminal-sequence checks and reports the portable ISO type_error(list) error term.

A bidirectional expression grammar

DCGs become more useful when the grammar produces a structured term rather than merely accepting a token list. The checked dcg-expression-language.pl example implements a small arithmetic language in both directions. Its parser respects precedence and left associativity while constructing an abstract syntax tree:

expression(AST) -->
  term(First),
  additive_tail(First, AST).

additive_tail(Left, AST) -->
  ['+'], term(Right),
  { Next = add(Left, Right) },
  additive_tail(Next, AST).
additive_tail(AST, AST) --> [].

The accumulator removes left recursion without moving parsing into JavaScript. A second DCG walks the AST in the other direction and emits only the parentheses needed to preserve its structure. The example therefore exercises parsing, semantic actions, nonterminal-to-nonterminal state hand-off, generation, backtracking, phrase/3 remainder handling, and AST-to-token-to-AST round-tripping. The checked answers are in examples/output/dcg-expression-language.pl.

Deep sequence hand-off

library(iso_ext) provides the common ... //0 helper, which describes an arbitrary number of input elements. It is not part of ISO Part 3, but it is a useful interoperability and stress-test relation. A compact hand-off test is:

a --> ..., epsilon.
epsilon --> [].

Here the remaining sequence is repeatedly passed from ... //0 to another nonterminal. For a finite compact list, EyeProlog can scan the arbitrary sequence iteratively instead of consuming one ordinary solver depth level per list cell. If the continuation is structurally proven to be a zero-width identity grammar such as epsilon//0, the hand-off can be continued without constructing a fresh general clause-resolution frame at every suffix. The list spine is still traversed; this is a control/allocation optimization rather than an O(1) semantic shortcut.

The optimization is deliberately narrow. phrase(..., Sequence, Rest) still enumerates the valid remainders, open or non-compact inputs retain ordinary relational behavior, and grammars that can consume or constrain the remainder are not treated as identity continuations. time/1 can be used in normal mode to measure such runs; its inference counter records solver-level inferences and does not count every internal step of an optimized scanner.

Part 3 leaves \+//1 and standalone ->//2 implementation dependent. EyeProlog uses non-consuming negation (\+ Body tests from the current state) and threads the state produced by the condition into the then-grammar.

Directives and protected built-ins

false/0 is the ISO always-failing built-in. It is protected as a static procedure, so source clauses headed by false are rejected instead of being interpreted as directives or integrity constraints.

Standard directives include dynamic/1, multifile/1, discontiguous/1, op/3, char_conversion/2, initialization/1, include/1, ensure_loaded/1, module/2, use_module/1, use_module/2, meta_predicate/1, and set_prolog_flag/2. Initialization goals run once after program preparation and before host queries. Included text is expanded in place; repeated ensure_loaded/1 designations are loaded once.

Normal output contains only ground query answers, one term and period at a time. Source facts are not echoed as new conclusions, and duplicate answers are suppressed. Answers are not asserted back into the running program. Supported output syntax is designed to be readable as Prolog input accepted by EyeProlog.

Automatic hybrid reasoning

The program loader detects predicate-dependency cycles, including dependencies inside conjunction, \+/1, once/1, and aggregate goals. Positive recursive components—including directly queried recursive relations—are tabled to an answer fixed point before answers are replayed. Components with a negative dependency retain guarded ordinary resolution, because positive least-fixed-point tabling does not define unstratified negation. Nonrecursive groups use indexed, depth-first resolution.

For calls with ground structural input, tabled answers can be reused within a solver run. The engine infers common structurally decreasing inputs from recursive heads. Fully open calls and calls whose inferred structural input is not ground may remain under ordinary resolution rather than forcing a possibly infinite relation into a table. This changes control, not declarative meaning.

Query execution

The host-supplied goal must be callable and may contain constants or variables. An unbound goal raises instantiation_error; a non-callable goal raises type_error(callable). A program without a supplied goal prints no normal answers. The host:

  1. parses all inputs into one program;
  2. collects source facts and host-supplied goals;
  3. runs initialization goals;
  4. solves each supplied goal;
  5. retains only ground answers;
  6. removes answers identical to source facts and suppresses duplicates;
  7. prints each answer and, only when requested, its why/2 explanation.

Goal selection affects host execution rather than the program’s logical meaning. One goal’s answers are not asserted for later goals, although internal tables may be reused during the solver run. For stable output, queries for known predicates are grouped by the source order in which their predicate groups first appear; goals within one group retain their supplied order. Queries for predicates with no group follow the known groups.

39. Built-in predicates by programming role

EyeProlog’s default registry contains the built-ins in its ISO compatibility profile. Where a predicate is defined by ISO/IEC 13211-1:1995, EyeProlog uses its standard predicate indicator; the registry also includes a few later or common compatibility predicates identified below. Arithmetic is expressed through is/2 rather than output arguments on arithmetic predicates. The registry contains 129 name/arity entries across 100 names.

Role Registered predicate indicators
Control and exceptions true/0, fail/0, false/0, !/0, call/1, call/2, call/3, call/4, call/5, call/6, call/7, call/8, \+/1, once/1, repeat/0, ;/2, ->/2, catch/3, throw/1, halt/0, halt/1
Unification and identity =/2, unify_with_occurs_check/2, \=/2, subsumes_term/2, ==/2, \==/2
Type tests var/1, nonvar/1, atom/1, integer/1, float/1, number/1, atomic/1, compound/1, callable/1, ground/1, acyclic_term/1
Term order compare/3, @</2, @=</2, @>/2, @>=/2, sort/2, keysort/2
Term inspection functor/3, arg/3, =../2, copy_term/2, term_variables/2
Collection findall/3, bagof/3, setof/3
Grammar processing phrase/2, phrase/3
Database and information clause/2, asserta/1, assertz/1, retract/1, retractall/1, abolish/1, current_predicate/1
Operators, conversion, and flags op/3, current_op/3, char_conversion/2, current_char_conversion/2, current_prolog_flag/2, set_prolog_flag/2
Atomic terms atom_length/2, atom_concat/3, sub_atom/5, atom_chars/2, atom_codes/2, char_code/2, number_chars/2, number_codes/2
Stream control open/3, open/4, close/1, close/2, current_input/1, current_output/1, set_input/1, set_output/1, flush_output/0, flush_output/1, stream_property/2, set_stream_position/2, at_end_of_stream/0, at_end_of_stream/1
Character input get_char/1, get_char/2, peek_char/1, peek_char/2, get_code/1, get_code/2, peek_code/1, peek_code/2
Character output put_char/1, put_char/2, put_code/1, put_code/2, nl/0, nl/1
Byte input/output get_byte/1, get_byte/2, peek_byte/1, peek_byte/2, put_byte/1, put_byte/2
Term input read/1, read/2, read_term/2, read_term/3
Term output write/1, write/2, writeq/1, writeq/2, write_canonical/1, write_canonical/2, write_term/2, write_term/3
Arithmetic is/2, =:=/2, =\=/2, </2, =</2, >/2, >=/2

Reading the built-in reference

The call patterns below use + for an argument that must be sufficiently instantiated, - for a result normally produced by the call, and ? for an argument that may be supplied or returned. These are principal operational modes, not a separate mode system enforced by the parser. A call described as semidet succeeds at most once; a nondet call may yield further answers on backtracking. Unless stated otherwise, checking a result that does not unify simply fails.

Built-in dispatch is authoritative and built-in procedures cannot be modified through the dynamic database predicates. Source clauses with the same indicator do not replace a built-in implementation. clause/2 and op/3 are the two dispatch exceptions: when a program defines a source predicate with that same indicator, EyeProlog uses the source clauses. false/0 is stricter still and is rejected as a source-clause head. Portable programs should avoid every such collision because other Prolog systems commonly reject it while loading.

Control, search, and exceptions

Predicate and principal call Behavior
true Succeeds once without binding variables.
fail, false Always fail. false/0 is provided as a compatibility alias and is also forbidden as a source-clause head.
! Commits to choices made since entry into the current predicate invocation. It does not erase alternatives belonging to an enclosing caller.
call(+Goal) Calls an atom or compound goal. An unbound argument raises instantiation_error; another non-callable term raises type_error(callable).
call(+Closure,?Arg,...) call/2 through call/8 append their extra arguments to an atom or compound closure, as specified by Corrigendum 2.
\+(+Goal) Negation as finite failure. It succeeds once when Goal has no solution and never exports bindings made while testing Goal. Bind variables needed by the test first.
once(+Goal) Returns only the first solution of Goal, or fails when there is none.
repeat Produces an unbounded sequence of successes; normally paired with a test, cut, exception, or halt/0.
Left ; Right Enumerates Left, then Right, restoring the incoming environment between branches. A cut inside a called predicate cannot discard the other branch.
If -> Then Commits to the first solution of If and runs Then; it does not provide an else branch by itself.
(If -> Then ; Else) Runs Then from the first solution of If, otherwise runs Else. Alternatives of If are discarded.
catch(+Goal,?Catcher,+Recovery) Runs Goal; on a matching thrown ball or PrologError, unifies it with Catcher and calls Recovery. Runtime errors are exposed as error(Formal,eyeprolog).
throw(+Ball) Throws a copied nonvariable term. An unbound ball raises instantiation_error.
halt, halt(+Status) Stops the processor with status 0 or the supplied integer. The JavaScript API reports the status without terminating its host process.

;/2 recognizes an ->/2 term on its left and implements the ISO if-then-else commitment described above. Cuts and committed conditions are operational controls; use ordinary relations when all alternatives should remain observable.

Definite clause grammar processing

Predicate and principal call Behavior
phrase(+Body,?Sequence) Parses or generates Sequence with a Part 3 grammar body and requires complete consumption.
phrase(+Body,?Sequence,?Rest) Parses or generates a prefix described by Body and unifies Rest with the unconsumed terminal sequence. The final unification is delayed so the third argument is steadfast.

Grammar rules are expanded during program preparation and therefore appear to the solver as ordinary predicates with two extra arguments. Dynamic grammar bodies passed to phrase/2-3 use the same expansion rules. This includes module qualification and the caller module used by embedded or meta-called nonterminals.

Unification, type tests, and term order

Predicate and principal call Behavior
?Left = ?Right Unifies two terms and returns the resulting bindings. EyeProlog rejects direct and indirect cyclic bindings.
unify_with_occurs_check(?Left,?Right) Performs occurs-check-safe unification. Because ordinary EyeProlog unification is already cycle-safe, it has the same successful bindings as =/2.
?Left \= ?Right Succeeds only when the terms cannot unify at call time. It is a test, not a delayed disequality constraint.
subsumes_term(+General,+Specific) Tests one-sided syntactic unification without binding either argument. Variables in Specific remain unchanged.
?Left == ?Right, ?Left \== ?Right Test term identity or non-identity without binding variables. Two distinct unbound variables are not identical.
var(?Term), nonvar(?Term) Test whether the dereferenced term is or is not an unbound variable.
atom(?Term), integer(?Term), float(?Term), number(?Term) Test the corresponding scalar category. Integer values retain arbitrary precision; finite noninteger numeric values are floats.
atomic(?Term), compound(?Term), callable(?Term), ground(?Term), acyclic_term(?Term) Test for an ISO atomic term, a compound, a callable atom/compound, a term containing no unbound variables, or a finite acyclic term. A default double-quoted value is a list and is therefore compound unless it is empty.
compare(?Order,+Left,+Right) Unifies Order with <, =, or > according to standard term order. A supplied order must be one of those atoms.
Left @< Right, Left @=< Right, Left @> Right, Left @>= Right Compare terms without arithmetic evaluation or bindings. These calls are semidet.
sort(+List,?Sorted) Sorts by standard term order and removes identical duplicates.
keysort(+Pairs,?Sorted) Stably sorts Key-Value pairs by key without removing duplicates.

For ISO terms, the standard term order is variables, numbers, atoms, then compounds; compound terms compare by arity, functor, and arguments. Within the numeric category, floats precede integers; floats compare by finite numeric value and integers compare exactly. ISO leaves the ordering of two distinct variables implementation dependent, subject to stability while a sorted list is being created. EyeProlog assigns a creation ordinal to each logical variable and carries that ordinal on the variable term itself; repeated occurrences share it within parsing or clause-freshening scope. It therefore does not keep a process-global table of every fresh variable name ever created, so long-running generators can create and discard fresh variables without growing an unrelated host Map. Double-quoted Prolog source follows the double_quotes flag and never creates an extra host-only scalar category.

Term construction and inspection

Predicate and principal call Behavior
functor(+Term,?Name,?Arity) Decomposes a term. Scalars have arity zero.
functor(-Term,+Name,+Arity) Constructs a scalar when Arity is zero or a compound with fresh arguments otherwise. Arity must be a nonnegative representable integer and a positive-arity name must be an atom.
arg(+Index,+Term,?Argument) Selects the one-based argument of a compound. Index zero or an index beyond the arity fails; a negative index is a domain error.
?Term =.. ?List Converts a term to [Functor\|Arguments] or constructs a term from a nonempty proper list. A one-item list constructs its atomic item.
copy_term(+Term,-Copy) Copies the dereferenced term while replacing every distinct unbound variable with a fresh variable and preserving variable sharing.
term_variables(+Term,?Variables) Returns distinct variables in first-occurrence traversal order. A supplied result may be a proper or partial list.

Construction calls raise instantiation_error when neither side supplies the required shape. =../2 distinguishes an incomplete list (instantiation_error) from an improper list (type_error(list)).

Solution collection

Predicate and principal call Behavior
findall(+Template,+Goal,?Bag) Collects a fresh copy of Template for every solution of Goal, preserving solution order. It succeeds with [] when there are no solutions and treats all free variables existentially.
bagof(+Template,+Goal,?Bag) Groups answers by free variables not present in Template. It yields one nonempty bag per witness group and fails when no group exists. Prefix variables with ^ in Goal to quantify them existentially.
setof(+Template,+Goal,?Set) Has the grouping behavior of bagof/3, then sorts each group by profile term order and removes identical duplicates.

Each collector runs its goal in an isolated inner search while sharing the current logical program and stream state. Collected terms are copied, so local variables do not escape accidentally. The bag argument must be a proper or partial list.

Dynamic database and procedure information

Predicate and principal call Behavior
clause(+Head,?Body) Enumerates fresh copies of source clauses matching the callable Head; facts have body true. Access to built-ins raises permission_error(access,private_procedure).
asserta(+Clause), assertz(+Clause) Insert a copied fact or rule at the beginning or end of a predicate declared dynamic/1. Static and built-in procedures cannot be modified.
retract(+Clause) Removes matching dynamic clauses one at a time on backtracking. A call sees the logical update view captured when it began. A fact pattern matches facts only.
retractall(+Head) Removes every matching clause from a dynamic procedure, succeeds when none match, and keeps the empty dynamic procedure known.
abolish(+Name/+Arity) Removes a dynamic procedure and its clauses. The indicator must contain an atom and a nonnegative representable integer.
current_predicate(?Name/?Arity) Enumerates predicate groups present in the loaded program, including empty dynamic groups. It does not enumerate registry-only built-ins.

Declare mutable predicates explicitly, including empty ones:

:- dynamic(cache/2).

remember(Key, Value) :- retract(cache(Key, _)), !, assertz(cache(Key, Value)).
remember(Key, Value) :- assertz(cache(Key, Value)).

Assertions and retractions invalidate affected reasoning tables. Mutating a predicate that was not declared dynamic raises a permission error rather than silently changing a static program.

Operators, character conversion, and flags

Predicate and principal call Behavior
op(+Priority,+Specifier,+NameOrNames) Defines or removes operators in the current program. Priority is 0..1200; specifiers are fx, fy, xf, yf, xfx, xfy, or yfx; names may be one atom or a proper list. Priority zero removes the definition. , and \| cannot be modified.
current_op(?Priority,?Specifier,?Name) Enumerates active operator definitions and filters supplied arguments.
char_conversion(+Input,+Output) Installs a one-character conversion. In prepared Prolog text, later unquoted characters are converted when char_conversion=on; quoted characters are unchanged. The same mapping initializes execution-time term input. Mapping a character to itself removes its custom mapping.
current_char_conversion(?Input,?Output) Enumerates installed nonidentity conversions.
current_prolog_flag(?Flag,?Value) Enumerates flags or retrieves one named flag. An unknown bound flag raises domain_error(prolog_flag).
set_prolog_flag(+Flag,+Value) Changes a supported mutable flag after validating its allowed atom value. Read-only flags raise a permission error.
Flag Default in normal EyeProlog Allowed values Mutable
bounded false false no
integer_rounding_function toward_zero toward_zero no
char_conversion on on, off yes
debug off on, off yes
max_integer no current value because bounded=false not applicable no
min_integer no current value because bounded=false not applicable no
max_arity unbounded unbounded no
unknown error error, fail, warning yes
double_quotes chars chars, codes, atom yes
occurs_check true true, error yes

Because bounded=false, current_prolog_flag(max_integer, _) and current_prolog_flag(min_integer, _) fail as required by ISO 7.11.1.1; EyeProlog does not expose an unbounded sentinel as either flag value. Preparation-time char_conversion/2 mappings affect later unquoted source text and also initialize the execution-time conversion mapping; setting the char_conversion flag to off disables conversion for following source text. Quoted source characters are not converted.

Both normal EyeProlog and strict ISO core mode use the ISO unknown=error default. Interactive set_prolog_flag/2 changes are retained when the REPL consults another file or imports a module instead of being reset by the host rebuild of the program. Programs that intentionally treat an undefined predicate as failure must opt in with set_prolog_flag(unknown, fail); bundled examples and non-ISO corpus cases that depend on that policy do so explicitly. The occurs_check flag is an EyeProlog diagnostic extension rather than an ISO-defined core flag: it is absent in strict mode, while normal mode keeps its true default and optional error diagnostic for STO attempts. Operator and flag directives are processed per program rather than changing global JavaScript state. The double_quotes setting affects subsequent source text, included files, command-line and API goal text, and terms read by read_term/*:

% Default: a list of one-character atoms.
chars("ab").                 % chars([a,b])

:- set_prolog_flag(double_quotes, codes).
codes("ab").                 % codes([97,98])

:- set_prolog_flag(double_quotes, atom).
quoted_atom("ab").           % quoted_atom(ab)

Atomic-term operations and conversions

Predicate and principal call Behavior
atom_length(+Atom,?Length) Counts Unicode code points, not UTF-16 code units. A supplied length must be a nonnegative integer.
atom_concat(?Prefix,?Suffix,?Whole) Concatenates two atoms, removes a supplied prefix or suffix, or enumerates every split when only Whole is bound. At least Whole, or both parts, must determine the operation.
sub_atom(+Atom,?Before,?Length,?After,?SubAtom) Enumerates substrings and their Unicode-code-point offsets. Supplied counts must be nonnegative integers.
atom_chars(?Atom,?Chars), atom_codes(?Atom,?Codes) Convert between an atom and a proper list of one-character atoms or character codes. Both profiles use EyeProlog’s Unicode scalar PCS/codes; surrogates and values above U+10FFFF are rejected. At least one side must be instantiated.
char_code(?Character,?Code) Converts one character atom and its collating/code value. Both profiles accept Unicode scalar codes and reject surrogates/out-of-range values.
number_chars(?Number,?Chars), number_codes(?Number,?Codes) Convert finite numbers to canonical text or parse a proper character/code list using ISO number and negative-number syntax, including radix integers, character-code constants, and leading layout. The input is not parsed as a general term: grouping such as (0) is a syntax error. At least one side must be instantiated; malformed numeric input raises syntax_error(number).

Conversions accept partial output lists when the atomic input is known, but constructing an atom or number requires a complete proper list with no unbound elements. Numeric parsing accepts ISO layout before tokens, including layout between a minus token and the following numeric token. A single-line %... comment may therefore follow - directly because % cannot continue a graphic token; an adjacent bracketed comment in -/**/1 remains a syntax error under the eager token-consumer rule. Decimal fractions and decimal exponents are supported; the apostrophe character code is written with a doubled apostrophe as 0''' and has value 39, while a literal space character code is 0' and has value

  1. Character-code constants consume one Unicode scalar, including a non-BMP character. Trailing layout, comments, and other material are rejected; bound integers are converted to their canonical decimal spelling, and non-finite values are rejected. Equivalent spellings of the same numeric type compare by value, preserving the standard conversion round trip, while integer and floating-point terms remain distinct. The regression gate vendors all 74 numbered cases from Ulrich Neumerkel’s contemporary number_chars/2 comparison, including the Cor.2 error-precedence cases; number_codes/2 shares the same numeric parser and has mirrored coverage for the recent numeric-syntax regressions.

Streams and unit I/O

Stream arguments accept an alias atom or the opaque handle returned by open/3 or open/4. Omitting a stream argument selects the current standard input or output.

Predicate and principal call Behavior
open(+Source,+Mode,-Stream), open(+Source,+Mode,-Stream,+Options) Opens an atom path in read, write, or append mode. Options are type(text or binary), alias(Atom), reposition(true or false), and eof_action(error, eof_code, or reset).
close(+Stream), close(+Stream,+Options) Closes a nonstandard stream. The only close option is force(true or false); standard streams remain available.
current_input(?Stream), current_output(?Stream) Return or test the current input or output handle.
set_input(+Stream), set_output(+Stream) Select an existing stream with the required direction.
flush_output, flush_output(+Stream) Completes successfully for the current output or validates and flushes the selected output stream. EyeProlog writes synchronously.
stream_property(?Stream,?Property) Enumerates streams and their properties: mode/1, type/1, reposition/1, eof_action/1, position/1, input, output, end_of_stream/1, and optional alias/1 and file_name/1.
set_stream_position(+Stream,+Position) Repositions a stream opened with reposition(true). Position is a nonnegative integer or position(Integer) within the stream content.
at_end_of_stream, at_end_of_stream(+Stream) Succeeds when the current or selected input position is at or beyond its content.
get_char(?Character), get_char(+Stream,?Character) Reads one text character; end of input is end_of_file.
peek_char(?Character), peek_char(+Stream,?Character) Observes the next text character without advancing.
get_code(?Code), get_code(+Stream,?Code) Reads a character code; end of input is -1. Both profiles return codes from EyeProlog’s Unicode scalar PCS.
peek_code(?Code), peek_code(+Stream,?Code) Observes the next Unicode scalar character code without advancing.
get_byte(?Byte), get_byte(+Stream,?Byte) Reads one unit from a binary stream; end of input is -1.
peek_byte(?Byte), peek_byte(+Stream,?Byte) Observes the next binary unit without advancing.
put_char(+Character), put_char(+Stream,+Character) Writes one character atom to a text stream.
put_code(+Code), put_code(+Stream,+Code) Writes one character code to a text stream. Both profiles accept Unicode scalar codes.
put_byte(+Byte), put_byte(+Stream,+Byte) Writes an integer in 0..255 to a binary stream.
nl, nl(+Stream) Writes a newline to a text stream.

Text operations on binary streams and byte operations on text streams raise permission errors. After EOF, eof_action(error) rejects another consuming read, eof_code continues returning the EOF value, and reset resumes from the beginning. A peek does not mark the stream as past-end.

Term input and output

Predicate and principal call Behavior
read(?Term), read(+Stream,?Term) Reads one full-stop-terminated Prolog term from a text stream. Returns end_of_file when no term remains.
read_term(?Term,+Options), read_term(+Stream,?Term,+Options) Reads a term and supports variables(List), variable_names(Pairs), and singletons(Pairs). Unknown options raise domain_error(read_option).
write(+Term), write(+Stream,+Term) Writes readable operator notation without quoting atoms merely because quoting would be required for reparsing. Number variables are enabled.
writeq(+Term), writeq(+Stream,+Term) Like write, but quotes atoms when required for unambiguous input syntax.
write_canonical(+Term), write_canonical(+Stream,+Term) Writes quoted canonical functor notation while ignoring operators and without interpreting $VAR/1.
write_term(+Term,+Options), write_term(+Stream,+Term,+Options) Writes with quoted(true or false), ignore_ops(true or false), numbervars(true or false), and variable_names([Name=Variable,…]). Normal mode also supports double_quotes(true or false) and spacing(true or false).

Term input uses the program’s current operator table and the same ISO quoted-character syntax as source text, including backslash-terminated octal and hexadecimal escapes such as '\7\' and '\x7\'. This applies equally to read/1-2 and read_term/2-3. Installed character conversions are applied outside quoted text when the char_conversion flag is on. variable_names/1 and singletons/1 omit anonymous variables. Output predicates do not append a period or newline; call write/1, then write('.') and nl/0 when emitting a complete source term manually.

A standalone numeric term read by read/1-2 or read_term/2-3 uses the same bounded numeric scanner and canonical value conversion as number_chars/2. Consequently every numeric character sequence accepted by number_chars/2 has the same value when read as a full-stop-terminated term, without requiring EOF after that term.

Arithmetic expressions

Predicate and principal call Behavior
is(?Result,+Expression) Evaluates Expression once and unifies its numeric value with Result. It is evaluation plus unification, not mutable assignment.
Left =:= Right, Left =\= Right Evaluate both sides and test numeric equality or inequality. Integer/float representation differences do not by themselves make values unequal.
Left < Right, Left =< Right, Left > Right, Left >= Right Evaluate both sides and perform the indicated numeric comparison.

Every variable in an arithmetic expression must already be bound to a number or evaluable expression. Integers use arbitrary-precision arithmetic while an operation remains in the integer domain; operations requiring floating point convert their operands to finite JavaScript numbers.

Expression family Supported forms and result rules
Literals and constants Integer and finite floating-point literals; pi and e produce floating-point constants.
Unary arithmetic Unary +, unary -, and integer bitwise complement \.
Basic binary arithmetic +, -, and * preserve integers when both operands are integers. / produces a float and rejects a zero divisor.
Exponentiation Base ^ Exponent remains an integer for nonnegative integer operands. Corrigendum 3 requires a float base for most negative integer exponents; ** is floating-point exponentiation.
Integer division // and div require integers and reject zero divisors. // rounds toward zero as reported by integer_rounding_function; div rounds down.
Integer remainder rem is the truncating remainder; mod normalizes the result with the divisor’s sign. Both require integers and a nonzero divisor.
Bit operations Integer /\, \/, xor, <<, and >>, plus unary \.
Numeric normalization abs, sign, and float. Integer abs and sign preserve integer results; float produces a float.
Rounding truncate, round, ceiling, and floor produce integers.
Float decomposition float_integer_part and float_fractional_part require a float and return floats.
Min/max and transcendental functions min, max, sin, cos, atan, asin, acos, atan2, tan, exp, log, and sqrt; pi is the Corrigendum 2 constant.

Arithmetic comparisons evaluate both operands. Standard term-order predicates (@<, @=<, @>, @>=) compare terms without arithmetic evaluation. EyeProlog’s documented profile order distinguishes floats from integers rather than applying arithmetic equality across representations. Double-quoted text does not introduce another ISO term-order category: it becomes the list or atom selected by double_quotes before comparison.

Errors

ISO built-ins distinguish logical failure from exceptional calls. Insufficient instantiation raises instantiation_error; wrong argument categories raise type_error; invalid values raise domain_error; and arithmetic faults raise evaluation_error. JavaScript embedders receive these as PrologError instances whose message contains the corresponding Prolog error term.

Error class Typical cause
instantiation_error A required callable, stream, number, list, option value, or construction input is still unbound.
type_error(Expected,Culprit) A bound value has the wrong term category, such as a noninteger index or non-callable goal.
domain_error(Domain,Culprit) The type is correct but the value is outside the supported domain, such as a bad stream option or operator priority.
representation_error(Flag) A value cannot be represented by the profile, such as an invalid Unicode scalar code.
evaluation_error(zero_divisor) Integer or floating-point division was attempted with a zero divisor.
evaluation_error(undefined) Floating-point evaluation produced a non-finite or undefined result.
permission_error(Operation,Permission,Culprit) A static procedure was modified, a stream was used in the wrong mode, or a protected resource was accessed.
existence_error(Object,Culprit) A stream, source sink, or required procedure does not exist.
syntax_error(number), syntax_error(read_term) Lexical number conversion or streamed term parsing failed.

catch/3 converts a PrologError into a catchable error(Formal,eyeprolog) term. throw/1 copies its ball before unwinding: bound parts are preserved, repeated variables remain shared within the copied ball, and unbound variables are fresh with respect to the protected goal and catcher. Catchable error terms follow the same variable-freshening rule. The interactive top level uses the same ISO error envelope for uncaught processor errors, so an ordinary runtime error is displayed as error(Formal,eyeprolog) rather than dropping the implementation-defined second argument. Variables that occur in an uncaught ISO error are rendered with fresh answer names such as _A rather than reusing query-variable spellings such as X or Xx; this keeps the displayed error consistent with the copied exception term. An unmatched ball or error continues outward.

Streams belong to one solver run and are shared by nested calls, exceptions, and solution collectors. user_input and user_output are always present. open/4 supports type/1, alias/1, reposition/1, and eof_action/1; read_term/3 supports variables/1, variable_names/1, and singletons/1. The JavaScript ioOptions.input and ioOptions.write hooks connect standard streams to an embedder. File-backed streams use synchronous lifecycle semantics so side effects occur in Prolog execution order.

Normal-mode cleanup controls

call_cleanup/2 and setup_call_cleanup/3 are normal EyeProlog runtime extensions rather than members of the isolated ISO builtin registry. They protect a goal across deterministic completion, exhaustion, cut, top-level abandonment, and exception unwinding, running Cleanup exactly once. setup_call_cleanup/3 runs Setup once and installs Cleanup only after Setup succeeds. A successful Cleanup run before a deterministic answer contributes its substitutions to that answer. Nested cleanups run inside-out, and strict ISO mode does not provide either predicate.

The EyeProlog library

EyeProlog exposes 299 distinct non-ISO library and normal-extension predicate indicators in addition to the 129 indicators in its isolated ISO profile. 241 are defined entirely as ordinary Prolog clauses in focused modules under src/lib/; 58 use host support for control, attributed variables, constraints, or observability. The ISO and library catalogs therefore cover 428 distinct predicate indicators. Normal-mode controls and observability relations that do not belong to a library, such as call_cleanup/2, setup_call_cleanup/3, statistics/0,2, and tnot/1, are documented in their own sections rather than counted as library predicates. time/1 is additionally registered directly in the normal runtime so Trealla-style timing works at the interactive top level without an import; it is absent from the strict ISO registry.

The sources are src/lib/aggregate.pl, src/lib/arithmetic.pl, src/lib/assoc.pl, src/lib/atts.pl, src/lib/between.pl, src/lib/charsio.pl, src/lib/clpb.pl, src/lib/clpz.pl, src/lib/comparison.pl, src/lib/dates.pl, src/lib/dcgs.pl, src/lib/debug.pl, src/lib/dif.pl, src/lib/error.pl, src/lib/format.pl, src/lib/freeze.pl, src/lib/gensym.pl, src/lib/iso_ext.pl, src/lib/lambda.pl, src/lib/lists.pl, src/lib/ordsets.pl, src/lib/pairs.pl, src/lib/pio.pl, src/lib/primes.pl, src/lib/prologue.pl, src/lib/random.pl, src/lib/reif.pl, src/lib/si.pl, src/lib/strings.pl, src/lib/tabling.pl, src/lib/terms.pl, src/lib/time.pl, src/lib/ugraphs.pl, src/lib/uuid.pl, and src/lib/when.pl. Each declares a same-named module with module/2; there is no catch-all library(eyeprolog). A program imports only the modules it needs, and use_module/2 can select an even smaller indicator list. The Prologue module exposes p.p.1 through p.p.11 of the working-draft Prologue, as a compatibility facade over the canonical lists, between, iso_ext, and freeze modules. The published Prologue, call_nth/2, and length/2 quads are retained as offline regressions. src/standard-library.js registers the module sources and private control and constraint adapters for Node and browser resolution. Explicit use_module/1-2 loads remain supported; outside strict ISO mode, the conservative interop autoloader may also load a module for one uniquely mapped common predicate. The core registry remains available through createDefaultRegistry() and getDefaultRegistry() for low-level embedding. The stricter Part 1 + Corrigenda registry is exposed as createStrictIsoRegistry() and getStrictIsoRegistry() and is paired with isoStrict: true when a complete strict-language boundary is required. Module-local predicate identity keeps private helpers and same-named predicates in different modules separate.

freeze(?Term,:Goal) runs Goal immediately when Term is already nonvariable; otherwise it delays the goal until Term becomes nonvariable. Suspensions are kept in the logical environment, so bindings and backtracking remain isolated between solution branches. When a suspension wakes, its goal is meta-invoked with its own cut scope: a ! inside the delayed goal may commit choices made by that invocation, but it cannot prune alternatives that were created before the freeze/2 call. Multiple suspensions on the same variable are stored internally as a binary join tree, making each merge constant-time instead of repeatedly appending an ever-growing list. Wakeup and residual projection traverse that tree left-to-right and emit the original suspensions separately. This keeps a call/1-style cut boundary for every delayed goal without collapsing the user-visible residuals into one conjunction. Thus call(((Y=1;Y=2),freeze(X,!),X=c));Y=3 retains the three answers Y=1, Y=2, and Y=3.

dif(?Left,?Right) posts a delayed finite-tree disequality when its arguments can still unify. Its residual store is normalized by logical implication: symmetric or equivalent constraints share one residual, and a stronger constraint removes weaker ones regardless of insertion order. Independent disequalities remain separate. Residual projection is re-evaluated in each solution environment, so a compound disequality is kept intact until later bindings make one aligned subterm pair sufficient. For example:

?- dif(f(X,A),f(Y,B)), ( true ; A = B ).
   dif(f(X, A), f(Y, B))
;  A = B, dif(X, Y).
Module Exported predicate indicators Primary role
library(aggregate) sumall/3, aggregate_min/5, aggregate_max/5 Aggregation
library(arithmetic) lsb/2, msb/2, popcount/2 CLP(Z) arithmetic support
library(assoc) empty_assoc/1, assoc_to_keys/2, assoc_to_list/2, assoc_to_values/2, del_assoc/4, del_max_assoc/4, del_min_assoc/4, gen_assoc/3, get_assoc/3, get_assoc/5, is_assoc/1, list_to_assoc/2, map_assoc/2, map_assoc/3, max_assoc/3, min_assoc/3, ord_list_to_assoc/2, put_assoc/4 AVL association trees; reused from the shared portable source
library(atts) put_atts/2, get_atts/2, put_attr/3, get_attr/3, del_attr/2, term_attributed_variables/2, call_residue_vars/2 Attributed variables
library(between) between/3, gen_int/1, gen_nat/1, numlist/2, numlist/3, repeat/1 Integer generation
library(charsio) char_type/2, get_line_to_chars/3, get_n_chars/3, get_single_char/1 Character classification and stream reads
library(clpb) labeling/1, random_labeling/2, sat/1, sat_count/2, taut/2, weighted_maximum/3 Boolean constraints and BDD reasoning; upstream Prolog source with small state adapters
library(clpz) #>/2, #</2, #>=/2, #=</2, #=/2, #\=/2, #\/1, #<==>/2, #==>/2, #<==/2, #\//2, #\/2, #/\/2, in/2, ins/2, all_different/1, all_distinct/1, nvalue/2, sum/3, scalar_product/4, tuples_in/2, labeling/2, label/1, indomain/1, lex_chain/1, serialized/2, global_cardinality/2, global_cardinality/3, circuit/1, cumulative/1, cumulative/2, disjoint2/1, element/3, automaton/3, automaton/8, zcompare/3, chain/2, fd_var/1, fd_inf/2, fd_sup/2, fd_size/2, fd_dom/2, clpz_t/2, #=/3, #</3 Constraint logic programming over integers; the final three indicators support reified compatibility libraries
library(comparison) lt/2, gt/2, le/2, ge/2 Generic comparison
library(dates) difference/3 ISO duration differences
library(dcgs) phrase/2, phrase/3, seq/3, seqq/3 DCG compatibility; seq/3 and seqq/3 are declared as seq //1 and seqq //1
library(debug) */1, $/1, $-/1, debug/1, debug/3, nodebug/1, bb_get/2, bb_put/2, bb_b_put/2, bb_global_get/2 Declarative debug operators and constraint-library blackboards
library(dif) dif/2 Common module facade over native delayed disequality
library(error) must_be/2, can_be/2, instantiation_error/0, instantiation_error/1, domain_error/2, domain_error/3, type_error/2, type_error/3, representation_error/1, resource_error/1, call_with_error_context/2 Error checking and construction
library(format) format_/4, format/2, format/3, listing/1, portray_clause_/3, portray_clause/1, portray_clause/2 Formatted DCG text and output; format_/4 and portray_clause_/3 are the expanded nonterminals
library(freeze) freeze/2 Delayed goals
library(gensym) gensym/2, reset_gensym/1 Process-local generated atoms
library(iso_ext) call_nth/2, countall/2, forall/2, succ/2, cfor/3, findall/4, variant/2, time/1, .../2 Common ISO extensions
library(lambda) ^/3, ^/4, ^/5, ^/6, ^/7, ^/8, ^/9, ^/10, \/1, \/2, \/3, \/4, \/5, \/6, \/7, \/8, +\/2, +\/3, +\/4, +\/5, +\/6, +\/7, +\/8, +\/9 Higher-order lambda notation
library(lists) member/2, memberchk/2, select/3, append/2, append/3, last/2, same_length/2, nth0/3, nth0/4, nth1/3, nth1/4, reverse/2, length/2, maplist/2, maplist/3, maplist/4, maplist/5, maplist/6, maplist/7, maplist/8, foldl/4, foldl/5, foldl/6, sum_list/2, min_list/2, max_list/2, list_to_set/2, list_max/2, list_min/2, permutation/2, transpose/2, set_nth0/4, take/3, drop/3, slice/4 List relations and shared matrix/permutation helpers
library(ordsets) is_ordset/1, list_to_ord_set/2, ord_add_element/3, ord_del_element/3, ord_disjoint/2, ord_empty/1, ord_intersect/2, ord_intersect/3, ord_intersection/2, ord_intersection/3, ord_intersection/4, ord_memberchk/2, ord_selectchk/3, ord_seteq/2, ord_subset/2, ord_subtract/3, ord_symdiff/3, ord_union/2, ord_union/3, ord_union/4 Ordered-set relations; reused upstream source
library(pairs) pairs_keys_values/3, pairs_keys/2, pairs_values/2, group_pairs_by_key/2, map_list_to_pairs/3 Key-value pair support
library(pio) phrase_from_file/2, phrase_from_file/3, phrase_to_file/2, phrase_to_file/3, phrase_to_stream/2 Eager portable DCG file and stream I/O
library(primes) smallest_divisor_from/3 Prime factor support
library(prologue) member/2, append/3, length/2, between/3, select/3, succ/2, maplist/2, maplist/3, maplist/4, maplist/5, maplist/6, maplist/7, maplist/8, nth0/3, nth0/4, nth1/3, nth1/4, call_nth/2, freeze/2, foldl/4, foldl/5, foldl/6, countall/2 Legacy facade over canonical focused modules
library(random) maybe/0, random/1, random/3, random_integer/3, set_random/1 Common mutable-seed interface plus EyeProlog’s pure state-threaded generator
library(reif) ,/3, ;/3, =/3, cond_t/3, dif/3, if_/3, memberd_t/3, tfilter/3, tmember/2, tmember_t/3, tpartition/4 Reified conditions and list filtering; reused upstream source
library(si) atom_si/1, integer_si/1, atomic_si/1, list_si/1, character_si/1, term_si/1, chars_si/1, dif_si/2, not_si/1, when_si/2 Sufficient-instantiation checks used by CLP(Z)
library(strings) matches/3, split/3, replace/4, lowercase/2, uppercase/2, trim/2, number_string/2, atom_string/2, term_string/2, string_concat/3, contains/2, matches/2, join/3, substring/4 Text relations
library(tabling) abolish_all_tables/0, start_tabling/2 Common explicit syntax over automatic recursive tabling
library(terms) numbervars/3, copy_term_nat/2 Term operations used by bundled libraries
library(time) current_time/1, format_time/4 Clock timestamps and the expanded format_time//2 nonterminal
library(ugraphs) add_edges/3, add_vertices/3, complement/2, compose/3, connect_ugraph/3, del_edges/3, del_vertices/3, edges/2, neighbors/3, neighbours/3, reachable/3, top_sort/2, top_sort/3, transitive_closure/2, transpose_ugraph/2, ugraph_union/3, vertices/2, vertices_edges_to_ugraph/3 Directed graph relations; reused upstream source
library(uuid) uuid/3, uuid_string/2, uuidv4/1, uuidv4_string/1 Common UUID byte/string conversion and generation plus pure state threading
library(when) when/2 Shared delayed-condition interface over attributed variables

Interoperability profile and conservative autoloading

EyeProlog keeps four related concepts separate:

Layer Meaning
ISO core The documented ISO predicate profile built into the processor. No EyeProlog library import is involved.
EyeProlog library surface Every module and exported predicate listed in the catalog above. Programs normally access these with use_module/1-2.
Interoperability profile A deliberately smaller set of library names and predicate interfaces that EyeProlog intends to keep source-compatible with Trealla and Scryer where practical.
Autoload map An even smaller convenience table that gives selected unqualified predicates one canonical EyeProlog provider.

These layers answer different questions. A predicate may be implemented entirely as ordinary Prolog and still be outside the cross-processor interoperability profile; conversely, an interoperable predicate may be backed by a private host adapter. In this section, portable refers to source portability between Prolog systems, not merely to the language in which a predicate happens to be implemented.

The shared module-name profile is the overlap of the Scryer src/lib and Trealla library layouts that EyeProlog can implement without pretending an engine-specific service exists. It includes arithmetic, assoc, atts, charsio, clpb, clpz, debug, dif, format, freeze, gensym, iso_ext, lambda, lists, ordsets, pio, random, reif, tabling, time, ugraphs, uuid, and when. The predicate profile is narrower than the union of their exports: for example, EyeProlog’s explicit-state random/3 and uuid/3 remain useful extensions rather than shared interfaces.

Source reuse is preferred over translation. clpb.pl, ordsets.pl, reif.pl, and ugraphs.pl retain the upstream Prolog algorithms and license headers; assoc.pl uses the complete upstream AVL implementation. gensym.pl and when.pl keep the same algorithms with small blackboard and parser-safe closure adaptations. dif.pl, tabling.pl, and the clock portion of time.pl are thin facades over EyeProlog runtime facilities. charsio.pl and pio.pl provide the common character and eager DCG I/O surfaces. The portable library overlap example composes Boolean constraints, ordered sets, graphs, reification, delayed goals, generated names, character conversion, transposition, and explicit table syntax in one checked program.

Two matching upstream basenames are intentionally not exposed as portable libraries. The two builtins.pl files are private engine facades and have no shared public predicate interface. sockets.pl requires a native networking event loop and host socket objects; EyeProlog does not provide a source-only facade that would accept calls and then fail at runtime. Rational-only library(arithmetic) predicates are likewise omitted until rational numbers are processor values.

For library(lists), the current interop predicate set is member/2, memberchk/2, select/3, append/2-3, last/2, same_length/2, nth0/3-4, nth1/3-4, reverse/2, length/2, maplist/2-8, foldl/4-6, sum_list/2, list_to_set/2, list_max/2, list_min/2, permutation/2, and transpose/2. Other exports from the same module, such as min_list/2, max_list/2, set_nth0/4, take/3, drop/3, and slice/4, remain available to EyeProlog programs but lie outside this conservative cross-engine subset.

length/2 remains fully relational. With both arguments variable, length(Xs, N) enumerates Xs = [], N = 0, then one-element lists with N = 1, and so on. Open-ended generation uses the normal memory guard with recovery headroom so finite-heap exhaustion remains a catchable resource_error(memory). A supplied nonnegative length selects at most one answer, and a supplied closed list has exactly one length; these modes do not retain an exhausted choicepoint.

library(iso_ext) is a common interop module name, but only part of its EyeProlog API belongs to the shared profile. call_nth/2, time/1, and .../2 are mapped there. time/1 measures each solution of a meta-call and prints elapsed time, EyeProlog inference count, and MLips in Trealla-style form, for example % Time elapsed 0.832s, 65551 Inferences, 0.079 MLips; ... //0 describes an arbitrary number of input elements. Together they let the Trealla/Scryer DCG hand-off benchmark run in EyeProlog without source changes (assuming the usual list library is already imported in an interactive session). The focused modules have one canonical implementation owner per predicate. library(prologue) re-exports those same owners, so legacy code can combine the facade with library(lists), library(iso_ext), and library(freeze) in either import order without an accidental collision.

library(lambda) follows Scryer’s higher-order notation, adapted from Ulrich Neumerkel’s permissively licensed implementation. Its public syntax is:

\X1^X2^...^XN^Goal
Free+\X1^X2^...^XN^Goal

The first form has no explicitly shared free variables. Before each invocation, EyeProlog copies the closure term so local variables are fresh on successive maplist/2-8, foldl/4-6, or direct call/N uses. In the second form, the variables contained in Free remain shared with the surrounding goal. Importing the library installs +\ as a priority-201 xfx operator; \ and ^ use their existing ISO operator definitions. Parenthesize lower-priority goal operators after ^, for example \X^(X > 3).

A continuation lambda may leave arguments for a later call:

f(x, y).

answer(A, B) :- call(\X^f(X), A, B).

This is equivalent to supplying both arguments directly. A lambda called with too few parameters raises existence_error(lambda_parameter, ...). EyeProlog uses its ISO copy_term/2 implementation for the fresh-copy step and does not require a separate copy_term_nat/2 predicate.

Autoloading is a convenience layered on top of the interoperability profile; it is not a general search through all EyeProlog libraries. When a source program or an explicit CLI/API goal is built, an otherwise undefined unqualified predicate may be autoloaded only when the interop table assigns it one canonical provider. The interactive top level keeps ordinary library imports explicit; time/1 is available there because it is also a normal EyeProlog runtime extension. For example, the canonical build-time providers are:

Predicate Canonical autoload provider
member/2 library(lists)
call_nth/2 library(iso_ext)
time/1 library(iso_ext)
.../2 library(iso_ext)
between/3 library(between)

Predicates outside that table require an explicit import even when EyeProlog provides them. Explicit imports therefore remain the clearest way to state library dependencies:

:- use_module(library(lists)).
:- use_module(library(iso_ext), [call_nth/2]).

Use --no-autoload, or the JavaScript option autoload: false, when every library dependency should be explicit. --iso-strict always disables EyeProlog library autoloading.

-w / --warnings reports explicit dependencies on non-profile libraries and calls to non-profile predicates from otherwise common modules. --portable turns those diagnostics into a failing run, making the conservative profile suitable for continuous integration. npm run test:interop executes the same portable Towers of Hanoi source under EyeProlog, Trealla, and Scryer when those commands are installed. Because those are external runtimes, the default npm test instead validates all four generated OpenRuleBench source trees and their engine-specific tabling and WFS adaptations without requiring them. The fast structural check is also available directly as npm run test:openrulebench.

Library notes beyond the interoperability profile

The catalog above is authoritative for the complete EyeProlog library surface. The following notes describe useful parts of that surface without extending the cross-engine claims made above.

library(atts) is the Prolog-facing attributed-variable layer over the persistent annotated-variable machinery in src/term.js, with its small host bridge in src/atts.js. It provides the attribute operations used by Scryer libraries, accepts :- attribute ... declarations, invokes module-local verify_attributes/3 before an attributed binding is committed, and schedules the returned goals immediately after the binding. Attribute maps are copied only when changed and therefore backtrack with Env branches; the interactive top level projects module attribute_goals//1 hooks as residual goals. The checked examples/attributed-variables.pl demonstrates binding verification and attribute transfer across aliases.

library(clpz) is Markus Triska’s MIT-licensed Scryer Prolog implementation of constraint logic programming over integers, bundled as src/lib/clpz.pl. EyeProlog executes the Prolog propagator implementation through the generic attributed-variable machinery in src/term.js and src/atts.js. The library provides relational arithmetic and reification, finite and union domains, labeling, all-different/all-distinct constraints, sums and scalar products, extensional tuple tables, lexicographic chains, serialized and cumulative scheduling, global cardinality with costs, Hamiltonian circuits, disjoint2/1, automaton/3,8, value counting, comparison, and domain reflection.

The compiler services used by the library are ordinary EyeProlog facilities: module-local and user term_expansion/2 and goal_expansion/2, clause-list expansion, and expand_term/2 for processor DCG lowering. The same runtime also provides a generic copy-on-write backtrackable blackboard and the supporting Prolog modules assoc, pairs, between, dcgs, terms, error, si, freeze, arithmetic, debug, and format. The bundled CLP(Z) source is synchronized with Scryer commit e3df91e25f8a09ee942c04e8baef553bba5c6110, Git blob 806445c11e14c8b2515f3de7f309e0ac04d9ad04.

Alongside its interop entries call_nth/2, time/1, and .../2, library(iso_ext) also exports EyeProlog’s extension relations countall/2, forall/2, succ/2, cfor/3, findall/4, and variant/2. forall/2 checks an action for every solution of a condition; cfor/3 enumerates an inclusive evaluated integer range; succ/2 relates adjacent nonnegative integers; findall/4 collects into a difference list; and variant/2 recognizes terms equal up to variable renaming. countall/2 counts solutions without exposing a template. These exports do not all belong to the conservative interop subset merely because they share the iso_ext module.

library(format) accepts the common format/[2,3], format_//2, portray_clause/[1,2], portray_clause_//1, and listing/1 interfaces. Its portable formatter currently implements literal text, ~~, ~n, ~w, ~q, ~a, and ~d; controls for field widths and floating-point presentation are not yet part of EyeProlog’s compatibility subset. library(pio) eagerly reads or materializes a DCG character list around ISO streams. It preserves the declarative grammar interface, but unlike Scryer’s lazy list implementation it does not defer file reads.

library(tabling) accepts :- table Name/Arity. and the common start_tabling/2 and abolish_all_tables/0 predicates. Recursive user predicates are already tabled by EyeProlog’s program analysis, so the directive is a compatible declaration rather than a second tabling engine. library(time) returns a timestamp association list from the local clock; format_time//2 supports the documented year, month, day, time, month-name, weekday-name, and day-of-year specifiers.

random/1 keeps the common mutable-seed interface but uses a private native state step for hot-loop performance; its public sequence remains the same Park-Miller sequence used by the portable explicit-state random/3. The helper is internal to the normal EyeProlog registry and is not part of the ISO or public library predicate catalogs.

uuidv4/1, uuidv4_string/1, and uuid_string/2 provide the common UUID byte list and character-list interface. uuid(+Seed0,-UUID,-Seed) remains an EyeProlog extension that creates a version 4 UUID atom using pure random/3. Passing the returned seed to the next call produces the next UUID; restarting with the same integer seed reproduces the same sequence. set_random/1 controls the common stateful generator used by uuidv4/1.

On the command line, a program can state its library dependencies explicitly:

printf '%s\n' ':- use_module(library(lists)).' 'answer(X) :- member(X, [ready]).' > program.pl
eyeprolog --goal 'answer(X)' program.pl
eyeprolog -p program.pl        # add proof output

JavaScript uses the same normal EyeProlog library registry by default:

import { run } from 'eyeprolog';

const source = `
:- use_module(library(lists)).
answer(Whole) :- append([red, green], [blue], Whole).
`;

const result = run(source, { goal: 'answer(X)' });
console.log(result.stdout);

The mode notation used in the reference tables below is descriptive:

Most EyeProlog library predicates are projections or filters. When an input is unbound, malformed, outside its domain, or incompatible with the requested output, they normally fail rather than raising the ISO errors described in the errors section above. They do not invent open-ended domains. Bind arithmetic operands, source text, proper lists, indexes, dates, and aggregate generators before calling the corresponding predicate.

Portable numeric, comparison, and date relations

Predicates and principal modes Behavior
lt(+A,+B), le(+A,+B), gt(+A,+B), ge(+A,+B) Compare integers exactly, finite numeric text numerically, PnYnMnD duration text component-wise, and other lexical values by string order. These differ from ISO arithmetic comparison and standard term order.
random(-Value) Stateful Park-Miller step using the library seed set by set_random/1; implemented through a private native fast path while retaining the same sequence and numeric conversion as random/3.
random(+Seed0,-Value,-Seed) Portable Park-Miller generator with explicit state. Value is in [0,1); pass the returned integer Seed to the next call. The same initial integer seed always reproduces the same sequence.
difference(+End,+Start,-Duration) Portable Prolog. Computes a nonnegative calendar difference between ISO date atoms/character lists and returns atom 'PnYnMnD'. Invalid dates or an end before the start fail. 
:- use_module(library(dates)).
:- use_module(library(between), [between/3]).
:- use_module(library(random)).
:- use_module(library(lists)).

answer(square, S) :- (S is 12 * 12).
answer(day_count, N) :- between(3, 5, N).
answer(age, D) :- difference('2026-07-28', '2020-05-20', D).
answer(random_pair, [A,B]) :- random(42, A, S), random(S, B, _).

eyeprolog --goal 'answer(Kind, Value)' program.pl

The library deliberately does not register named arithmetic wrappers such as add/3, mul/3, abs/2, or sqrt/2, because ISO arithmetic already expresses them: for example, R is A + B, R is abs(A), and R is sqrt(A). The same applies to subtraction, multiplication, division, modulo, powers, sine, cosine, exponential, logarithm, and the ISO rounding functions.

The bundled library layer defines between/3 in library(between) and smallest_divisor_from/3 in library(primes) as ordinary Prolog clauses. Choose the smaller or larger of two arithmetic values directly with ISO control, for example (A =< B -> Min = A ; Min = B) or (A >= B -> Max = A ; Max = B).

List relations

These relations are the actual Prolog implementations in src/lib/lists.pl. Every list-consuming relation below expects a proper list unless explicitly stated otherwise. Indexes and counts are zero-based, nonnegative safe integers.

Predicate and principal mode Behavior
append(+Prefix,+Suffix,-Whole) Appends a proper prefix to any suffix, including an improper tail.
append(-Prefix,-Suffix,+Whole) Enumerates every split of a proper Whole, from empty prefix to empty suffix.
member(?Item,+List) Produces one answer per matching position, so duplicates remain observable.
select(?Item,+List,-Rest) Removes one occurrence at a time and preserves the order of all other elements. Duplicate occurrences may produce duplicate answers.
\+ member(+Item,+List) Succeeds only when Item does not unify with any member. Use it after binding the item and list.
nth0(?Index,+List,?Item) Checks a bound zero-based index or enumerates indexes and their items.
nth1(?Index,+List,?Item) Checks a bound one-based index or enumerates one-based indexes and items.
maplist(+Closure,+List1,?List2) Applies a two-argument closure pairwise through ISO call/3; partially applied compound closures are supported.
[Head|Tail] = List Decomposes a nonempty list directly with ISO unification; no library wrapper is needed.
set_nth0(+Index,+List,+Item,-NewList) Replaces one existing position without mutating the input list.
last(+List,?Last) Returns the final element of a nonempty proper list.
take(+Count,+List,-Prefix), drop(+Count,+List,-Suffix) Select the first Count elements or remove them. Counts beyond the list length fail.
slice(+Start,+Count,+List,-Slice) Selects exactly Count elements beginning at Start; an out-of-range slice fails.
reverse(+List,-Reversed) Reverses a proper list.
length(?List,?Length) Reports or checks the length of a proper list, or generates a list skeleton when Length is a bound nonnegative integer.
sum_list(+List,-Sum) Sums numeric elements with ISO is/2. The empty sum is 0; invalid arithmetic raises the corresponding ISO error.
min_list(+List,-Min), max_list(+List,-Max) Select by EyeProlog term order, not numeric coercion. Empty lists fail.
list_to_set(+List,-Set) Removes later structural duplicates while preserving first-occurrence order. 

:- use_module(library(lists)).

answer(split, pair(Prefix, Suffix)) :-
  append(Prefix, Suffix, [a, b]).

answer(second, Item) :-
  nth0(1, [a, b, c], Item).

eyeprolog --goal 'answer(Kind, Value)' program.pl

Portable text, lexical values, and pattern matching

The portable text API uses ISO atoms or proper lists of one-character atoms. A generated text result defaults to an atom. Double-quoted source text uses the ISO representation selected by double_quotes; with the default chars, it is already a proper character list accepted by this API. The 56-predicate portable library itself has no STRING or JavaScript dependency.

Predicate and principal mode Behavior
string_concat(?Left,?Right,?Text) Concatenates or splits atom/character-list text. At least two arguments must determine the operation; generated text is an atom.
contains(+Text,+Needle) Tests literal containment.
matches(+Text,+Pattern) Tests |-separated literal alternatives.
matches(+Text,+Pattern,-Context) Portable named-capture matcher. Supports literals, ^/$, named groups (?<name>...), optional named groups, \w+, [A-Za-z]+, [0-9]+, and literal group bodies. Captures are atoms in comma-context data such as (year('2026'), month('07')).
split(+Text,+Separator,-Parts) Literal split into a proper list of atoms.
join(+Parts,+Separator,-Text) Joins atom/number/character-list lexical values. The empty list produces the empty atom ''.
substring(+Text,+Start,+Count,-Part) Extracts characters using zero-based nonnegative integer indexes.
replace(+Text,+Search,+Replacement,-Result) Replaces every literal occurrence. An empty search leaves the text unchanged.
lowercase(+Text,-Lower), uppercase(+Text,-Upper) Portable ASCII case mapping. Non-ASCII characters are preserved unchanged rather than delegated to host Unicode case conversion.
trim(+Text,-Trimmed) Removes the ISO-portable ASCII whitespace set at both ends.
number_string(?Number,?Text) Historical predicate name retained for compatibility; converts a number to atom/character-list text or parses such text.
atom_string(?Atom,?Text) Historical predicate name retained for compatibility; relates an atom to atom/character-list text.
term_string(+Term,-Text) Renders a nonvariable term into atom/character-list text using the portable library serializer. It does not parse text back into a term.

The named-capture matcher deliberately implements a small, auditable Prolog subset rather than JavaScript regular-expression semantics. Use a host predicate when an application genuinely requires a full host regex engine.

:- use_module(library(strings)).
:- use_module(library(lists)).

answer(words, Words) :-
  trim('  Logic Made Visible  ', Clean),
  lowercase(Clean, Lower),
  split(Lower, ' ', Words).

answer(captures, Context) :-
  matches('Ada Lovelace',
          '^(?<first>[A-Za-z]+) (?<last>[A-Za-z]+)$',
          Context).

eyeprolog --goal 'answer(Kind, Value)' program.pl

Portable aggregation and bounded control

These Prolog relations follow the documented collection, arithmetic, term-order, and scoping contracts. The caller is responsible for making that search finite. Bind outer variables before the nested goal when they are intended to restrict its domain.

Predicate and principal mode Behavior
countall(+Goal,-Count) Counts all solutions, including solutions that produce the same visible template. The empty count is 0.
sumall(+Template,+Goal,-Sum) Sums the numeric value of Template in every solution. The empty sum is 0; invalid arithmetic raises the corresponding ISO error.
aggregate_min(+KeyTemplate,+ValueTemplate,+Goal,-BestKey,-BestValue) Retains the solution with the smallest resolved key under standard term order.
aggregate_max(+KeyTemplate,+ValueTemplate,+Goal,-BestKey,-BestValue) Retains the solution with the largest resolved key. Both best-value predicates fail on an empty solution set and retain the first solution on an equal key.

ISO findall/3 is present in both registries. The EyeProlog library aggregates follow the same scoping principle: variables created inside the nested search do not leak except through the declared templates and outputs.

There is no not/1 alias; use ISO \+/1. forall/2 is available from library(iso_ext), and once/1 is supplied directly by the ISO registry.

:- use_module(library(aggregate)).
:- use_module(library(lists)).
:- use_module(library(iso_ext)).

cost(a, 8).
cost(b, 3).
cost(c, 3).

answer(count, N) :- countall(cost(_, _), N).
answer(best(Name), Cost) :-
  aggregate_min(CandidateCost, CandidateName,
                cost(CandidateName, CandidateCost),
                Cost, Name).

eyeprolog --goal 'answer(Kind, Value)' program.pl

Contexts with ordinary terms

A comma-context needs no special native predicate. A small program relation can walk its members, and ISO =../2 can expose any member’s name and argument list.


:- use_module(library(lists)).

message(event_17,
        (severity(high), source(sensor_3), reading(temp, 91))).

context_member((Left, _right), Member) :- context_member(Left, Member).
context_member((_left, Right), Member) :- context_member(Right, Member).
context_member(Member, Member) :- Member \= (_left, _right).

context_parts(Context, Name, Args) :-
  context_member(Context, Member),
  (Member =.. [Name | Args]),
  atom(Name).

answer(field(Name, Args)) :-
  message(event_17, Context),
  context_parts(Context, Name, Args).

eyeprolog --goal 'answer(X)' program.pl

The ISO profile includes functor/3, arg/3, and =../2. Use =../2 for whole-argument-list decomposition and construction, =/2 for unification, and \=/2 for non-unifiability; redundant aliases are not registered.

Typical ISO extensions

Import library(iso_ext) when a program needs portable solution counting, universal checks, inclusive integer generation, difference-list collection, or variant comparison:

:- use_module(library(iso_ext)).

task(parse).
task(check).
task(report).

extension_answer(all_tasks_are_atoms, true) :-
  forall(task(Task), atom(Task)).

extension_answer(numbered, Pairs) :-
  findall(N-S, (cfor(1, 3, N), succ(N, S)), Pairs).

extension_answer(with_tail, Tasks) :-
  findall(Task, task(Task), Tasks, [done]).

extension_answer(same_shape, true) :-
  variant(node(X, X), node(Y, Y)).

40. Running EyeProlog: command line and corpus

The command line is an observation boundary around a theory. Keep the program fixed while selecting the evidence you need: ordinary output for answers, proof output for support, warnings for portability risks, and statistics for search behavior.

An EyeProlog source and query enter the CLI, which separates ground answers and proofs on standard output, warnings and statistics on standard error, and a process status for automation; comparison leads back to program revision.
The CLI exposes three independent channels. Compare each with the right prediction before revising the theory: answers and proofs on stdout, diagnostics on stderr, and status for the calling process.
eyeprolog
eyeprolog [options] [file-or-url.pl|- ...]

Interactive queries

Run eyeprolog without arguments to enter the interactive top level. Queries may span lines and end with a full stop, as in Scryer Prolog:

?- use_module(library(lists)).
   true.
?- member(X, [prolog, logic]).
   X = prolog
;  X = logic.
?- halt.

When another answer exists in an interactive terminal, press ;, Space, or n to ask for it immediately; no Return is needed. Return or . stops enumeration, a enumerates all remaining answers, and f advances to the next five-answer boundary (5, 10, 15, … displayed leaf answers), regardless of how many answers were stepped through individually beforehand. h displays the answer-control help. Enumeration of goal continuations is demand-driven: after an answer is found, the top level does not execute a later program branch or side effect merely to discover whether the current answer is the last one. The solver’s uniform choicepoint protocol uses explicit clause and control frames, permits a one-answer buffer only for effect-free host relations, and requires stateful or meta-control iterators to report their pending state directly. Search that can perform an effect starts only after an answer-control command asks to continue. Stopping enumeration closes any active call_cleanup/2 or setup_call_cleanup/3 protection exactly once; detecting that a choicepoint remains does not execute that next branch. If an unresolved alternative ultimately has no solution, asking for it may therefore finish with false.. In scripted non-TTY input, a new query line implicitly stops the preceding answer enumeration without consuming the new query; explicit ;, n, Space, a, or f still requests more answers. Once the top-level reader has accepted a complete query, the following line begins with two spaces to mark active execution; a third space appears when its result is ready for formatting. The answer prompt is ; with no trailing space while it waits for input; after an advance command, one space marks active search and a second marks an answer ready for formatting. While a query is actively computing, EyeProlog releases readline’s terminal signal handling: Ctrl-C therefore terminates the current EyeProlog process immediately, and on POSIX terminals Ctrl-Z suspends it in the usual shell-managed way. This remains a host top-level convention rather than an ISO/IEC 13211-1 language feature. A period-terminated query with no solutions prints false.; a solution without visible variable bindings prints true.. Answer substitutions are rendered as valid Prolog syntax under the current operator table: when a bound value would not be a valid right operand of the displayed =/2, EyeProlog adds parentheses, for example T = (a = b). rather than the invalid T = a = b.. When an answer ends in a graphic token, the top level inserts layout before its terminating full stop so the two tokens cannot merge; for example ?- X = .* . displays X = .* ., not X = .*.. Use [file]., ['file.pl']., or consult(file). to consult local source; reconsult(file). is accepted as a compatibility alias. Use halt. or halt(Status). to leave the top level. For an extensionless designation such as [file]. or consult(file)., the top level tries file.pl before the unsuffixed file. Both the shorthand and consult/1 have modern reconsult semantics: consulting the same resolved file again replaces its previous source, so clauses removed from the file do not remain active. When read/1-2 or read_term/2-3 actually reaches interactive user_input, the top level requests the next full-stop-terminated Prolog term with a |: input prompt instead of treating the terminal stream as already exhausted. The request is made at execution time, so multiple reads in one goal and reads reached through user predicates work independently. For example:

?- read(X), read(Y).
|: hello.
|: world.
   X = hello, Y = world.

Typing Ctrl-D at an empty |: prompt makes that Prolog read return end_of_file; it does not close the surrounding EyeProlog top-level loop, so a new ?- query can still be entered afterwards. The top-level prompts and this terminal EOF convention are host-interface behavior rather than part of ISO/IEC 13211-1; terms supplied to the reads are parsed by the same ISO term-input machinery as read/1-2 and read_term/2-3 on other text streams. Up and Down recall queries from the current session. Explicit eyeprolog -h displays command-line help.

Selecting goals

A Prolog source file states facts, rules, and ISO directives; the command line selects what to solve. Supply -g or --goal followed by a callable Prolog goal:

eyeprolog --goal 'ancestor(ada, Who)' examples/ancestor.pl

Repeat -g or --goal to request several result relations in one run. EyeProlog prints their ground answers in the order the goals were supplied.

For a self-running example, place the host goal in an ordinary comment:

%% goal: ancestor(ada, Who)

When no -g or --goal option is present, the CLI reads these comments from all input sources and runs them in source order. An explicit goal option overrides them. Because %% goal: is a comment rather than a Prolog directive, another ISO processor may ignore it and the program remains portable Prolog text. External goals are still preferable when a script, shell history, or API call should make the observed question explicit.

Option Meaning
-h, --help Show usage
-p, --proof Print why/2 explanations
-q, --quads Run embedded quad tests and fail if any do not hold
--iso-strict Restrict parsing and execution to ISO/IEC 13211-1:1995 + Corrigenda 1–3; reject EyeProlog language extensions, disable interop autoloading, and disable automatic tabling
--portable Enforce the conservative EyeProlog/Trealla/Scryer interoperability profile
--no-autoload Disable conservative interop predicate autoloading
-s, --stats Print final solver and memory statistics to stderr after execution
-v, --version Print the package version
-w, --warnings Print non-fatal portability warnings
-g, --goal Goal Solve a callable goal; may be repeated; overrides %% goal: comments
-- Treat following arguments as inputs

Short flags may be combined, so -pqw is equivalent to -p -q -w. --iso-strict cannot be combined with --quads, because quads and their predefined infix (?-)/2 form are an EyeProlog testing extension. Strict mode retains the Part 1 prefix (?-)/1 operator and treats -->/2 as ordinary Part 1 operator syntax; it does not perform Part 3 grammar-rule expansion or expose phrase/2-3. Part 2 module directives and EyeProlog libraries are rejected, the implementation-specific occurs_check flag is absent, and automatic tabling/recursion guards are disabled. Normal mode continues to support Parts 2–3 and EyeProlog extensions, plus conservative interop autoloading for the profile documented above.

Inputs may be local files, HTTP(S) URLs, or one - for stdin. The bare command eyeprolog starts the normal REPL; eyeprolog --iso-strict starts the strict core REPL. When options are present but no input is named, stdin is normally used, but the strict-mode-only invocation is reserved for the REPL, so write eyeprolog --iso-strict - explicitly when strict source should come from stdin. Multiple sources are parsed as one program, so facts, rules, and directives can be separated across files. A relative include/1 inside a local file resolves from that file’s directory.

For example:

eyeprolog --iso-strict --goal 'p(X)' program.pl
eyeprolog --iso-strict
printf 'p(a).\n' | eyeprolog --iso-strict --goal 'p(X)' -

A reproducible run

Work in a fixed sequence:

  1. predict the ground answers before running the program;
  2. run without observation flags and compare stdout with that prediction;
  3. add --proof when the support for an answer is the question;
  4. add --warnings when portability or negative dependencies are the question; use --portable when non-profile dependencies must fail CI;
  5. add --stats only when comparing two executions of the same semantic case.

For example:

eyeprolog --goal 'ancestor(X, Y)' examples/ancestor.pl
eyeprolog --proof --goal 'type(X, Y)' examples/socrates.pl
eyeprolog --warnings --goal 'answer(X)' test/conformance/warnings/negation/unstratified_mutual.pl
eyeprolog --portable --goal 'sudoku9_solution(S)' examples/clpz-sudoku-9x9.pl
eyeprolog --stats --goal 'path(a, X)' examples/path-discovery.pl > answers.pl 2> run.stats

Normal answers and why/2 terms go to stdout, which makes them suitable for a golden file or another EyeProlog input. Warnings and statistics go to stderr so they do not corrupt that logical stream. A successful run normally exits with status zero; loading, syntax, option, and other uncaught errors use status 1. halt/0-1 can deliberately choose the process status from inside a program.

Embedded quad tests

A quad places a query directly before a description of its expected top-level answer. The answer is ordinary Prolog syntax rather than quoted text or a comment, so a small test reads like the interaction it checks:

color(red).
color(green).

colors ?- color(X).
   X = red
;  X = green.

?- color(blue).
   false.

Run all quads in a file with eyeprolog --quads file.pl or eyeprolog -q file.pl. A label such as colors is optional. A label is not a separate mini-language: it is the ordinary first argument of (?-)/2, and therefore may be any Prolog term admitted there by the normal term grammar. Quad execution requires that argument to be ground; a non-ground label is reported as a quad failure rather than aborting source parsing. Loading the file normally only records its quads; it does not execute them or add their queries and answers as program clauses. A quad run prints a summary and exits with status 1 when any description fails. If no description fails but a bounded search cannot decide an exact answer sequence, the case is reported separately as UNDECIDED and the CLI exits with status 2. Quad mode imports library(prologue) as a compatibility prelude because the ISO Prolog working-example files use those predicates as system predicates without an explicit module directive.

Unless the source explicitly selects another unknown flag, quad execution uses unknown=error, so an undefined predicate is reported rather than being accepted as a negative answer.

Answer descriptions support ordered answers separated by ;, acceptable alternatives separated by |, true, false, standard error descriptions, and the unexpected annotation for an answer that must not occur (inattendue is its synonym). In an ordered answer sequence, unexpected is a negative assertion about the answer at that position: once the next observed answer does not match the annotated leaf, that description succeeds and does not require the query to have no further answers. Variables named in the query keep their identity inside answer descriptions; variables introduced only by a description are fresh. For example, a query throw(g(X)) is described by throw(g(_X)), while throw(g(X)), unexpected verifies that ISO throw/1 did not retain the query variable in the renamed exception term. ... and ad_infinitum accept further answers. The maybe annotation describes a successful answer that still has at least one pending residual constraint. It does not stand for an arbitrary answer and it does not weaken substitution matching: X = a, maybe still requires the X = a substitution. Conversely, a successful answer description without maybe requires that no residual constraint remain. For example, a pending dif/2 constraint can be checked as:

?- dif(X,Y), X = a.
   true, unexpected.
   X = a, unexpected.
   X = a, maybe.
   maybe, unexpected.

EyeProlog treats native variable constraints, attributed-variable residue, and delayed goals as pending residue for this purpose. Multiple indented descriptions after one query are independent checks: each re-runs the query, each is counted in the quads: summary, and a failing description does not suppress later descriptions for that query. inputs/1 supplies and checks exactly the characters consumed by the query. peeks/1 may add one character that is available for look-ahead but must remain unconsumed. The runner puts an invalid-character sentinel immediately after the declared input boundary, so a reader cannot accidentally use an artificial end-of-file to decide that a full stop terminates the term. For example:

?- read(X).
   inputs("1."), X = 1, unexpected.
   inputs("1."), peeks(" "), X = 1.
   inputs("1. "), peeks(" "), X = 1, unexpected.

outputs/1 checks characters emitted while reaching the described answer or error, including output produced before a later exception. Its argument may be an exact character list/string or a DCG body: terminal sequences, conjunction/disjunction, .../ad_infinitum sequence wildcards, and user-defined DCG nonterminals are matched against the captured characters. The waits and unordered other_answer_sequence annotations are not executed by the current runner.

STO, loops, and undecided quad results

Following Trealla’s quad convention, sto declares that a query is subject to occurs-check. EyeProlog checks this conservatively rather than attempting a complete STO/NSTO decision procedure. During the query’s ordinary execution, the finite-tree unifier records a concrete occurs-check event as positive STO evidence; the query is not run a second time merely to probe STO-ness. A finite execution that completes naturally without such an event disproves sto, while a search or resource boundary leaves the declaration conservatively unchecked. The answer portion of an sto-annotated leaf remains implementation-dependent and is therefore not compared.

For example, the cyclic binding in the first query provides positive STO evidence, whereas the second query is finite and cannot be STO:

?- X = s(X).
   X = ..., unexpected.
   false, unexpected.
   sto, false
|  sto, true.

?- true.
   sto.                  % fails: no STO evidence

When a quad declares STO and the execution observes an occurs-check event, an unannotated unexpected leaf does not reject the implementation-dependent finite-tree outcome. This is partial STO detection only: EyeProlog makes a definite statement where execution provides definite evidence and otherwise does not guess.

loops is kept distinct from merely exhausting the quad runner’s resources. EyeProlog accepts structural nontermination evidence such as an active-variant recursion cycle, with the loop depth/inference bounds as a bounded fallback. A structural cycle is also strong enough to refute a finite false description; it is not reported as undecided merely because the same query was checked by a different answer description:

inf :- inf, inf.

?- inf.
   loops.

Ordinary answer descriptions also have a finite inference budget (100000 by default). Exhausting that budget does not establish loops and does not turn an unfinished search into false; instead the description is reported as UNDECIDED, for example:

quads: UNDECIDED expensive_case, program.pl:12
   undecided: inference limit reached.

Thus quad execution has three useful outcomes: passed, failed, and undecided. When there are no failures but at least one undecided description, the CLI exits with status 2. The JavaScript API may override the ordinary search budget with quadMaxInferences; loopMaxDepth and loopMaxInferences control the explicit loops probe.

The JavaScript API exposes the same operation without process I/O:

import { Program, runQuads } from 'eyeprolog';

const program = Program.parse(source);
const report = runQuads(program);
console.log(report.passed, report.failed, report.undecided, report.stdout);

The syntax follows the “queries using answer descriptions” convention used by Trealla and the ISO Prolog working examples. Because answer descriptions are layout-sensitive, indent every description while keeping ordinary clause heads and the next quad query at the left margin. A quad label may contain any number of comma-separated metadata fields, including across layout before ?-; for example 9, "case", passes ?- Goal. is one labelled query. Quad recognition is structural after ordinary term parsing: functional, mixed, quoted-functor, and parenthesized spellings of the same ?-/1 or ?-/2 term are semantically equivalent. For example ?-(Label, Query). and (?-(Label, Query))., followed by the same indented answer descriptions, create the same labelled quad as Label ?- Query..

Statistics are comparative evidence, not a score in isolation. Preserve the program, input, runtime version, selected query, answers, and counters together. An optimization is acceptable only when the intended answers remain unchanged and the chosen resource measure improves on the relevant scale case.

The corpus as executable documentation

The files under examples/ pair readable programs with checked output under examples/output/. The conformance cases under test/conformance/ focus on language behavior, including success, failure, errors, warnings, and file loading. Use an example to learn a modeling pattern and a conformance case to settle an exact processor question. npm test checks both along with the book’s extracted programs; npm run generate refreshes those extracted examples after changing executable book blocks.

Checkpoint. Run one example with --proof --stats. Identify which bytes belong to the reusable logical result, which describe this execution, and which process status an automated caller observes. Then change one fact and predict all three channels before rerunning it.

41. Study paths, review, and further examples

For a first week, run socrates.pl and ancestor.pl, rewrite them from memory, inspect their proofs, learn member/2, append/3, and select/3, solve one finite puzzle, and add one explicit integrity query.

Course-length schedules

These schedules name a spine rather than a reading quota. Every meeting should include prediction, execution, one changed input, and a short explanation.

Meeting Six-meeting introduction Ten-meeting course Fourteen-meeting course
1 Chapters 1–2; Socrates and family facts Chapters 1–2; Laboratory 1 begins Chapters 1–2; predicates, terms, and unification
2 Chapters 3–5; recursion and lists Chapters 3–5; Laboratories 1–2 Chapters 3–4; rules, semantics, and recursion
3 Chapters 6–10; one finite puzzle Chapters 6–8; finite generation and absence Chapters 5–6; lists and arithmetic
4 Chapters 11–14 and 17–20; proof, integrity, construction Chapters 9–12; contexts, models, proofs, and integrity checks Chapters 7–8; negation and aggregation
5 Choose Chapters 21–25 or 26–30 Chapters 13–16; performance and boundaries Chapters 9–10; structured data and finite models
6 Chapters 31–33; release matrix and reflection Chapters 17–20; construction and improvement Chapters 11–12; answers, proofs, and integrity
7 — Chapters 21–25; one advanced case Chapters 13–14; termination and knowledge engineering
8 — Choose Chapters 26–30 Choose Chapters 15–16 or an alternate domain route
9 — Chapters 31–32; test and debug Chapters 17–20; construction, correctness, improvement
10 — Chapter 33; project review Chapters 21–25; advanced relational design
11 — — Chapters 26–27; witnesses and induction
12 — — Chapters 28–30; representation, experiment, limits
13 — — Chapters 31–33; test, debug, patterns
14 — — Laboratory demonstrations and rubric review

For a classroom, use checkpoints as exit questions and laboratories as multi-meeting projects. A six-meeting introduction should prefer one small, finished theory over hurried coverage of every feature.

Domain routes

Modelers should study access-control-policy.pl, clinical-trial-screening.pl, gdpr-compliance.pl, and trust-flow-provenance-threshold.pl. Identify facts, derived concepts, decisions, closed-world assumptions, and proof premises.

Algorithm students should study graph-reachability.pl, dijkstra-risk-path.pl, stable-marriage.pl, sat-solver-dpll.pl, and type-inference.pl. For each, identify the finite domain, branching relation, pruning goals, witness, and termination argument.

Mathematics students should read Chapters 3, 19, and 26–30 together, then study peano-calculus.pl, fundamental-theorem-arithmetic.pl, stirling-bell-numbers.pl, d3-group.pl, and matrix-noncommutativity.pl. For each program, distinguish definition from theorem, computation from justification, finite evidence from universal proof, and syntactic equality from the domain’s mathematical equality.

Review questions

Review questions:

  1. What distinguishes an atom constant from an atomic formula?
  2. Why can one append relation construct lists and split them?
  3. When does goal order affect performance but not declarative meaning?
  4. Why should variables usually be bound before \+/1?
  5. What does automatic tabling solve, and what does it not solve?
  6. Why is proof output useful when the answer is already known?
  7. When should a host query an invalid/1 relation before domain decisions?
  8. Why should external data conversion remain outside the reasoning core?
  9. In what sense is a ground query answer an existential witness?
  10. Why are partial correctness, completeness, and termination three different claims?
  11. When can exhaustive computation constitute a proof, and when is it only evidence?
  12. Which parts of an answer’s trust come from its proof, and which remain outside the formal theory?

Further examples

A map connects EyeProlog examples across mathematics, search, planning, policy, science, program analysis, and symbolic systems.
The corpus is a connected landscape. Every path leads from a readable source program to checked answers and, for selected examples, checked proofs.

The examples directory is the book’s executable companion. The top-level directory contains 224 self-contained runnable programs. Every source program has an exact answer file under examples/output, and 61 selected programs have a checked explanation under examples/proof. The thematic tables below link every top-level program and open the program itself rather than merely naming it.

The generated examples/book/ tree serves a different purpose: it mirrors the complete inline EyeProlog displays chapter by chapter. Those files are checked for syntax, and displays containing queries are executed, but some teaching fragments deliberately depend on neighboring facts or helpers. Use the top-level catalog below when you want a self-contained program with a golden answer; use examples/book/ when you want the exact display being discussed on a page.

For any named example, the three useful views are:

Run one program directly:

node bin/eyeprolog.js examples/ancestor.pl
node bin/eyeprolog.js --proof examples/ancestor.pl

Then compare the result with its linked golden file. A productive reading sequence is:

  1. read the query declarations and predict their ground answers;
  2. identify facts, base clauses, recursive clauses, and mode-sensitive built-ins;
  3. state one intended mode and its finiteness argument;
  4. run the program and compare with the answer golden;
  5. inspect the proof, when supplied, and mark which source clauses support the conclusion;
  6. change one fact or bound and predict the changed answer before rerunning.

Standard Prolog profile

These examples compose ISO facilities that isolated conformance cases test one mode at a time.

Program Standard facility Checked answer
CLP(B) Boolean circuit A NOT/AND/OR XOR circuit is enumerated with labeling/1, then taut/2 verifies equivalence to the XOR (#) specification. answers
CLP(B) cardinality A two-of-four review quorum combines card/2, implication, exclusive-or, labeling, and model counting. answers
CLP(B) feature model Deployment-feature dependencies are expressed as Boolean constraints, enumerated with labeling/1, and counted directly with sat_count/2. answers
CLP(B) weighted planning A bounded release plan uses implications and cardinality constraints, then weighted_maximum/3 selects the highest-value admissible feature set. answers
CLP(Z) factorial Declarative predecessor and product constraints propagate a factorial without mode-sensitive is/2. answers
CLP(Z) global constraints Compatibility tables, lexicographic and serialized schedules, global cardinality with costs, circuits, value counting, and integer comparison. answers
CLP(Z) N-queens A checked eight-queens witness using finite domains, delayed diagonal constraints, all_distinct/1, and first-fail labeling, plus a four-queens multi-solution search. answers
CLP(Z) resource allocation Resource assignment using element/3, sum/3, scalar_product/4, reification, labeling options, and domain reflection. answers
CLP(Z) Sudoku 9×9 The AI Escargot 9×9 model with finite domains, 27 all-distinct constraints, and first-fail labeling; the default golden verifies its known solution while sudoku9/1 remains the search relation. answers
Combinatorics Findall Sort Eyelet-inspired combinations example using findall/3 and ISO sort/2. answers
Floating Point Floating-point arithmetic and comparisons. answers · proof
Atomic conversion Atom splitting, character atoms, Unicode codes, and numeric parsing. answers
Control and errors call/1, once/1, cut, if-then-else, throw/1, and catch/3. answers
DCG command parser A Part 3 grammar parses token lists into application terms, generates tokens, preserves a remainder, and rejects malformed input. answers
DCG expression language A precedence-aware bidirectional grammar builds arithmetic ASTs, evaluates variable expressions, regenerates minimally parenthesized tokens, round-trips syntax, and preserves a remainder. answers
Dynamic database Initialization and ordered updates to a declared dynamic procedure. answers · proof
Grouped solutions findall/3, bagof/3, setof/3, existential qualification, and clause/2. answers
Integer arithmetic Integer quotient/remainder choices plus bit operations. answers
ISO extension pipeline audit A bounded pipeline audit composing every library(iso_ext) relation: nested counting, universal validation, successor generation, difference-list collection, and schema comparison modulo variable names. answers
ISO extensions Common control, collection, integer, and term-variant extensions from library(iso_ext). answers
Operators Custom syntax, standard term order, and operator-table inspection. answers · proof
Portable library overlap Shared Scryer/Trealla interfaces for CLP(B), ordered sets, graphs, reification, delayed goals, generated names, character conversion, matrix transposition, and explicit table syntax. answers
Reflective terms Term shape, construction, copying, variables, identity, and standard order. answers
Term I/O Text-stream lifecycle, canonical writing, reading, metadata, and end state. answers
Term Tools Term-tool builtins for inspecting, constructing, rendering, and validating structured terms. answers · proof

Read these beside Part VIII. Then use the ISO conformance cases when a program depends on the exact failure or error behavior of a particular mode.

First encounters

These programs isolate one idea at a time. Read them before the larger case studies.

Program What to notice Checked companions
Age Arithmetic comparison acts as a filter after a fact supplies the age. answers · proof
Ancestor The canonical base-plus-recursive definition computes a transitive family relation. answers · proof
Animal Several clauses form a small classification theory with inspectable reasons. answers · proof
Annotation Terms attach descriptive data while the logical relation remains ordinary. answers · proof
Backward A tiny derived fact justified by a numeric comparison in an ordinary Horn rule. answers · proof
Cat Koko Named Skolem-style witnesses standing in for the existential witnesses of the original N3 example. answers · proof
Derived rule A conclusion depends on another derived predicate rather than directly on a source fact. answers · proof
Dog A compact inheritance chain shows how intermediate concepts appear in a proof. answers · proof
Existential rule Structured Herbrand terms carry explicit generated witnesses. answers · proof
Good cobbler Multiple premises combine into a conclusion without hidden mutation or control state. answers · proof
Herbrand Semantics Herbrand terms denote themselves: distinct names and constructor applications remain distinct without extra unique-name or free-constructor axioms. answers · proof
Herbrand witnesses Functional witness terms make existential structure and syntactic identity visible in both answers and derivations. answers · proof
Reusable built-ins Arithmetic, strings, lists, and term inspection compose through ordinary variables. answers · proof
Skolem Functions Skolem functional terms in rule heads. answers
SNAF Negation as failure establishes that Alice does not hate Bob before deriving that she hates Nobody. answers · proof
Socrates A fact and one rule turn the classical syllogism into a ground derivation. answers · proof
UUID uuid/3 reproducibly creates one version 4 UUID atom from explicit random state; the example validates its canonical shape. answers
Witch Burn the witch, adapted from Eyeling’s examples/witch.n3. answers · proof

Suggested path: Socrates → Age → Ancestor → Derived rule → Reusable built-ins. At each step, say aloud what one ground instance of every predicate means.

Recursion, lists, and graph closure

These examples make termination arguments visible. Compare structural descent, visited-state search, and fixed-point tabling rather than treating all recursion as one technique.

Program What to notice Checked companions
Chart parser A finite chart represents shared parsing subproblems and recursive grammatical structure. answers · proof
Cyclic path A deliberately cyclic graph exposes repeated calls and the need for disciplined recursion. answers
Deep taxonomy: 10 A small generated hierarchy is readable by hand and establishes the benchmark shape. answers
Deep Taxonomy 100 A 100-step taxonomy chain that exercises deep recursive closure and side-label derivation. answers
Deep taxonomy: 1,000 The same logical theory tests indexing and recursive closure at a realistic depth. answers
Deep Taxonomy 10000 A 10,000-step taxonomy chain used as a large-depth tabling and closure stress test. answers
Deep taxonomy: 100,000 A stress case separates semantic simplicity from implementation scale. answers
Family cousins Several relational joins derive kinship beyond a simple transitive closure. answers
Graph reachability A visited list bounds cyclic traversal and makes explicit negative test cases finite. answers · proof
Graph Productive right-recursive transitive closure over a directed map, contrasted with an under-generating left-recursive formulation. answers
List collection findall/3, list construction, and aggregation turn a solution stream into data. answers · proof
Path discovery Witness paths, not only endpoint pairs, are constructed during a larger graph search. answers
Service Impact Practical cyclic recursion: incident impact analysis for a service dependency graph. answers

Read the three taxonomy programs as one experiment: the mathematical relation does not change as the data scale changes. Any difference in runtime belongs to control, indexing, memory, and table management.

Finite search, puzzles, and optimization

The central question for every program in this group is: what exactly is the finite search space, and which constraint removes which branches?

Program Search design Checked answer
Dijkstra Findall Sort Eyelet-inspired Dijkstra example using findall/3 and ISO sort/2. answers
Dijkstra Weighted path enumeration adapted from Eyeling dijkstra.n3. answers
DONALD + GERALD = ROBERT All ten decimal digits are assigned to ten distinct letters. Right-to-left carry propagation cuts a naive 10! search space to one solution. answers
Enigma1225 New Scientist Enigma 1225, retaining the best board in one pass with aggregate_max/5. answers
Eulerian path The state tracks remaining edges rather than merely visited vertices. answers
Four-color map A finite color assignment is filtered by adjacency constraints. answers
Hamiltonian path A witness must visit every vertex exactly once; path construction and global coverage meet. answers
Job-shop scheduling Resource and precedence constraints interact in a larger finite schedule space. answers
Knapsack optimization Candidate subsets become feasible solutions, then aggregation selects a best value. answers
Map Four Color Search Four-colour search for the European Union neighbour graph. answers
Markov Logic Network Markov Logic Network style scoring over a tiny finite domain. answers
Matrix Chain Order Matrix-chain multiplication order by automatically tabled interval dynamic programming. answers
Register allocation Interference constraints turn compiler allocation into graph coloring. answers
SEND + MORE = MONEY Digit assignments are generated under distinctness, leading-zero, and column constraints. answers
Stable marriage Preference data, matching generation, and the absence of blocking pairs define stability. answers
Weighted interval scheduling Compatibility constraints and an ordered objective select a maximum-value schedule. answers · proof
Zebra puzzle House records, adjacency relations, and clue constraints jointly determine the famous solution. answers

A useful comparative exercise is to draw the first three levels of the search tree for N-Queens, SEND + MORE = MONEY, DONALD + GERALD = ROBERT, and Knapsack. Mark whether each branching decision chooses a permutation element, assigns a digit, derives a carry-constrained digit, or includes an item. The syntax is similar; the combinatorial objects and pruning strength are different.

Planning and state transition

Planning programs represent a world state as a term, define legal transitions, and search for a sequence whose final state satisfies a goal.

Program State-space idea Checked answer
Allen Interval Calculus Allen interval relations over integer time offsets, with interval records kept as scoped data. answers
Blocks world Symbolic actions transform a compact arrangement of blocks. answers
Critical-path schedule Dependency closure and duration arithmetic derive project timing. answers
Dijkstra Risk Path Risk-adjusted route selection that combines delivery cost, accumulated risk, path length, and a trust gate. answers
Dining Philosophers Chandy-Misra dining philosophers trace adapted from Eyeling dining-philosophers.n3. answers
Drone corridor planner Route feasibility combines graph structure with domain restrictions. answers
GPS Route planning over scoped map data, accumulating actions, duration, cost, belief, and comfort. answers
Gray Code Counter Gray-code counter adapted from Eyeling gray-code-counter.n3. answers
Hanoi A recursive plan mirrors the inductive structure of moving a tower. answers · proof
Lee routing Breadth-first wave expansion reaches a destination on a grid, then reconstructs a path around rectangular obstacles using the standard list relations. answers
Microgrid dispatch Candidate operating decisions are checked against supply, demand, and engineering limits. answers
Missionaries and cannibals Numeric state constraints must hold on both banks after every crossing. answers
Monkey and bananas Actions change location, support, and possession facts until the goal becomes true. answers
Route planning Weighted edges construct candidate routes and expose the chosen path as a witness. answers
Wolf, goat, and cabbage Safety invariants reject river-bank states before they enter a valid plan. answers

Compare the witness shape: Hanoi returns an inductively constructed move list; route planning returns a graph path; Lee routing reconstructs a path from breadth-first wave layers; Blocks world and the river puzzles expose a sequence of whole states. Representation determines which plan properties are easy to check.

Mathematics as relations

These examples accompany Part VI. They range from executable definitions to finite counterexample searches. Do not call every computed result a theorem: state which domain was exhausted and which general property was proved only by the clauses.

Program Mathematical content Checked answer
Ackermann Ackermann-style fast-growing recursion benchmark adapted from Eyeling ackermann.n3. answers
Binomial Vandermonde Two finite sums compute the sides of Vandermonde’s identity. answers
Catalan convolution A classic convolution identity is evaluated over a bounded range. answers
Collatz 1000 Collatz conjecture suite translated from Eyeling’s examples/collatz-1000.n3. answers
Complex Complex numbers, adapted from Eyeling complex.n3. answers
Composition Of Injective Functions Is Injective Composition of injective functions is injective, adapted from Eyeling’s examples/composition-of-injective-functions-is-injective.n3. answers · proof
Continued Fraction Sqrt2 Convergents of sqrt(2) by automatically tabled recurrence. answers
D3 group A finite Cayley table, inverses, and subgroup closure make group laws executable. answers · proof
Diamond Property Diamond property, adapted from Eyelet’s input/diamond-property.pl. answers · proof
Easter Computus Gregorian Easter computus adapted from Eyeling’s easter.n3. answers
Equivalence Classes Overlap Implies Same Class Equivalence-class overlap example adapted from Eyeling. answers · proof
Fast exponentiation Algebraic decomposition by parity changes a linear recurrence into logarithmic-depth recursion. answers
Fibonacci A recurrence becomes an executable relation with a visibly decreasing argument. answers
Fundamental theorem of arithmetic Two factorization strategies construct normalized prime-factor witnesses and check reconstruction. answers
Goldbach Bounded search checks Goldbach decompositions for powers of two using the portable Prolog primality relation. answers
Greatest lower bound uniqueness Order-theoretic definitions support a uniqueness argument. answers · proof
Group inverse uniqueness A short derivation exposes the algebraic premises needed for uniqueness. answers · proof
Heron Theorem Heron’s theorem: area = sqrt(s(s-a)(s-b)(s-c)). answers
Integer partitions Recursive generation constructs unordered additive decompositions without permutation duplicates. answers
Law Of Cosines Law of cosines: c^2 = a^2 + b^2 - 2ab cos(C). answers
Matrix noncommutativity Two concrete products provide a counterexample to universal commutativity. answers
Modular exponentiation Intermediate reduction preserves the residue while controlling numeric growth. answers
Newton Raphson Newton-Raphson root finding, adapted from Eyelet input/newton-raphson.pl. answers
Peano arithmetic Explicit natural-number terms support arithmetic relations and structural recursion. answers
Peano calculus Addition, multiplication, and factorial follow the constructors z and s/1. answers
Peasant Peasant multiplication and exponentiation cases, adapted from Eyelet. answers
Pell equation Bounded generation searches for integer witnesses to a Diophantine equation. answers
Pi The Nilakantha series is a deterministic numeric recurrence; EyeProlog recognizes its accumulator shape and executes 10,000 terms without tabling or heap growth. answers
Prime range Bounded integer generation and divisor tests enumerate primes over an explicit finite interval. answers · proof
Quadratic Formula Quadratic formula over sample equations. answers
Riemann Hypothesis A deliberately finite audit of catalogued non-trivial zeros, illustrating the boundary between evidence and universal proof. answers
Shoelace Polygon Area Polygon area by the shoelace formula. answers
Sieve List filtering presents a different operational route to finite prime generation. answers
Stirling and Bell numbers Inclusion–exclusion and recurrence count set partitions in two related ways. answers
Takeuchi The Takeuchi function as a demanding nested-recursion benchmark. answers
Totient summatory function Divisibility, coprimality, counting, and summation compose over finite domains. answers

For a focused seminar, read Peano calculus, Fast exponentiation, D3 group, Matrix noncommutativity, and Fundamental theorem of arithmetic. They exhibit, respectively, structural induction, program improvement by algebra, finite model checking, refutation by one witness, and witness-producing number theory.

Symbolic mathematics, languages, and metaprogramming

Here terms denote syntax, formulas, expressions, or programs. The crucial discipline is to keep object language and EyeProlog metalanguage distinct.

Program What the terms represent Checked answer
SAT solver: CDCL The example extends the SAT vocabulary toward conflicts and learned information. answers
Chart parser Shared chart items prevent grammatical subproblems from being rediscovered independently. answers · proof
Context Schema Audit Schema auditing for heterogeneous context terms by decomposing members with =../2 and checking predicate arity. answers
Derived Backward Rule Derived backward rule example adapted from Eyeling derived-backward-rule.n3. answers · proof
Equality saturation Repeated rewrite closure explores equivalent symbolic forms to a fixed point. answers
Expression evaluator Arithmetic expression trees are interpreted under an explicit environment. answers · proof
Fast Fourier Transform Recursive evaluation builds a shared expression tree and treats graphic operators such as + and * as data atoms. answers
Intuitionistic Logic Kripke Intuitionistic logic emulation with a finite Kripke model. answers · proof
Knuth–Bendix completion Oriented equations and critical interactions seek a more canonical rewrite system. answers
Language A small grammar recognizes a finite relational language. answers
Linear Logic Resources Linear logic emulation with explicit consumable resources. answers · proof
Modal Logic Kripke Modal logic emulation with a finite Kripke frame. answers · proof
Partial evaluator Known inputs specialize an expression or program while unknown parts remain symbolic. answers · proof
Polynomial Structured coefficients and powers support symbolic polynomial operations. answers
Proof Contrapositive Proof by contrapositive example adapted from Eyelet input/proof-by-contrapositive.pl. answers · proof
Quine–McCluskey Boolean minimization with the Quine–McCluskey method, including essential implicants and deterministic cover selection. answers
SAT solver: DPLL Formula representation, assignment, simplification, and branching form a compact solver. answers
Symbolic derivative Differentiation rules transform expression trees without evaluating them numerically; the proof golden exposes the recursive construction. answers · proof
Turing machine Machine configuration terms and transition rules expose a classical computation model. answers

Inspect the outermost functor of every data term. In the derivative example it names an expression constructor; in the SAT examples it names logical syntax; in the Turing example it helps describe a machine configuration. None of those nested terms is automatically asserted as an EyeProlog goal.

Program analysis and verification

These programs make programs or system configurations the subject of reasoning.

Program Analysis idea Checked answer
Abstract interpretation A finite sign domain conservatively approximates many concrete executions. answers
Cache performance Configuration and workload facts derive performance classifications and reasons. answers · proof
Canary release Observations and thresholds support a deployment decision with auditable evidence. answers · proof
Network SLA Technology example: network path SLA check. answers
Observability log correlation Structured log events join across identifiers and time-related facts. answers
Pointer analysis Allocation and assignment constraints derive a points-to relation by closure. answers
Register allocation Liveness interference becomes a finite coloring problem. answers
Relational Cube Lookup Performance example: repeated multi-key relational lookups. answers
Security incident correlation Distributed observations combine into incident conclusions. answers · proof
Truth-maintenance system Justifications remain explicit when conclusions depend on defeasible information. answers
Type inference Structural unification solves type constraints for a tiny expression language. answers
Vulnerability Impact Vulnerability impact analysis over a transitive dependency graph. answers

Abstract interpretation deserves special care: an abstract warning is not the claim that every concrete execution fails. It says the abstraction cannot rule the failure out. The direction of approximation is part of the theorem.

Policies, provenance, and auditable decisions

These examples are best read in layers: source facts, normalized concepts, decisions, reasons, integrity conditions, and proof.

Program Decision domain Checked companions
Access control policy Attribute and policy facts derive permit status and reasons. answers · proof
Clinical-trial screening Inclusion and exclusion criteria produce an evidence-backed eligibility result. answers · proof
Data negotiation Offered and required data conditions derive an agreement or mismatch. answers · proof
Deontic Logic Deontic logic: obligations, prohibitions, compensations, and violations. answers · proof
GDPR compliance Purpose, basis, and processing facts support compliance conclusions. answers · proof
Illegitimate Reasoning Illegitimate reasoning detector. answers
Integrity check An explicit invalid-state relation reports contradictory input and a diagnostic status. answers · proof
Nixon Diamond Nixon diamond: two independent defaults support incompatible conclusions. answers · proof
Trust-flow provenance threshold Provenance and trust values remain premises of the derived threshold decision, including its arithmetic and comparison steps. answers · proof
Workplace compliance Training, role, and workplace conditions feed a compact compliance theory. answers

When studying a policy proof, circle every premise imported from outside the theory. The derivation validates the transition from those premises to the decision; it does not authenticate the source by itself.

This explicit separation between premises, rules, questions, alternatives, and proofs is also why Prolog is a natural human-facing layer. It is not a model of the whole brain, but its computational vocabulary is unusually close to the way people communicate deliberate reasoning: assert something, state a generalization, ask a question, consider another answer, reject an alternative, and explain why. The symbiotic KG example uses that closeness as an interface between machine proposals and human judgment rather than treating the model’s latent state as the shared source of truth.

RDF 1.2 and policy roundtrips

These programs combine generated rdf/4 source facts with ISO Prolog rules adapted from the rdf-prolog-roundtrip example corpus. Each query materializes ground RDF-shaped results that can be serialized back to RDF.

The Symbiotic Knowledge Graphs example extends the same boundary into a human/AI feedback loop. Named graphs preserve source and governance context, RDF 1.2 triple terms carry AI-proposed statements without asserting them, EyeProlog decides which claims become operational knowledge, and result_rdf/4 materializes accepted knowledge and derived decisions for conversion back to RDF.

Program Roundtrip idea Checked answer
Cross-organization data sharing Combine ODRL/DPV policy, recipient properties, safeguards, jurisdiction, and retention into permit, deny, or review decisions with obligations. answers · deck
Explainable EV-depot configuration Select a compatible charger while deriving blockers and reversible required changes from the same relational rules. answers · deck
DPV–ODRL purpose mapping Verify six correspondences between a DPV process and an ODRL policy. answers
ODRL–DPV–FPV trust flow Combine policy rules and trust scores into permit, review, and deny decisions. answers
ODRL–DPV healthcare risk ranking Detect and rank healthcare-policy risks with clauses and mitigations. answers
ODRL–DPV consumer risk ranking Score consumer-policy conflicts and return a deterministic risk ranking. answers
ODRL policy Read one purpose-constrained permission from an ODRL policy graph. answers
Advanced ODRL policy Evaluate permission, duty, constraint failure, and prohibition outcomes. answers
ODRL policy reasoning Query action relationships, rule and enforcement outcomes, conflict strategies and kinds, action/rule/policy subsumption, and three-valued WFS defaults. answers
RDF 1.2 annotated claims Rank conflicting annotated claims by confidence and source trust. answers
RDF 1.2 annotation Recover an asserted triple together with its reifier and annotations. answers
RDF 1.2 directional language Preserve language and base-direction metadata in derived labels. answers
RDF 1.2 nested triple term Match nested triple terms and derive the innermost relationship. answers
RDF 1.2 TriG graph join Join default-graph metadata with measurements from a named graph. answers
RDF 1.2 TriG named graph Derive ancestor relationships inside the source named graph. answers
RDF 1.2 TriG triple term Project a triple term while retaining its named-graph context. answers
RDF 1.2 triple term Project a triple term into an ordinary asserted relationship. answers
Operational incident response Correlate symptoms and telemetry through a service dependency graph to derive root cause, transitive impact, evidence, and a guarded failover action. answers · deck
SBOM vulnerability response Traverse transitive dependencies, apply severity and waiver policy, expose the exact vulnerable path, and derive an upgrade action. answers · deck
Scientific evidence graph Use RDF 1.2 triple terms plus study metadata to distinguish supported claims, lower-quality counterevidence, and genuinely contested conclusions. answers · deck
Symbiotic Knowledge Graphs Roundtrip a city heatwave KG through RDF 1.2 triple-term proposals, human review, explicit Prolog governance, and materialized decisions. answers · deck

Science, engineering, and numerical models

These examples make mathematical assumptions operational. Their values are illustrative models, not professional engineering or medical advice.

Program Model Checked companions
Bayes Diagnosis Bayesian diagnosis adapted from Eyeling bayes-diagnosis.n3. answers · proof
Bayes Therapy Memoize shared inference layers: the score vector, disease likelihood tails, and expected therapy success are reused by several report relations. answers
Beam deflection A mechanics equation combines load, geometry, and material parameters. answers · proof
BMI Metric and US-unit normalization, BMI classification, healthy-weight bands, and audit checks. answers
Braking Safety Worlds EYE reasoning-inspired example: braking safety in alternative worlds. answers
Buck converter design Electrical design candidates are checked against component and performance constraints. answers
Competitive enzyme kinetics A biochemical rate law becomes a numeric relational model. answers
Control system System parameters derive stability- and response-related quantities. answers
Dairy energy balance Intake and expenditure quantities are combined in an agricultural model. answers
Electrical RC filter Component values derive circuit behavior under an explicit formula. answers · proof
Epidemic policy Observations and thresholds connect a simple epidemic model to policy conclusions. answers · proof
EV Range Worlds EYE-inspired electric-vehicle range worlds. answers
Exoplanet Validation Worlds EYE reasoning-inspired example: exoplanet candidate validation worlds. answers
FFT-8 Numeric An eight-point radix-2 FFT over explicit complex pairs, showing butterflies, twiddle factors, and selected bins. answers
Field nitrogen balance Inputs, removal, and losses form a conservation-style accounting relation. answers
GD Step Certified A proof-friendly certified gradient-descent step with memoized interval bounds and explicit acceptance evidence. answers
Hamming Code Technology example: Hamming(7,4) single-bit error correction. answers
Heat Loss Engineering example: one-dimensional conductive heat loss through a wall. answers · proof
Ideal Gas Law Science example: ideal gas law. answers · proof
Least-squares regression Finite observations are summarized into a fitted linear model. answers
Orbital transfer design Candidate orbital parameters are evaluated against transfer equations. answers
Pendulum Period Science example: simple pendulum period. answers
Radioactive Decay Science example: radioactive decay. answers
Spacecraft battery diagnosis Telemetry, P = I²R, limits, and redundant sensing support diagnosis and action. answers · proof
Statistics summary Aggregates compute descriptive statistics over a finite list. answers
Superdense Coding Superdense coding using discrete quantum computing, adapted from Eyelet’s input/superdense-coding.pl. answers
Vector Similarity Vector dot product, Euclidean norm, and cosine similarity. answers

For each scientific example, write a five-column audit: quantity, unit, source, equation, and approximation. A machine-checked derivation is only as interpretable as that modeling boundary.

Large integrated cases

After the focused examples, these programs are useful for whole-program reading. Begin by drawing their predicate dependency layers.

Program Why it is a capstone Checked answer
AuroraCare A large healthcare-oriented knowledge theory combines many domain concepts and decisions. answers
Basic monadic A large generated symbolic theory stresses parsing, terms, and relational execution. answers
Delfour Delfour insight-economy case adapted from Eyeling delfour.n3. answers
Flandor A broad rule set provides practice navigating a less tutorial-shaped theory. answers
Knowledge-engineering alignment flow Source concepts, mappings, validation, and derived alignment are kept in explicit layers. answers
LLDM A larger logical model demonstrates layered derivation over substantial source data. answers
Manufacturing quality control Measurements, limits, classifications, and actions form an auditable industrial decision. answers

Do not read a capstone from the first line to the last as if it were prose. Start at the supplied goal, find its predicate heads, follow their dependencies downward, and only then inspect the source facts. This is backward slicing by hand.

Running and extending the corpus

Run all 210 normal answer goldens and the 61 selected proof goldens with:

npm run test:examples

Run the complete conformance, regression, example, and proof corpus with:

npm test

When adding an example:

  1. choose a filename that names the mathematical or domain idea;
  2. begin with comments stating the intended lesson and model boundary;
  3. keep queries finite and outputs small enough to inspect;
  4. add the exact normal output under examples/output/;
  5. add a proof golden under examples/proof/ when explanation is central;
  6. include both a positive case and a meaningful boundary or failure case;
  7. run the full corpus before treating the example as documentation.

The full set of runnable source programs is checked against exact output, and the tables in this chapter link every top-level program under examples/. The thematic tables remain the recommended reading routes; the final alphabetical table completes the index. Apply the same reading discipline to every example— sentence, mode, finite domain, answer, proof, and revision.

42. Standards, limits, and implementation boundaries

This book is the single reference for the EyeProlog implementation. Chapters 38–40 describe its supported ISO Prolog syntax, directives, execution model, built-in predicates, and command-line interface. The earlier chapters explain the reasoner, automatic tabling, proof terms, warnings, answer formatting, embedding, and explicit host data boundaries.

The executable corpus under test/conformance/ tests the JavaScript implementation. Positive programs and exact output cover arithmetic, text relations, lists, terms, atoms, variables, negation, queries, rules, and syntax. Separate corpora cover expected errors, warnings, and proofs:

npm run test:conformance
npm run test:iso-strict
npm run test:wg17
# Refresh the vendored TU Wien WG17 inventory when upstream changes:
npm run wg17:upgrade
node test/run-conformance-report.mjs

test/conformance/ISO-COMPLIANCE.md is the processor-requirement ledger for the Part 1 conformance audit. It records explicit dispositions for the tracked processor, syntax, semantic, built-in, and arithmetic requirements. test/conformance/ISO-COMPLIANCE.md maps language families to representative executable cases. test/conformance/ISO-IMPLEMENTATION-DEFINED.md is the ISO 5.4 decision index: it enumerates the Part 1 implementation-defined decisions and the implementation-specific extension families without turning draft WG17/STC proposals into the licensed baseline. ISO-TERM-SEMANTICS-MATRIX.md closes the 7.1-7.3 type/order/unification rows, ISO-PROLOG-TEXT-EXECUTION-MATRIX.md closes 7.4-7.8 preparation, database, conversion, execution, and control, and ISO-EVALUABLE-FUNCTOR-MATRIX.md closes 7.9/Clause 9 expression and arithmetic rows. The exit checklist in ISO-COMPLIANCE.md records the closure criteria and their evidence. test/conformance/WG17-SYNTAX-STATUS.md separately traces the vendored active upstream syntax cases. Reviewed cases can pin exact strict-reader outcomes, while newly upgraded cases execute directly against the upstream Codex expectation.

The syntax audit also cross-checks extension safety: each vendored WG17 case accepted by the strict Part 1 reader is executed through the normal profile and must preserve the same observable outcome. Additional normal-mode syntax may accept texts outside the strict grammar, but it may not reinterpret an accepted standard case.

The complete suite must pass before release. The file-based conformance corpus contains 802 cases, including 386 focused ISO cases derived from the success, failure, mode, and error behavior in ISO/IEC 13211-1 clauses 7 and 8, Part 2 modules, and Part 3 grammar rules. Separate exact-output suites check 210 normal examples and 61 proof examples; all extracted book programs are parsed and their declared goals are executed. The eight-case playground contract suite imports the production worker, sends real reasoning requests through its message protocol, and crawls the served module graph for missing assets, bad MIME types, and static Node-only imports. The generated conformance-report.md is the authoritative source for the current executable WG17 syntax result and file-based conformance category totals.

Generated and checked repository material

Repository artifacts have distinct roles:

Release preparation runs the complete suite and refreshes the conformance report. Keeping these details here allows the README to remain a short project landing page while this book remains the implementation reference.

Run the browser contract independently with:

npm run test:playground

Supported ISO Prolog implementation

EyeProlog executes a documented and tested ISO-oriented Prolog profile. Its strict-core target is ISO/IEC 13211-1:1995 with Technical Corrigenda 1-3. Normal mode additionally provides the documented module compatibility surface and a Part 3-oriented definite-clause-grammar implementation. The exact supported predicate indicators are listed in Chapter 39. The normal profile includes control and exceptions, term operations, arithmetic, grouped solutions, dynamic clauses, operators, atomic-term processing, flags, character conversion, streams, character/byte and term I/O, initialization, source inclusion, module compatibility forms, definite-clause grammar rules, and EyeProlog extensions.

For a Part 1 conformance boundary, --iso-strict (or API option isoStrict: true) limits the processor to ISO/IEC 13211-1:1995 plus Technical Corrigenda 1–3. Corrigendum 2 additions—including subsumes_term/2, acyclic_term/1, sort/2, keysort/2, term_variables/2, retractall/1, and call/2-8—remain part of that strict baseline. Part 2 modules, Part 3 DCG expansion/phrase/2-3, quads, EyeProlog libraries, the occurs_check flag, automatic tabling, call_cleanup/2, and setup_call_cleanup/3 are outside that Part 1 strict surface.

The strict-core audit has explicit dispositions for the Clause 5 processor obligations, Clause 6 syntax and rejection families, Clause 7 term/execution/I/O and error semantics, the 8.2-8.17 built-in families, and Clause 9 evaluable functors. The complete vendored WG17 syntax matrix is a release gate, and each strict-success WG17 observation is also checked through normal mode so syntax extensions cannot reinterpret accepted standard text. Implementation-defined choices—including the Unicode-scalar processor character set, stream details, flag defaults, floating behavior, and signed bitwise/shift semantics—are indexed in test/conformance/ISO-IMPLEMENTATION-DEFINED.md. The release-facing closure ledger is test/conformance/ISO-COMPLIANCE.md.

Notable implementation boundaries are:

Write terms explicitly, keep variables uppercase or underscore-prefixed, and quote atom names that are neither lowercase plain names nor graphic tokens. The conformance ledger and release gates verify this documented strict-core boundary. Their closure is implementation evidence, not independent ISO certification.

Security and resource use

EyeProlog has no general host-call primitive, yet an untrusted theory is still executable input. It can request enormous finite searches or construct unbounded terms. URL inputs also cross a network and trust boundary. Applications should restrict accepted sources and impose suitable input-size, time, depth, memory, and solution limits. Proof output can be larger than answer output and needs its own budget.

43. Glossary and notes for continued study

Notes and references

The book is self-contained as an EyeProlog guide. These sources provide historical and technical background for the ideas that EyeProlog adapts. They describe larger languages and theories, so they should not be read as additional EyeProlog specifications.

The aim of EyeProlog is not to make every difficult problem easy. It is to keep the theory visible while the machine searches it: facts you can inspect, rules you can discuss, answers you can test, and proofs you can carry forward as data.

Glossary

This glossary fixes the book’s vocabulary. Definitions describe EyeProlog unless a broader mathematical meaning is explicitly stated.

Aggregate. A relation that evaluates a finite nested solution space and combines its solutions, as findall/3, countall/2, sumall/3, aggregate_min/5, or aggregate_max/5 does.

Answer. A ground instance of a declared query goal produced by successful search. EyeProlog suppresses duplicate printed answers and source facts already identical to queried conclusions.

Answer set. The distinct ground answers for a query, considered without their discovery order or number of proofs.

Arity. The number of arguments of a predicate or compound term. Predicate identity includes arity: edge/2 and edge/3 are different.

Atom constant. A symbolic scalar such as alice, ready, or 'a quoted atom'. An atom constant is data; an atomic formula uses a predicate name, possibly with arguments, as a proposition.

Atomic formula. A callable proposition such as ready or parent(ada, byron).

Base case. A nonrecursive clause that gives recursion a directly solvable case.

Binding. An association between a variable and a term accumulated during unification and search.

Binding pattern. Which arguments of a call are known, unknown, or partly structured at call time. See also mode.

Body. The comma-separated goals to the right of :- in a rule. Every body goal must succeed for that rule use to succeed.

Built-in. A predicate whose relation is supplied by the host implementation rather than by source clauses. Built-ins may have restricted operational modes.

Call. A goal selected for solving, together with its current bindings.

Canonical form. A chosen representative for all values considered equivalent in a domain. Canonicalization can make some domain equality decidable by structural equality.

Clause. A fact or rule terminated by a period.

Choicepoint. A remaining search alternative that may produce another answer if the caller asks the solver to continue. Every resumable engine iterator follows the same pending-alternative protocol. A suspended iterator is conservatively a choicepoint unless it reports that no search position remains; the engine never executes an unrequested effect or program branch to look for a later successful answer.

Cleanup. A protected finalization goal installed by normal-mode call_cleanup/2 or setup_call_cleanup/3. It runs exactly once when the protected search ends, is pruned or abandoned, or unwinds through an exception.

Closed-world assumption. The decision to treat failure to derive a sufficiently scoped claim as evidence for its absence. EyeProlog’s \+/1 performs negation as failure; the modeler is responsible for justifying the scope.

Compound term. Structured data with a functor and one or more arguments, such as point(3, 4) or reason(limit, exceeded).

Conformance corpus. The executable cases defining the supported ISO Prolog profile and implementation extensions under test/conformance/.

Conjunction. Several goals joined by commas. Operationally they normally run left to right while carrying bindings forward.

Constraint. In this book, a goal that rejects candidates not satisfying a property. EyeProlog does not provide a general persistent constraint store.

Declarative reading. What ground instances of clauses mean independently of the particular order in which a solver searches.

Definite clause. A clause with exactly one positive head and a conjunction of positive body goals. The pure definite fragment has a least-Herbrand-model semantics.

Dependency graph. A graph whose vertices are predicate indicators and whose edges record calls between predicates. Recursive components are cycles in this graph.

Environment. The current collection of variable bindings during a branch of search.

Fact. A clause with no body, such as parent(ada, byron).

Failure. The absence of a solution for the selected goal along the current branch. Failure causes search to reconsider alternatives; it is not an exception and not automatically an explicit negative fact.

Finite domain. An explicitly bounded set of candidates a search can exhaust. Finiteness is a property of a call and its generators, not merely of a predicate name.

Fixed point. A stage of repeated consequence generation at which no new answers are added.

Functor. The name at the root of a compound term. In point(3,4), the functor is point and the arity is two.

Generator. A goal that produces candidate bindings, usually from facts, finite lists, or bounded numeric ranges.

Goal. An atomic formula the solver is asked to establish.

Golden file. Checked expected output stored in the repository. Normal example goldens record answers; proof goldens record explanations.

Ground. Containing no variables. EyeProlog prints only ground query answers.

Head. The atomic formula to the left of :-, or the entire formula in a fact. A successful rule use derives an instance of its head.

Herbrand base. The set of all ground atomic formulas constructible from a language’s predicate symbols and Herbrand universe.

Herbrand interpretation. A selection of ground atomic formulas treated as true over the Herbrand universe.

Herbrand universe. The set of ground terms constructible from the constants and function symbols of a program.

Indexing. Implementation machinery that narrows candidate clauses using bound arguments without changing the intended answer set.

Integrity check. An ordinary predicate whose answers identify invalid input. The host decides whether to reject, report, or inspect those answers.

Least Herbrand model. The smallest Herbrand interpretation satisfying a definite program; equivalently, the fixed point obtained by repeatedly adding supported ground consequences.

List. Either [] or a cons cell written [Head | Tail]. A proper list eventually ends in [].

Mode. An intended direction of use described by which arguments are supplied and which are produced.

Negation as failure. The operational meaning of \+ Goal: succeed when a terminating nested search finds no solution for Goal.

Operational reading. How a clause directs computation: which subgoal is selected, which bindings it needs and produces, and which alternatives it creates.

Occurs check. A unification check that prevents binding a variable to a term containing that variable. EyeProlog performs it consistently for ordinary unification as well as unify_with_occurs_check/2.

Predicate indicator. A predicate name paired with its arity, conventionally written name/arity.

Proof. A successful derivation showing which clauses, facts, and built-ins support a ground answer. A proof records success, not every failed search branch.

Proof tree. The tree of successful subgoals supporting one derivation. Unlike a search tree, it omits failed alternatives.

Proper list. A finite list whose final tail is [].

Host goal. A callable Prolog goal supplied by the CLI or embedding API to select the relation whose answers are observed.

Readiness. The binding condition under which a mode-sensitive built-in can run safely and productively.

Recursion. A predicate depending on itself directly or through other predicates.

Relation. A set of tuples described by the ground instances for which a predicate holds.

Resolution. The proof-search step that matches a goal with a clause head and replaces it with the instantiated clause body.

Rule. A clause with a head and body, written Head :- Body.

Search branch. One sequence of clause and solution choices considered by the solver.

Search tree. The tree of successful, failed, and repeated alternatives explored while seeking answers.

Source fact. A fact explicitly present in loaded input, as opposed to a derived conclusion.

Stratified negation. Negative dependencies arranged in layers so no predicate depends negatively on itself through a dependency cycle.

Substitution. A mapping from variables to terms. Applying a substitution replaces those variables consistently throughout a term or clause.

Tabling. Evaluation that shares recursive calls and accumulates their answers toward a fixed point.

Term. An atom constant, number, variable, compound term, list, or parenthesized comma term. Double-quoted notation denotes a list or atom as selected by the ISO double_quotes flag.

Termination measure. A value in a well-founded order that strictly decreases along every recursive branch in a stated mode.

Theory. The collection of source facts and rules loaded together and interpreted as claims about a domain.

Unification. Structural equation solving that finds a substitution making two terms identical, when one exists.

Variable. A clause-local placeholder beginning with uppercase or underscore. Bare _ is fresh at every occurrence.

Variant call. A call identical to another up to consistent renaming of variables. Variant recognition is important for tabling and cycle analysis.

Witness. A constructed ground term demonstrating an existential result, such as a path, assignment, factorization, schedule, or proof-relevant object.

Part X — Laboratories

44. Twelve laboratories

These laboratories turn the book into a course. Each has a deliverable, an acceptance test, and a reflection question. Complete them in order or choose a route suited to a study group.

Twelve laboratories progress from relational foundations through finite search, mathematical and symbolic methods, domain reasoning, and a release-quality reasoning service.
The laboratories enlarge one construction discipline rather than form twelve unrelated projects: state meaning, control a finite computation, preserve evidence, name the boundary, and finally integrate all four.

The estimates below assume familiarity with the listed chapters and include design, implementation, tests, and reflection. They are planning ranges, not deadlines.

Laboratories Preparation Typical scope
Laboratories 1–2 Chapters 1–5 2–4 hours each
Laboratories 3–4 Chapters 6–10 and 13 4–8 hours each
Laboratories 5–7 Chapters 19 and 26–29 4–8 hours each
Laboratories 8–10 Chapters 14, 25, and 31–33 6–12 hours each
Laboratory 11 Chapters 15–16 4–8 hours
Laboratory 12 Chapters 16, 25, and 31–33 multi-session capstone

Laboratory 1. A family theory

Build: facts for at least six people and relations for parent, sibling, grandparent, and cousin.

Requirements:

Acceptance: normal output contains the predicted ground relations; one proof for a cousin conclusion passes through named intermediate concepts.

Reflect: which conclusions depend on absence, and are those closed-world assumptions justified?

Laboratory 2. A relational list toolkit

Build: user-defined relations for membership, concatenation, reversal, and prefix.

Requirements:

Acceptance: bounded differential queries find no disagreement in either direction.

Reflect: which logically meaningful modes are operationally infinite?

Laboratory 3. A cyclic transport network

Build: a network with at least ten stations, cycles, weighted edges, and two disconnected components.

Requirements:

Acceptance: every returned witness begins and ends at the queried stations, uses known edges, and contains no repeated station.

Reflect: why can endpoint reachability table finitely while the set of arbitrary walks is infinite?

Laboratory 4. A finite puzzle

Build: encode a small Latin square, scheduling puzzle, or house puzzle.

Requirements:

Acceptance: the solver returns every intended solution and no permutation duplicate representing the same mathematical object.

Reflect: which source line contributes the greatest pruning power?

Laboratory 5. Arithmetic by construction

Build: Peano addition and multiplication, then one relation of your choice: exponentiation, comparison, division with remainder, or factorial.

Requirements:

Acceptance: the proof and program share a clearly identified base and recursive structure.

Reflect: did the representation make the induction easier or merely the computation slower?

Laboratory 6. Counterexample laboratory

Build: finite operation tables over carriers of two or three elements.

Requirements:

Acceptance: one deliberately nonassociative table is rejected with a specific triple; one valid group table passes every finite law.

Reflect: why does one counterexample settle the negative question while a thousand random confirmations do not settle the positive one?

Laboratory 7. A symbolic language

Build: a small expression language with literals, variables, addition, conditionals, and local bindings.

Requirements:

Acceptance: the transformation is idempotent over the chosen corpus and does not change evaluated results.

Reflect: where is the boundary between Prolog syntax and the object language represented by Prolog terms?

Laboratory 8. A static analyzer

Build: a sign, nullness, taint, or permission analysis for a tiny statement language.

Requirements:

Acceptance: every tested concrete behavior is covered by its abstract result; the analyzer may overapproximate but must not miss the chosen unsafe case.

Reflect: why is a warning not necessarily evidence that a concrete failure occurs?

Laboratory 9. An auditable policy

Build: an access, consent, eligibility, or compliance theory.

Requirements:

Acceptance: changing one source fact changes exactly the predicted decision and its supporting proof.

Reflect: which trust claims are established by derivation, and which require authentication outside the theory?

Laboratory 10. A scientific model

Build: encode a compact model from mechanics, circuits, chemistry, epidemiology, or statistics.

Requirements:

Acceptance: a proof for the final classification includes measurements, equations represented by built-ins, and thresholds in an intelligible order.

Reflect: what has been proved conditionally, and what empirical claim remains outside formal logic?

Laboratory 11. An input boundary

Build: start with a small external record, validate it in JavaScript, convert it to ordinary Prolog facts, and derive one new relation.

Requirements:

Acceptance: invalid records are rejected before solving, valid records map to explicit finite terms, and the checked answer has an inspectable proof.

Reflect: which claims belong to host validation and which are established by the Prolog derivation?

Laboratory 12. A release-quality reasoning service

Build: combine the preceding techniques into a small embedded service.

Requirements:

Acceptance: another person can clone the repository, run one command, and reproduce answers and proofs from the preserved inputs without oral instructions.

Reflect: if the service gives a wrong real-world decision, which of the four trust layers—source, model, engine, or derivation—would reveal the fault?

Laboratory review rubric

Evaluate each project on five independent axes:

Axis Excellent work demonstrates
Meaning every public ground relation has one stable domain sentence
Logic clauses derive the intended answers and reject counterexamples
Control supported modes terminate for a stated mathematical reason
Evidence tests, witnesses, and proofs expose why results hold
Boundary sources, assumptions, versions, limits, and host duties are named

A beautiful program is not merely short. It makes the reason for its correctness, the shape of its search, and the boundary of its trust available to the next reader.

Part XI — Review

45. Checkpoint notes and selected answers

Checkpoints are for retrieval and diagnosis, not grading by hidden wording. Attempt one before reading these notes. When a checkpoint asks about a program of your own, compare the structure of your argument rather than expecting one canonical implementation.

A program artifact is examined through five review lenses: meaning, logic, control, evidence, and boundary, followed by a cycle of prediction, execution, explanation, and revision.
Review the same artifact through five independent lenses. A failure under one lens should lead to a specific revision, not to the vague conclusion that logic programming itself is mysterious.

Foundations: Chapters 1–10

Chapter 1. parent(ada, byron) says that Ada is a parent of Byron. eyeprolog --goal 'child(X, Y)' program.pl asks for every ground child–parent pair derivable by the program. Adding parent(diego, elena). adds child(elena, diego).; it does not change the earlier three child answers.

Chapter 2. point(X, X) unifies with point(red, red) by binding X to red. It does not unify with point(red, blue) because one variable cannot be both distinct atoms. [Head | Tail] unifies with [a, b, c] using Head = a and Tail = [b, c].

Chapter 3. In adult(Person) :- age(Person, Years), Years >= 18., a ground reading is: every person with a recorded age of at least 18 is an adult. Operationally, age/2 supplies Person and Years before >=/2 checks the numeric bound. Reversing those goals asks >=/2 to inspect unbound terms.

Chapter 4. With ada → byron → clara → diego, direct ancestor answers are the three edges. Recursive answers additionally include ancestor(ada, clara), ancestor(byron, diego), and ancestor(ada, diego). A successful derivation advances along a known parent edge until a direct parent clause closes the proof.

Chapter 5. joins([a], [b, c], Whole) yields [a, b, c]. With the whole list bound, the prefix/suffix splits are:

[]          and [a, b, c]
[a]         and [b, c]
[a, b]      and [c]
[a, b, c]   and []

[a | Tail] is not yet known to be proper because Tail might never resolve to a finite chain ending in [].

Chapter 6. is/2, numeric comparisons, and the recursive arithmetic steps require their documented numeric inputs. In between(1, 10, N), an unbound N is generated from a finite interval; a bound N is checked for membership in that interval.

Chapter 7. user(User), \+ blocked(User) first selects each known user, then asks a ground absence question for that user. \+ blocked(User), user(User) first asks whether the database contains no blocked user at all. Calling either result “allowed” requires a justified, complete user and blocked-status boundary.

Chapter 8. Over an empty nested search, findall/3 produces [], countall/2 produces 0, and sumall/3 produces numeric zero. aggregate_min/5 and aggregate_max/5 fail because no candidate can supply a best key. The goal passed into the aggregate, not the aggregate’s punctuation, must establish finiteness.

Chapter 9. message/2 is asserted as an atomic formula. Its context argument is structured data. The program-defined context_member/2 relation examines members inside that term; it does not add those members as globally callable source facts.

Chapter 10. The complete coloring has six answers. Removing A \= C leaves the requirements A ≠ B and B ≠ C, producing twelve answers. The six new answers are those with equal first and third colors: red–green–red, red–blue–red, green–red–green, green–blue–green, blue–red–blue, and blue–green–blue.

Trust and construction: Chapters 11–20

Use this table to check that the checkpoint response separates concepts that are often collapsed:

Chapter A sound response distinguishes
11 ground answer, successful proof, failed search branches, and source trust
12 ordinary absence, invalid theory, process exit, and resource failure
13 structural descent, finite table growth, and unbounded term construction
14 source evidence, derived concepts, policy decisions, and integrity
15 host validation, explicit term conversion, and logical derivation
16 host validation, solver derivation, proof retention, and operational ceilings
17 ground meaning, intended mode, answer set, first answer, and proof shape
18 examples, near misses, finite generators, invariants, and presentation
19 partial correctness, completeness in a mode, and termination in that mode
20 semantic regression, observable control change, and measured improvement

A response that says only “the program works” is incomplete. It should name the claim, the mode, the evidence inspected, and the boundary that remains outside that evidence.

Advanced work: Chapters 21–33

Later checkpoints often admit several good programs. Evaluate them with five questions:

  1. Meaning: is the disputed or transformed ground relation stated clearly?
  2. Scope: are modes, finite domains, equivalence notions, and trust assumptions explicit?
  3. Observation: were answers, failures, proofs, and statistics used for the different questions they can actually answer?
  4. Preservation: if a program changed, which semantic and observable properties were expected to remain invariant?
  5. Evidence: is the result reproducible as a query, test, golden output, counterexample, proof, or preserved source snapshot?

For mathematical checkpoints, add a sixth question: does the conclusion claim only what the computation warrants? One witness proves existence; one counterexample refutes a universal claim; an exhausted finite carrier proves a property only for that model; repeated bounded confirmations do not become an unbounded theorem.

For laboratory checkpoints, leave an artifact. A useful completion is not merely a paragraph: it is a small source file, predicted output, actual output, and one sentence explaining any difference. The extracted chapter examples, top-level goldens, and npm test demonstrate that rhythm at repository scale.

Part XII — Development note

46. AI-assisted editing

GPT-5.6 was used during the development of this book to assist with chapter reorganisation, refinement of explanations, and review of examples and diagrams.

All suggestions were evaluated and directed by the author, who remains responsible for the book’s claims, choices, and any remaining errors.

This site is open source. Improve this page.