# Why EyeProlog?

Many systems can apply rules to data. The harder questions are whether people
can understand those rules, whether another implementation can run them, and
whether a conclusion can be traced back to the facts and rules that produced
it.

EyeProlog is a small, inspectable ISO Prolog implementation for JavaScript. It
turns facts and rules into answers, and it can show a proof for each answer. Its
aim is not to invent a new reasoning language, but to make a mature standard
practical in command-line tools, applications, and browsers.

Its design rule is simple:

> **Keep the ISO language core explicit and auditable, keep extensions small
> and visible, and implement portable conveniences as ordinary Prolog whenever
> possible.**

## A shared language for facts and rules

Prolog describes knowledge through relations. A program can state facts such
as “Socrates is human,” define a rule saying that every human is mortal, and
then ask whether Socrates is mortal. Variables, unification, and search let the
same rule answer more general questions without turning it into a sequence of
manual data-processing steps.

This relational style is useful well beyond textbook examples. It can express
graph reachability, policy decisions, validation rules, parsers, schedules,
constraints, and explanations. Because the program says what relationships
must hold, its logical structure remains visible to readers and tools.

## Close to the explicit surface of human reasoning

Prolog's attraction is not only standardization. Among widely used computational formalisms, it is arguably unusually close to the *explicit, communicable* surface of human cognition: facts resemble assertions, rules resemble reusable generalizations, queries resemble questions, variable bindings fill in answers, backtracking considers alternatives, and proofs give reasons.

That is not a claim that the brain literally executes Prolog. Human cognition includes perception, emotion, embodiment, analogy, learning, uncertainty, and many processes that Horn-clause reasoning does not model. The narrower engineering point is powerful enough: when people externalize what they know and why they think something follows, Prolog preserves those objects of thought directly instead of hiding them behind imperative state changes or opaque vectors. That makes it a strong reasoning layer for systems in which humans and machines must inspect and revise shared knowledge together.

## Why the ISO standard matters

