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 runs portable ISO Prolog programs and turns their facts and rules into answers and inspectable proofs. This book teaches logic programming with it: describe a world as relations, state the rules that connect them, and let unification and search find the answers.

This book is also the reference for the EyeProlog implementation. Chapters 38–40 define the supported ISO Prolog profile, every built-in and library predicate, and the command line; Chapter 41 states the standards and the limits of the implementation.

A logic program can be read in two ways: as a set of sentences that are true in a domain, and as a procedure that searches for proofs. The first reading says which answers are justified; the second says whether the machine will find them. Robert Kowalski summed this up as “algorithm = logic + control”. Most of the craft of Prolog lies in keeping the logic fixed while improving the control.

The title acknowledges a debt. Leon Sterling and Ehud Shapiro’s The Art of Prolog (1986) taught a generation to read a logic program first as a definition and only then as a computation, to build programs from small, well-understood relations, and to treat accumulators, generate-and-test, grammars, and interpreters as a craft with principles of its own. This book follows the same plan. It begins with logic programs as relations and the search that computes them (Parts I–III), turns to constructing, transforming, and applying programs (Parts IV–VII), and then covers the practical ISO language and its reference (Parts VIII–IX), ending with laboratories (Part X). Every chapter ends with exercises, and every Part closes with a historical note.

Getting started

EyeProlog requires Node.js 18 or newer. Check with:

node --version

Upgrade an older runtime through a Node version manager or the official Node.js download. Then run EyeProlog without installing it:

npx --yes eyeprolog

For a persistent command, install into a user-owned prefix and add its bin directory to your PATH in your shell startup file:

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

Do not use sudo npm install; npm’s EACCES guidance recommends a Node version manager or a user-owned prefix instead.

The first program says that Socrates is a man and that every man is mortal. From a source checkout, run it with:

node bin/eyeprolog.js examples/socrates.pl

The EyeProlog command should print:

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

The answers are themselves Prolog facts, so the output can be saved, loaded and queried like any other program. Now ask why they hold:

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

After the answers, the proof lists the program clauses as clause/3 records and one step/4 term per proved goal, naming the clause that justifies it, the variable bindings, and the subgoals it used:

step(type(socrates, mortal), rule(2), ['X' = socrates], [type(socrates, man)]).
step(type(socrates, man), fact(1), [], []).
step(holds_result(test, true), rule(3), [], [type(socrates, mortal)]).

SPEC.md specifies this format and the checks a proof checker performs on it.

If you would rather not install anything, paste the program into the browser playground. It runs the same engine and libraries as the command line; only file-system predicates and include/1 need Node.

Reading the code

The complete runnable programs live under examples/, with their outputs in examples/output/, their proofs in examples/proof/, and the results of checking those proofs in examples/check/.

Read beside a running interpreter. Before each run, predict the answer; after it, change one fact or query and explain the difference.

Where to start

Newcomers should read Parts I–III in order. Experienced Prolog programmers can start with Chapters 3, 11, 13 and 17, which show how EyeProlog adds explicit tabling, forward rules and proofs to ordinary depth-first Prolog. Parts V–VIII can be read in any order, and Part IX is reference material to consult as needed.

Contents

Chapters are numbered continuously across ten parts, from Chapter 1 to Chapter 43.

Part I — Relations

Part II — Search

Part III — Trustworthy reasoning

Part IV — The craft of logic programming

Part V — Advanced relational design

Part VI — Mathematics made executable

Part VII — The reasoning laboratory

Part VIII — Standard Prolog in practice

Part IX — Reference as practice

Part X — Laboratories

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.

1. A program is a little theory

Instead of listing the steps that compute an answer, a logic program states sentences that are true in a domain:

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

Each line is a fact. parent/2 is a relation with name parent and arity two; parent/2 and parent/3 would be different predicates.

A rule derives new sentences from old ones:

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

Ask for every child/2 pair:

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

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

Nothing was copied through named slots. EyeProlog found substitutions for Child and Parent that made the body true and applied them to the head.

The command line prints derived answers, not answers that merely repeat source facts: --goal 'parent(X, Y)' finds three solutions but prints nothing. Chapter 11 explains this output policy. It does not affect what rules can use.

Relations have no direction

A function has an input side and an output side. A relation is a set of tuples, and direction appears only when you ask a question. From the single relation parent/2 you can ask for a person’s parents, a person’s children, whether two people are related, or every known pair. The program stays the same; only the pattern of known arguments changes.

So name and shape a relation by reading one ground instance aloud:

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

Then replace one argument at a time with a question: For which Child is Ada a parent? Who is a parent of Byron? If each question is a natural use of the same sentence, the relation is well shaped. If an argument means different things in different questions, split the concept before the ambiguity spreads into later rules.

Facts are statements, not commands. Their order can affect the order of answers, but a fact never means “do this now”.

Exercises.

  1. Add grandparent/2 using two calls to parent/2. Query all grandparents, then only those of diego.
  2. Predict which answers change after adding parent(diego, elena)., then run both versions and compare.
  3. Define sibling/2 from parent/2 so that nobody is their own sibling. Which built-in from Chapter 2 does the definition need?
  4. Write child/2 and parent/2 as two independent fact tables instead of a rule. Which facts can now disagree, and why does the rule rule that out?

2. Terms, variables, and substitution

Everything in a Prolog program is a term:

Atoms begin with a lowercase letter or are quoted; variables begin with an uppercase letter or an underscore. Each bare _ is a fresh anonymous variable, while repeated occurrences of _Name or X denote the same variable. A variable is local to its clause.

Keep symbolic vocabulary as atoms (ready) and use character lists ("ready") only when text must be taken apart relationally.

Normal mode adds two conveniences that --iso-strict rejects: digit groups such as 1_000 or 0xCA_FE, and the splice notation "ab"||Tail, which means [a,b|Tail] under double_quotes(chars) and [97,98|Tail] under double_quotes(codes).

Unification

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

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

These unify with Sensor = temp and Value = 91. Functor and arity must match, and arguments are compared recursively: point(X, X) unifies with point(2, 2) but not with point(2, 3).

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.

Unification is not assignment. A variable on either side may be bound, and the result is the most general substitution: it commits to exactly what agreement requires and nothing more.

The built-in =/2 performs unification:

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 succeeds. \=/2 succeeds when two terms do not unify.

Compound terms carry domain structure directly:

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

The outer measurement(...) is a statement; the nested sample(...) is data. The syntax is the same, and position decides the role.

Exercises.

  1. Without running anything, 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 check each with =/2.
  2. Write diagonal/1, which succeeds for point(X, X), and query it with point(2, 2) and point(2, 3).
  3. Give the most general unifier of reading(S, V, unit(U)) and reading(temp, 91, unit(celsius)), then of f(X, g(X)) and f(a, Y).
  4. Represent a calendar date as a compound term and write same_month/2 for two dates. Which arguments of the term does the unification compare?

3. Rules and their two readings

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

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

Read it declaratively: a person is eligible if they have an age of at least 18 and are registered. Read it operationally: to solve the head, solve the body goals from left to right, carrying each binding into the later goals.

Both readings matter, and they answer different questions. The declarative reading says what the program means and guards against an efficient program that answers the wrong question. The operational reading says how answers are found and guards against a correct specification that searches forever. Here, age/2 must run before Years >= 18, because comparison needs a number: put a generator before a test that needs its input. (As a safe optimization, EyeProlog may run a deterministic built-in test early once its inputs are bound; that never adds answers.)

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.

Much of programming in Prolog is holding one reading steady while improving the other. Later chapters refer back to this distinction rather than repeating it.

Several clauses for the same head are alternatives:

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

Helper predicates name a concept once, which makes both the rules and their proofs easier to read:

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: the Herbrand world

The declarative reading needs a precise answer to a simple question: what does a term denote? EyeProlog uses Herbrand semantics, named after Jacques Herbrand, whose 1930 thesis made ground terms and their instances central to proof theory. Robinson’s resolution principle (1965) and the least-model semantics of van Emden and Kowalski built on that foundation. You can skip to Chapter 4 on a first reading.

The Herbrand universe contains exactly the ground terms that can be built from the program’s atoms, numbers, lists and functors: pat, 3, [red, blue], ticket(alice). A ground term denotes itself. The Herbrand base contains the ground atomic formulas over those terms, such as person(pat) or owns(alice, ticket(17)). A term is a possible argument; a formula is a claim that may be true or false.

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.

A rule stands for all its ground instances, so

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

says that for every substitution of Herbrand terms for X, Y and Z, if both body formulas are true, so is the head. Rule variables are implicitly universally quantified.

The meaning of a pure program is its least Herbrand model: the smallest set of ground formulas that contains every fact and is closed under every rule. You can build it by starting from the facts and repeatedly adding the head of any ground rule instance whose body is already true, until nothing changes. That construction defines the meaning; it does not say that EyeProlog computes it bottom-up.

Terms denote themselves

In ordinary first-order logic, alice and bob might denote the same object, and ticket(alice) and ticket(bob) might too, unless extra axioms rule it out. In the Herbrand universe they differ by construction: distinct atoms are distinct terms, and compound terms are equal only when functor, arity and arguments are equal. Unification, output and proofs therefore all share one predictable notion of identity:

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

This is a property of the notation, not a claim about the world. If robert and bob name the same person, say so with a domain relation such as same_as(robert, bob) or normalize both to one term. The runnable examples/herbrand-semantics.pl shows the distinction with its outputs and proof.

Witnesses instead of hidden objects

Variables in a query are existential: EyeProlog searches for substitutions that make the goal follow. A rule head, however, cannot introduce an anonymous new object. When a rule needs to name one, construct an explicit witness term:

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

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

The same inputs build the same witness, and different inputs build different ones. The witness is printable, queryable and visible in a proof.

The occurs check

EyeProlog performs the occurs check on every unification that binds a variable, so terms are always finite trees. This clause fails instead of building a cyclic term:

cyclic_unification :- X = wrapper(X).

(The goal sits inside a clause because a bare X = wrapper(X). in a file would be a clause for the built-in =/2, which ISO forbids.)

ISO calls such unifications subject to occurs check (STO). For diagnosis, setting the flag occurs_check to error turns a unification that fails only because of the occurs check into an error:

:- set_prolog_flag(occurs_check, error).

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

The flag accepts true (the default) and error; there is no false, because EyeProlog never builds cyclic terms. unify_with_occurs_check/2 ignores the flag and simply fails on unify_with_occurs_check(X, wrapper(X)).

Meaning is not the search strategy

EyeProlog solves goals top-down: it selects a goal, tries matching clauses in order, and backtracks. For pure Horn clauses every answer it finds belongs to the least Herbrand model, but it may fail to find a true answer if the search runs into infinite recursion. Termination is a property of the procedure, not of the meaning; Chapters 13 and 19 deal with it.

Built-ins extend the pure core. X is 2 + 3 binds X to the term 5, and \+ Goal succeeds when a finite search finds no solution for Goal. Negation adds no negative facts to the model, so negative dependencies should be stratified: every negated predicate must be fully defined in a lower layer.

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

A cycle through negation is not stratified:

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

eyeprolog --warnings reports such programs. JavaScript embedders can inspect stratifiedNegation, negationStratificationErrors, negationDependencies and per-group negationStratum, request the analysis with analyzeNegation, reject unstratified programs with strictNegation, or call program.assertStratifiedNegation().

Exercises.

  1. Read eligible/1 once as a sentence about all of its ground instances and once as a sequence of subquestions, and say which body goal first binds each variable. Then move Years >= 18 to the front and predict what happens.
  2. Write the least Herbrand model of the can_enter/1 clauses for staff(ann), visitor(bob), visitor(cy), and escorted(bob).
  3. Extend different/2 to compare pair(a, b) and pair(b, a), and explain in Herbrand terms why they denote different objects.
  4. Write a three-predicate program whose negative dependencies are stratified, then add one clause that breaks the stratification and run it with --warnings.

4. Recursion: describing reachability

An ancestor is a parent, or a parent of an ancestor:

:- table ancestor/2.

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 a question to the same question one edge farther along. To design a recursion, draw one proof, find the repeated subquestion, and make sure every path can reach a base case.

A recursive program should carry the argument you would give on paper. For ancestor/2: the base case is one parent/2 edge; each recursive call moves one vertex along the graph; and the program is finite because a finite graph has finitely many endpoint pairs. Note that progress here is not “the term gets smaller”. List recursion consumes a tail, arithmetic recursion decreases a number, graph recursion walks a finite relation. State the real reason the recursion stops.

Clause order is a control preference: trying the direct edge first finds short proofs early but does not change which pairs are ancestors. Reordering the body of the recursive clause is different. ancestor(Y, Z), parent(X, Y) means the same thing, but asks an open recursive question before choosing an edge and may never terminate.

Cycles and tabling

Real graphs have cycles, and plain depth-first recursion can revisit the same call forever. The declaration :- table p/n. makes EyeProlog record the answers of p/n calls, iterate recursive calls to a fixed point, and reuse the results. With edge(a, b), edge(b, c) and edge(c, a), the tabled query reach(a, Y) returns b, c and a and stops. Predicates without a table declaration keep ordinary Prolog control; the program decides where tabling applies.

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 relation finite. A rule that builds ever larger terms still produces infinitely many distinct calls or answers.

A relation can also build the evidence for its answer:

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

ancestor/2 and path/3 make different promises. There is at most one answer per pair of endpoints, but there can be infinitely many paths between them on a cyclic graph. Table the finite relation; bound the witness relation, for example by keeping a list of visited vertices and requiring \+ member(Next, Visited) so that only simple paths are built.

Exercises.

  1. For the family in Chapter 1, predict every ancestor/2 answer (there are six). For one indirect answer, name the clauses used and say what moves closer to a known fact at each step.
  2. Write edge/2 facts for a three-vertex cycle and query a tabled reach/2. Remove the table declaration and explain what changes.
  3. Give path/3 a visited list so that it returns only simple paths, and check that it terminates on the cyclic graph from exercise 2.
  4. State the termination argument for ancestor/2 over a finite acyclic parent/2 relation, without tabling.

5. Lists as relations

[a, b, c] abbreviates nested pairs ending in [], and [Head | Tail] exposes the first pair.

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).

Because joins/3 is a relation, one definition serves several uses: with the first two arguments bound it concatenates; with only the third bound it enumerates every way to split a list; with the first and third bound it finds the missing suffix.

Some algorithms thread 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).

Nothing is mutated; each call receives a new term.

The lists library provides the standard relations, including member/2, append/3, select/3, nth0/3, reverse/2 and length/2, alongside ISO sort/2. A partial list such as [a | Tail] is a valid term whose length is not yet known; a relation that needs a proper list may enumerate possible tails or raise an instantiation error, so bind the tail first.

Exercises.

  1. Trace joins([a], [b, c], Whole) by hand. Then bind Whole to [a, b, c], leave the first two arguments open, and predict every split.
  2. Use joins/3 to define last_item/2 and prefix_of/2 without writing any new recursion.
  3. Write length_of/2 with an accumulator in the style of reverse_acc/2, and say which argument must be bound for it to terminate.
  4. Define contains_item/2 for a list that may contain duplicates. How many answers does contains_item(a, [a, b, a]) give, and why?

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’s 1930 thesis 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 came from 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. Kowalski’s procedural interpretation of Horn clauses, worked out in Edinburgh at the same time, explained why a set of logical sentences could be run as a program. Lists then became more than containers. They represented sentences, syntax trees, proof states, and sequences of goals, and the two-clause list program condensed 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 the machine still has to find them. This Part is about the finite domains, failure, and choice that turn a field of possibilities into a computation that ends.

6. Arithmetic and finite generation

Arithmetic is the standard is/2 predicate, usually written infix:

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)).

is/2 evaluates its right side, so every variable there must already hold a number: next(X, 4) raises an instantiation error rather than finding X = 3. Comparisons are filters on values something else produced:

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

between(Low, High, Value) is the usual generator. It enumerates the integers in the range, or merely checks a bound Value:

square(N, Square) :-
  between(1, 10, N),
  (Square is N * N).
A finite generator binds a number before arithmetic computes a result and a comparison filters it.
Generate a finite candidate, compute from ready inputs, then filter the ground result.

Recurrences work only in the direction they were written for:

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

factorial(5, F) gives F = 120; factorial(N, 120) raises an error at N > 0. Record the intended mode in tests and comments.

Exercises.

  1. In square/2, which goal binds N? Swap the two body goals and run the query; explain the instantiation error.
  2. Write cube_below/2 that enumerates the cubes of the integers from 1 to a given bound.
  3. Define triangle_number(N, T) for T = 1 + 2 + ... + N by recursion, then by a closed formula with is/2, and compare them for N from 0 to 10.
  4. Explain why factorial(N, 120) cannot run backwards, and write a separate relation that finds N by bounded generation.

7. Failure, negation, and quantification

A goal fails when nothing proves it under the current bindings, and search backs up to the most recent choice. \+ Goal turns failure into a test: it succeeds exactly when Goal has no solution:

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

With user(ann), user(bob), and blocked(bob), the query allowed(U) gives allowed(ann). Swap the body goals and the query gives nothing: \+ blocked(U) with U unbound asks “is nobody blocked?”, which is false. Bind variables before you negate them.

\+ means “cannot be proved from this program”, not “is false”. Reading one as the other is the closed-world assumption: right for a complete roster or configuration, wrong for open data where a missing fact may just be unknown. There, model the state you mean, such as confirmed_absent(Item).

A receptionist checks a complete guest registry against a blocked list.
Absence is informative only inside a boundary declared complete.

Universal statements need no special predicate. “Every test in the suite passes” is “no test in the suite fails”:

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

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

Negation through recursion

Ordinary \+ should be stratified: compute a relation completely, then negate it from a higher layer. eyeprolog --warnings program.pl reports recursion through negation.

Some finite rule systems need that recursion anyway. A game position is won if there is a move to a position that is not won:

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

Plain \+ would loop here. EyeProlog’s normal mode provides tnot/1, which evaluates such cycles under the well-founded semantics. When the component is finite, function-free, and range-restricted Datalog, every atom is true, false, or undefined. In this two-position cycle neither player can force a win, and wfs_truth/2 says so:

?- wfs_truth(win(a), Truth).
   Truth = undefined.

Add move(b, c) and the cycle is broken: win(c) is false, win(b) true, win(a) false.

An undefined atom is not an answer; the query win(a) prints nothing. The goal of wfs_truth/2 must be ground, as must direct calls to tnot/1, and in WFS rules every variable in the head or under tnot/1 must occur in a positive body literal. Strict ISO mode has no tnot/1; \+/1 is unchanged.

Exercises.

  1. With user(ann), user(bob), and blocked(bob), run allowed(U), then swap the two body goals and explain why the answer disappears.
  2. Write all_tests_pass/1 for a suite in which one test has no passed/1 fact, and name the closed-world assumption the answer depends on.
  3. In the three-position game, change move(b, c) to move(c, b) and predict the truth value of each win/1 atom before running wfs_truth/2.
  4. Rewrite allowed/1 for open data, where a missing blocked/1 fact means “unknown”, using an explicit status relation.

8. Collecting and choosing answers

Sometimes the question is about all the answers at once: how many, what total, which one is best. Given edge(From, To, Cost) facts:

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

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

findall/3 collects a list, countall/2 counts solutions, and sumall/3 adds them. On an empty search they return [], 0, and 0. The inner goal is a search of its own, and it must be finite.

Counting solutions is not the same as counting things. Two derivations can yield the same value; findall/3 keeps both. When identity matters, collect the identifying term and remove duplicates with ISO sort/2. When the number of derivations matters, keep them.

Optimization keeps only the best candidate:

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

The key [Cost, Route] breaks ties deterministically by standard term order. Unlike the collectors, aggregate_min/5 and aggregate_max/5 fail when there are no candidates. That is the right behavior: “there is no route” should not be disguised as a route with an artificial cost.

Market baskets with weights flow into count, sum, minimum, and maximum results.
The same finite family of solutions can be listed, counted, summed, or compared.

Keep candidate generation (route/4) separate from choice (best_route/4). The candidates can then be listed, counted, tested, and optimized by different queries without rewriting the search.

Exercises.

  1. With no route/4 facts at all, predict the result of findall/3, countall/2, sumall/3, and aggregate_min/5 over it.
  2. Give two edge/3 facts with the same cost from one node and compare outgoing_costs/2 with the sorted set of costs.
  3. Change the key of best_route/4 so that ties are broken by the route with fewer stops before term order.
  4. Write cheapest_per_origin/2 that returns one best route for every origin. Which variable must be bound before the aggregate runs?

9. Structured data, text, and contexts

Most of the time you know the shape of a term and match it directly. Generic code that must work on any term uses the ISO inspectors:

functor(Term, Name, Arity)
arg(Index, Term, Value)
Term =.. [Name | Arguments]

arg/3 counts from 1. =.. converts between a term and a list of its name and arguments.

Text should be turned into terms as soon as it enters the program, so the rules in the middle work on structure, not strings. library(strings) works on atoms or lists of one-character atoms, and returns atoms:

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

The library also offers conversions such as number_string/2 and term_string/2, and pattern tests such as contains/2, matches/2, and matches/3 with named captures. Double-quoted source text follows the ISO double_quotes flag; there is no separate string type.

A comma term can carry a bundle of related data:

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).

hot_event(event_17) succeeds. Notice what does not happen: severity(high) never becomes a fact of the program. It stays data inside one message, and context_member/2 is an ordinary relation that walks it.

Raw text becomes structured members inside one message context, which ordinary term traversal inspects without asserting those members globally.
Normalize text into structure at the boundary; inspecting a member inside one context does not make it a fact.

Exercises.

  1. Use functor/3, arg/3, and =../2 to take reading(temp, 91) apart, and to build reading(humidity, 40) from its name and arguments.
  2. Extend normalized/2 to remove punctuation before splitting, and test it on two inputs that should normalize to the same words.
  3. Add a second message to the hot_event/1 program and query hot_event(Id). Confirm that severity(high) is still not a fact of the program.
  4. Write context_value(Context, Name, Value) for members of the form Name(Value), using context_member/2 and =../2.