[ISO/IEC 13211-1](https://www.iso.org/standard/21413.html) defines Prolog's
general core: terms, variables, unification, clauses, recursion, arithmetic,
control, streams, errors, and processor behavior. That published foundation
gives programmers a common vocabulary and gives implementations an external
reference against which behavior can be tested.

Standards do not make every implementation identical, but they sharply reduce
the number of hidden choices. A portable Prolog rule is not tied to one product,
one JavaScript API, or one project-specific syntax. It can be studied in books,
compared across conforming systems, and preserved independently of the engine
that happens to run it today. This is especially important for knowledge and
policy rules, which often need to remain understandable longer than the
application that first used them.

EyeProlog therefore starts with ISO Prolog and labels its additions. Normal
mode provides practical libraries, modules, definite clause grammars, tabling,
and embedding facilities. Strict mode removes EyeProlog-specific language
extensions so the standardized core can be tested on its own. The distinction
keeps convenience from quietly redefining the language.

## Small enough to inspect, useful enough to embed

A language standard is most valuable when the implementation can be examined
and tested against it. EyeProlog keeps a narrow architecture: one parser and
term model, one solver, an explicit built-in registry, portable Prolog library
modules, and optional proof generation. The same implementation runs in Node.js
and browser workers.

Common relations such as list processing remain Prolog clauses imported with
`use_module/1-2`. Sorting, arithmetic, meta-calls, streams, and database
operations use their ISO definitions directly. JavaScript is reserved for the
engine, host integration, and operations that genuinely belong at the runtime
boundary.

Internally, focused JavaScript modules handle parsing, static analysis, clause
indexing, arithmetic, errors, and cleanup lifecycles. Performance-critical
execution paths remain direct rather than being hidden behind layers added only
for architectural appearance. [`src/ARCHITECTURE.md`](src/ARCHITECTURE.md)
records these boundaries, and an automated test rejects import cycles.

## Visible choices instead of hidden semantics

Some useful reasoning behavior lies outside the ISO Part 1 core. EyeProlog
keeps those choices explicit in the program or execution profile.

Ordinary Prolog `\+/1` is negation-as-failure. It is useful when a closed,
usually stratified relation has already been computed, but non-stratified rule
systems need a different semantic choice. Normal mode therefore provides
`tnot/1` for finite, range-restricted, function-free Datalog components that
need three-valued well-founded semantics. EyeProlog does not silently change
the meaning of `\+/1`, and strict ISO mode does not expose `tnot/1`.

EyeProlog keeps tabling explicit. A predicate uses ordinary depth-first Prolog
control unless its source declares `:- table p/n.`; declared tables may then use
shared finite-Datalog evaluation and other indexing optimizations internally.
This avoids a heuristic silently changing answer multiplicity, termination, or
resource behavior for an otherwise ordinary recursive predicate.

Forward chaining is explicit too. Normal mode recognizes `Conclusion :+ Premise`
and executes those rules with the Prolog fixed-point driver in the bundled
`library(eyelet)`. That module owns the forward-rule semantics—rule selection,
fixed-point iteration, skolemization, `stable/1`, `becomes/2`, and the
`true :+ Goal` / `false :+ Goal` control conventions—rather than duplicating the
reasoning algorithm in JavaScript. The remaining JavaScript support is limited to
syntax recognition, static dependency/autoload planning, driver bootstrap, and
private database-mutability/output-event adapters. Strict ISO mode removes the operator.
Because resource exhaustion is not logical failure, normal execution has no hidden
depth cutoff; an explicitly requested depth limit raises `resource_error(depth_limit)`.

Library convenience is explicit at the profile boundary too. Outside strict ISO
mode, an unresolved unqualified predicate may autoload its unique provider from
the bundled `src/lib/` modules after program definitions, standard built-ins,
and explicit imports have had precedence. `--no-autoload` disables this
convenience, and strict ISO mode disables it unconditionally. Autoloading happens
after parsing, so libraries that introduce operators still require an explicit
`use_module/1-2` before that syntax is read.

That compatibility boundary is intentionally driven by observable upstream
interfaces rather than by library names alone. The compatibility layer is now
systematic rather than a collection of one-off ports: all 33 bundled modules that
overlap Scryer's current `src/lib/` tree are checked against the frozen export
snapshot in `test/scryer-library-exports.json` and cover that public predicate
surface. Runtime-dependent primitives have explicit ownership: code in
`src/lib/foo.pl` is backed, when necessary, by `src/foo-host.js`, while pure Prolog
libraries need no host adapter. The completed surface includes character/UTF-8/term
and Base64 predicates, arithmetic helpers, the full Scryer `library(files)` API,
character-list paths in `library(pio)`, the `time` and `iso_ext` predicates, and
the full Scryer `library(crypto)` interface. The conservative Trealla/Scryer
intersection remains a separate portability profile; its crypto overlap is still
`hex_bytes/2`, `crypto_n_random_bytes/2`, and `crypto_data_hash/3`. Hashing, KDF,
authenticated encryption, Ed25519, and X25519 use Node's crypto backend; secure
random bytes also use Web Crypto when available, and unsupported operations
report `resource_error(crypto)`. Filesystem, environment, shell, PID, argument, and TCP socket operations are likewise Node host services rather than simulated browser facilities.
EyeProlog still has integer and float processor numbers only, so non-integral
rational conversion results use a documented structural `rdiv(N,D)` form rather
than silently extending arithmetic semantics.

Definite clause grammars follow the ISO Part 3 difference-list model. Internal
fast paths make deep finite sequence processing economical while preserving
relational modes. The checked
[`dcg-expression-language.pl`](examples/dcg-expression-language.pl) example
shows both directions: a grammar builds syntax trees from tokens, and another
generates minimally parenthesized tokens from syntax trees.

Resource cleanup follows Prolog search rather than ordinary JavaScript return.
A protected goal may succeed, fail, be cut, be abandoned while alternatives
remain, or unwind through an exception. Normal-mode `call_cleanup/2` and
`setup_call_cleanup/3` run cleanup exactly once across those exits. Keeping this
behavior tied to the actual search lifecycle also preserves demand-driven
interaction at the top level.

## Output, proof, and check

Giving an answer is good. Giving the reason for it is better. Giving a reason
that has been checked is better still — and the step from the second to the
third is longer than it looks.

A run can produce all three, and keeping them apart is the point.

The **output** is the answer: the goal succeeded, with these bindings. It is
what a program is usually asked for, and on its own it is a claim that has to
be taken on trust. Nothing about it says how it was reached, so nothing about
it can be disputed except by running something else and comparing.

The **proof** is why. It records one successful route through the supplied
clauses and built-ins as ordinary Prolog data — one `step/4` fact per justified
conclusion, naming the clause it used, the bindings that use made, and the
conclusions it rested on. Because it is data rather than a log, it can be
saved, sent to someone else, and read back later without the program that
produced it being present. A reader can now follow the reasoning instead of
trusting it, which is a real gain — but following it is still their work, and
a long derivation is not something a person checks by reading.

The **check** is whether that reason holds, decided mechanically. This is not
the same question as whether the proof is well written, and it is deliberately
not answered by the engine that produced the answer. A proof can be internally
flawless and still be wrong, which is exactly why the third step is worth more
than the second: it is the one that can come back and say no.

That last distinction is why checking is stronger than replaying. An
explanation is not verification: a convincing explanation can be produced for a
wrong result, so a check is only worth something if it is capable of
*disagreeing* with the answer it checks. A condition that cannot fail is not
much of a check.

`--check-proof` therefore tests seven conditions, specified in
[SPEC.md](SPEC.md). Five read the document against the program, and two, C5
and C6, also confront it with evidence the document did not supply:

- **C1 Resolution** — every checked step really is an instance of the clause it
  cites. The clause is taken from the program, not from the document, so a
  proof cannot be made valid by restating the rule it used.
- **C2 Well-founded** — following what a step used never leads back to it. A
  proof that rested on itself would prove anything.
- **C3 Justification** — every step carries exactly one known justification,
  in the shape that justification requires.
- **C4 Coverage** — every claim has a step, and every use resolves either to a
  step or to an instance of a fact the program gives.
- **C5 Re-decision** — a step the document only *asserts*, rather than derives,
  is computed again and must agree; a control step must be composed of its uses.
- **C6 Boundary consistency** — a `\+` or `findall/3` taken on trust is
  confronted with the program's facts and the document's own steps, and fails
  when they contradict it.
- **C7 Relevance** — every claim answers a goal that was asked, and every step
  serves a claim.

C5 is what makes the rest worth having. The largest class of steps in a typical
proof is the primitive: arithmetic, comparison, string and date operations that
no clause derives. Reading a document cannot tell whether those are true, so
they are run again — against a program holding the bundled libraries and
nothing else. No clause of the theory under proof is present, which means the
recomputation cannot be talked into agreeing by the very rules it is meant to
audit. When it disagrees, the proof fails.

The difference is not theoretical. A document can pass C1 through C4 completely
— every step a proper instance of its clause, every use accounted for, no
cycles — and still record a computed value that is simply false, so long as it
tells the same lie consistently throughout. Only recomputation catches that
one.

Some steps still cannot be recomputed, and the check says so rather than
quietly passing them. A **reflective** goal reads the theory's own database or
syntax, which is exactly what C5 excludes in order to stay independent of it. A
**stateful** goal — an attributed variable, a constraint store, an open stream —
depends on state the original run accumulated and a fresh solver has no way to
reconstruct; re-running stream operations would also perform I/O of its own,
and a checker must not have side effects. Deciding these in the library-only
program would pass them on the wrong evidence, which is weaker than admitting
they were trusted. They are named individually in the checker, counted
separately in the result, and reported as what the check still rests on rather
than what it establishes.

The packaged corpus makes the proportion visible. Every one of the 239
examples carries a proof: 213091 steps, of which 156944 are verified against
their source clause, 55460 are recomputed independently, 220 are carried by the
goals they wrap, and 467 — 0.2% — remain obligations, each one named; 53
trusted boundaries are confronted with evidence and none is contradicted. `npm test` re-checks all of them on every run, and the
proof directory is read from disk rather than from a list, so a document cannot
be added without being checked. An unverified proof is worse than none, because
it still looks like evidence.

Verification and discovery therefore have different jobs: solving searches for
a derivation, while checking verifies a supplied one. A proof does not
authenticate source data or replace application security. Embedders remain
responsible for validating inputs and imposing suitable time, memory, depth,
and solution limits.

## One engine across JavaScript environments

JavaScript makes EyeProlog available from a command line, server, test suite,
application, or browser worker. A newcomer can run a `.pl` file or experiment
in the playground. An application developer can call the convenience `run`
function. An advanced embedder can work directly with `Program`, `Solver`,
terms, environments, and a custom built-in registry.

This range does not require separate language variants. The same Prolog text
and the same reasoning engine cross those environments, which makes examples,
tests, and production behavior easier to compare.

## What the conformance claim means

EyeProlog targets the ISO Part 1 core together with Technical Corrigenda 1, 2,
and 3. It provides separately documented compatibility profiles for Part 2
modules and Part 3 definite clause grammars in normal mode. The post-N289
WG17/STC working draft is review input, not a published Corrigendum silently
added to the strict baseline.

The executable conformance matrix records explicit dispositions for the
Part 1 processor, syntax, semantic, built-in, and arithmetic requirements. It
includes the complete vendored WG17 syntax cases and verifies that successful
strict syntax remains successful across profiles. Implementation-defined
choices, including mixed-type `max/2` and `min/2` and signed bitwise and shift
operations, are pinned by regression tests.

The character model is also explicit: EyeProlog uses Unicode scalar values as
its processor character set and as collating-sequence integers in normal and
strict modes. Strict mode removes implementation-specific language extensions
without changing that processor choice.

This is extensive, executable implementation evidence, not independent ISO
certification. The Part 2 and Part 3 compatibility profiles likewise remain
separate from the Part 1 strict-core claim. Stating those limits is part of the
standards commitment: users should be able to tell which behavior comes from a
published standard, which comes from a compatibility profile, and which is an
EyeProlog extension.

## Who is EyeProlog for?

EyeProlog is intended for several audiences that benefit from the same visible
language boundary:

- learners who want a runnable logic language whose implementation and proofs
  can be inspected;
- application developers who need rules in Node.js or the browser without
  inventing an application-specific rule format;
- researchers and implementers who want executable conformance evidence and a
  compact engine suitable for comparison; and
- teams maintaining policies or knowledge rules that must remain reviewable,
  reproducible, and portable over time.

The project is deliberately not a database, a distributed query service, or a
replacement for host security. Those concerns belong in surrounding systems
with storage, access control, and operational limits appropriate to the
application.

## A focused direction

EyeProlog should improve by becoming more correct, portable, and economical,
not by accumulating unrelated subsystems. New capabilities should normally be
required ISO behavior, a small portable Prolog relation, or a narrowly
documented embedding hook.

It should resist duplicate aliases, hidden execution phases, advisory syntax,
and integrations that can live outside the reasoning engine. The durable idea
is that useful, proof-producing reasoning does not require an opaque language
or an enormous runtime. A carefully reviewed standard core, portable modules,
and an ordinary JavaScript API can remain both practical and understandable.

## References

- [ISO/IEC 13211-1:1995 — Prolog, Part 1: General core](https://www.iso.org/standard/21413.html)
- [ISO/IEC 13211-2:2000 — Prolog, Part 2: Modules](https://www.iso.org/standard/20775.html)
- [ISO/IEC TS 13211-3:2025 — Prolog, Part 3: Definite clause grammar rules](https://www.iso.org/standard/83635.html)
- [ARC — answer, reason, check](https://josd.github.io/arc/), on why a check
  has to be able to disagree with the answer it checks
- [The Art of EyeProlog](the-art-of-eyeprolog.md)
- [EyeProlog README](README.md)