10. From puzzles to models

A finite search problem has three layers: generate candidates, constrain them, and report a witness. Coloring three mutually adjacent regions:

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

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)).

Each test runs as soon as its inputs are bound: A \= B prunes before C is chosen. Moving the tests to the end gives the same answers after trying all 27 combinations; on larger problems that is the difference between instant and hopeless.

For state-transition problems, make the state and the moves explicit, and carry the states already visited:

:- 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 the search finite: no state is entered twice on one path. EyeProlog is at its best when the answer has a small witness such as a path, schedule, or proof; numerical kernels belong in the host.

Exercises.

  1. Remove (A \= C) from coloring/3 and predict the number of answers before running it. (There are twelve; account for the six new ones.)
  2. Move all three tests to the end of coloring/3 and compare the work reported by --stats with the original.
  3. Color the four regions of a map in which one region touches the other three, using color/1 and as few tests as possible.
  4. Write transition/3 facts for a two-jug water puzzle and use plan/4 to find a sequence of moves. What makes the search finite?

Historical note: control, databases, and finite failure

Early Prolog made a decisive engineering choice: clauses would be tried in textual order and subgoals selected left to right. That choice made logic executable, and it 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 by Apt, Blair, and Walker disciplined negative dependencies, and the well-founded semantics gave recursion through negation a three-valued meaning. 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 an 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 is useful when you can see what it rests on. This Part covers proofs, integrity checks, termination, and the boundary between the logic program and the system that feeds it.

11. Queries, answers, and proofs

The host supplies the goals, for example eyeprolog --goal 'child(X, Y)' program.pl. EyeProlog prints the ground answers, removes duplicates, and leaves out answers that merely repeat source facts. Answers are never added back into the program.

Add --proof (or -p) and the output also says why:

eyeprolog --proof examples/socrates.pl

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

clause(1, type(socrates, man), true).
clause(2, type(var('X'), mortal), type(var('X'), man)).
clause(3, holds_result(test, true), type(socrates, mortal)).

step(type(socrates, mortal), rule(2), ['X' = socrates], [type(socrates, man)]).
step(type(socrates, man), fact(1), [], []).
step(holds_result(test, true), rule(3), [], [type(socrates, mortal)]).

The document has three layers. First come the claims, the same answers as before. Then the clause/3 records the proof cites, numbered by position in the source file. Last, one step/4 per conclusion:

step(Conclusion, By, Bindings, Uses)

Read the first step as: type(socrates, mortal) holds by rule 2, with X bound to socrates, using the conclusion type(socrates, man). That conclusion has its own step, citing fact 1. Each use is named by its conclusion, so you can read a proof downward from the claim without joining ids.

By is rule(N) or fact(N) for a program clause, builtin for a built-in or bundled-library goal, absent for a completed \+, collected for a completed findall/3, and asserted for a clause added at run time. Because clauses are numbered by source position, assert/1 and retract/1 cannot change what a citation means.

The document is flat. A resolution proof is a tree in which the same goal may be proved twice (as in p(ok) :- q(1), q(1).), but each conclusion gets exactly one step. Proofs grow with the number of distinct conclusions, not with the shape of the search. Turning on --proof, --warnings, or --stats never changes which answers are found.

Checking a proof

A proof is valid EyeProlog input, so it can be saved and checked later:

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

The checker does not search for a proof. It re-performs each recorded step against the clause it cites: the clause must exist, and with the recorded bindings it must yield exactly this conclusion from exactly these uses. Every claim needs a step, every use must resolve, and no conclusion may rest on itself. A builtin step cites no clause, so the checker recomputes it in a program that holds only the bundled libraries, and the result must agree. So is an absent step whose goal those libraries can decide, such as \+ 1 > 3. An absence of the program’s own predicates, a collected step and an asserted step cannot be recomputed that way; they are reported as trusted boundaries. An if-then-else is recorded as the branch it took: its condition and then-goals, or \+ of its condition and its else-goals.

The report is itself a set of Prolog facts: one condition/4 for each of the seven conditions C1–C7, the counts of verified, recomputed, and trusted steps, and a verdict/1. SPEC.md specifies the format and the conditions. The proof file is read as data, never executed, so a hostile proof cannot run directives.

A run checks its own proof before printing it. If the solver found an answer that the explanation cannot reproduce, the step is recorded as unproven, the check fails, and the run reports an error instead of writing a proof that does not hold.

A proof is also a design review: detours point at overgrown helpers, and a premise hidden inside a computed value should become a fact.

A proof as a dialogue

A checked proof can also be read as an argument between two parties. In the dialogue logic of Paul Lorenzen and Kuno Lorenz, a proponent defends a claim and an opponent challenges everything that is not common ground; the claim holds when the proponent can answer every challenge. --dialogue plays each answer out that way, with the checker as the opponent:

eyeprolog --dialogue examples/dialogue/contract.pl

move(1, 1, proponent, claims(valid(c17))).
move(1, 2, opponent, why(valid(c17))).
move(1, 4, opponent, concedes(offer(c17, bob, ann))).
move(1, 7, opponent, grants(\+ minor_party(c17))).
outcome(1, valid(c17), won).
obligation(1, \+ minor_party(c17)).

The opponent asks why of every derived goal, concedes facts, verifies what it can recompute, and grants what it can only trust. A won dialogue still rests on what was granted, and says so.

An opponent can do one thing a checker cannot: bring evidence of its own.

eyeprolog --evidence examples/dialogue/evidence.pl examples/dialogue/contract.pl

move(1, 7, opponent, counters(\+ minor_party(c17), minor_party(c17), [born(ann, 2009)])).
move(1, 8, proponent, retracts(valid(c17), rule(15))).
move(1, 17, opponent, concedes(born(ann, 2009))).
outcome(1, valid(c17), won).
outcome(2, valid(c18), lost).

The absence the opponent had granted is refuted: Ann was a minor when she signed. The proponent retracts its defence and, by the formal rule of dialogue logic, may now use what the opponent asserted. It defends c17 again through Ann’s ratification at nineteen, built on the opponent’s own evidence, but has nothing left for c18. Negation as failure is the place where a closed-world proof is open to challenge, and the dialogue makes that place visible. examples/dialogical-reasoning.pl writes the same game as an ordinary program, so the moves can be read in Prolog.

Exercises.

  1. Run --proof on examples/socrates.pl and read each step/4 downward from the claim, naming the clause it cites.
  2. Save the proof as socrates.why.pl, edit the first step so that it binds 'X' to plato, and run --check-proof again. Which condition fails?
  3. Write a program in which the same goal is used twice in one body, and confirm that the proof records one step for it.
  4. Add a \+ goal to a rule and find the absent step in its proof. Why is it reported as a trusted boundary?
  5. Run --dialogue on examples/dialogue/contract.pl, then add ratified(c18, dave, 2029). to the program and run it with --evidence examples/dialogue/evidence.pl. Which moves change, and why?

12. Integrity checks as ordinary predicates

An integrity check is a relation whose answers are defects:

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

invalid_assignment(Person, Role, Other) :-
  assigned(Person, Role),
  incompatible_roles(Role, Other),
  assigned(Person, Other).

There is nothing special about these predicates. A host that needs valid input queries them first, and then decides: reject the input, report every defect, or continue in a diagnostic mode. The policy stays visible in the host instead of being buried in the rules. Nothing runs implicitly before the supplied goals.

examples/integrity-check.pl shows the pattern end to end:

eyeprolog examples/integrity-check.pl

invalid_state(stone, conflicting_colors).
status(stone, invalid(conflicting_colors)).

To write one, start from a sentence that must never be accepted — “no person holds two incompatible roles” — and turn its counterexamples into positive, finite goals. Give the relation arguments that identify the offending records, so the answer is a diagnosis rather than a bare “no”.

An explicit invalid-state query identifies conflicting engineering limits before operation.
The integrity relation reports the invalid state; the host decides whether it blocks later decisions.

Reserve integrity checks for states that must be handled before any decision is trusted. A declined application or an unreachable destination is usually a perfectly valid answer, not invalid input. Keep four outcomes apart:

false/0 keeps its ISO meaning: a built-in that always fails. Clauses for false are rejected with permission_error(modify, static_procedure). Exercises.

  1. Add probability/2 facts, one of them above 1, and query invalid_probability/2.
  2. Write an integrity relation for a person holding two incompatible roles at the same time, with arguments that identify both role records.
  3. For a loan-approval theory, give one example of each of the four outcomes: no answer, an integrity answer, a resource limit, and an error.

13. Termination, tabling, and performance

Ordinary goals, including recursive calls, use depth-first resolution unless the source explicitly declares :- table p/n. That is standard Prolog, and it has a well-known failure mode: on a cyclic graph,

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

can ask reach(a, Z) again inside its own proof, forever.

Three recursive call patterns: decreasing lists, finite tabled graph answers, and terms that grow without bound.
Termination needs an argument: a decreasing measure, or a finite space of tabled calls and answers. Ever-growing terms have neither.

A :- table reach/2. declaration changes the unit of work. Each call pattern becomes a shared subproblem; its answers are stored, and a repeated call reuses them instead of recursing again. For finite positive recursion, the table is filled round by round until nothing new appears: the least fixed point. This is the natural tool for reachability, grammars, and dependency analysis.

Tabling is never applied automatically. Undeclared predicates keep ordinary depth-first control, so the source states when fixed-point execution is part of the contract. For large finite Datalog cones rooted at a tabled predicate, the engine may compute one shared most-general table and answer bound calls from its indexes; that is an optimization of the declared table, not a change in meaning.

Tabling repairs repeated questions, not unbounded ones. A rule that builds ever-larger terms makes infinitely many distinct calls, and a table cannot help. The usual causes of nontermination are:

The fixes are the same each time: bind the query more strongly, add a finite domain, track visited states, or expose an argument that decreases.

Measuring work

--stats prints counters to standard error and leaves the answers unchanged:

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

The counters (solver calls, unifications, depth, table and wfs_fixpoint_rounds, wfs_undefined_answers, memory) measure work, not truth; compare them only across equivalent queries on one EyeProlog version.

Deeper implementation: clause indexing

Each predicate keeps indexes on scalar values in each argument position. The key includes the type, so 7, '7', and "7" stay distinct. Clauses whose indexed argument is a variable or a compound stay in a fallback set, and the candidates are merged back into source order before unification. For predicates with ten or more clauses, a call with several bound arguments may build a combined index on demand, if it pays for itself.

An index decides where to look, never whether a clause matches. Removing every index would change running time, not answers or their order.

Forward rules

EyeProlog normal mode also accepts :+ at priority 1200 as an xfx operator. A source term

Conclusion :+ Premise.

is a forward rule. When a program contains forward rules and no goal is given, the engine loads library(eyelet) and runs its closure driver: solve each premise against the current program, assert the new conjuncts of each conclusion, and repeat until a round adds nothing.

Two conclusions are special. true :+ Goal is a query; it prints each distinct instance of Goal. false :+ Goal is an integrity fuse; if Goal succeeds, EyeProlog prints fuse(Goal) and exits with status 2. Variables that appear only in a derived conclusion are existential and become sk_0, sk_1, and so on. stable(Level) waits for a closure level, and becomes(From, To) replaces state linearly without a separate dynamic/1 declaration.

The driver is Prolog, in src/lib/eyelet.pl, not a second engine written in JavaScript. From JavaScript, run() selects forward mode when no goal or goals option is given; hasForwardRules(program) and executeForwardRules(program, solver, callbacks) are available for finer control. Strict ISO mode removes the :+ operator.

Resource limits are never answers. Normal execution has no implicit depth limit; if an embedder sets maxDepth and a search exceeds it, EyeProlog raises resource_error(depth_limit) rather than quietly failing the branch.

Exercises.

  1. Classify three recursive calls: one over a shrinking list, one over a finite cyclic graph, one that builds s(s(...)) terms without bound. Which terminate without tabling, which with it, and which with neither?
  2. Run the untabled reach/2 on a two-vertex cycle under a depth limit, then add :- table reach/2. and compare the outcomes.
  3. Write a forward rule Conclusion :+ Premise that derives ancestor/2 from parent/2 facts, and run it without a goal.
  4. Compare --stats for reach(a, Z) and reach(Z, a) on the same tabled graph, and explain the difference.

14. Knowledge engineering

A battery overheats when resistive heating exceeds a limit and the measured temperature confirms it. Written as rules:

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).

Each layer is a separate predicate, so each becomes a separate step in the proof: physics (heating/2), evidence from two independent sensors (thermal_warning/1), and policy (action/2). A reviewer can dispute the threshold without touching the physics, or replace the policy without re-deriving the warning. examples/spacecraft-battery-diagnosis.pl is the complete case.

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

The same layering works for most theories:

Prefer positive concepts, negate only across a closed boundary, and keep confidence and provenance as data, not rule order.

Exercises.

  1. Which facts in the battery example can a proof not authenticate? (Hint: where do the numbers come from?)
  2. Add a cooling_failed/1 fact and a second policy rule for action/2, and check that the physics predicates did not change.
  3. Run examples/spacecraft-battery-diagnosis.pl with --proof and sort its steps into the five layers listed in this chapter.
  4. Lay out the layers for a small theory of your own: source facts, helpers, decisions, integrity relations, and outputs.

15. Explicit data boundaries

A proof shows that a conclusion follows from the clauses it was given. It cannot show that those clauses were true, that a sensor was calibrated, or that a file was authentic. That is the host’s job, and EyeProlog keeps it there: the host validates input, converts it to Prolog terms, and asks a focused goal.

Here is a host receiving one JSON temperature record:

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);

Four separate claims are being made, each with its own owner:

  1. Parse: the bytes are valid JSON (the host’s parser).
  2. Validate: the sensor is known and the temperature is in range (the adapter).
  3. Convert: those values denote exactly these Prolog terms (the adapter).
  4. Derive: the reading satisfies thermal_alert/1 (EyeProlog, with a proof).

The allow-list is what makes string interpolation safe here: the sensor name can only become one of two known atoms, and the temperature must be a finite number. General text must go through a term constructor or serializer, never straight into source. The resource options cap the work an untrusted input can cause.

Exercises.

  1. For one record your application receives, write down what the host validates, the term it builds, the goal it asks, and the limit that bounds the work.
  2. Change allowedSensors so that a sensor name could contain a quote, and explain why string interpolation is then unsafe.
  3. Extend the host to accept a list of readings and ask one goal per reading. Which of the four claims gains a new owner?

16. Embedding EyeProlog

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

import { run } from 'eyeprolog';

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

The first line prints answer(ok). and a newline; the second prints the work counters for this run.

run() accepts source text or an already parsed Program. Its options include proof (aliases why and explain), proofDetail (abstract or expanded), maxDepth, maxInferences, maxMemoryBytes, solutionLimit, a custom registry, and strictNegation or analyzeNegation. It returns stdout, the numeric stats, and a nullable haltCode, and never writes to the process streams.

When run receives an already parsed Program, bundled-library imports needed only by its goals are added before solving, as they are when source text is parsed. The autoload index covers every exported predicate in the bundled src/lib/ modules. Pass autoload: false to keep only explicitly imported predicates.

Proof certificates

Applications that exchange proofs separately from answers can use proofCertificate, proofCertificatesFromText, and verifyProof:

import {
  Program, parseGoalText,
  proofCertificate, proofCertificatesFromText, verifyProof
} from 'eyeprolog';

const program = Program.parse(`
p(a).
q(X) :- p(X).
`, { sourceMetadata: true });

const made = proofCertificate(program, parseGoalText('q(a)'));
console.log(verifyProof(program, made).ok); // true

const received = proofCertificatesFromText(made.text, program)[0];
console.log(verifyProof(program, received).ok); // true

proofCertificate returns both the proof text and a JSON-serializable certificate. verifyProof walks the certificate instead of searching again; its trusted array lists every built-in or library boundary it assumed. With proofDetail: 'expanded', bundled-library clauses appear in the certificate, so the remaining trust shrinks to the built-ins those clauses use.

Programs and solvers

To inspect or prepare a theory before running it, use Program and Solver directly:

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

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
});

Programs report stratification through stratifiedNegation, negationStratificationErrors, and assertStratifiedNegation().

The limits are safety ceilings, not logic. Reaching the depth, inference, or solution limit may cut a search short; it never proves that no further answer exists, so report it as an incomplete computation. At the Solver boundary solutionLimit is opt-in: without it, re-executable goals such as repeat/0 and relations such as call_nth/2 are never turned into failure by an internal threshold.

Memory is guarded separately. EyeProlog periodically checks JavaScript heap use and keeps a quarter of the host heap ceiling in reserve, so it can unwind and raise resource_error(memory) before the host aborts. Under --max-old-space-size, the guard compares against V8’s old-generation spaces, so short-lived allocations do not trigger it. maxMemoryBytes overrides the derived ceiling; Infinity disables the check. V8 capacity errors such as Map maximum size exceeded are also reported as resource_error(memory). ISO leaves the resource name implementation dependent; EyeProlog uses memory for a finite host ceiling and reserves finite_memory for computations that no finite amount of memory could finish. After a memory error the same solver can run later queries, but the exhausted query is not resumed.

Treat remote source as executable logic. EyeProlog has no arbitrary host-call primitive, but search alone can consume CPU and memory, so set depth, solution, input-size, and time limits.

Deeper implementation: execution details

These details affect speed and memory, never answers.

Variable order. ISO 13211-1 section 7.2.1 leaves the order of two distinct variables implementation dependent and requires it to stay constant only while one sorted list is built. EyeProlog ranks variables locally for each comparison, and sort/2, keysort/2, and the sort inside setof/3 share one ranking for the duration of that operation. No global variable ordinal exists.

Active-call frames. The iterative solver keeps active-call frames only where cut scope or recursive variant guards need them, so cut-free library helpers do not copy a growing frame sequence at every step.

Compact lists. In the normal registry, the bundled length/2 counts or builds named lists without recursive interpreter frames, and does not materialize an anonymous list at all. A new fixed-length list starts as a lazy compact skeleton that expands one ./2 cell at a time when something inspects it. It is a storage optimization, not a different kind of term. Embedders that inspect the JavaScript term model can recognize it with CompactListTerm, isCompactList, and compactListLength, or build one with compactVariableList. length/2 still reserves memory headroom in proportion to the list, so a heap limit is raised inside its search as a catchable resource_error(memory).

Fresh variables. A variable that first appears in a direct =/2 goal, or a singleton head variable, cannot already occur in the value it receives, so EyeProlog skips the occurs traversal for that binding only. X = f(X), a variable seen earlier in the clause, and unify_with_occurs_check/2 keep the full check. Such a first-use equality also acts as an ordering barrier for deterministic-goal scheduling. This recovers much of the classic WAM “local variable” optimization for DCG tails without a WAM stack layout.

Grammars. phrase/2 passes its final remainder [] straight into the expanded grammar. phrase/3 keeps a private output variable and unifies its third argument last, which keeps it steadfast. The ordinary length/2 clauses remain the definition used by the ISO-only registry and whenever delays or finite-domain constraints need their wake-up points.

Implementation boundary

The JavaScript runtime is flat under src/:

src/ARCHITECTURE.md records the layering rules, and a regression test rejects JavaScript import cycles.

The CLI, the JavaScript API, Solver, proof checking, and the playground share one parser, term representation, solver, stream layer, module loader, and proof machinery. A library joins a Program only through use_module/1 or use_module/2 (or autoloading); exported predicates are imported and private ones stay module-local. getStrictIsoRegistry() with isoStrict: true selects the strict Part 1 + Corrigenda surface.

Extending the built-in registry

An embedder can add a host relation to the default registry. A handler is a generator over environments: clone, bind, and yield only the environments in which the call succeeds.

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)' });

Mark a built-in deterministic only if it yields at most one environment. An unmarked iterator is treated as a possible further choice, and the solver never resumes it just to find out. An iterator that knows its remaining positions can provide hasPendingAlternatives(), updated before each yield, so its choice point is dropped as soon as nothing is left. Mode-sensitive extensions can also supply ready, fallbackWhenNotReady, and shouldUse metadata, which affect dispatch and early filtering and are therefore part of the extension’s contract. Exercises.

  1. Run the run() example and print result.stats. Then set solutionLimit: 1 on a goal with several answers and explain why the limit is not a proof of absence.
  2. Use proofCertificate and verifyProof on q(a), then edit the program so that p(a) is missing and verify the old certificate again.
  3. Add a host relation host_time/1 to the registry with createEyePrologRegistry(), and decide whether it may be marked deterministic.

Historical note: from answers to accountable inference

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

In parallel, deductive databases asked where facts come from and how derived claims keep their provenance. The lesson is architectural. A proof procedure can attest that a conclusion follows from the supplied clauses. It cannot authenticate a database, calibrate a sensor, or authorize a request. Systems became more trustworthy when those boundaries were named rather than left 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.

Good programs are rarely typed top to bottom. They are found through examples, held in shape by invariants, and improved without losing the relation they express. This part is about those habits.

17. Logic and control

Two clauses, two readings:

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

As logic, every edge is a path, and an edge followed by a path is a path. As control, the solver tries a direct edge first, then picks an outgoing edge and continues from its endpoint. Kowalski’s 1979 slogan “algorithm = logic + control” names the split: the logic fixes which answers are admissible, the control decides which are explored, in what order, at what cost. Ideally you can improve the second without touching the first. In practice, modeful built-ins and incomplete search mean you reason about both.

So write the sentence first:

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

That sentence does not mention clause order, and it is what examples and counterexamples are judged against. Only then ask the procedural questions: which argument is usually known, which goal generates a finite set, and which recursive call is smaller or already tabled.

Same meaning, different computation

Conjunction is commutative in logic, not in search. These two rules mean the same thing:

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

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

The first works with Person unbound: person/1 and age/2 bind values before >=/2 compares them. The second reaches >=/2 with Age unbound and raises instantiation_error. Logical equivalence does not give equivalent behaviour once built-ins have modes.

Recursion that calls itself before consuming anything is the classic control bug:

% 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

append(Prefix, Suffix, Whole) has one meaning and several useful calling patterns. With the first two arguments known it concatenates; with Whole known it enumerates the finitely many splits. With all three free it is useless as a generator, because there are infinitely many lists. Note the intended modes next to a predicate — append(+,+,-), append(-,-,+) — as documentation; the marks are not Prolog syntax. A rule that calls a helper outside its promised mode can stay logically plausible while becoming operationally useless.

Proof trees and search trees

A proof tree holds only the successful choices behind one answer. A search tree also holds every failed alternative and repeated attempt. --proof shows the first; --stats hints at the second. That is why a tiny proof can hide a large search, and why removing a dead branch can make a program much faster without changing its proof at all.

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.

When a program is slow, sketch the first few levels of its search tree: the selected goal, the clauses that match it, the bindings each produces, and the calls that repeat. The sketch usually shows a generator that is too broad or a test placed too late.

Exercises.

  1. Swap two body goals in a rule of your own. Before running it, predict whether the answer set, termination, first answer, or proof shape changes.
  2. Run both adult/1 clauses with Person unbound and explain the difference.
  3. Rewrite bad_member/2 so that it terminates, and state the measure that decreases.
  4. Write the intended modes of append/3 that terminate, and give one call that does not.

18. Constructing a program

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 a ground sentence

Parcels must be routed through compatible hubs. Start without variables:

routeable(parcel_7, hub_north).

What does it claim — that the parcel can enter the hub, leave it, or complete a route through it? An ambiguous ground sentence makes every rule built on it ambiguous. Once the meaning is fixed, name the evidence:

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

The shared variables are the joins already present in the English. A repeated variable asserts identity; a variable that appears only “in case it is needed later” asserts nothing and should go.

Examples before recursion

For a recursive relation, write the smallest positive case, the next one, and a near miss:

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

The empty case is the base clause. Comparing the second with a smaller one suggests stripping a matching head from both lists:

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

That is the general method: find something that shrinks, keep the invariant while shrinking it, and state the case where nothing needs to shrink.

Generate, then test

Finite combinatorial programs read better when generating and testing are separate:

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

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

candidate_pair/2 makes the closed domain visible and guarantees that \= and \+ see bound arguments. Proofs then say whether a step generated or rejected a choice. The final clause may interleave the tests with the generators for speed; the conceptual split survives.

Representations follow the questions

A graph can be edge/2 facts, a list of edge terms, or part of a state term. Facts suit indexed lookup and proof provenance; a list suits a private, changing graph passed through recursion; a compound state term suits transitions that replace several components at once. Whatever you choose, do not pack structure into strings and re-parse it throughout the theory. Parse once at the boundary: address(City, PostalCode) can be unified, inspected, and explained.

Grow in layers

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

Point negation down this stack, at a complete lower layer. Cycles among positive concepts can be tabled; a cycle through negation usually means a concept has no stable meaning yet. Add one representative query per layer as you go, so a silent failure in normalization shows up before the final decision predicate does.

Exercises.

  1. For a domain of your own, write three positive ground examples, one near miss, and the intended query mode before writing any rule.
  2. Write suffix/2 from examples, as prefix/2 was written, starting with the smallest positive case.
  3. Split a rule of your own into generate and test parts, as in compatible_pair/2, and compare the proofs.
  4. Choose a representation for a timetable and justify it by the questions it must answer.

19. Correctness and termination

Overlapping circles for partial correctness, completeness, and termination meet at a dependable operational contract.
Partial correctness, completeness, and termination are independent promises; a dependable intended call needs all three.

Tests sample a relation; an argument covers it. Ask three separate questions:

  1. Partial correctness: is every returned answer justified?
  2. Completeness: for intended calls, is every required answer found?
  3. Termination: do intended calls finish?

For prefix/2, both of the first two follow by induction. The base clause returns only the empty prefix; the recursive clause adds the same head to a smaller valid prefix, so the result is still a prefix. Conversely, every nonempty prefix shares its first element with the list, and removing it leaves a smaller prefix problem that the recursive clause covers. That is usually enough: justify each base clause, assume the recursive calls are right, and show each recursive clause preserves the property.

Termination needs its own measure

Name a quantity that strictly decreases before each recursive call in the intended mode and cannot decrease forever: list length, a nonnegative integer, unvisited states, tree size. For factorial it is N:

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

Move the subtraction after the recursive call and the equation still holds, but the measure is gone.

Tabled graph recursion terminates differently. Nothing need shrink at each edge; termination comes from a finite number of distinct calls and answers. Tabling cannot rescue a rule that builds s(s(s(...))) without bound.

Negation and aggregation need bounded subsearch

\+ Goal and aggregates must settle a nested search before answering. Before writing \+ disqualified(Person), make sure Person is bound and disqualified/1 finishes for it. Before collecting routes, decide which finite family you mean: simple routes, routes under a cost, and so on.

Integrity is not failure

Failure says one attempted proof did not work. An integrity relation returns the evidence that the input itself is wrong:

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

A failed eligibility query may be a legitimate “no”. A successful invalid_limits/3 query means the host should stop deciding until the data is repaired.

Exercises.

  1. For one recursive relation of your own, state its invariant and its termination measure in one sentence each.
  2. Prove by induction that prefix/2 returns only prefixes, then that it finds every prefix of a proper list.
  3. Move the subtraction in factorial/2 after the recursive call and show which of the three claims fails.
  4. Write an integrity relation in the style of invalid_limits/3 for a range whose lower bound exceeds its upper bound.

20. Improving a program

Improvement starts with observation: keep representative answers and proofs, collect --stats, and change one thing at a time.

Ask a better question first

The cheapest optimization is a more specific call. Ask route(brussels, Destination) instead of an open enumeration when the origin is known. Put selective relations early so they bind arguments for later goals. Don’t build a witness when the caller needs only existence:

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

This may enumerate many distinct paths to establish one fact. A tabled reachability relation records the pair itself; keep the path-producing relation for callers that actually need a path.

Name invariants with helpers

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

The helper puts a domain statement into every proof that uses it and gives the limit policy one home. Prefer helpers that add vocabulary; step2/3 adds none.

Hoist invariant work

If every recursive step recomputes the same value, compute it once and pass it in:

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

The helper’s arguments then show exactly which values change from step to step.

Check that the meaning survived

After reordering goals or specializing a predicate, rerun positive examples, expected failures, boundary values, cyclic data, and duplicate derivations, and compare proof premises, not just printed conclusions. A change that alters which proof is found first also changes once/1, tie-breaking aggregates, and explanations, even when the answer set is identical. If callers depend on those, they are part of the contract.

Finally, resist generality nobody needs. A predicate that supports three modes can be harder to terminate, explain, and index than two simple predicates with clear contracts. Generalize when the second real use appears.

Exercises.

  1. Make exactly one control change to a program and classify each difference in answers, proofs, and --stats as intended, harmless but observable, or a regression.
  2. Replace connected/2 by a tabled reachability relation and compare the number of answers and the work on a graph with many paths.
  3. Find a predicate of your own named like step2/3 and replace it with a helper that adds vocabulary, as within_thermal_limits/1 does.
  4. Hoist one invariant computation out of a recursion, then check that the answers and the first proof are unchanged.

Historical note: logic plus control

Kowalski’s 1979 formulation “algorithm = logic + control” gave a durable name to the dual reading developed in this Part. The logic component states what is known; 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 fixed, and that programs are easier to reason about when the two are kept apart.

The craft tradition of Prolog grew around this tension. Goal ordering, accumulators, generate-and-test, and changes of representation were never mere 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. Later work on the verification of logic programs, collected in Apt’s From Logic Programming to Prolog (1997), gave the same intuition a formal footing: partial correctness, completeness, and termination are separate obligations, each with its own proof method.

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.

This part works with whole computations: tracing a search, treating languages and evaluators as relations, transforming correct programs, and building a decision service whose conclusions can be audited.

21. Reading the computation

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

The query branches two ways. An or step chooses between the two clauses; an and step requires every goal in the chosen body. The first clause asks parent(ada, Who) and yields byron. The second asks parent(ada, Y), binds Y = byron, and leaves ancestor(byron, Who) — the same choice one generation down. The three answers sit at 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)
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.

Bindings flow forward

A binding is not a local return value. Once a goal binds a variable, every later occurrence sees the same term:

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

After parent(ada, Y) binds Y = byron, the second goal is the selective parent(byron, Z). A repeated variable in a head or goal is an equality built into the pattern:

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

This does not fetch an arbitrary edge and compare its endpoints afterwards; it only matches edges whose endpoints already unify.

Failure rewinds choices, not facts

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

If verified(Person) fails, the current combination of bindings is rejected and search resumes at the latest open choice — another age/2 fact, another applicant. Nothing in the program is retracted, and answers already printed stay printed. Backtracking explores alternatives; it does not undo the world.

Variants and tables

path(a, X) and path(a, Y) differ only in variable names; they are variants and pose the same question. Tabling shares their answers and stops a cycle from re-asking forever. It cannot help when every call is new:

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

grows(A), grows(wrapper(A)), grows(wrapper(wrapper(A))) are distinct calls, and remembering them does not make them finitely many.

Tracing by hand

When a query surprises you, write down for each step the selected goal, its current arguments, the matching clause, the unifier, the new body goals, and where failure would return. Compare with --proof for one successful answer and --stats for the total work. Neither is a full trace, but together they usually locate the problem.

Exercises.

  1. Draw the and–or tree for ancestor(byron, Who). Then add a second parent of clara and mark where the tree gains a branch.
  2. For eligible/1, keep a binding ledger for an applicant whose verified/1 fact is missing, and name the choice that search resumes from.
  3. Write a cyclic edge/2 graph, table path/2, and compare its answers with the table counters reported by --stats.
  4. Write a recursive rule whose call grows a term on every step, like grows/1, and explain why tabling cannot make it finite.

22. Trees, languages, and symbolic evaluation

Compound terms are finite trees: the functor labels a node, the arguments are its children. Lists are one tree encoding; syntax, plans, formulas, and circuits can be represented just as directly.

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

A structural relation follows the shape:

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 also fix a search order — root, left, right. For membership the order is invisible; under 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.

Relating two trees

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

Called forward, mirror/2 builds a mirror; with both trees ground, it checks one. Nothing is mutated; the rule relates two persistent terms. Its correctness argument is structural induction: the empty tree is its own mirror, and if both recursive calls are right, so is the rebuilt node.

A definite clause grammar

Grammar rules (ISO/IEC TS 13211-3) describe sequences; the processor adds the two list arguments that thread the input through:

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

sentence//0 expands to an ordinary sentence/2: input before, suffix after. noun_phrase//0 hands its leftover input to verb_phrase//0. phrase/2 demands that everything is consumed; phrase/3 returns the rest. A grammar is also a search program, so a recursive grammar called with unbound Words can generate sentences without end. It needs the same mode and termination thinking as any other recursion.

An evaluator

Keep the expression separate from 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, and the proof follows the syntax tree: two literal evaluations support a multiplication, which supports the addition. Variables need an environment, passed explicitly as data rather than held in global state:

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

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

List order decides shadowing; say so in the contract of lookup/3.

Rewriting

Evaluation collapses syntax into a value. Rewriting keeps syntax and replaces one form with an equivalent one:

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 give several answers — useful for exploring equivalent forms, but a normalizer needs a strategy and a measure. Add the reverse of the first rule, expanding X into add(X, number(0)), and rewriting never stops.

Exercises.

  1. Define tree_size/2 and tree_height/2 for the tree/3 representation.
  2. Add adjectives to the sentence grammar and subtraction to evaluate/2.
  3. Extend simplify/2 with constant folding for add(number(A), number(B)), and give a measure showing that repeated simplification terminates.
  4. Prove by structural induction that applying mirror/2 twice returns the original tree.

23. Transforming programs

A transformation rewrites clauses while trying to keep the relation. The real question is not whether the new version runs but for which calls it preserves answers, termination, answer order, and explanations. Four transformations recur: unfolding replaces a call by the bodies of its clauses; folding names a repeated conjunction; specialization fixes known arguments; an accumulator carries a partial result through recursion.

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

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

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

Unfolding adult_age/1 gives:

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

The answers are unchanged, but the proof has lost the concept adult_age/1 — a real loss in an auditable policy. A helper with several clauses unfolds into several caller clauses; a recursive one may unfold forever.

Folding goes the other way. Two rules repeat a condition:

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 it:

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 gain is not three lines saved. The closed-world assumption behind \+ suspended(Person) now has one place to be stated and tested.

Specialization

A rail planner over a general connection(Mode, From, To, Cost) relation can define:

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

The wrapper states a stronger contract and gives indexing a bound first argument. Deeper specialization precomputes invariant classifications or drops irrelevant branches. Keep the general relation as the specification the specialized one is checked against.

This idea runs deep. In the 1970s Futamura observed that specializing an interpreter to a fixed source program yields a compiled program; partial evaluation of logic programs grew from the same unfold-fold-specialize toolkit.

Accumulators change modes

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

With an accumulator, the partial sum becomes an argument:

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).

On a ground numeric list both return the same sum. They are not the same relation in every mode: the accumulator version needs each element ready on the way down. Claim equivalence for the intended mode, not unconditionally.

Comparing versions

Before replacing a definition, write down its intended relation, supported modes, termination measure, whether duplicates and answer order matter, and whether callers read its proofs. Compare semantics first, then cost. --stats counts calls and unifications, but counts are not time: one expensive host call can outweigh thousands of cheap ones. A faster program that silently drops a mode is a different program.

Exercises.

  1. Unfold a helper with two clauses into its caller and count the resulting caller clauses. What did the proof lose?
  2. Compare a direct and an accumulator-based list length in every mode you can call them in. Which modes does each support, and which terminate?
  3. State the invariant of sum_from/3 and use it to show that sum_numbers/2 and sum_numbers_acc/2 agree on ground numeric lists.
  4. Find a transformation that keeps the answer set but changes the first proof that once/1 selects.

Nondeterminism is not randomness. A nondeterministic relation has several legitimate continuations, and search explores them systematically. The design task is to keep the useful ones, make their number finite, and put the productive ones first.

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 and constrain

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 and finite; qualified/2 prunes it. A caller that knows the task asks assignment(Worker, repair) and never generates the other task.

Search over states

A state-space search needs a state term, a finite move relation, a goal test, a policy for repeated states, and a witness. Here the visited list is both the repeat policy and the witness:

:- 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).

On a finite graph this terminates — but it also changes the question from walks to simple paths. That is a modeling decision, not an optimization. A caller who wants repeated stops needs a different bound, such as a step or cost limit.

Existence, one witness, all witnesses

reachable(From, To)                                 one pair; table it
once(simple_path(From, To, Path))                   stops at the first path
findall(Path, simple_path(From, To, Path), Paths)   may be exponential

All three are finite on a finite graph, and their costs differ enormously. Ask for the weakest result that meets the caller’s need.

Optimization is search plus an order

:- use_module(library(aggregate)).

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

The key [Cost, Plan] breaks ties deterministically. It does not shrink the search: aggregate_min/5 enumerates every candidate before it knows the minimum. It is not branch-and-bound. For a large problem, strengthen candidate_plan/3 or write a domain-specific dynamic program.

Depth-first is not fair

Depth-first search can disappear into an infinite branch before reaching a finite proof further along. Put reachable base cases before recursive expansion, and make each recursive step consume a finite resource or enter a finite table. once/1 turns the first success into a deliberate choice; use it only when that order is part of the specification.

Exercises.

  1. Add skills and time slots to assignment/2, keeping the search finite.
  2. Make simple_path/3 return the accumulated cost of the path as well.
  3. Change the key in best_plan/3 so that equal-cost plans prefer the shorter plan, and explain why the new key does so.
  4. Write a recursive first clause that starves a valid later base clause, then repair it and explain why the repair terminates.

25. Case study: an auditable decision service

This chapter turns a small access policy from prose into an explainable theory.

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.

The requirements

A research facility says: a person may enter a zone when their badge is active, the badge grants the zone’s clearance, their training is current, and they are not suspended. Contradictory badge records invalidate the service. Every permit must be traceable to source facts.

The prose leaves questions open. Is the suspension list complete? Is missing training a denial or unknown? Can someone hold two active badges? Which clock defines “current”? A rule engine cannot answer these; it can only make the chosen answers precise.

Sources and concepts

Record observations, not decisions:

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

Keeping the badge identifier explicit matters. active_badge(ada) would hide the record used as evidence and make conflicting records harder to see. Then build vocabulary that reads like the policy:

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).

The closed-world choice

If the suspension list is authoritative and complete, absence is evidence:

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

If it is incomplete, this rule is unsound policy; require a positive fact such as standing(Person, good) instead. The difference is an agreement about what the data covers, not a matter of syntax.

Decision and reason

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 --proof --goal 'permit(Person, Zone)' program.pl

reason/3 is a stable summary in domain vocabulary. --proof gives the derivation: the actual clauses and bindings. Users read the first; auditors check the second.

Integrity before decisions

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).

An answer here does not mean a permit failed. It means the input is unfit for a trusted decision. The host queries it — together with checks for a badge held by two people or a zone with conflicting clearances — before any permit goal.

Tests are policy examples

Test an ordinary permit, missing training, suspension, insufficient clearance, contradictory status, and a proof that names the exact badge and training facts. Boundary cases expose requirements: with two valid badges, permit(Person, Zone) yields one decision with two proofs. If the badge belongs in the answer, the relation should be permit(Person, Zone, Badge).

Embedding and audit

authenticated source snapshot
  -> normalized EyeProlog facts
  -> integrity checks
  -> permit and reason
  -> proof referencing clauses and facts

The host authenticates sources and converts records to facts; EyeProlog derives and explains; the host stores the answer with its proof and the input and theory versions. The solver can explain logical support. It cannot attest that the badge database was current. Keep old inputs, theories, and proofs, so a past decision can be reconstructed under the rules that governed it.

Exercises.

  1. Add a second badge for ada and observe that permit(Person, Zone) gives one answer with two proofs. Redesign the relation so the badge is part of the answer.
  2. Add time-bounded training using explicit dates and difference/3 from library(dates).
  3. Write an integrity relation for a badge assigned to two people.
  4. Model denial/3 without assuming that every failed permit has the same reason.

Historical note: interpreters, transformation, and the art tradition

Logic programming became a laboratory for symbolic computation because its principal data (terms, clauses, substitutions, and proof trees) could be represented with the same structures as any other domain. Meta-interpreters made resolution itself a topic of programs; Pereira and Warren’s definite clause grammars (1980) 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 reading: specializing an interpreter to a source program yields a compiled program. Tamaki and Sato’s unfold/fold transformations (1984) gave logic programs a calculus of meaning-preserving rewrites. EyeProlog does not build every classic transformation in. What it inherits 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 one sustained account of craft. This Part follows that breadth with EyeProlog’s explicit means: 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.

A logic program works because parts of mathematical reasoning can be written as finite symbols, transformed by explicit rules, and checked step by step. EyeProlog is not a theorem prover or a computer algebra system, but its small fragment of logic makes the old mathematical acts visible: a clause defines a class, a variable is an unknown, a helper relation is a lemma, two clauses are a case split, recursion is induction, a binding is a witness, and a proof term is the argument. This Part follows that correspondence and marks where it stops.

For a short route, read Chapters 26, 27, and 29, then continue at Chapter 31.

26. A proof can be a computation

Ask for Pythagorean triples with sides up to 20:

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

triple(A, B, C) :-
  between(1, 20, A),
  between(A, 20, B),
  between(B, 20, C),
  (C * C =:= A * A + B * B).

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

triple(3, 4, 5).
triple(5, 12, 13).
triple(6, 8, 10).
triple(8, 15, 17).
triple(9, 12, 15).
triple(12, 16, 20).

The query is an existential claim: there are A, B, and C in range with A² + B² = C². Each answer does more than say “true”. It hands back the object that makes the claim true. The substitution is the computational content of the existence statement.

Witnesses need a source

With all three arguments bound, the same clause only checks a candidate. With them unbound, the bounded between/3 goals supply candidates and the comparison filters them. The equation by itself says nothing about where numbers come from.

That is the gap between mathematical existence and executable witness. A classical proof may show that something exists without saying how to build it. An EyeProlog query produces a witness only when its clauses and control actually reach one.

Proofs as evidence

Run the same goal with --proof and each answer carries its derivation: the facts, rules, built-in calls, and bindings that produced it. That record supports three distinct activities:

These are different jobs. A derivation can be valid and unreadable, readable and built on a bad source fact, or correct for floating-point arithmetic and wrong for the physical quantity it was meant to model. Proof output makes scrutiny possible; it does not do the scrutiny for you.

The least model as closure

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

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

Start from the facts and repeatedly add every rule head whose body is already satisfied. The first round adds path(a, b) and path(b, c); the second adds path(a, c); the third adds nothing. That fixed point is the least Herbrand model, and it is what the program means. Goal-directed search reaches the same meaning from the other side: it asks only what this particular goal needs.

A tabled predicate makes the connection concrete. Its table grows with each new answer until no rule adds another — a local, demand-driven fixed-point computation.

Exercises.

  1. Run triple/3 with one, two, and three arguments bound. Compare the question asked, the answers, and the amount of search.
  2. Keep only primitive triples by rejecting those whose sides share a divisor. Which generators must run first to make the negation safe?
  3. Draw the fixed-point rounds of the least model for a four-edge graph with one cycle.
  4. For one printed answer of triple/3, state the existential claim its bindings witness, the finite domain that made the search possible, and what further argument a universal theorem would need.

27. Recursion is induction in motion

Represent natural numbers 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 two plus/3 clauses are the textbook definition of addition: zero plus Y is Y, and the successor of X plus Y is the successor of X plus Y. Run backwards, the same clauses split a number into summands:

eyeprolog --goal 'plus(X, Y, s(s(z)))' program.pl

plus(z, s(s(z)), s(s(z))).
plus(s(z), s(z), s(s(z))).
plus(s(s(z)), z, s(s(z))).

To prove something about plus/3 for every natural number, induct on the first argument: the base clause is the base case, the recursive call is the induction hypothesis, and the rule head is the conclusion it preserves.

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.

Correctness is not termination

Induction shows that every answer is right. It does not show that the search finishes. Chapter 19 separates the three claims — partial correctness, completeness for a mode, and termination — and they apply here unchanged.

For plus(+,+,-) the termination measure is the number of s/1 wrappers on the first argument. Every recursive call removes one, and natural numbers have no infinite descending chain. “It seems to get smaller” is not an argument; a measure into a well-founded set, decreasing on every recursive branch, is.

Data shapes give you the induction

Lists carry their induction principle in their constructors: [] and [Head | Tail]. A relation that follows them is easy to prove correct:

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

Prove the empty case, assume the claim for Tail, prove it for [Head | Tail]. Program and proof share a skeleton because both follow the same constructors.

Representation decides whether that skeleton is available. An expression tree built from number/1, plus/2, and times/2 supports structural recursion directly; a flat token list must be parsed first. Good representations make the proof principle visible, not just the code shorter.

Accumulators need stronger invariants

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

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

“Reversed is the reverse of Xs” is false for reverse_go/3 and cannot be proved by induction. The statement that works is stronger:

reverse_go(Xs, Acc, Reversed) holds when Reversed is the reverse of Xs followed by Acc.

This is the mathematician’s standard move: when a theorem is too weak to carry its own induction, generalize it until the hypothesis contains what the next step needs. Program transformation and proof discovery meet at the invariant.

Tabling changes the argument

On a cyclic graph, following an edge can lead back to a vertex already seen, so no term gets smaller. Tabled reachability terminates for a different reason: a finite graph has finitely many ground path/2 answers, the table only grows, and each productive round adds an answer it did not have. Termination comes from a finite answer space, not from structural descent.

The argument also states its own limit. If rules build terms of unbounded depth, the space of calls or answers is infinite and tabling no longer bounds it.

Exercises.

  1. Define multiplication on Peano naturals using plus/3 and give its decreasing measure.
  2. Prove the strengthened reverse_go/3 invariant by induction on the first argument.
  3. Compare the termination arguments for list membership and for tabled reachability on a cyclic graph.
  4. In examples/peano-calculus.pl, line up one recursive predicate with its induction proof (base clause and base case, recursive call and hypothesis, head and conclusion), then give a separate termination measure.

28. Algebra, symmetry, and representation

Unification solves equations between terms:

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

The outer functors and arities agree, so the arguments must agree pairwise. But unification works in the free term algebra: distinct constructors are always different, and two terms are equal only if they have the same shape. It knows nothing of commutativity, so 2 + 3 = 3 + 2 fails even though both evaluate to 5.

Keep two kinds of equality apart:

A canonical representation turns some domain equalities into syntactic ones. For polynomials, sets, or fractions that is often the right design, but the normalizer then owes a proof: equivalent objects must normalize alike, and inequivalent ones must not.

A triangle given by three side lengths can be listed in six orders. Generate only the ordered one:

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

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

Because A =< B =< C, each triangle appears once. This is more than a speedup. It picks one representative from each permutation class — a quotient. Much of mathematics advances by choosing the right equivalence: fractions with equal cross-products, graphs up to renaming, formulas up to variable renaming. A logic program must decide which distinctions belong to the problem and which are accidents of notation.

Relations expose inverse problems

A function runs one way. A relation can be asked in several:

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

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

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

integer_rectangle(24, 1, 24).
integer_rectangle(24, 2, 12).
integer_rectangle(24, 3, 8).
integer_rectangle(24, 4, 6).

Multiply versus factor, evaluate versus interpolate, simulate versus infer the initial state: mathematics constantly moves between direct and inverse problems. A relation lets both share one specification, provided some argument supplies a finite direction for search — here, between/3.

Laws as testable relations

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

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

Over a finite carrier, define a relation for a violating pair and ask with \+/1 whether it has any answer. Over an infinite carrier, finite testing is evidence, not proof.

The examples cover the main roles: d3-group.pl computes a finite operation table, matrix-noncommutativity.pl refutes commutativity with one pair, group-inverse-uniqueness.pl proves uniqueness from axioms, and composition-of-injective-functions-is-injective.pl composes preserved properties.

Representation is a commitment

Writing a rational number as fraction(N, D) raises questions at once. May D be zero? Are signs normalized? Are fraction(1, 2) and fraction(2, 4) the same term or merely equivalent? These are not serialization details: they fix the equality relation, the search space, and the meaning of every later proof. Before choosing a representation, state its valid values, its equivalence, whether it has a canonical form, which operations must be fast, and which induction it exposes.

Exercises.

  1. Give two representations of an undirected edge. Compare their equality and indexing behavior.
  2. Design a normalized rational representation and write integrity relations for a zero denominator and a noncanonical zero.
  3. Use examples/d3-group.pl to check identity, inverses, and associativity. Which checks are exhaustive, and why?
  4. Use integer_rectangle/3 to list the rectangles of area 36, then explain which argument supplies the finite direction for the inverse problem.

29. Search as experimental mathematics

Mathematicians compute small cases, look for patterns, and hunt for counterexamples long before they prove anything. Logic programming makes that experiment transparent: generate a finite world, state the property as a relation, and ask for witnesses or failures.

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

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

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

The run prints nothing. That means only that no odd number from 1 to 100 has an even square under the implemented arithmetic. The theorem for every odd integer needs algebra: (2k+1)² = 2(2k²+2k)+1.

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.

The asymmetry of counterexamples

Search is weak at confirming and strong at refuting. No answer over a bounded range is evidence. One answer refutes a universal claim outright. examples/matrix-noncommutativity.pl multiplies two fixed 2×2 matrices both ways and gets different results; that single pair settles that matrix multiplication is not commutative.

When the claim itself is bounded — “for every integer from 1 to 10,000” — exhaustive search is a proof, provided the generator is complete, the predicate says what is meant, and the arithmetic is trusted.

Finite model exploration

A finite structure is a finite carrier plus interpretations of its operations. EyeProlog can enumerate candidate tables, apply axioms as filters, and return models or countermodels. For three elements a binary operation has nine entries and 3⁹ possible tables. The axioms prune them: closure keeps outputs in the carrier, an identity fixes a whole row and column, commutativity ties mirrored cells, associativity checks triples.

The order of those filters is itself mathematics. A strong law applied to partial tables collapses the search; the same law applied after full generation merely rejects thousands of finished candidates.

Count before you optimize

Search cost is usually a counting problem first. n alternatives at each of k positions give nᵏ leaves; ignoring a symmetry multiplies them; a constraint checked on partial choices removes whole subtrees. So before reordering goals or adding indexes, ask:

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

Otherwise the optimization may only speed up the production of duplicates. clpz-n-queens.pl, send-more-money.pl, integer-partitions.pl, stirling-bell-numbers.pl, and weighted-interval-scheduling.pl show different shapes of choice: permutations, digit assignments, recursive decompositions, set partitions, and ordered optimization. (The N-queens example searches at four queens; its eight-queens goal checks a known solution against the same model.)

Numerical models

beam-deflection.pl, orbital-transfer-design.pl, competitive-enzyme-kinetics.pl, and least-squares-regression.pl combine rules with floating-point models. A derivation inside such a model proves a conditional: given these measurements, equations, units, approximations, and thresholds, the conclusion follows under the implementation’s numeric semantics. It does not show that the sensor was calibrated, that the model applies in this regime, or that a float is an exact real. Name those conditions alongside the result.

Exercises.

  1. Turn a familiar universal conjecture into a bounded counterexample search in the style of counterexample_to_odd_square/1. State what an empty result proves and what it does not.
  2. Estimate the naive search space of examples/send-more-money.pl, then identify the constraint that removes the most branches.
  3. Search a three-element carrier for a noncommutative operation with an identity, and return the offending pair as a witness.
  4. Classify one computation of your own as witness construction, counterexample, exhaustive finite check, bounded evidence, or numerical model evaluation, and say what its success and its failure establish.

30. What mathematics promises

Mathematics does not promise that premises describe the world. It promises that one can check whether a conclusion follows from them. An EyeProlog answer has the same shape as a theorem:

axioms + definitions + inference rules       -> theorem
source facts + clauses + built-in semantics  -> ground answer + proof

The proof disciplines the arrow. It cannot vouch for the premises just by using them.

Four layers of trust

  1. Sources: are the facts authentic, current, complete enough, and in the right units?
  2. Model: do the predicates and rules say what the domain means?
  3. Engine: do parsing, unification, built-ins, tabling, and proof output behave as the documented profile says?
  4. Derivation: does this answer have a valid proof from this exact theory?

Integrity relations catch contradictions inside the theory. Conformance tests cover the engine. Proof checking covers the derivation. Provenance, signatures, calibration, and domain review cover the rest. No single mechanism replaces the others.

Limits are part of the result

Gödel, Church, and Turing did not weaken mathematics by proving limits; they made vague hopes precise enough to refute. EyeProlog has smaller, everyday limits, and a trustworthy tool states them:

A counterexample deserves standing against any number of confirming cases. Write the negative tests before the theory becomes expensive to change, keep the failed model that forced a redesign, and record which conclusions came from which version of the theory.

Before trusting a conclusion

  1. What does the ground answer say in the domain?
  2. Which facts and rules support it, and which facts came from outside?
  3. Which built-ins add semantics of their own?
  4. Was the search finite, and why?
  5. Does any negation mean “not proved” where “false” was intended?
  6. What counterexample would overturn the model?

Exercises.

  1. Classify every dependency of one policy example under the four layers of trust.
  2. Write a conclusion that is valid from false premises, and explain why proof checking cannot repair it.
  3. Prefix one strong conclusion with every condition it depends on: source authenticity, model scope, built-in semantics, finite search, theory version, and derivation validity.
  4. Write a one-page trust contract for an embedded EyeProlog service: accepted sources, model scope, numeric assumptions, resource bounds, proof retention, and known limits.

Historical note: mathematics examines its own methods

The path to logic programming ran through mathematics examining its own methods. 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 decision problems have no algorithm. Herbrand and Robinson supplied the 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 its methods fail, separating truth, provability, decidability, and computation. Finite bounds, mode restrictions, search risks, and trust boundaries belong in an account of EyeProlog 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.

This Part adds no language features. It is about keeping a theory correct while it changes: testing it, debugging it, and recognizing the designs that work.

31. Testing a theory

A unit test usually compares one returned value with one expected value. A relation needs more: a call can have several answers, none, duplicates, or several useful modes. Its contract covers the answer set, the absence of forbidden answers, the shape of witnesses, and the finiteness of the 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.

Start with a table in domain language

Case Given Question Expected Why
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 set
reflexive no loop edge path from a to a? design choice relation boundary

The last row matters most. Many bugs are not coding mistakes but meanings nobody settled. Does a path need at least one edge? No test framework can decide that for you.

Positive and negative observers

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

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

no_path_to_d :-
  \+ path(a, d).

eyeprolog --goal 'path(a, X)' --goal no_path_to_d program.pl

path(a, b).
path(a, c).
no_path_to_d.

The first goal pins down the answer set; the second turns an expected absence into a visible success. Both are ground or finite questions. no_path_to_d does not assert that classical negation holds; it records that this finite theory derives no such path. For a small example, the golden output file is the executable specification of the expected answers.

Test every supported mode

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

The first call builds one list; the second must enumerate three splits. Testing only the first misses a regression in relational generality. Testing the fully open call asks for an infinite relation and proves little. For each public predicate, record its principal mode, any secondary modes, meaningful modes that are deliberately unsupported, and which calls must be finite.

Properties over finite domains

Examples test points. A bounded property tests every point in a declared range:

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

double_is_even(N) :-
  (0 =:= (N + N) mod 2).

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

bounded_double_law :-
  \+ bounded_double_counterexample(_).

That is exhaustive for 201 integers and nothing more; the name says so. Useful bounded properties include round trips (parse then render), idempotence (normalizing twice equals once), symmetry, invariants on every generated state, and agreement between a simple reference relation and an optimized one.

Metamorphic tests

When the right answer is hard to list, a controlled change may still have a predictable effect. Adding an isolated vertex should not change existing reachability. Scaling every edge cost by a positive constant should not change the cheapest route. Reordering source facts should not change the answer set, only its order. These tests check an invariant across runs rather than one frozen output, which makes them well suited to guarding optimizations.

Answers, proofs, and integrity

An answer golden asks whether the conclusions changed; a proof golden asks whether their support changed. A new proof may be welcome after introducing a clearer helper — or may reveal that a decision now rests on an unintended fact. Review proof goldens; never regenerate them blindly. Use answer goldens broadly and proof goldens where provenance is part of the product.

Keep three outcomes distinct:

A minimum test matrix

Dimension Minimum evidence
Meaning one positive, one absent, and one boundary case per public relation
Modes every documented mode; a clear rejection for unsupported ones
Recursion base case, multi-step case, cycle, termination argument
Search smallest witness, competing witnesses, ties, empty domain
Negation ground success, ground failure, stratification
Aggregation empty, singleton, duplicates, tie handling
Integrity each invalid state detected; valid input not flagged
Proof one representative derivation with source premises visible
Scale a case large enough to expose indexing or table behavior

Exercises.

  1. Build the domain-language test table for ancestor/2, including a cycle and the disputed reflexive case.
  2. Extend bounded_double_law/0 into bounded commutativity and associativity tests for a finite operation table. Which is cheaper, and why?
  3. Write a metamorphic test for a route planner.
  4. Design a test that tells “no answer” apart from “invalid input”.
  5. Fill in the minimum test matrix for one public relation and say which expected outputs should be exact goldens.

32. Debugging by meaning, search, and proof

“The query failed” is not a diagnosis. Failure can mean a missing fact, a variable bound too early, a built-in called outside its mode, a negation that saw an unintended answer, recursion that never reaches its base case, or a relation that was misstated from the start. Look through four lenses, in 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 premises support the answer you got?
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.

Shrink to one ground question

Don’t start from an open query that prints hundreds of answers. Name one conclusion that is missing or wrong, such as eligible(alex), and expand only the clause meant to prove it. If you can’t say what the ground question should answer, stop debugging code and fix the domain sentence.

Follow bindings left to right

age(alex, 19).

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

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

eyeprolog: error(instantiation_error)

The comparison runs before anything binds Age. A binding ledger shows it immediately:

Before goal Goal Bindings produced
Person = alex Age >= 18 none; Age unbound, error
— age(Person, Age) never reached

Swap the goals so age/2 binds Age first, and the clause works. For longer bodies, the ledger reveals more than rereading the source. Record structure as well as values: a variable may be bound to a partial list or a compound term with open variables inside.

Symptoms and first moves

Compare with a reference

Temporary relations expose intermediate concepts. A stronger version of the same idea is differential testing: write a deliberately simple reference relation over a bounded domain and look for disagreement with the optimized one.

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

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).

A full equivalence check needs the other direction as well. Within a finite domain, this is the best guard you have while transforming a program. Once a fault is understood, delete temporary helpers or promote them to real domain concepts; debug2/3 does not belong in a theory whose proofs people read.

Read statistics as questions

--stats reports work, not meaning. Many solutions may be necessary or may point to a generator that should be constrained. Many table hits show reuse; many distinct table entries may show an argument that keeps calls from sharing. On the Node CLI it also reports heap use, the amount counted against the memory guard, resident-set size, and the soft and hard memory ceilings, even when the run ends in a Prolog error.

--stats summarizes at the end. For a long or deliberately non-terminating computation, call the EyeProlog extension statistics/0 where a live snapshot helps, as in loop :- work, statistics, loop. statistics/2 gives the program one value, for example statistics(memory_guard_used_bytes, Used); with an unbound key it enumerates all of them, and an unknown key raises a domain_error for statistics_key. Neither is available under --iso-strict.

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

Keep the lesson

Every repaired defect should leave something behind: a new positive or negative case, an integrity regression, a documented mode, a bounded property, a proof golden, or a comment stating the invariant that was violated. Otherwise the repository remembers the fix and forgets the reason.

Exercises.

  1. Introduce a missing join into a two-relation rule, then use the proof of a false positive to find it.
  2. Make optimized_square/2 differ from reference_square/2 at one point and show that disagreement/2 finds it. Add the check for the other direction.
  3. Compare --stats before and after moving an invariant calculation out of a recursion.
  4. Turn one defect into a regression: the smallest disputed ground question, the expected answer, the first wrong binding or search choice, the repaired invariant, and the test that fails if the defect returns.

33. A pattern catalog for reasoning

A pattern is a recurring arrangement of meaning, representation, and control that solves a named problem. Choose one when its problem is present, not because the code looks similar.

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.

1. Ground sentence first. When argument order and meaning start to drift, write one representative ground fact and read it aloud before adding variables. assigned_badge(alex, badge_17). makes argument roles reviewable.

2. Normalize at the boundary. Keep source spellings, aliases, and units out of domain rules. Retain the source facts, derive one canonical vocabulary, and make the core rules depend only on it:

:- use_module(library(strings)).

source_role(person_7, 'Doctor').

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

Adapters can change without touching policy, and proofs still trace back to the source.

3. Generate, constrain, describe. Produce a finite candidate, apply the cheapest selective constraints in dependency order, then build the witness or reason:

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

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

4. Carry the witness. A yes/no relation that did the work of finding a path should return the path. Add an argument for the path, assignment, schedule, or evidence (see path/3 in Chapter 4). Witness size and duplicate witnesses then become explicit design questions.

5. Bound absence. Bind the subject and the finite scope before \+/1, and give the closed-world step one named home:

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

This is not an explicit fact that the person is unregistered; the name and the bound domain make that visible.

6. Explicit state transition. Instead of mutable state, relate an old state, an action, and a new state:

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

Histories become ordinary lists and invariants become queries over states.

7. Fixed-point closure. For reachability, inheritance, and dataflow, state the positive recursive relation directly and table it. Termination then rests on a finite call and answer space, not on pretending the graph is acyclic.

:- table depends/2.

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

8. Proof façade. When helper clauses make proofs unreadable, introduce named domain concepts and a small public decision relation whose premises read as reasons:

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

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

9. Integrity before inference. Encode forbidden combinations as ordinary relations with diagnostic arguments, so a caller can list every defect before asking for decisions:

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

10. Version the evidence. Keep the source snapshot, theory version, and numeric assumptions beside the proof, so an old decision can be reconstructed under the theory that made it rather than rerun under today’s:

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

Anti-patterns

Patterns compose; a decision service typically normalizes at the boundary, generates and constrains, carries witnesses, presents a proof façade, checks integrity, and versions its evidence. A three-fact example needs none of that. Use the smallest set of patterns the problem actually calls for.

Exercises.

  1. Find three patterns and two anti-patterns in one of the large examples.
  2. Refactor an opaque rule into boundary, concept, and decision layers, and compare the proofs before and after.
  3. Write a versioned evidence envelope for the Chapter 25 decision service.
  4. For one real theory, pick the smallest set of patterns that solves its problem and name the pressure that justifies each.

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. Shapiro’s algorithmic program debugging (1983) turned this into a method, locating a wrong clause by asking an oracle about the intended meaning of the program’s subgoals. Testing practice later absorbed ideas from theorem proving, database validation, regression testing, and property-based testing.

A repository makes this practice durable. A theory, its exact answer files, proof files, conformance corpus, and version tags preserve not only a program but expectations about its meaning. Regression tests make old decisions reviewable; property tests seek counterexamples; metamorphic tests state what must stay invariant under controlled change. Patterns complete the cycle by naming recurring design knowledge, so that 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.
Relational term operations stay at the center; control, mutable state, and I/O enter at explicit boundaries.

Libraries, language tools and programs that touch files need more than the relational core: control, reflection, state, operators and streams. Term inspection and atomic conversion are still relations. Cut, database updates and stream operations are not, so keep them at named boundaries.

--iso-strict on the CLI, or isoStrict: true in the JavaScript API, limits the language to ISO/IEC 13211-1:1995 plus Technical Corrigenda 1–3. Both modes use the same processor character set: Unicode scalar values U+0000..U+10FFFF without surrogates, collated by scalar value. Isolated and error cases live in test/conformance/cases/iso/.

34. Control, exceptions, and grouped solutions

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

If-then-else commits to the first solution of its condition. call/1 runs a goal held in a variable, and call/2-8 add arguments to a closure; a meta-call is its own cut boundary. once(Goal) keeps one solution of Goal, while cut discards every alternative created since the current predicate was entered. A cut inside a predicate called from one branch of Left ; Right stays local to that predicate, so if the branch later fails, Right is still tried. Keep cuts next to the choice they document, and compare the full answer set before and after adding one.

Exceptions

A missing route is an ordinary negative answer and should fail. A call the caller cannot interpret should throw:

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; on a match the recovery goal runs in the environment of the catch/3 call, and other exceptions continue outward. ISO instantiation, type, domain, permission, representation and evaluation errors travel the same way.

Normal mode also has call_cleanup(Goal, Cleanup) and setup_call_cleanup(Setup, Goal, Cleanup), which --iso-strict omits. Cleanup runs exactly once, whether the goal finishes deterministically, is exhausted, is cut, is abandoned at the top level or throws. It is installed only after Setup succeeds. After a cut it sees the goal’s bindings; after an exception, only those of Setup. If a deterministic goal runs Cleanup before answering, the cleanup’s bindings are part of the answer. Cleanup failure is ignored, an exception already in flight beats a cleanup exception, and nested cleanups run inside-out.

Grouped solutions

findall/3 returns one list. bagof/3 returns one list per binding of the goal’s free variables and fails when there are none; setof/3 also sorts and removes duplicates. Var^Goal hides a variable from grouping:

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

This gives one total per region. Without Seller^ it would give one per region and seller, which is the usual reason a collection arrives as several answers instead of one.

Integer arithmetic

Integer division has two roundings. For -7 and 3, // truncates to -2 and div floors to -3; mod gives 2 and rem gives -1. Bitwise operations and shifts require integers.

The examples iso-control-and-errors.pl, iso-grouped-solutions.pl and iso-integer-arithmetic.pl run each of these side by side.

Exercises.

  1. Rewrite travel_status/3 as two clauses, one for connected and one using \+ route(From, To). With route(a, b) stated twice, count the solutions of each version with findall/3 and explain the difference.
  2. Make require_route/2 throw type_error(atom, From) when From is not an atom, and show that checked_route/3 lets that error pass outward.
  3. Remove Seller^ from regional_total/2 and predict its answers for a region with two sellers.
  4. In a route planner, name one absence that should fail and one broken precondition that should throw.

35. Reflective terms and atomic conversion

When the shape of a term is itself the input, as in walkers, schema checkers and interpreters, reflect on it:

term_shape(Term, shape(Name, Arity, Arguments)) :-
  functor(Term, Name, Arity),
  (Term =.. [Name | Arguments]).
One structured event term fans out into functor, argument, univ-list, variable, ordering, character, and code views.
Reflection does not change a term; it exposes its structure, ordering, or spelling.

functor/3 relates a term to its name and arity, arg/3 picks a one-based argument, and =../2 (“univ”) relates a term to the list of its functor and arguments. Run backwards, they build terms. A missing name, negative arity or partial list raises an error instead of failing quietly.

copy_term/2 renames variables apart and keeps their sharing. term_variables/2 lists distinct variables in order of first occurrence. ==/2 and \==/2 test identity without binding; unify_with_occurs_check/2 rejects cyclic bindings explicitly. compare/3 and @<, @=<, @>, @>= order terms without evaluating them: 3 + 4 < 8 compares numbers, and 3 + 4 @< 8 compares syntax.

At text boundaries, atom_concat/3 joins or splits atoms, sub_atom/5 relates an atom to a fragment and its position, atom_chars/2, atom_codes/2 and char_code/2 convert to characters or codes, and number_chars/2 and number_codes/2 parse and render numbers. 'λ' is an atom; with the default flag, "λ" is the list ['λ'].

See iso-reflective-terms.pl and iso-atomic-conversion.pl, which lists every three-character sub-atom of eyeprolog.

Exercises.

  1. Given pair(X, X), predict the result of term_variables/2 before and after copy_term/2.
  2. Write term_size/2, counting the nodes of a term, once with functor/3 and arg/3 and once with =../2.
  3. Explain why 3 + 4 < 8 succeeds while 3 + 4 @< 8 fails.
  4. Use sub_atom/5 with findall/3 to collect every three-character sub-atom of eyeprolog, and predict their number before running it.

36. Dynamic predicates, directives, and operators

:- dynamic(task/2).

prepare_queue :-
  asserta(task(check_power, urgent)),
  assertz(task(check_network, normal)).
Initialization and assertions establish an ordered dynamic task queue beside an operator declaration that parses readable syntax into an ordinary reports term.
Database updates change solver-local clause order; operator declarations change how later source is parsed.

asserta/1 adds a clause at the front and assertz/1 at the end. retract/1 removes the first matching clause and retries for later ones, and abolish/1 removes a dynamic procedure. clause/2 and current_predicate/1 inspect the program. Changing a static or built-in procedure raises a permission error.

Backtracking does not undo updates, so later goals see the changed database. Each update invalidates cached tabled and ground-chain answers, and a rule change refreshes the recursion and negation analysis. Run setup from an initialization goal so the state does not depend on query order:

:- initialization(prepare_queue).

Initialization goals run after the program is prepared and before host queries. include/1 expands a file in place, and ensure_loaded/1 loads it at most once. multifile/1 and discontiguous/1 permit clause layouts. Flags and character conversions are per solver.

Operators

:- op(600, xfx, reports).

sensor_7 reports temperature.

The fact is exactly reports(sensor_7, temperature). Priority sets binding strength, and fx, fy, xf, yf, xfx, xfy and yfx set position and associativity. A declaration affects only later text; current_op/3 inspects the table and op(0, Specifier, Name) removes an entry.

An operator atom may appear bare as an argument, list element, or the whole content of parentheses or braces: current_op(P, S, :-), [:-,-], (+) and {*} are all valid. writeq/1 follows the same rule, so writeq({*}) writes {*} and writeq(f(;,'|',';;')) writes f(;,'|',';;'). The bar stays quoted because an unquoted | is a list separator.

ISO declares ?- as prefix operator 1200 fx. Because EyeProlog’s embedded quads allow Label ?- Query., it also declares ?- as 1200 xfx, and current_op(P, S, ?-) returns both. In normal mode a quad is recognized from the parsed ?-/2 term, so ?-(Label, Query). and other spellings of the same term work too. The label is an ordinary term and must be ground; a non-ground label is reported as BAD_ID and later quads still run. Under --iso-strict, ?-/2 is plain term syntax.

See iso-dynamic-database.pl and iso-operators.pl.

Exercises.

  1. Give the clause order of task/2 after one asserta/1 and two assertz/1 calls.
  2. Write pop_task/1, which retracts the first task/2 clause and returns it, and show that backtracking into a later failure does not restore the task.
  3. Declare an infix operator such as implies and write three facts with it. Use write_canonical/1 to show the terms that were stored.
  4. Write an embedded quad test that checks the task/2 order produced by prepare_queue/0.

37. Streams and term I/O

To write a term another Prolog can read back, open a text stream, write canonical syntax, end with a period and always 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)
  ).
A structured event is written with a terminating period to a text stream, read back as a term, and followed to end of file.
Open the right stream type, write readable syntax with a period, read in order, observe the end, and close.

open/4 adds options to open/3: type, alias, repositioning and end-of-file action. In strict mode, which lacks setup_call_cleanup/3, close streams on every path yourself.

write/1-2 writes readable syntax, writeq/1-2 adds quotes where needed, and write_canonical/1-2 ignores operators. Output uses only the separators the syntax needs: writeq([a,b]) writes [a,b] and writeq(1+2) writes 1+2, but a+ -b keeps its space so the tokens do not merge. A graphic atom with a period, such as ./*, needs no quotes.

write_term/2-3 takes quoted/1, ignore_ops/1, numbervars/1 and variable_names/1. Normal mode adds two options that strict mode rejects:

get_char, peek_char, put_char and their code forms work on text streams, and the byte predicates on binary streams. Mixing them raises a permission error instead of guessing an encoding. read/1-2 reads the next term, and read_term/2-3 can also return its variables, their source names and its singletons. Every read makes fresh variables: an X in one read term shares nothing with an X anywhere else. stream_property/2 reports a stream’s mode, type, alias, position and end state, and set_input/1 and set_output/1 change the defaults.

With eof_action(eof_code), reading at the end returns end_of_file for terms and characters and -1 for codes and bytes; at_end_of_stream/1 tests for it. iso-term-io.pl writes a fixture under /tmp, reads it back and observes the end of the stream.

Exercises.

  1. Use write_event/2 to write two events, then read them back with read/2 until end_of_file.
  2. Write f('A b', 1+2, "ab") with write/1, writeq/1, and write_canonical/1, and say which outputs another Prolog can read back.
  3. Open a text stream for writing and call put_byte/2 on it. Which error is raised, and why is that better than guessing an encoding?
  4. Why does write_event/2 belong outside the relation that decides what an event means?

Historical note: the practical language becomes portable

By the late 1970s and 1980s, Prolog had spread from Marseille into several implementation traditions. David H. D. Warren’s DECsystem-10 Prolog compiler (1977), whose techniques he later distilled into the Warren Abstract Machine (1983), established much of the practical vocabulary in Edinburgh: ordered control, term inspection, dynamic clauses, operators, and streams. These facilities made Prolog useful far beyond theorem-proving examples, but differences between systems also made portability a recurring concern.

ISO/IEC 13211-1:1995 gave that accumulated practice a common core. It did not freeze the language: constraints, modules, tabling, coroutining, and other facilities continued to develop in implementations and in later standardization work. What the standard supplied was a stable, shared account of ordinary Prolog terms, control, state, errors, and I/O, against which extensions could be named.

Part IX — Reference as practice

Enter the reference with a question. Chapter 38 says what source means, Chapter 39 helps you choose a predicate, and Chapter 40 turns a file into answers and proofs and points to further examples. Chapter 41 states the standards and implementation boundaries, and Chapter 42 collects notes and vocabulary. Look things up as needed; there is no need to read them straight through.

38. Language and ISO profile

The 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 to find defects, not treated as an unpublished fourth Corrigendum. test/conformance/STC-DRAFT-STATUS.md tracks the 2026-08-23 draft through items #73-#76. Where a proposal changes published semantics, such as #75’s conditional power-underflow proposal, strict mode keeps the published baseline until the change is standardized or adopted as a compatibility extension.

Normal EyeProlog adds a module interface aligned with later WG17 module amendment work and a definite clause grammar profile following ISO/IEC TS 13211-3. The requirements clarified by the 2013 Part 2 amendment have their own executable coverage ledger. The rest of Part 2 and the Part 3 profile are documented and tested compatibility surfaces, not clause-by-clause certifications.

Source text

Normal-mode source is UTF-8. % starts a line comment and /* ... */ a block comment. Plain atoms begin with a lowercase ASCII letter; variables begin with an uppercase letter or underscore, and each bare _ is fresh. Single quotes delimit quoted atoms, and double quotes use ISO double-quoted-list notation. Integers, decimals, scientific notation, binary, octal and hexadecimal integers, and character-code constants are accepted. Normal mode also accepts digit-separated integers such as 1_000 and 0xCA_FE (layout may follow the underscore) and the Trealla-compatible "text"||Tail splice for chars and codes lists. Strict ISO mode accepts neither extension.

The processor character set is the same in normal and --iso-strict modes, because Part 1 leaves it implementation defined. EyeProlog’s PCS (processor character set) is the Unicode scalar repertoire. Printable ASCII keeps the Part 1 lexical classes. Unicode letters extend alphanumeric names, Unicode white space is layout, and the remaining non-ASCII symbols and punctuation are extended graphic characters. Character codes and collation values are the Unicode scalar integers. Quote any atom whose spelling should not depend on an extended lexical class:

city('München').
message("café").

Inside a quoted atom, a single quote is doubled: 'don''t'. Escapes follow the ISO quoted-character grammar:

A literal layout character other than space, such as a tab or newline, is not allowed inside quotes. A quoted token crosses a line only through a continuation escape: a backslash followed directly by the newline, which adds no character. NUL is written '\0\'. 8 and 9 are not octal digits, so '\8\' is a syntax error. writeq/1 writes other non-symbolic control characters as octal escapes; ESC is '\33\'. Double-quoted lists use the same rules. Doubling the active delimiter works in both quoted forms, so "" inside double quotes is one double-quote character. Whitespace between tokens is insignificant.

Graphic tokens use the characters #$&*+-./<=>?@^~\; ! and ; are solo atoms. A colon is the Part 2 module qualification operator in Module:Goal. Normal mode predeclares it; --iso-strict does not, since it is not in the Part 1 operator table. Quote an atom whose name contains a colon. Unquoted angle-bracket IRIs are not syntax.

/* opens a block comment only at the start of a token; inside a graphic token the slash and star are atom characters. Graphic tokens are formed maximally before a period can count as the end of a clause. So *. or ./*. typed at the prompt is not yet a complete term: the period belongs to the atom, and the reader waits for a separate full stop. ./*. . reads the atom ./*. and takes the second period as the terminator.

Grammar

Below, { x } means zero or more repetitions of x, [ x ] means optional x, and parentheses group alternatives. These marks are not EyeProlog source characters.

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 not supported; write ready. Every clause ends in a period. The initial operator table contains these operators, all read as ordinary compound terms:

op/3, as a directive or a call, defines or removes prefix, infix and postfix operators with the ISO specifiers fx, fy, xf, yf, xfx, xfy and yfx. Variables cannot stand in functor or predicate position. Parentheses around one term denote that term; around two or more comma-separated terms they build a right-associated ','/2 term, which is conjunction in goal position and plain data elsewhere.

Meaning and execution

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. Unification is first-order finite-tree unification with an occurs check: binding a variable to a term that contains it 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. Nested inside another term, the same text is compound data; context decides the role. Predicate identity includes arity, so edge/2 and edge/3 are different predicates.

Execution is goal-directed, not bottom-up saturation. Body goals normally run left to right, though the solver may run a ready deterministic built-in early as a pure filter. Ordinary user-defined calls, including recursive calls, use depth-first resolution unless the source explicitly declares :- table p/n.. An explicitly tabled grammar invoked through phrase/2-3 gets a separate invocation-keyed table scope, so tables are not retained across unrelated input sequences. \+/1 is negation as failure, not classical negation; the separate tnot/1 extension provides well-founded semantics for eligible finite Datalog components.

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 adds call_cleanup/2 and setup_call_cleanup/3, which --iso-strict excludes, the module compatibility surface, and a Part 3-oriented DCG profile.

Module compatibility profile

A module adds one component to predicate identity: module name, predicate name and arity. The first directive of a module source names the module and its public predicates:

% colors.pl
:- module(colors, [tone/1]).

tone(blue).
hidden(module_private).

Another source imports all exports or selected indicators. An unqualified call uses a predicate local to the calling module first and then an import, so a local hidden/1 stays distinct from the private one in colors:

:- use_module('colors.pl', [tone/1]).

hidden(user_local).
answer(Tone, Hidden) :- tone(Tone), hidden(Hidden).
qualified(ok) :- colors:tone(blue).

use_module(library(lists)) and use_module(library(strings)) resolve the bundled modules in Node and the browser. Atom designations such as 'colors.pl' resolve relative to the importing file in Node. use_module/1 imports every export; use_module/2 imports only the listed indicators, and an empty list imports nothing when only qualified calls are wanted. Module:Goal selects a module explicitly. Loading a module again has no effect. Conflicting imports and imports of unexported predicates are errors.

Part 3-oriented definite clause grammars

A grammar rule Head --> Body. becomes an ordinary predicate with two extra difference-list arguments. A parameterized nonterminal keeps its written arguments, so token(Type)//1 is implemented by token/3. Nonterminal indicators can be exported and imported:

:- module(vocabulary, [word//1]).

word(noun) --> [robot] | [scientist].

Grammar bodies may use terminal lists, [], sequencing with a comma, alternatives with ; or |, if-then-else, embedded goals {Goal}, call//1, phrase//1 and !//0. A pushback (semicontext) looks ahead by returning 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, and a non-callable body raises type_error(callable).

EyeProlog performs the optional terminal-sequence checks of the ISO/IEC TS 13211-3 working draft, 8.18.1.3 g and h. It reports type_error(list, Culprit) for an invalid sequence in both arities and for an invalid remainder in phrase/3, including improper lists. Variables, proper lists and partial lists pass. The check runs before the grammar, so a failing grammar does not hide the error. Dedicated regressions enforce this choice, while the portable quads accept both checking and non-checking outcomes. ISO-PART3.md records that the 2023-08-14 working draft specifies type_error(terminal_sequence, Culprit) for this case.

Part 3 leaves \+//1 and standalone ->//2 implementation dependent. EyeProlog’s \+ Body tests from the current state without consuming input, and ->//2 threads the state produced by the condition into the then-branch.

A bidirectional expression grammar

dcg-expression-language.pl parses arithmetic into a syntax tree with correct precedence and left associativity, using an accumulator instead of left recursion:

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) --> [].

A second grammar prints the tree back to tokens with only the parentheses it needs, and the checked answers in examples/output/dcg-expression-language.pl confirm the round trip.

Deep sequence hand-off

library(dcgs) provides ... //0, which matches any number of elements. It is not in ISO Part 3. In a grammar such as

a --> ..., epsilon.
epsilon --> [].

the remaining sequence is handed from ... //0 to another nonterminal at every suffix. For a finite compact list, EyeProlog scans iteratively instead of using one solver depth level per cell, and when the continuation is provably a zero-width identity such as epsilon//0 it skips building a resolution frame per suffix. The list is still traversed. Open or non-compact inputs, and continuations that consume or constrain the remainder, keep ordinary behavior, and phrase/3 still enumerates every remainder. The inference count of time/1 covers solver-level inferences, not the scanner’s internal steps.

Directives and protected built-ins

false/0 is the ISO always-failing built-in. It is a protected static procedure, so a source clause with head false is rejected, not read as a directive or integrity constraint.

The standard directives are 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 the program is prepared and before host queries. Included text is expanded in place, and a repeated ensure_loaded/1 designation loads once.

Normal output contains only ground query answers, one term and period at a time. Source facts are not echoed as conclusions, duplicate answers are suppressed, and answers are not asserted back into the program. Supported output syntax reads back as EyeProlog input.

Explicit tabling and recursion planning

The loader analyzes predicate dependencies and recursion so the solver can choose indexes and fast paths that preserve meaning. That analysis does not decide tabling. Ordinary predicates, recursive ones included, use indexed depth-first resolution unless the source declares :- table p/n..

A tabled positive recursive predicate is evaluated through an answer table: recurring calls consume answers already found, new answers are recorded, and evaluation continues to a fixed point. For eligible large, finite, function-free Datalog components, EyeProlog may represent a declared table as one shared most-general relation or an indexed least model. Every call to a declared predicate is tabled, whatever its arguments: open and partly bound calls each get a table keyed by their variant, so a left-recursive rule such as anc(X, Z) :- anc(X, Y), p(Y, Z). terminates for anc(X, Y) as well as for anc(a, Y). These choices happen inside an explicit declaration; they never table an undeclared predicate.

Ordinary \+/1 remains ISO negation as failure. tnot/1 requests well-founded evaluation for eligible finite, range-restricted Datalog dependencies, and wfs_truth/2 reports the three-valued state of a ground callable as true, false or undefined. Strict ISO mode has no table, tnot/1 or wfs_truth/2.

Query execution

A host-supplied goal must be callable and may contain constants or variables. An unbound goal raises instantiation_error, and a non-callable goal raises type_error(callable). A program run without a 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. keeps only ground answers;
  6. drops answers identical to source facts and suppresses duplicates;
  7. prints each answer and, only when requested, its proof.

Goal selection changes what the host runs, not what the program means. One goal’s answers are not asserted for later goals, though declared tables may be reused within the run. For stable output, goals for known predicates are grouped in the source order of their predicate groups, keeping the supplied order within a group. Goals for predicates with no group come last.

39. Predicate reference

EyeProlog’s normal predicate surface has two layers: 129 core registry indicators and 404 distinct non-ISO library or normal-extension indicators. Because phrase/2 and phrase/3 occur in both layers, their union contains 533 distinct predicate indicators.

Core predicates need no import. Bundled libraries add relations for collections, constraints, graphs, text, time, cryptography, files, and other domains. The interoperability notes identify the subset shared with Trealla and Scryer, and the alphabetical reference at the end gives one compact contract per indicator.

Notation and conventions

Call patterns 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 modes, not a mode system the parser enforces. A semidet call succeeds at most once; a nondet call may yield more answers on backtracking. Unless stated otherwise, a supplied result that does not unify simply fails.

Built-in dispatch is authoritative: built-ins cannot be modified through the dynamic database, and source clauses with the same indicator do not replace them. clause/2 and op/3 are the exceptions: a program that defines a source predicate with either indicator gets its own clauses. false/0 is stricter still and is rejected as a clause head. Portable programs should avoid every such collision, since other Prolog systems commonly reject it at load time.

Core registry

The default registry contains the built-ins of EyeProlog’s ISO compatibility profile. Where ISO/IEC 13211-1:1995 defines a predicate, EyeProlog uses its standard indicator; the registry also includes the later or common compatibility predicates listed below. Arithmetic is expressed through is/2, not through output arguments on arithmetic predicates. The registry contains 129 name/arity entries across 100 names.

Core registry at a glance

Control, search, and exceptions

;/2 recognizes an ->/2 term on its left and implements ISO if-then-else commitment. Cuts and committed conditions are control; use ordinary relations when all alternatives should stay observable.

Definite clause grammar processing

Grammar rules are expanded during program preparation, so the solver sees ordinary predicates with two extra arguments. Grammar bodies passed to phrase/2-3 at run time use the same expansion, including module qualification and the caller module of embedded or meta-called nonterminals.

Unification, type tests, and term order

Standard term order is variables, numbers, atoms, then compounds; compounds compare by arity, functor, and arguments. Among numbers, floats precede integers; floats compare by value and integers exactly. ISO leaves the order of two distinct variables implementation dependent, provided it is stable while a sort runs. EyeProlog attaches no permanent ordinal to a variable: it ranks variables in order of first encounter within one comparison, and sort/2, keysort/2 and setof/3 share one ranking for the whole operation. No process-global table of variables is kept, so long-running generators can create and discard variables without growing host state. Double-quoted source follows the double_quotes flag and never creates an extra scalar category.

Term construction and inspection

Construction raises instantiation_error when neither side supplies the shape. =../2 distinguishes an incomplete list (instantiation_error) from an improper one (type_error(list)).

Solution collection

Each collector runs its goal in an isolated inner search that shares the current program and stream state. Collected terms are copied, so local variables cannot escape. The bag must be a proper or partial list.

Dynamic database and procedure information

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 tables. Changing a predicate not declared dynamic raises a permission error instead of silently altering a static program.

Operators, character conversion, and flags

Because bounded=false, current_prolog_flag(max_integer, _) and current_prolog_flag(min_integer, _) fail; EyeProlog does not invent an unbounded sentinel. This is a deliberate choice, not a requirement: ISO 7.11.1.2 and 7.11.1.3 give max_integer and min_integer an implementation-defined value unconditionally, so the bounded flag constrains what the value means rather than whether it exists. A processor with unbounded integers has no largest integer to report. See conformance-report.md for the alternative reading. Setting char_conversion to off disables conversion for the source text that follows.

Normal and strict ISO mode both default to unknown=error. Interactive set_prolog_flag/2 changes survive when the REPL consults another file or imports a module. A program that wants an undefined predicate to fail must opt in with set_prolog_flag(unknown, fail); the bundled examples that rely on it do so explicitly.

Reading static procedures

A procedure defined by Prolog text is static, so clause/2 refuses it (ISO 7.5.2, 7.5.3, 8.8.1.3). Declaring it dynamic lifts the restriction but also makes it modifiable, and for a meta-interpreter it means annotating a program you may not want to edit.

ISO 7.5.3 notes that a public/1 directive for user-defined procedures would be an extension. Normal EyeProlog provides it:

:- public(elk/1).

elk(X) :- moose(X).

moose(bertha).

clause(elk(bertha), Body) now succeeds with Body = moose(bertha), while moose/1 stays private. A public procedure is still static: assertz(elk(clara)) raises permission_error(modify,static_procedure). The directive grants read access only.

To open every user-defined procedure at once, set default_procedure_access to public:

:- set_prolog_flag(default_procedure_access, public).

solve(true) :- !.
solve((A, B)) :- !, solve(A), solve(B).
solve(H) :- clause(H, Body), solve(Body).

elk(X) :- moose(X).
moose(bertha).
grazes(X) :- elk(X).

solve(grazes(W)) yields W = bertha with no declaration on the interpreted program. The flag changes access, not mutability: procedures remain static, and built-ins remain private, so clause(atom(_), _) still raises permission_error(access,private_procedure). The values are private (the ISO default) and public.

Both are extensions, so strict ISO mode offers neither: public/1 is rejected as an implementation-specific directive, and current_prolog_flag(default_procedure_access, _) raises domain_error(prolog_flag).

The occurs_check flag is likewise a normal-mode diagnostic extension, absent in strict mode; it defaults to true and offers error to report STO attempts. Operator and flag directives apply per program, not to global JavaScript state. The double_quotes setting affects subsequent source text, included files, command-line and API goals, 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

Conversions accept a partial output list when the atomic input is known, but constructing an atom or number requires a proper list with no unbound elements. Layout may precede tokens, including between a minus sign and the number. So a % comment may follow - directly, since % cannot continue a graphic token, while -/**/1 remains a syntax error under the eager token rule. The apostrophe code is written 0''' (value 39) and a space 0' (value 32); a character-code constant consumes one Unicode scalar, including non-BMP characters. Trailing material is rejected. Integers convert to canonical decimal; finite floats use the shortest decimal that round-trips, always with a fractional part, so 1.0000000000000001 becomes 1.0. Non-finite values are rejected. The behavior follows the 74 numbered cases of Ulrich Neumerkel’s number_chars/2 comparison, including the Corrigendum 2 error-precedence cases; number_codes/2 shares the parser.

Streams and unit I/O

A stream argument is an alias atom or the handle returned by open/3-4. Omitting it selects the current input or output.

Text operations on binary streams, and byte operations on text streams, raise permission errors. After end of file, eof_action(error) rejects another consuming read, eof_code keeps returning the end value, and reset starts again from the beginning. A peek does not mark a stream as past the end.

Term input and output

Term input uses the program’s current operators and the same quoted-character syntax as source text, including backslash-terminated escapes such as '\7\' and '\x7\', for both read/1-2 and read_term/2-3. Character conversions apply outside quotes when char_conversion is on. variable_names/1 and singletons/1 omit anonymous variables. Output predicates add no period or newline; write . and call nl/0 yourself to emit a complete clause.

A standalone number read as a term uses the same scanner as number_chars/2, so every sequence that predicate accepts has the same value when read as a full-stop-terminated term.

Arithmetic expressions

Every variable in an expression must already be bound to a number or an evaluable expression. Integer operations use arbitrary precision; operations that need floating point convert their operands to finite JavaScript numbers.

Arithmetic comparison evaluates; term-order comparison (@< and friends) does not, and it distinguishes floats from integers. Double-quoted text is compared as the list or atom selected by double_quotes.

Errors

ISO built-ins distinguish failure from error. Insufficient instantiation raises instantiation_error, a wrong category type_error, an invalid value domain_error, and an arithmetic fault evaluation_error. JavaScript embedders receive these as PrologError instances whose message holds the Prolog error term.

catch/3 presents a PrologError as error(Formal,eyeprolog). throw/1 copies its ball before unwinding: bound parts are kept, repeated variables stay shared within the copy, and unbound variables are fresh relative to the protected goal and the catcher. The interactive top level shows uncaught errors in the same error(Formal,eyeprolog) form, naming their variables _A and so on rather than reusing query variable names. An unmatched ball continues outward.

Streams belong to one solver run and are shared by nested calls, exceptions, and collectors. user_input and user_output always exist. The JavaScript ioOptions.input and ioOptions.write hooks connect the standard streams to an embedder. File streams are synchronous, so side effects happen in Prolog execution order.

Normal-mode extensions

The normal profile adds a few runtime controls outside the isolated ISO registry, listed separately to keep that boundary visible.

Cleanup controls

call_cleanup/2 and setup_call_cleanup/3 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 Cleanup that runs before a deterministic answer contributes its bindings to that answer. Nested cleanups run inside-out. Strict ISO mode provides neither predicate.

Bundled libraries

EyeProlog exposes 404 distinct non-ISO library and normal-extension predicate indicators in addition to the 129 indicators in its isolated ISO profile. 282 are defined entirely as ordinary Prolog clauses in focused modules under src/lib/; 122 use host support for control, attributed variables, constraints, character conversion, filesystem and OS access, timing, cryptography, or observability. Together the ISO and library catalogs cover 533 distinct predicate indicators. A normal-runtime predicate re-exported by a compatibility module is counted once: call_cleanup/2 and setup_call_cleanup/3 are exported by library(iso_ext), and time/1 and statistics/2 by library(time). statistics/0, tnot/1, and wfs_truth/2 remain normal-runtime extensions outside the library catalog. None of these are in 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/crypto.pl, src/lib/dates.pl, src/lib/dcgs.pl, src/lib/debug.pl, src/lib/dif.pl, src/lib/error.pl, src/lib/eyelet.pl, src/lib/files.pl, src/lib/format.pl, src/lib/http.pl, src/lib/freeze.pl, src/lib/gensym.pl, src/lib/iso_ext.pl, src/lib/json.pl, src/lib/lambda.pl, src/lib/lists.pl, src/lib/ordsets.pl, src/lib/os.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/sockets.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 narrow that to a list of indicators. library(prologue) exposes p.p.1 through p.p.11 of the working-draft Prologue as a facade over the canonical lists, between, iso_ext, and freeze modules.

src/standard-library.js registers the module sources and their host adapters. When src/lib/foo.pl needs a private runtime primitive, it is registered from src/foo-host.js: attributed-variable support lives in src/atts-host.js, cryptography in src/crypto-host.js. Pure Prolog libraries have no host file. Each runtime bridge thus stays with the module that owns its public semantics. Explicit use_module/1-2 loads always work; outside strict ISO mode, the autoloader may also load the canonical owner of any exported src/lib/ predicate.

For low-level embedding, the core registry is available through createDefaultRegistry() and getDefaultRegistry(), and the stricter Part 1 plus Corrigenda registry through createStrictIsoRegistry() and getStrictIsoRegistry(), paired with isoStrict: true for a complete strict-language boundary. Module-local predicate identity keeps private helpers and same-named predicates in different modules apart.

Module catalog

Using bundled libraries

A program states its library dependencies with ordinary directives:

printf '%s\n' ':- use_module(library(lists)).' 'answer(X) :- member(X, [ready]).' > program.pl
eyeprolog --goal 'answer(X)' program.pl
eyeprolog -p --goal 'answer(X)' program.pl   # with proof output

JavaScript uses the same 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);

Library relations by programming role

The mode marks below are descriptive, as in the core registry. Most library predicates are projections or filters: given an unbound, malformed, out-of-domain, or incompatible argument they normally fail rather than raise the ISO errors above, and they never invent open-ended domains. Bind operands, text, lists, indexes, dates, and aggregate generators before the call.

Portable numeric, comparison, and date relations

:- use_module(library(dates)).
:- use_module(library(between), [between/3]).
:- use_module(library(random)).
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

There are no named arithmetic wrappers such as add/3, abs/2, or sqrt/2; ISO arithmetic already says R is A + B, R is abs(A), R is sqrt(A), and likewise for the other operations. between/3 (in library(between)) and smallest_divisor_from/3 (in library(primes)) are ordinary Prolog. Choose a minimum or maximum with ISO control, for example (A =< B -> Min = A ; Min = B).

List relations

These are the Prolog definitions in src/lib/lists.pl. Each list argument must be a proper list unless stated otherwise; indexes and counts are nonnegative safe integers.

:- 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 text API works on ISO atoms or proper lists of one-character atoms, and generated text is an atom. With the default double_quotes=chars, a double-quoted literal is already such a list. The library has no JavaScript string dependency.

The matcher is a small, auditable Prolog subset, not JavaScript regular expressions. Use a host predicate when an application needs a full regex engine.

:- use_module(library(strings)).
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 relations follow the collection, arithmetic, and term-order contracts above. The caller keeps the search finite; bind outer variables first when they should restrict the nested goal.

Like findall/3, these aggregates let nothing escape the nested search except through their templates and outputs. There is no not/1; use \+/1. forall/2 comes from library(iso_ext), and once/1 is core.

:- use_module(library(aggregate)).
:- 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 predicate. A small relation walks its members, and =../2 exposes each member’s name and arguments.

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

Use =../2 to decompose or build whole argument lists, =/2 to unify, and \=/2 to test non-unifiability; no redundant aliases are registered.

Typical ISO extensions

library(iso_ext) supplies solution counting, universal checks, inclusive integer ranges, difference-list collection, and 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)).

Interoperability, autoloading, and portability

Four layers are kept apart:

A predicate written in pure Prolog may still lie outside the interoperability profile, and an interoperable one may rely on a host adapter. Here portable means source portability between Prolog systems, not the language a predicate happens to be implemented in.

The conservative Trealla/Scryer profile is derived from Scryer library modules and indicators that Trealla also documents. Where Trealla exposes a predicate globally, EyeProlog follows Scryer’s module name so Scryer-style imports keep working. The profile spans 27 modules and is deliberately narrower than either system’s exports; EyeProlog’s explicit-state random/3 and uuid/3, for example, are extensions rather than shared interfaces. Separately, all 33 bundled modules whose basenames match Scryer’s src/lib/ tree cover the corresponding Scryer public predicates, and the 26 modules with counterparts in Trealla’s library/ cover Trealla’s exports at pinned upstream commit f7a93bd521c07a4841f5123348111dd005918c89. That is module-overlap coverage; EyeProlog does not bundle Trealla’s native host libraries such as curl, gsl, janus, raylib, socket, or sqlite3.

Upstream source is reused rather than translated where possible. clpb.pl, ordsets.pl, reif.pl, and ugraphs.pl keep the upstream algorithms and license headers; assoc.pl is the complete upstream AVL implementation. gensym.pl and when.pl keep their algorithms with small blackboard and parser-safe closure adaptations. dif.pl, tabling.pl, and part of time.pl are thin facades over runtime facilities. charsio.pl covers Scryer’s UTF-8, chars/term, and Base64 relations; pio.pl covers Scryer’s full export surface and accepts both character-list and atom paths. files.pl covers Scryer’s filesystem exports and os.pl its environment and shell surface, with the side effects isolated in module-owned Node adapters. crypto.pl exposes Scryer’s public crypto surface; its strict Trealla/Scryer overlap is hex_bytes/2, crypto_n_random_bytes/2, and crypto_data_hash/3. Trealla-specific additions include aggregate_all/3, aggregate/3, frozen/2, the set, filter, and list helpers, tasklist/2-8, maybe/1-2, resource_error/2, and abolish_table/1. With no task scheduler, tasklist/2-8 runs sequentially with maplist-like success and failure; it does not promise Trealla’s parallelism. The portable library overlap example combines Boolean constraints, ordered sets, graphs, reification, delayed goals, generated names, character conversion, transposition, and table declarations in one program.

The builtins.pl files of Scryer and Trealla are not exposed as a library: EyeProlog keeps those procedures in the core registry rather than creating a second authority for them.

library(http) combines Scryer’s http_open/3 options with Trealla’s http_get/3, http_post/4, http_patch/4, http_put/4, http_delete/3, http_server/2, and http_request/5. Requests go through the Node adapter in src/http-host.js. http_open/3 returns the body as a text stream that pulls bytes lazily in bounded chunks; the convenience predicates return complete character lists. A GET or HEAD sends no entity unless data/1 is given, repeated request headers are preserved, and an explicitly empty entity gets Content-Length: 0. The client follows redirects and accepts Scryer request and response options, Trealla header(Name,Value) options, and Trealla’s host/path address lists. http_request/5 parses a request line and headers from a stream. http_server/2 accepts one connection per call, since there is no fork primitive.

library(json) is the BSD-licensed Scryer JSON grammar also shipped by Trealla. json_chars//1 is bidirectional: objects are pairs/1, arrays list/1, strings string/1, numbers number/1, booleans boolean/1, and null null. \u escapes are UTF-16 units: surrogate pairs combine into one scalar when parsing and are emitted as a pair when generating escapes; unpaired surrogates are rejected. See examples/json.pl and examples/http-client.pl.

library(sockets) follows Scryer’s TCP stream interface. socket_client_open/3 connects to Host:Port; socket_server_open/2 takes a port or Host:Port and binds an unbound port to the chosen ephemeral one. socket_server_accept/4 returns the peer address and a bidirectional stream. Socket streams report mode(read_append), position(0), and their address as file_name/1, and support text or binary I/O, aliases, eof_action/1, flush_output/1, and close/1, but not reposition(true). Closing a server stops new accepts without closing accepted streams. current_hostname/1 returns the host name. Without the Node socket capability these predicates raise resource_error(sockets).

library(arithmetic) provides number_to_rational/2 and rational_numerator_denominator/3. Processor numbers are still integers and IEEE-754 floats, so a non-integral rational is the ordinary term rdiv(Numerator,Denominator), which is/2 and arithmetic comparison do not yet evaluate.

library(files) uses Scryer’s character-list paths and includes directory_files/2, delete_file/1, rename_file/2, make_directory/1, make_directory_path/1, and working_directory/2. library(os) likewise uses character lists for environment names, values, commands, and arguments; Trealla documents the same indicators, though some of its versions take atoms. Both need the Node host and raise a resource error in a browser.

library(crypto) follows Scryer’s character-list and byte-list conventions: hexadecimal conversion, secure random bytes, hashes and HMAC, HKDF, PBKDF2-SHA512 password hashes, ChaCha20-Poly1305, Ed25519, X25519, and Scryer’s secp256k1 representation and helpers. Hashing, key derivation, authenticated encryption, Ed25519, and X25519 use Node’s backend; crypto_n_random_bytes/2 can also use Web Crypto. Without a backend these raise resource_error(crypto); hex_bytes/2 and the static curve data still work. As in Scryer, prefer X25519 over the generic secp256k1 helper for new key agreement.

The interoperable part of library(lists) 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 such as min_list/2, max_list/2, set_nth0/4, take/3, drop/3, and slice/4 remain available but outside that subset.

length/2 is fully relational: length(Xs, N) with both unbound enumerates Xs = [], N = 0, then one-element lists, and so on, under the normal memory guard, so heap exhaustion stays a catchable resource_error(memory). A bound length or a closed list gives one answer and leaves no choicepoint.

Only part of library(iso_ext) belongs to the shared profile: call_nth/2, time/1, and .../2. time/1 measures each solution of a goal and prints elapsed time, inferences, and MLips in Trealla’s form, for example % Time elapsed 0.832s, 65551 Inferences, 0.079 MLips; ... //0 describes any number of input elements. With these, the Trealla/Scryer DCG hand-off benchmark runs unchanged. Each predicate has one implementation owner; library(prologue) re-exports those owners, so it combines with library(lists), library(iso_ext), and library(freeze) in any import order without collisions.

library(lambda) follows Scryer’s higher-order notation, adapted from Ulrich Neumerkel’s permissively licensed implementation:

\X1^X2^...^XN^Goal
Free+\X1^X2^...^XN^Goal

The closure is copied before each call, so its local variables are fresh on each maplist/2-8, foldl/4-6, or call/N use; in the second form the variables in Free stay shared with the surrounding goal. Importing the library installs +\ as a priority-201 xfx operator; \ and ^ keep their ISO definitions. Parenthesize lower-priority goals after ^, as in \X^(X > 3).

A lambda may leave arguments for a later call:

f(x, y).

answer(A, B) :- call(\X^f(X), A, B).

This is the same as supplying both arguments directly. Calling a lambda with too few parameters raises existence_error(lambda_parameter, ...). The copy step uses ISO copy_term/2; no copy_term_nat/2 is needed.

Autoloading is a convenience on top of the module system, independent of the interoperability profile. An otherwise unresolved predicate in source, initialization code, an explicit CLI/API goal, or an interactive top-level query autoloads its canonical bundled provider. For example:

Resolution is conservative: a predicate the program defines wins; ISO built-ins are never replaced; an explicit import wins over autoloading; only then is the autoload index consulted. Facades such as library(prologue) re-export, so autoloading picks the module that actually defines the predicate. If two bundled modules genuinely define the same export, EyeProlog reports the ambiguity and asks for an explicit use_module/1-2. The top level resolves a query the same way after parsing it. Autoloading therefore supplies predicates, not retroactive syntax: a library that adds operators (for example library(clpz) and ins) must be imported before a query or clause uses them.

Explicit imports remain the clearest statement of dependencies:

:- use_module(library(lists)).
:- use_module(library(iso_ext), [call_nth/2]).

--no-autoload, or the JavaScript option autoload: false, requires every dependency to be explicit. --iso-strict always disables autoloading.

-w / --warnings reports dependencies on non-profile libraries and calls to non-profile predicates from shared modules; --portable turns those warnings into a failing run, for use in continuous integration. With EyeProlog, Trealla, and Scryer installed, node test/run-interop.mjs exercises cross-engine portability.

Specialized library implementation notes

These notes cover libraries whose attributed variables, delayed goals, host services, tabling, or runtime state have consequences worth knowing. They do not extend the cross-engine compatibility claims.

freeze(?Term,:Goal) runs Goal at once when Term is nonvariable, and otherwise delays it until Term is bound. Suspensions live in the logical environment, so backtracking keeps solution branches isolated. A woken goal has its own cut scope: a ! inside it commits only that invocation, not alternatives created before freeze/2 was called. Several suspensions on one variable are kept as a binary join tree, so each merge is constant-time; wakeup and residual projection walk it left to right and report each suspension separately. Thus call(((Y=1;Y=2),freeze(X,!),X=c));Y=3 keeps all three answers Y=1, Y=2, and Y=3.

dif(?Left,?Right) posts a delayed finite-tree disequality when its arguments can still unify. Residuals are normalized by implication: equivalent constraints share one residual, and a stronger one removes weaker ones in any order, while independent disequalities stay separate. Projection is redone in each solution, so a compound disequality stays whole until bindings reduce it to one aligned pair:

?- dif(f(X,A),f(Y,B)), ( true ; A = B ).
   dif(f(X, A), f(Y, B))
;  A = B, dif(X, Y).

library(atts) is the Prolog layer over the persistent attributed-variable machinery in src/term.js, with its host bridge in src/atts-host.js. It provides the attribute operations Scryer libraries use, accepts :- attribute ... declarations, calls module-local verify_attributes/3 before an attributed binding is committed, and runs the returned goals right after it. Attribute maps are copied only when changed, so they backtrack with the environment; the top level projects attribute_goals//1 hooks as residual goals. examples/attributed-variables.pl shows binding verification and attribute transfer across aliases.

library(clpz) is Markus Triska’s MIT-licensed CLP(Z) from Scryer Prolog, bundled as src/lib/clpz.pl and run unchanged on the generic attributed-variable machinery. It provides relational arithmetic and reification, finite and union domains, labeling, all-different and all-distinct, sums and scalar products, 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. It relies on ordinary EyeProlog facilities: module-local and user term_expansion/2 and goal_expansion/2, clause-list expansion, expand_term/2 for DCG lowering, a copy-on-write backtrackable blackboard, and the modules assoc, pairs, between, dcgs, terms, error, si, freeze, arithmetic, debug, and format. The bundled source matches Scryer commit e3df91e25f8a09ee942c04e8baef553bba5c6110, Git blob 806445c11e14c8b2515f3de7f309e0ac04d9ad04.

Besides call_nth/2, time/1, and .../2, library(iso_ext) re-exports call_cleanup/2, setup_call_cleanup/3, call_residue_vars/2, and copy_term_nat/2 from their canonical implementations, and exports the extensions countall/2 (count solutions), forall/2 (check every solution), succ/2 (adjacent nonnegative integers), cfor/3 (inclusive evaluated integer range), findall/4 (collect into a difference list), and variant/2 (equal up to renaming). Sharing the iso_ext module does not put them in the interop subset.

library(format) accepts format/[2,3], format_//2, portray_clause/[1,2], portray_clause_//1, and listing/1. The formatter implements literal text, ~~, ~n, ~w, ~q, ~a, and ~d; field widths and float presentation are not supported yet. library(pio) reads or materializes a DCG character list around ISO streams eagerly; unlike Scryer’s lazy lists, it does not defer file reads.

library(tabling) is a compatibility module for :- table Name/Arity. source. Tabling stays explicit: only declared predicates are tabled. The library adds start_tabling/2, abolish_all_tables/0, and abolish_table/1 on top of the processor’s own tables rather than providing a second tabling engine. library(time) returns a timestamp association list from the local clock; format_time//2 supports year, month, day, time, month-name, weekday-name, and day-of-year specifiers. It also exports sleep/1, re-exports time/1, and exposes statistics/2.

random/1 keeps the common mutable-seed interface through a private native step for speed; its sequence is the same Park-Miller sequence as the explicit-state random/3. That helper is internal and appears in neither the ISO nor the library catalog.

uuidv4/1, uuidv4_string/1, and uuid_string/2 provide the common UUID byte-list and character-list interface, using the stateful generator seeded by set_random/1. The extension uuid(+Seed0,-UUID,-Seed) creates a version 4 UUID atom from pure random/3; passing the returned seed on yields the next UUID, and the same initial seed reproduces the sequence.

Complete predicate indicator reference

The normal EyeProlog surface contains 533 distinct predicate indicators: 129 core registry indicators plus 406 bundled-library indicators, with phrase/2 and phrase/3 present in both layers and therefore counted once.

Each entry is a compact contract. + marks a principal input, - a principal output, and ? an argument that may be supplied or produced. These are documented operating modes rather than parser-enforced mode declarations. Solutions uses det, semidet, multi, nondet, delayed, meta, mode-dependent, declaration, or terminal; meta means the solution behavior depends materially on a called goal.

Predicate index

Each indicator links directly to its contract.

Symbols: -->/2 · ->/2 · ,/3 · ;/2 · ;/3 · !/0 · .../2 · @</2 · @=</2 · @>/2 · @>=/2 · */1 · \/1 · \/2 · \/3 · \/4 · \/5 · \/6 · \/7 · \/8 · \+/1 · \=/2 · \==/2 · #/\/2 · #\//2 · #\/1 · #\/2 · #\=/2 · #</2 · #</3 · #<==/2 · #<==>/2 · #=/2 · #=/3 · #=</2 · #==>/2 · #>/2 · #>=/2 · ^/10 · ^/3 · ^/4 · ^/5 · ^/6 · ^/7 · ^/8 · ^/9 · +\/2 · +\/3 · +\/4 · +\/5 · +\/6 · +\/7 · +\/8 · +\/9 · </2 · =:=/2 · =../2 · =/2 · =/3 · =\=/2 · =</2 · ==/2 · >/2 · >=/2 · $-/1 · $/1

A: abolish_all_tables/0 · abolish_table/1 · abolish/1 · acyclic_term/1 · add_edges/3 · add_vertices/3 · aggregate_all/3 · aggregate_max/5 · aggregate_min/5 · aggregate/3 · all_different/1 · all_distinct/1 · append/2 · append/3 · arg/3 · argv/1 · asserta/1 · assertz/1 · assoc_to_keys/2 · assoc_to_list/2 · assoc_to_values/2 · at_end_of_stream/0 · at_end_of_stream/1 · atom_chars/2 · atom_codes/2 · atom_concat/3 · atom_length/2 · atom_si/1 · atom_string/2 · atom/1 · atomic_si/1 · atomic/1 · automaton/3 · automaton/8

B: bagof/3 · bb_b_put/2 · bb_get/2 · bb_put/2 · becomes/2 · between/3

C: call_cleanup/2 · call_nth/2 · call_residue_vars/2 · call_with_error_context/2 · call_with_inference_limit/3 · call/1 · call/2 · call/3 · call/4 · call/5 · call/6 · call/7 · call/8 · callable/1 · can_be/2 · catch/3 · cfor/3 · chain/2 · char_code/2 · char_conversion/2 · char_type/2 · character_si/1 · chars_base64/3 · chars_si/1 · chars_utf8bytes/2 · circuit/1 · clause/2 · close/1 · close/2 · clpz_t/2 · compare_si/3 · compare/3 · complement/2 · compose/3 · compound/1 · cond_t/3 · connect_ugraph/3 · contains/2 · copy_term_nat/2 · copy_term/2 · copy_term/3 · countall/2 · crypto_curve_generator/2 · crypto_curve_order/2 · crypto_curve_scalar_mult/4 · crypto_data_decrypt/6 · crypto_data_encrypt/6 · crypto_data_hash/3 · crypto_data_hkdf/4 · crypto_n_random_bytes/2 · crypto_name_curve/2 · crypto_password_hash/2 · crypto_password_hash/3 · cumulative/1 · cumulative/2 · current_char_conversion/2 · current_hostname/1 · current_input/1 · current_op/3 · current_output/1 · current_predicate/1 · current_prolog_flag/2 · current_time/1 · curve25519_generator/1 · curve25519_scalar_mult/3

D: debug/1 · debug/3 · del_assoc/4 · del_attr/2 · del_edges/3 · del_max_assoc/4 · del_min_assoc/4 · del_vertices/3 · delete_directory/1 · delete_file/1 · dif_si/2 · dif/2 · dif/3 · difference/3 · directory_exists/1 · directory_files/2 · disjoint2/1 · domain_error/2 · domain_error/3 · drop/3

E: ed25519_keypair_public_key/2 · ed25519_new_keypair/1 · ed25519_seed_keypair/2 · ed25519_sign/4 · ed25519_verify/4 · edges/2 · element/3 · empty_assoc/1 · exclude/3 · expmod/4

F: fail/0 · false/0 · fd_dom/2 · fd_inf/2 · fd_size/2 · fd_sup/2 · fd_var/1 · file_access_time/2 · file_copy/2 · file_creation_time/2 · file_exists/1 · file_modification_time/2 · file_size/2 · findall/3 · findall/4 · float/1 · flush_output/0 · flush_output/1 · foldl/4 · foldl/5 · foldl/6 · forall/2 · format_/4 · format_time/4 · format/2 · format/3 · freeze/2 · frozen/2 · functor/3

G: ge/2 · gen_assoc/3 · gen_int/1 · gen_nat/1 · gensym/2 · get_assoc/3 · get_assoc/5 · get_attr/3 · get_atts/2 · get_byte/1 · get_byte/2 · get_char/1 · get_char/2 · get_code/1 · get_code/2 · get_line_to_chars/3 · get_n_chars/3 · get_single_char/1 · getenv/2 · global_cardinality/2 · global_cardinality/3 · ground/1 · group_pairs_by_key/2 · gt/2

H: halt/0 · halt/1 · hex_bytes/2 · http_delete/3 · http_get/3 · http_open/3 · http_patch/4 · http_post/4 · http_put/4 · http_request/5 · http_server/2

I: if_/3 · in/2 · include/3 · indomain/1 · ins/2 · instantiation_error/0 · instantiation_error/1 · integer_si/1 · integer/1 · intersection/3 · is_assoc/1 · is_ordset/1 · is_set/1 · is/2

J: join/3 · json_chars/3

K: keysort/2

L: label/1 · labeling/1 · labeling/2 · last/2 · lcm/3 · le/2 · length/2 · lex_chain/1 · list_max/2 · list_min/2 · list_si/1 · list_to_assoc/2 · list_to_ord_set/2 · list_to_set/2 · listing/1 · lowercase/2 · lsb/2 · lt/2

M: make_directory_path/1 · make_directory/1 · map_assoc/2 · map_assoc/3 · map_list_to_pairs/3 · maplist/2 · maplist/3 · maplist/4 · maplist/5 · maplist/6 · maplist/7 · maplist/8 · maplist/9 · matches/2 · matches/3 · max_assoc/3 · max_list/2 · max_sleep_time/1 · maybe/0 · maybe/1 · maybe/2 · member/2 · memberchk/2 · memberd_t/3 · min_assoc/3 · min_list/2 · msb/2 · must_be/2

N: neighbors/3 · neighbours/3 · nl/0 · nl/1 · nodebug/1 · nonvar/1 · not_si/1 · nth0/3 · nth0/4 · nth1/3 · nth1/4 · number_chars/2 · number_codes/2 · number_string/2 · number_to_rational/2 · number_to_rational/3 · number/1 · numbervars/3 · numlist/2 · numlist/3 · nvalue/2

O: once/1 · op/3 · open/3 · open/4 · 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_list_to_assoc/2 · 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

P: pairs_keys_values/3 · pairs_keys/2 · pairs_values/2 · partial_string_tail/2 · partial_string/1 · partial_string/3 · path_canonical/2 · path_segments/2 · peek_byte/1 · peek_byte/2 · peek_char/1 · peek_char/2 · peek_code/1 · peek_code/2 · permutation/2 · phrase_from_file/2 · phrase_from_file/3 · phrase_from_stream/2 · phrase_to_file/2 · phrase_to_file/3 · phrase_to_stream/2 · phrase/2 · phrase/3 · phrase/4 · phrase/5 · pid/1 · popcount/2 · portray_clause_/3 · portray_clause/1 · portray_clause/2 · put_assoc/4 · put_attr/3 · put_atts/2 · put_byte/1 · put_byte/2 · put_char/1 · put_char/2 · put_code/1 · put_code/2

R: random_integer/3 · random_labeling/2 · random/1 · random/3 · rational_numerator_denominator/3 · raw_argv/1 · reachable/3 · read_from_chars/2 · read_term_from_chars/3 · read_term/2 · read_term/3 · read/1 · read/2 · rename_file/2 · repeat/0 · repeat/1 · replace/4 · representation_error/1 · reset_gensym/1 · resource_error/1 · resource_error/2 · retract/1 · retractall/1 · reverse/2

S: same_length/2 · sat_count/2 · sat/1 · scalar_product/4 · select/3 · selectchk/3 · seq/3 · seqq/3 · serialized/2 · set_input/1 · set_nth0/4 · set_output/1 · set_prolog_flag/2 · set_random/1 · set_stream_position/2 · setenv/2 · setof/3 · setup_call_cleanup/3 · shell/1 · shell/2 · sleep/1 · slice/4 · smallest_divisor_from/3 · socket_client_open/3 · socket_server_accept/4 · socket_server_close/1 · socket_server_open/2 · sort/2 · split/3 · stable/1 · start_tabling/2 · statistics/2 · stream_property/2 · string_concat/3 · sub_atom/5 · substring/4 · subsumes_term/2 · subtract/3 · succ/2 · sum_list/2 · sum/3 · sumall/3

T: take/3 · tasklist/2 · tasklist/3 · tasklist/4 · tasklist/5 · tasklist/6 · tasklist/7 · tasklist/8 · taut/2 · term_attributed_variables/2 · term_si/1 · term_string/2 · term_variables/2 · tfilter/3 · throw/1 · time/1 · tmember_t/3 · tmember/2 · top_sort/2 · top_sort/3 · tpartition/4 · transitive_closure/2 · transpose_ugraph/2 · transpose/2 · trim/2 · true/0 · tuples_in/2 · type_error/2 · type_error/3

U: ugraph_union/3 · unify_with_occurs_check/2 · union/3 · unsetenv/1 · uppercase/2 · uuid_string/2 · uuid/3 · uuidv4_string/1 · uuidv4/1

V: var/1 · variant/2 · vertices_edges_to_ugraph/3 · vertices/2

W: weighted_maximum/3 · when_si/2 · when/2 · working_directory/2 · write_canonical/1 · write_canonical/2 · write_term_to_chars/3 · write_term/2 · write_term/3 · write/1 · write/2 · writeq/1 · writeq/2

Z: zcompare/3

Predicate reference — Symbols

Predicate reference — A

Predicate reference — B

Predicate reference — C

Predicate reference — D

Predicate reference — E

Predicate reference — F

Predicate reference — G

Predicate reference — H

Predicate reference — I

Predicate reference — J

Predicate reference — K

Predicate reference — L

Predicate reference — M

Predicate reference — N

Predicate reference — O

Predicate reference — P

Predicate reference — R

Predicate reference — S

Predicate reference — T

Predicate reference — U

Predicate reference — V

Predicate reference — W

Predicate reference — Z

40. Running EyeProlog: command line and corpus

The command line keeps the program fixed and lets you choose what to observe: answers, the proof behind them, portability warnings, or search statistics.

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: answers and proofs on stdout, diagnostics on stderr, and an exit status for the calling process.
eyeprolog
eyeprolog [options] [file-or-url.pl|- ...]

Interactive queries

Run eyeprolog without arguments to enter the interactive top level. A query may span several lines and ends with a full stop, as in Scryer Prolog:

?- use_module(library(lists)).
   true.
?- member(X, [prolog, logic]).
   X = prolog
;  X = logic.
?- halt.

Answer control. When another answer may exist, press ;, Space, or n to ask for it; no Return is needed. Return or . stops, a enumerates all remaining answers, f advances to the next five-answer boundary (5, 10, 15, … answers shown, however many were stepped through individually), and h shows this help. Enumeration is demand-driven: after an answer, the top level does not run a later branch, or any side effect in it, just to learn whether that answer was the last. Search that could perform an effect starts only when you ask to continue. Stopping closes any active call_cleanup/2 or setup_call_cleanup/3 protection exactly once. Because a pending choicepoint is not explored early, asking for one more answer can end in false..

In scripted, non-TTY input, a new query line stops the preceding enumeration without being consumed; an explicit ;, n, Space, a, or f still asks for more. After the reader accepts a complete query, the next line starts with two spaces while it runs and a third when the result is ready to format. The answer prompt ; has no trailing space while it waits; after an advance command, one space marks active search and a second an answer ready to format.

While a query runs, EyeProlog releases readline’s terminal signal handling, so Ctrl-C ends the process immediately and, on POSIX terminals, Ctrl-Z suspends it. These are top-level conventions, not ISO/IEC 13211-1 features.

Answer display. A query with no solutions prints false.. A solution without visible bindings prints true. only when no residual goals remain. Residual constraints are part of the displayed answer even when the attributed variable was created inside a called predicate and is not a visible query variable; the top level names such variables _A, _B, and so on. With ffalse :- freeze(_, false)., the query ffalse. displays freeze:freeze(_A, false)., and call_residue_vars(ffalse, Vs). displays Vs = [_A], freeze:freeze(_A, false)..

Bindings are written as valid Prolog under the current operator table. When a value would not be a valid right operand of =/2, it is parenthesized: T = (a = b)., not T = a = b.. When an answer ends in a graphic token, a space precedes the final full stop so the two cannot merge: ?- X = .* . displays X = .* ..

Consulting. [file]., ['file.pl']., and consult(file). load local source; reconsult(file). is an accepted alias. For an extensionless name the top level tries file.pl before file. Consulting has modern reconsult semantics: loading the same resolved file again replaces its previous clauses, so clauses deleted from the file disappear. [user]., consult(user)., and reconsult(user). read source from the terminal until end_of_file. or end of input. halt. or halt(Status). leaves the top level.

Reading from the terminal. When read/1-2 or read_term/2-3 reaches interactive user_input, the top level prompts with |: for the next full-stop-terminated term. The request happens at execution time, so several reads in one goal, or reads inside called predicates, each prompt separately:

?- read(X), read(Y).
|: hello.
|: world.
   X = hello, Y = world.

Ctrl-D at an empty |: prompt makes that read return end_of_file without leaving the top level. The prompts and this end-of-file convention are host behavior; the terms themselves are parsed by the same ISO term reader used for every text stream. Up and Down recall earlier queries in the session, and eyeprolog -h prints command-line help.

Selecting goals

A source file states facts, rules, and directives; the command line chooses what to solve. Pass a callable goal with -g or --goal:

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

Repeat the option to ask several questions in one run. Goals are answered grouped by predicate, in the order the predicates first appear in the source, and in the order given within one predicate, so a program’s answers come out in the same order however its goals are listed. --quiet suppresses the answer terms while keeping Prolog output such as write/1, which suits command-style goals.

A program can also carry its own question, either as an ISO query or as the same query in a comment:

?- ancestor(ada, Who).      % run by this and any other ISO processor
%% ?- ancestor(ada, Who).   % run by this one, invisible to the rest

Without -g or --goal, the CLI runs the queries it finds in the sources, in source order; an explicit goal option overrides them.

Both spellings are extensions in the sense of 7.7.3: “the method by which a user delivers a goal to the Prolog processor shall be implementation defined”. A Prolog text (6.2.1) contains only directives and clauses, and the standard’s query (3.143) is top-level input that a processor need not support. The two spellings differ in who else runs them. Nearly every Prolog accepts a ?- term as a goal, so a program written that way runs in most engines, although --iso-strict rejects it. A %% ?- comment is invisible to every other processor, which keeps a file portable to the external Prologs used by the conformance harness. The standard’s own way to put a goal in a text, :- initialization(Goal). (7.4.2.6), works as well. Prefer an external goal when a script, shell history, or API call should record which question was asked.

Option Meaning
-h, --help Show usage
-p, --proof Print a proof (clause/3 and step/4 facts) after the answers
--proof-detail abstract\|expanded Stop proofs at bundled library predicates, or explain through them; implies --proof
--check-proof File Check a saved proof against the input program without proof search; write condition/4, failure/3, obligation/3, and verdict/1 facts; - reads the proof from stdin; exit 2 when the proof is not valid. With --goal, the goals the proof answers
--strict-proof With --check-proof, forbid trusted boundaries
-d, --dialogue Play each answer out as a dialogue, the checker as opponent; write move/4, outcome/3, and obligation/2 facts
--evidence File Give the dialogue’s opponent the clauses of File, to counter an absence it can refute; implies --dialogue
--json With --check-proof, write the report as JSON
-q, --quads Run embedded quad tests and fail if any do not hold
--quiet Suppress answer terms; keep Prolog output and diagnostics
--iso-strict Restrict parsing and execution to ISO/IEC 13211-1:1995 + Corrigenda 1–3; reject EyeProlog extensions (including table and :+) and disable autoloading
--portable Enforce the EyeProlog/Trealla/Scryer interoperability profile
--no-autoload Disable bundled-library autoloading
-s, --stats Print solver and memory statistics to stderr
-v, --version Print the package version
-w, --warnings Print non-fatal portability warnings
-g, --goal Goal Solve a callable goal; may be repeated; overrides queries in the source
-- Treat the remaining arguments as inputs

Short flags combine, so -pw means -p -w. Note that -q is --quads; --quiet has no short form.

--iso-strict cannot be combined with --quads, because quads and their infix (?-)/2 form are an EyeProlog testing extension. Strict mode keeps the Part 1 prefix (?-)/1 operator and reads -->/2 as an ordinary operator; it does not expand grammar rules or provide phrase/2-3. It also rejects Part 2 module directives and EyeProlog libraries, and has neither the occurs_check flag nor the table declaration. Normal mode supports Parts 2–3, the EyeProlog extensions, and autoloading of the bundled src/lib/ exports.

Inputs may be local files, HTTP(S) URLs, or a single - for stdin. Bare eyeprolog starts the normal REPL and eyeprolog --iso-strict the strict one. Other options without a named input read stdin, but because the strict-only invocation is reserved for the REPL, write eyeprolog --iso-strict - to read strict source from stdin. Several sources are parsed as one program, and a relative include/1 resolves from the including file’s directory.

eyeprolog --iso-strict --goal 'p(X)' program.pl
eyeprolog --iso-strict
printf 'p(a).\n' | eyeprolog --iso-strict --goal 'p(X)' -

A reproducible run

Observe one thing at a time:

  1. predict the answers, then run without observation flags and compare;
  2. add --proof when the support for an answer is the question, and save the proof and use --check-proof when it must cross a process or review boundary;
  3. add --warnings for portability or negative-dependency questions, and --portable when non-profile dependencies should fail CI;
  4. add --stats only to compare two runs of the same case.
eyeprolog --goal 'ancestor(X, Y)' examples/ancestor.pl
eyeprolog --proof --goal 'type(X, Y)' examples/socrates.pl
eyeprolog --proof examples/socrates.pl > socrates.why.pl
eyeprolog --check-proof socrates.why.pl examples/socrates.pl
eyeprolog --warnings --goal 'answer(X)' test/conformance/warnings/negation/unstratified_mutual.pl
eyeprolog --portable --goal 'sudoku9(S)' examples/clpz-sudoku-9x9.pl
eyeprolog --stats --goal 'path(a, X)' examples/path-discovery.pl > answers.pl 2> run.stats

Answers and proofs go to stdout, so the output can serve as a golden file or as input to another run. Warnings and statistics go to stderr and never mix into that stream. A successful run exits with status 0; loading, syntax, option, and other uncaught errors exit with 1. A program can choose its own status with halt/0-1. --check-proof exits with 2 when the checked proof is not valid, after writing its report.

Statistics are only meaningful in comparison. Keep the program, input, runtime version, query, answers, and counters together, and accept an optimization only when the answers are unchanged and the measure improves on the case that matters.

Embedded quad tests

A quad places a query directly before a description of its expected answer. The description is ordinary Prolog syntax, not quoted text, so a test reads like the interaction it checks:

color(red).
color(green).

colors ?- color(X).
   X = red
;  X = green.

?- color(blue).
   false.

Run the quads in a file with eyeprolog --quads file.pl or eyeprolog -q file.pl. The syntax follows the “queries using answer descriptions” convention of Trealla and the ISO Prolog working examples.

Labels and layout. A label such as colors is optional. It is the ordinary first argument of (?-)/2, so it may be any term, including several comma-separated metadata fields (9, "case", passes ?- Goal.), but it must be ground when the quad runs; a non-ground label is reported as a failure rather than a parse error. Recognition happens after ordinary parsing, so ?-(Label, Query). and Label ?- Query. are the same quad. Descriptions are layout-sensitive: indent each one, and keep clause heads and the next query at the left margin.

Running. Loading a file only records its quads; it neither runs them nor adds them as clauses. A quad run prints a summary and exits with 1 if any description fails. Quad mode imports library(prologue), because the ISO working-example files call its predicates as system predicates, and uses unknown=error unless the source sets the flag, so an undefined predicate is reported instead of silently failing.

Description language.

?- dif(X,Y), X = a.
   true, unexpected.
   X = a, unexpected.
   X = a, maybe.
   maybe, unexpected.

Each indented description after a query is an independent check: it re-runs the query, is counted in the quads: summary, and does not hide later descriptions when it fails.

Approximate floats. V ~~ '14.2000' accepts a float in the closed decimal interval 14.19995 to 14.20005. The right-hand side is a decimal atom so that trailing zeroes keep their meaning; exponent notation such as '1.42000e1' works the same way. An integer never matches, and a numeric right-hand side such as V ~~ 14.2000 is rejected because parsing it would discard the written precision.

?- V is 0+(3.2+11).
   V ~~ '14.2000'.

~~ is a normal-profile operator (priority 700, xfx, like =); there is no ~~/2 predicate. An approximation is well-formed only when its interval holds at least three distinct finite floats: the lowest, the one nearest the written midpoint, and the highest. This rejects spellings that claim more precision than a float can carry. Endpoints are rounded inward, so binary rounding can never admit a float that lies outside the decimal interval.

Input and output. inputs/1 supplies exactly the characters the query must consume. peeks/1 adds one character that may be looked at but must remain unread. A sentinel follows the declared input, so a reader cannot use an artificial end of file to decide that a full stop ends a term:

?- read(X).
   inputs("1."), X = 1, unexpected.
   inputs("1."), peeks(" "), X = 1.
   inputs("1. "), peeks(" "), X = 1, unexpected.

outputs/1 checks the characters written while reaching the described answer or error, including output emitted before a later exception. Its argument is a character list or string, or a DCG body with terminals, conjunction, disjunction, .../ad_infinitum wildcards, and user-defined nonterminals.

Unordered answers. Appending | other_answer_sequence accepts any permutation of the preceding complete answer sequence. Substitutions, residue, per-answer output, and duplicate counts must still match, and a final failure or exception stays last. Overlapping wildcard or approximate descriptions are matched one-to-one. Prefix (...), unexpected, STO, and input annotations are not allowed in a permuted sequence. For setof(1, (Y=2 ; Y=1), L), the description Y=2, L=[1] ; Y=1, L=[1] | other_answer_sequence accepts either group order.

STO, loops, and undecided results

sto, following Trealla’s convention, declares that a query is subject to occurs check. EyeProlog checks this conservatively. During the ordinary run, a concrete occurs-check event in the unifier is positive evidence; the query is not run again just to probe. A finite run that ends without such an event disproves sto, while a run cut short by a search or resource bound leaves it unchecked. The answer part of an sto leaf is implementation-dependent and is not compared, and when STO evidence is observed an unannotated unexpected leaf does not reject the finite-tree outcome. EyeProlog states a result only where execution gives definite evidence.

?- X = s(X).
   X = ..., unexpected.
   false, unexpected.
   sto, false
|  sto, true.

?- true.
   sto.                  % fails: no STO evidence

loops is distinct from running out of budget. EyeProlog accepts structural nontermination evidence, such as an active-variant recursion cycle, with depth and inference bounds as a fallback. A structural cycle also refutes a false description.

inf :- inf, inf.

?- inf.
   loops.

Ordinary descriptions have an inference budget (100000 by default). Exhausting it neither establishes loops nor turns an unfinished search into false; the description is reported as undecided:

quads: UNDECIDED expensive_case, program.pl:12
   undecided: inference limit reached.

A quad run therefore has three outcomes: passed, failed, and undecided. With no failures but at least one undecided description, the CLI exits with status 2. The JavaScript API exposes the same operation without process I/O; quadMaxInferences overrides the search budget, and loopMaxDepth and loopMaxInferences bound the loops probe:

import { Program, runQuads } from 'eyeprolog';

const program = Program.parse(source);
const report = runQuads(program);
console.log(report.passed, report.failed, report.undecided, report.stdout);

Further examples

A map connects EyeProlog examples across mathematics, search, planning, policy, science, program analysis, and symbolic systems.
Every program in the corpus leads from readable source to an answer, the reason for it, and the check of that reason.

The examples directory is the book’s executable companion. Its top-level directory contains 239 self-contained runnable programs. Every program has an exact answer file under examples/output, and 239 programs have a checked explanation under examples/proof, with the result of that check under examples/check. So each example comes in three parts, making three different claims:

A check result is itself ordinary Prolog: condition/4 for each of the seven conditions, failure/3 for anything that did not hold, one obligation/3 for each conclusion the check rests on rather than establishes, and verdict/1. npm test re-checks every proof, re-performing each recorded inference against its source clause and recomputing each primitive the proof asserts.

examples/book/ holds the inline EyeProlog displays, chapter by chapter. They are parsed and their declared goals run, but some depend on facts from the surrounding text; use the top-level examples for self-contained programs with golden answers.

To study an example, predict its answers from the declared queries, run it, compare with the golden output, then read the proof and change one fact:

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

A selection, grouped by theme:

node test/run-examples.mjs runs every answer and proof golden; npm test runs the whole correctness corpus, and its elapsed time doubles as the project’s performance indicator. A new example should name its idea in the filename, open with a comment stating the lesson and the model’s boundary, keep its queries finite and its output small, include a positive and a boundary case, and come with its answer, proof, and check files.

Exercises.

  1. Run one example with --proof --stats. Which output is the reusable logical result, which describes this particular run, and which status does a calling process see? Change one fact and predict all three before rerunning.
  2. Save the proof of examples/socrates.pl and check it with --check-proof. Delete the step for type(socrates, man) and check again; then restore it and delete the step for type(socrates, mortal) instead. Why does only the second deletion fail, and which conditions report it?
  3. Write a three-quad test file for ancestor/2 with one ordered answer sequence, one false. description, and one labelled quad, and run it with --quads.

41. Standards, limits, and implementation boundaries

This book is the single reference for the EyeProlog implementation. Chapters 38–40 define its ISO Prolog syntax, directives, execution model, built-in predicates, and command line; the earlier chapters cover the reasoner, tabling, proofs, warnings, answer formatting, embedding, and data boundaries.

Conformance evidence

The file-based corpus under test/conformance/ covers success, failure, errors, warnings, proofs, and file loading:

node test/run-conformance-all.mjs
node test/run-iso-strict.mjs
node test/run-conformance-report.mjs

The file-based conformance corpus contains 905 cases, including 479 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 every example’s answer, proof, and proof check, and every chapter display is parsed with its declared goals run. The playground suite drives the production worker through its message protocol and crawls the served module graph for missing assets, wrong MIME types, and static Node-only imports (node test/run-playground.mjs).

The review documents are:

WG17 syntax cases are discovered live, not taken from a vendored snapshot; a small offline file (test/conformance/wg17-syntax-cases.json) pins reviewed strict-reader outcomes for most of them, and every case is checked against the upstream expectation. Each case the strict reader accepts is also run in the normal profile and must give the same result: extensions may accept more texts, but may not reinterpret a standard one.

The supported profile

The strict-core target is ISO/IEC 13211-1:1995 with Technical Corrigenda 1–3. Normal mode adds the module compatibility surface, a Part 3-oriented definite-clause grammar, and the EyeProlog extensions. Chapter 39 lists every supported predicate indicator. The normal profile covers control and exceptions, term operations, arithmetic, grouped solutions, dynamic clauses, operators, atomic terms, flags, character conversion, streams, character, byte, and term I/O, initialization, source inclusion, modules, and grammar rules.

--iso-strict (API option isoStrict: true) limits the processor to the Part 1 baseline. Corrigendum 2 additions such as subsumes_term/2, acyclic_term/1, sort/2, keysort/2, term_variables/2, retractall/1, and call/2-8 belong to that baseline. Modules, grammar-rule expansion and phrase/2-3, quads, libraries, the occurs_check flag, table, call_cleanup/2, and setup_call_cleanup/3 do not.

The strict-core review gives explicit dispositions for the Clause 5 processor obligations, Clause 6 syntax, Clause 7 term, execution, I/O, and error semantics, the 8.2–8.17 built-in families, and the Clause 9 evaluable functors. Implementation-defined choices, among them the Unicode-scalar character set, stream details, flag defaults, floating-point behavior, and signed bitwise and shift semantics, are indexed in ISO-IMPLEMENTATION-DEFINED.md. This is executable evidence for a documented boundary, not independent ISO certification.

Notable boundaries:

Security and resource use

EyeProlog has no general host-call primitive, but an untrusted theory is still executable input: it can request enormous finite searches or build unbounded terms, and URL inputs cross a network and trust boundary. Restrict accepted sources and impose limits on input size, time, depth, memory, and solutions. Proof output can be much larger than the answers and needs its own budget.

42. Glossary and notes

References

These sources give historical and technical background. They describe larger languages and theories and are not EyeProlog specifications.

Glossary

Aggregate. A predicate that runs a finite nested search and combines its solutions, such as findall/3, countall/2, sumall/3, aggregate_min/5, or aggregate_max/5.

Answer. A ground instance of a query goal produced by successful search. EyeProlog does not print duplicate answers or answers identical to source facts.

Answer set. The distinct answers to a query, regardless of order or number of proofs.

Arity. The number of arguments of a predicate or compound term. edge/2 and edge/3 are different predicates.

Atom constant. A symbolic constant such as alice or 'a quoted atom'. It is data; an atomic formula uses a predicate name as a proposition.

Atomic formula. A callable proposition such as ready or parent(ada, byron).

Base case. A nonrecursive clause that ends a recursion.

Binding. An association between a variable and a term, made by unification.

Binding pattern. Which arguments of a call are bound, unbound, or partly structured when it is called. See mode.

Body. The goals to the right of :- in a rule; all must succeed for the rule to apply.

Built-in. A predicate implemented by the system rather than by source clauses. Many built-ins accept only certain modes.

Call. A goal selected for solving, with its current bindings.

Canonical form. One chosen representative for a class of equivalent values, so that equivalence can be tested by structural equality.

Choicepoint. A remaining alternative that may yield another answer if the caller asks for more. The engine never runs an unrequested branch or effect to find out whether one exists.

Cleanup. A goal installed by call_cleanup/2 or setup_call_cleanup/3 that runs exactly once when the protected goal completes, is cut, is abandoned, or raises an exception.

Clause. A fact or rule, terminated by a full stop.

Closed-world assumption. Treating failure to derive a claim as evidence that it is false. \+/1 implements negation as failure; the modeler must justify the scope in which that is sound.

Compound term. A term with a functor and one or more arguments, such as point(3, 4).

Conformance corpus. The executable cases under test/conformance/ that define the supported profile.

Conjunction. Goals joined by commas, normally solved left to right.

Constraint. A goal that restricts the values of its variables. Delayed constraints such as dif/2, freeze/2, and CLP(Z) constraints remain as residual goals until they are decided.

Declarative reading. What the ground instances of clauses mean, independently of search order.

Definite clause. A clause with one positive head and a conjunction of positive body goals. Definite programs have a least Herbrand model.

Dependency graph. A graph of predicates with an edge from caller to callee. Recursive predicates form its cycles.

Fact. A clause with no body, such as parent(ada, byron).

Failure. The absence of a solution along the current branch. It makes the search try alternatives; it is neither an exception nor a stored negative fact.

Finite domain. An explicitly bounded set of candidates that a search can exhaust. Finiteness belongs to a call and its generators, not to a predicate name.

Fixed point. The stage at which repeated derivation adds no new answers.

Functor. The name and arity at the root of a compound term: point/2 in point(3, 4).

Generator. A goal that produces candidate bindings from facts, lists, or bounded ranges.

Goal. An atomic formula or control construct the solver is asked to prove.

Golden file. Checked expected output stored in the repository: answers, proofs, or proof checks.

Ground. Containing no variables. The CLI prints only ground answers.

Head. The atomic formula left of :-, or the whole of a fact.

Herbrand base. All ground atomic formulas built from a program’s predicate symbols and Herbrand universe.

Herbrand interpretation. A subset of the Herbrand base, taken as the true atoms.

Herbrand universe. All ground terms built from a program’s constants and function symbols.

Host goal. A goal supplied by the CLI or the embedding API to select which answers to observe.

Indexing. Selecting candidate clauses by bound arguments, without changing the answers.

Integrity check. An ordinary predicate whose answers identify invalid input; the host decides what to do with them.

Least Herbrand model. The smallest Herbrand interpretation satisfying a definite program, reached by repeatedly adding supported ground consequences.

List. Either [] or [Head | Tail] where Tail is a list. A partial list ends in a variable, as in [X,Y|Xs]; a variable alone is also a partial list. [X,Y|non_list] is an instance of a partial list that is not a list.

Mode. An intended direction of use: which arguments are supplied and which are produced.

Negation as failure. \+ Goal succeeds when a terminating search finds no solution for Goal.

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.

Operational reading. How a clause directs computation: which goal is selected, which bindings it needs and makes, and which alternatives it leaves.

Predicate indicator. A predicate name with its arity, written name/arity.

Proof. A successful derivation showing which clauses, facts, and built-ins support an answer. It records success, not failed branches.

Proof tree. The tree of subgoals supporting one derivation, without the failed alternatives of the search tree.

Proper list. A finite list whose final tail is [].

Readiness. The binding condition under which a mode-sensitive built-in can run safely.

Recursion. A predicate depending on itself, directly or through others.

Relation. The set of tuples for which a predicate holds.

Resolution. The step that unifies a goal with a clause head and replaces the goal by the instantiated clause body.

Rule. A clause with a head and a body: Head :- Body.

Search tree. All alternatives explored while seeking answers, successful or not.

Source fact. A fact present in the loaded input, as opposed to a derived conclusion.

Stratified negation. Negative dependencies arranged in layers, so that no predicate depends negatively on itself.

Substitution. A mapping from variables to terms, applied consistently throughout a term or clause.

Tabling. Evaluation that shares calls and accumulates their answers up to a fixed point.

Term. An atom, number, variable, or compound term. Double-quoted text denotes a list or atom according to the double_quotes flag.

Termination measure. A value in a well-founded order that strictly decreases on every recursive call in a stated mode.

Theory. The facts and rules loaded together, read as claims about a domain.

Unification. Solving an equation between two terms by finding a substitution that makes them identical.

Variable. A clause-local name beginning with an uppercase letter or underscore. Each _ is a fresh variable.

Variant. A term identical to another up to consistent renaming of variables. Tabling recognizes variant calls.

Witness. A ground term demonstrating an existential claim: a path, an assignment, a factorization, a schedule.

Historical note: manuals become specifications

Early Prolog programmers learned from implementation manuals, examples, and books whose descriptions were often inseparable from one particular system. As the language spread, reference writing acquired a second task: telling the portable language apart from implementation convention. Predicate indexes, precise mode and error descriptions, and standards documents became tools for comparing systems rather than merely operating one of them.

Standardization made that distinction explicit, and conformance suites such as Ulrich Neumerkel’s ISO conformity assessment made many disagreements between systems executable. A mature reference therefore joins several kinds of evidence: normative prose, named predicates and flags, examples, implementation boundaries, and reproducible tests. It is not a substitute for programming practice; it is a map from a concrete question to the contract that governs it.

Part X — Laboratories

43. Laboratories

Each laboratory asks for a working artifact, states when it is done, and ends with one question worth answering in writing.

Twelve laboratories progress from relational foundations through finite search, mathematical and symbolic methods, domain reasoning, and a release-quality reasoning service.
The laboratories apply one discipline at growing scale: state meaning, control a finite computation, preserve evidence, name the boundary, and finally integrate all four.

Laboratory 1. A family theory

Chapters 1–5. Facts for at least six people; relations for parent, sibling, grandparent, and cousin. State the reading and modes of each predicate, include a branch with several cousins, query in both directions, and add an integrity relation that reports anyone recorded as their own parent.

Done when the output matches your prediction and one cousin proof passes through named intermediate relations. Reflect: which conclusions depend on absence, and is that closed-world assumption justified?

Laboratory 2. A relational list toolkit

Chapters 1–5. Your own membership, concatenation, reversal, and prefix relations, written with facts, rules, and list syntax only. Document each finite mode and test empty, singleton, proper, and partial lists.

Done when bounded queries comparing each relation with its library counterpart find no disagreement in either direction. Reflect: which logically meaningful modes fail to terminate?

Laboratory 3. A cyclic transport network

Chapters 6–10 and 13. At least ten stations with cycles, weighted edges, and two disconnected components. Derive reachability, construct simple paths, and pick a least-cost path with deterministic tie-breaking. Test a cycle, an unreachable pair, and equal-cost routes, and compare --stats before and after one justified control change.

Done when every path starts and ends at the queried stations, uses known edges, and repeats no station. Reflect: why can reachability be tabled finitely when the set of walks is infinite?

Laboratory 4. A finite puzzle

Chapters 6–10. A small Latin square, schedule, or house puzzle. Separate generation from constraints, remove at least one symmetry, return a structured witness, and predict the size of the naive and reduced search spaces.

Done when every intended solution appears exactly once, with no permuted duplicates. Reflect: which line of the program does the most pruning?

Laboratory 5. Arithmetic by construction

Chapters 19 and 26–29. Peano addition and multiplication, plus one of exponentiation, comparison, division with remainder, or factorial. State a termination measure for each mode, prove one property by induction on paper, and add a bounded executable test of the same property.

Done when the proof and the program visibly share their base and recursive cases. Reflect: what does the bounded test establish that the proof does not, and the other way round?

Laboratory 6. Counterexamples

Chapters 26–29. Operation tables over carriers of two or three elements. Test closure, identity, commutativity, and associativity, searching for a counterexample before confirming a law, and return each offending tuple.

Done when a nonassociative table is rejected with a specific triple and a group table passes every law. Reflect: why does one counterexample settle a question that a thousand confirmations cannot?

Laboratory 7. A symbolic language

Chapters 19 and 26–29. An expression language with literals, variables, addition, conditionals, and local bindings, represented as terms and evaluated under an explicit environment. Add a size measure and a constant-folding transformation.

Done when folding is idempotent on your test corpus and never changes an evaluated result. Reflect: where does Prolog syntax end and the object language begin?

Laboratory 8. A static analyzer

Chapters 14, 25, and 31–33. A sign, nullness, taint, or permission analysis for a tiny statement language. Define a finite abstract domain and its join, propagate to a fixed point, and report both safe conclusions and warnings. Include one concrete execution that illustrates an abstract result.

Done when every tested concrete behavior is covered by its abstract result and the chosen unsafe case is never missed. Reflect: why is a warning not proof that a failure can occur?

Laboratory 9. An auditable policy

Chapters 14, 25, and 31–33. An access, consent, eligibility, or compliance theory with separate layers for sources, normalized concepts, decisions, and reasons. State every closed-world assumption, add three integrity relations, record source and theory versions, and keep checked proofs for one permit and one denial.

Done when changing one source fact changes exactly the predicted decision and its proof. Reflect: which trust claims does the derivation establish, and which need authentication outside the theory?

Laboratory 10. A scientific model

Chapters 14, 25, and 31–33. A compact model from mechanics, circuits, chemistry, epidemiology, or statistics. Document every quantity and unit, expose intermediate quantities, include valid, boundary, and invalid scenarios, and state the floating-point assumptions.

Done when the proof of the final classification shows measurements, equations, and thresholds in a readable order. Reflect: what has been proved conditionally, and which empirical claim lies outside the logic?

Laboratory 11. An input boundary

Chapters 15–16. Validate a small external record in JavaScript, convert it to Prolog facts, and derive one new relation. Keep conversion code apart from the rules, run the generated program with EyeProlog directly, and document what the host authenticates.

Done when invalid records are rejected before solving and the answer for a valid one matches a checked golden with its proof. Reflect: which claims belong to host validation and which to the derivation?

Laboratory 12. A reasoning service

Chapters 16, 25, and 31–33. An embedded service that loads facts through a JavaScript boundary, validates them, and answers with proofs. Test the modes and solution counts of its public predicates with semantic cases, bounded properties, metamorphic tests, integrity queries, proof goldens, and one scale case. Keep source snapshot, theory version, and proof with every result, state time, memory, and proof-size budgets, and write one page each on what the service guarantees and what it does not.

Done when someone else can clone the repository, run one command, and reproduce every answer and proof without help. Reflect: if the service makes a wrong real-world decision, which layer (source, model, engine, or derivation) would reveal the fault?

Reviewing a laboratory

Judge each project on five independent axes:

Axis Strong work shows
Meaning every public relation has one clear sentence
Logic the clauses derive the intended answers and reject counterexamples
Control each supported mode terminates for a stated reason
Evidence tests, witnesses, and proofs show why results hold
Boundary sources, assumptions, versions, limits, and host duties are named

Selected answers

Unification (Chapter 2). point(X, X) unifies with point(red, red) by binding X = red, but not with point(red, blue): one variable cannot be two different atoms. [Head | Tail] unifies with [a, b, c] with Head = a and Tail = [b, c].

Goal order (Chapter 3). In eligible/1, age(Person, Years) binds Years before Years >= 18 compares it, and registered(Person) then checks the person already chosen. Moving the comparison first leaves the meaning unchanged but makes >=/2 raise an instantiation error.

Appending (Chapter 5). joins([a], [b, c], Whole) uses the recursive clause once, binding Whole = [a | Zs], then the base clause binds Zs = [b, c]. With only Whole = [a, b, c] bound there are four splits: [] and [a, b, c], [a] and [b, c], [a, b] and [c], [a, b, c] and [].

Negation order (Chapter 7). user(U), \+ blocked(U) asks, for each known user, whether that user is blocked. \+ blocked(U), user(U) first asks whether nobody is blocked, which is a different question. Either reading of “allowed” still assumes a complete record of users and blocks.

Empty aggregates (Chapter 8). Over a search with no solutions, findall/3 gives [], countall/2 gives 0, and sumall/3 gives 0; aggregate_min/5 and aggregate_max/5 fail, since there is no best element. Finiteness must come from the inner goal, not from the aggregate.

Mathematical claims (Chapters 26–30). A witness proves existence. A counterexample refutes a universal claim. Exhausting a finite carrier proves a property of that model only. Any number of bounded confirmations does not make an unbounded theorem.

Laboratories. A finished answer is an artifact, not a paragraph: a source file, the predicted output, the actual output, and one sentence explaining any difference.

Historical note: logic programming grows through exercises

Logic programming has long been taught by construction. Lists, family relations, puzzles, grammars, interpreters, search problems, and small expert systems became recurring exercises because each exposes both a logical relation and the control needed to compute with it. Clocksin and Mellish’s Programming in Prolog (1981), Bratko’s Prolog Programming for Artificial Intelligence (1986), and Sterling and Shapiro’s The Art of Prolog (1986) made this dual reading the core of teaching: an exercise was not finished when a clause parsed, but when its meaning, modes, and behavior could be explained.

Laboratory practice later absorbed regression testing, property-based checking, benchmark corpora, and reproducible command-line runs. These tools fit logic programming unusually well, because a small change can be examined at several levels at once: answers, failures, witnesses, proofs, and search. The laboratory is where a declarative claim becomes an executable experiment.

This site is open source. Improve this page.