eyeon Specification

Document: eyeon-spec-0001
Category: Language Specification
Language version: 0.0.8
Date: 2026-10-18

Table of contents

• Status of This Memo
• 1. Conventions and conformance
• 2. Program model
• 3. Lexical conventions and terms
• 4. Clauses and binding
• 5. Builtins and arithmetic
  • 5.1. Builtin predicates and special forms
  • 5.2. Arithmetic operators
  • 5.3. Arithmetic functions and constants
  • 5.4. Ordinary predicates
• 6. Inference and negation
  • 6.1. Herbrand semantics
  • 6.2. Evaluation and negation
• 7. Queries and aggregation
• 8. Explanations
  • 8.1. Proof certificates
  • 8.2. Independent checking
• 9. Checks
• 10. Errors and command-line interface

Status of This Memo

This project specification is not an IETF RFC. It defines the subset of Prolog implemented by eyeon. It does not claim full ISO Prolog conformance or compatibility with every Prolog program.

1. Conventions and conformance

MUST, MUST NOT, SHOULD, and MAY express the requirement levels of RFC 2119 and RFC 8174. A conforming implementation MUST implement the syntax and behavior below. Answer order and the first selected successful derivation are unspecified. A ground term contains no variables. A predicate is identified by its atom name and arity; parent/1 and parent/2 are distinct predicates.

2. Program model

Source files are UTF-8 and conventionally use .pl. Programs use these forms:

human(socrates).                        % ground fact
mortal(Person) :- human(Person).        % clause
?- mortal(Who).                         % query
?- human(X), mortal(X).                 % conjunction
?- why.                                 % explain previous answers
?- why(mortal(socrates)).               % explain a goal
:- assertion(mortal(socrates)).         % executable check
:- table fibonacci/2, ackermann/2.      % tabled predicate declarations

All statements MUST end in ., followed by whitespace, a comment, or end of file. The interpreter MUST parse the entire source, load all facts, complete requested inference, answer queries in source order, and evaluate checks in source order. A query MAY use later facts or clauses. Checks MUST NOT assert facts. Queries and checks MUST request the backward computation they need. why follow-ups refer to the preceding ordinary query, even when checks or other follow-ups intervene.

why/0, why/1, and assertion/1 have the special top-level meanings described here; they are not ordinary user-defined control predicates. why MAY wrap a parenthesized conjunction. Directives other than table and assertion MUST be rejected. Query forms belong in program files in this interpreter; other Prolog systems may require entering them at a top level.

3. Lexical conventions and terms

Names are case-sensitive. Unquoted atoms match [a-z][A-Za-z0-9_]*. Variables match [A-Z_][A-Za-z0-9_]*. A variable’s scope is one clause, query, or assertion. Repeating a variable name MUST require the same term. Every _ MUST be a fresh variable. Names beginning with _ MUST remain shared when repeated, but MUST be omitted from displayed query bindings.

Single quotes delimit atoms, including Unicode names and punctuation: 'red-fox', 'Élodie', '7'. Quoted and unquoted spellings of the same atom MUST unify. Double quotes delimit strings, which MUST remain distinct from atoms and numbers. Quotes MAY be doubled inside the corresponding quoted value. Supported backslash escapes are \n, \r, \t, \b, \f, \\, \', \", and Unicode \uXXXX / \UXXXXXXXX. Comments start with % and run to the end of the line, or use /* ... */. Block comments are not nested. Quoted comment markers are literal content. Comments and multiline terms MUST preserve diagnostic source lines.

Integers are decimal digits with an optional unary sign and MUST be exact, using arbitrary-precision arithmetic limited by available resources. Reals have a decimal fraction or exponent and MUST use finite binary64 values. Integers and reals are distinct terms: 1 = 1.0 fails, while 1 =:= 1.0 succeeds. Real overflow and non-finite arithmetic MUST raise an error.

A term MAY be an atom, integer, real, string, variable, compound term such as point(2, 3), or list. Compounds have a fixed atom functor and one or more arguments. Arity-zero predicates use a bare atom. Lists use [], [a, b], and [Head | Tail]; tails MUST be lists or variables. Improper lists are outside this subset. Nested compounds and lists MUST match structurally. The quoted constructor '.'(Head, Tail) is equivalent to [Head | Tail] and has the same tail restrictions. The empty list [] is distinct from the quoted atom '[]'. Unification MUST perform an occurs check and MUST NOT create cyclic terms. Ground facts are loaded directly. Unit clauses containing variables, such as append([], List, List)., MUST act as demand-driven clauses with an empty body; their calls MUST supply enough bindings to produce ground answers. Compound arithmetic syntax in a fact is an ordinary compound term and MUST NOT be implicitly evaluated.

4. Clauses and binding

A clause has one ordinary predicate head and one or more body goals, separated by commas. Goals MAY be grouped in parentheses. Multiple clauses for one predicate provide alternative derivations. There is no separate forward-rule syntax. Arithmetic expressions in ordinary arguments remain terms; use an explicit is/2 step to compute an argument or a result:

:- table fibonacci/2.
fibonacci(0, 0).
fibonacci(1, 1).
fibonacci(N, Value) :-
    N > 1,
    PreviousIndex is N - 1,
    EarlierIndex is N - 2,
    fibonacci(PreviousIndex, Previous),
    fibonacci(EarlierIndex, Earlier),
    Value is Previous + Earlier.

Ordinary positive goals bind variables by structural matching. Left = Right unifies terms. Left is Expression evaluates the right side and unifies its numeric result with the left. Arithmetic inputs MUST be bound at that point; computations MUST NOT solve backward. A successful materialized head MUST be ground; calls that leave output variables unresolved MUST raise an error.

5. Builtins and arithmetic

eyeon provides 20 builtin predicates, 39 arithmetic operations, and two arithmetic constants. The operations comprise 18 unary/binary operator forms and 22 named functions; xor/2 appears in both groups and is counted once. Special forms are listed separately below.

Arithmetic expressions are data until evaluated by is/2, a numeric comparison, or an aggregate’s numeric template. An arithmetic function is not a callable goal: sqrt(9) alone does not compute a square root.

5.1. Builtin predicates and special forms

The following builtin predicates MAY appear in clause bodies, queries, and assertions. Inputs described as bound MUST have their required values when the goal is reached. These predicates MUST NOT be redefined by facts or clauses.

For the two text conversions, a bound first argument MUST have the specified text type. Its codes are unified with the second argument, which MAY contain variables. If the first argument is a variable, the second MUST be a ground proper list of integers from 0 through 1114111, excluding surrogate values 55296 through 57343. Text containing an unpaired surrogate MUST raise an error. Supplementary characters occupy one code; empty text corresponds to []. Conversion MUST preserve code points without Unicode normalization. Invalid decoding inputs and calls with neither required input supplied MUST raise an error; a valid conversion with an incompatible output simply fails.

For =../2, a compound decomposes to [Functor | Arguments], for example point(2, 3) =.. [point, 2, 3]. An atom, number, or string decomposes to a singleton list containing itself. The empty list decomposes to [[]]; a nonempty list decomposes to ['.', Head, Tail]. In the construction direction, Parts MUST have a known, nonempty, proper list spine. A singleton MUST contain a bound atom, number, string, or []; a longer list MUST begin with a bound atom functor. Arguments MAY contain variables that are bound by subsequent goals. Constructing '.'/2 MUST obey the list-tail restrictions in Section 3. Neither direction introduces cyclic terms, and displayed answers MUST still be ground. Missing inputs or invalid parts MUST raise an error; incompatible terms and parts fail by unification.

The following special forms complete the language’s built-in facilities; they are not additional ordinary predicates:

Conjunction with , and parenthesized goal groups are supported syntax. The predicates above introduce no mutation or I/O effects. A failed test produces no solution; an invalid arithmetic input or an unmet input requirement MUST raise an error rather than silently failing.

5.2. Arithmetic operators

The following table is exhaustive. Rows run from lower to higher precedence; operators on the same row share precedence. Parentheses override precedence. All operands MUST evaluate to numbers; the integer-only operations reject reals, even those with an integral value such as 3.0.

Unary + preserves its operand; unary - negates it. Unary \ is integer bitwise complement. Unary operators bind more tightly than multiplication and less tightly than powers: -2^2 evaluates to -4.

Addition, subtraction, and multiplication of two integers MUST be exact. Unary signs MUST preserve the operand’s numeric type. / and ** MUST produce reals. ^ MUST produce an exact integer for integer operands and a nonnegative exponent, and a real otherwise. Other mixed integer/real arithmetic MUST convert its operands to binary64; conversion and results MUST remain finite.

//, div, rem, mod, and bit operations MUST require integers. // truncates toward zero; div floors. rem has the dividend’s sign; mod has the divisor’s sign. With -7 and 3, the four results are -2, -3, -1, and 2. Division or remainder by zero MUST raise an error. Bit operations MUST use unbounded signed two’s-complement semantics. Shift counts MUST be nonnegative; right shift preserves the sign.

5.3. Arithmetic functions and constants

Functions use ordinary argument syntax inside arithmetic expressions: sqrt(9), min(A, B). The following table lists every supported function. Arguments MUST evaluate to numbers, subject to the additional requirements shown. Integer and real result types remain distinct terms.

pi and e evaluate to the binary64 approximations 3.141592653589793 and 2.718281828459045. Outside arithmetic evaluation they remain ordinary atoms. Transcendental functions return binary64 approximations; their last result bit MAY differ between implementations.

floor, ceiling, round, and truncate MUST retain every digit of an integer input. float_integer_part and float_fractional_part convert integer inputs to binary64 and MUST return reals. Numeric comparisons and min/max MUST preserve an integer operand’s exact value rather than first rounding both operands to binary64. Atoms, strings, and lists MUST NOT be coerced to numbers. Non-finite conversions, overflow, and real function domain errors MUST raise an error. Unsupported arithmetic functions MUST report their name and arity.

5.4. Ordinary predicates

Predicates outside the listed builtin indicators and special forms have no implicit implementation. Programs MAY define them with facts and clauses; without a matching definition, a ground call has no solution. Term-type tests and structural identity tests are not provided as builtins.

Integer ranges, list operations, and polar-angle normalization can be defined using ordinary clauses. For example, with bound integer endpoints:

:- table between/3.
between(Low, High, Low) :- Low =< High.
between(Low, High, Value) :-
    Low < High,
    Next is Low + 1,
    between(Next, High, Value).
?- between(2, 4, Value).

This defines an ordinary between/3 predicate with answers 2, 3, and 4. Its arithmetic inputs MUST be bound, as with any other clause using arithmetic.

6. Inference and negation

6.1. Herbrand semantics

eyeon MUST use Herbrand semantics for ordinary predicates, with the interpreted builtins specified in Section 5. Ground terms denote themselves: socrates denotes the atom socrates, and point(2, 3) denotes that compound term. A functor constructs data; it does not implicitly call a function. Distinct ground terms MUST remain distinct after the lexical normalization and structural matching described in Section 3. For example, socrates and plato are different values, while socrates and 'socrates' are the same atom. Asserting a relation between two terms does not make them identical.

The Herbrand universe is the set of finite ground terms constructible from the language’s constants and constructors, including its supported numeric values, strings, and proper lists. Variables range over these terms. The Herbrand base is the set of all ordinary predicate applications to ground terms, such as human(socrates). These applications are called ground atoms; here, “atom” means a proposition, distinct from an atom used as a term. A Herbrand interpretation specifies which ground atoms are true.

For positive clauses, the program’s meaning MUST be the least Herbrand model, relative to the specified builtins: the smallest set of ground atoms containing the facts and closed under rule application. Clause variables are universally quantified: whenever a ground instance of a rule’s body holds, its head holds. Thus the facts and clause in Section 2 make human(socrates) and mortal(socrates) true. A query returns ground bindings that make its goals true, subject to the input requirements of this subset.

Arithmetic builtins have their specified numeric interpretation. For example, 1 + 2 remains a compound term in an ordinary argument, while Value is 1 + 2 binds Value to the integer 3. 1 = 1.0 fails because the terms differ; 1 =:= 1.0 succeeds by numeric comparison. Stratified negation extends the positive semantics by testing absence only after the relevant producers complete, as specified below. The universe can be infinite; these semantics do not require enumerating it or guarantee that evaluation terminates.

6.2. Evaluation and negation

Facts and answers have set semantics. Every distinct ground tuple MUST be stored at most once, regardless of the number of derivations. Positive recursion MUST reach a least fixed point when its domain is finite.

The implementation evaluates range-restricted clauses forward: each head variable and each builtin input can be bound from preceding positive goals. It MUST evaluate other clauses using demand-driven tables. A table declaration MUST make every clause of the declared predicate demand-driven, regardless of where the declaration appears. Declarations are optional for clauses already requiring inputs, and useful to prevent eager enumeration of recursive list constructors. All demand-driven calls MUST be tabled. Calls differing only in variable spelling MUST share evaluation, preserving repeated-variable constraints. Recursive consumers MUST suspend and resume as answers arrive, without requiring an unbounded chain of nested calls. Tables MUST be local to each run.

This execution model differs from conventional Prolog depth-first search: clause order MUST NOT change the answer set for terminating positive programs whose calls supply required inputs. Answer order, duplicate derivations, cut, and procedural side effects are not provided.

\+ Goal holds when no matching ground positive answer exists after its producers complete. Negative ordinary goals MUST be ground when reached. Negation of a conjunction and nested negation are outside this subset; define a helper predicate. Negated tests MUST NOT introduce bindings. Negated is/2 and unification require bound operands, as do negated atom_codes/2, string_codes/2, and =../2; negated aggregate goals require a helper predicate.

The implementation MUST reject dependency cycles through negation or aggregation. A negative consumer MUST run after its producer strata finish. Dependency analysis distinguishes predicates by name/arity and excludes producer heads with incompatible atomic argument constants; other argument constraints MAY be treated conservatively. Arithmetic tests have no fact producers. Absence means no evidence in this completed program, not a claim about the world.

No semantic depth limit is defined. Arithmetic, compound construction, or expanding call patterns can create infinite computation. Tabling MUST NOT be described as guaranteeing termination for arbitrary programs. The playground MUST allow cancellation by terminating its computation worker.

7. Queries and aggregation

A query MUST return all distinct tuples of its displayed variables, once each. Variables beginning with _ are existentially projected out. Successful queries with no displayed variables yield true.; unsuccessful queries yield false.. false. describes query failure, not an explicitly asserted negative fact. Conjunctions share bindings and process goals from left to right.

?- aggregate_all(count, mortal(Person), Count).
?- aggregate_all(sum(Value), score(Person, Value), Total).
?- aggregate_all(min(Value), score(Person, Value), Minimum).
?- aggregate_all(max(Value), score(Person, Value), Maximum).
?- aggregate_all(list(result(Person, Value)), score(Person, Value), Results).

aggregate_all/3 MAY appear in a body, query, or assertion. Its goal MAY be a parenthesized conjunction. It MUST complete all matching producer work before aggregating, including demand-driven definitions. A bound result constrains the computed answer. Existing outer bindings MAY constrain the producer call; local producer variables MUST NOT escape into the caller.

Aggregation operates on distinct tuples of all producer variables under the set semantics of this interpreter. It does not count repeated proof paths. Equal values from distinct subjects contribute separately. Empty counts and sums yield integer zero; empty minima and maxima fail. Counts and integer sums MUST be exact; sums and extrema also support finite real arithmetic. A producer that requires unavailable input bindings MUST report an error.

list(Term) MUST collect one instance of Term per distinct producer tuple, without evaluating arithmetic expressions inside that term. Elements MAY be atoms, strings, numbers, compounds, or lists, but MUST be ground. Empty collections MUST yield []. Equal projected terms from different producer tuples MUST remain repeated list elements; repeated facts or proof paths MUST NOT add elements. List order is unspecified. A supplied result or list pattern MUST unify with the computed list; it MUST NOT bind producer variables or filter the producer before collection. Unlike Prolog’s findall/3, this operation does not collect nonground answers or repeated derivations.

8. Explanations

?- why. MUST explain all answers of the preceding non-follow-up query. Consecutive follow-ups MUST retain that context. Without a previous query, it MUST prompt for a query; after an unsuccessful query, it MUST report that there is no successful answer to explain. ?- why(Goal). MUST explain all successful answers to that goal and MUST become the current context.

Every derived tuple MUST retain a successful rule and its supporting evidence. Supplied facts, completed absence searches, computed tests, and aggregates MUST be identified separately. All successful explanations MUST use one numbered format: each rule is listed once, and each step is shown once before the steps that use it. This includes explanations of single supplied facts. Derived steps MUST identify their source clause, actual supporting goals, and local variable bindings when present. Unit clauses have no supporting steps. Ordinary predicate steps MUST show actual ground terms, and arithmetic evidence MUST include concrete operands and results. Explanations MUST NOT silently omit steps or numeric digits. Explanations MUST use the proof certificate format below. There is one certificate per run, shared across all requested successful explanations. It records one selected derivation per goal. Repeated follow-ups MUST NOT repeat claims or steps. The Reason section is the certificate; the Check section MUST include its verification report after the program’s assertions.

8.1. Proof certificates

Certificate generation MUST record successful instances of queries selected by why, including explicit why(Goal) queries. A why follow-up MUST refer to the preceding query rather than introduce another claim. Generation MUST first complete inference and validate the program’s assertions. Assertions are not automatically included as certificate claims. Without a requested successful explanation, no certificate or proof check report is emitted; the existing empty or unsuccessful explanation message applies. Non-certificate messages in Reason MUST be comments so that a successful certificate can be extracted and checked as Prolog data.

A version 1 certificate MUST contain only Prolog data records:

certificate(eyeon, 1).
claim(query(1), [mortal(socrates)]).
clause(1, human(socrates), []).
clause(2, mortal(var('Person')), [human(var('Person'))]).
% step 1
step(human(socrates), fact(1), [], []).
% step 2
step(mortal(socrates), rule(2), ['='('Person', socrates)], [human(socrates)]).

There MUST be exactly one certificate(eyeon, 1) header. Each claim(Request, Goals) identifies a nonempty proper list of successful goals. query(N) refers to the Nth source query, counting explanation follow-ups; check(N) MAY identify the Nth source assertion in a manually supplied certificate. The claimed conjunction MUST preserve variable sharing in that request and ground its displayed variables. Claims MUST NOT represent false. query results or assert that every answer has been found.

Source facts and clauses MUST be numbered together in source order, starting at 1. Queries, directives, and generated helper rules MUST NOT receive source clause numbers. Optional clause(Number, Head, Body) display records MUST agree with the source. Body is a list; source variables appear as var('Name'), and open list templates as list(Items, Tail). These display records MUST NOT supply authority for checking.

Each step(Goal, By, Bindings, Uses) supplies one justification for a goal. Bindings is a proper list of '='('SourceVariable', Value) pairs with distinct variable names. Uses is a proper list of recorded premises. Ordinary predicate steps MUST be ground. fact(N) cites a source unit clause; rule(N) cites a source clause and its body instance. builtin identifies a pure builtin whose result MUST be recomputed. absent identifies a ground negated ordinary goal and MUST have no bindings or uses.

An aggregate goal is represented as data with its producer goals in a list, for example aggregate_all(sum(V), [score(P, V)], 9). Its justification is collected, its bindings MUST be empty, and each member of Uses MUST be a list containing one successful instance of the producer conjunction. Those instances MUST have supporting steps and distinct producer-variable tuples. The checker MUST recompute the aggregate from the recorded tuples. Completeness of that collection remains a trust obligation.

Generated steps MUST appear after their supporting steps, with sequential % step N labels. These labels aid reading and are not authority for checking. Certificate variables are local to a record and MAY be consistently renamed. Goal identity MUST preserve variable sharing while ignoring variable spelling. Arithmetic compounds MUST be written in explicit function notation, such as '**'(-3.0, 2.0), to preserve their parsed structure. The certificate MUST retain full numeric values and the complete reachable derivation.

8.2. Independent checking

The checker MUST follow the recorded premises without invoking the inference engine, searching source rule bodies for missing proofs, or executing source assertions. It MAY share parsing, term operations, and pure builtin arithmetic with the reasoner; those facilities form part of its trusted implementation. Every generated certificate MUST pass checking before it is returned.

Every report MUST identify all seven conditions, their coverage counts, and their failure counts:

Negation of an ordinary predicate MUST remain an absent obligation: recorded positive evidence cannot establish that the complete program has no answer. Aggregate membership MUST be justified, but an omitted derivable tuple may be invisible without further inference. Collection completeness MUST therefore remain a collected obligation. C6 MUST detect direct contrary evidence and missing collection tuples supported by available positive evidence and pure builtin computation. It MUST NOT be described as proving completeness.

Reports MUST use ordinary Prolog data records: condition/4, failure/3, obligation/3, counts, and verdict/1. Failure and obligation records SHOULD retain the goal as a structured term, with variables and open lists encoded as templates as in Section 8.1 so that the report remains ground data. A valid certificate without obligations yields verdict(checked). A valid certificate with obligations yields verdict(checked_with_obligations). Invalid certificates yield verdict(failed(Count)). Strict checking MUST reject all trust obligations. A report’s valid field means that the recorded conditions passed under its listed obligations; callers MUST inspect those obligations or request strict checking when unconditional checking is required.

Checking establishes derivability of the recorded claims relative to the supplied source and interpreted builtins, subject to any listed obligations. It MUST NOT claim that source facts are true, that all answers were found, that unsuccessful queries have no answers, or that the shared parser and builtin implementation are independently verified. Certificates are not cryptographic signatures or source-authenticity guarantees.

9. Checks

:- assertion(Goal). MUST test the existence of a successful solution. A parenthesized conjunction MAY use local variables and calculations. Checks MUST run after query inference, in source order, without changing explanation context. Certificate generation and checking MUST finish before output is returned or printed. A successful check emits check passed: Goal.. The first failed check MUST stop the run and identify its source line with Check failed: Goal.. Runtime errors in assertions SHOULD identify the assertion’s source line. Checks use the same inference engine; programs SHOULD use independent expected values or mathematical identities.

10. Errors and command-line interface

For installation and invocation instructions, see the project introduction.

The CLI MUST accept exactly one program path or - for standard input. -h/--help and -v/--version display usage and the version respectively. Successful queries, including false., MUST exit zero. Errors MUST go to stderr and produce a nonzero status. The CLI MUST prepare the complete transcript before printing it, so failed checks produce no partial successful transcript.

The CLI and playground MUST group output under % Answer, % Reason, and % Check, in that order. Answers and assertion results retain source order; requested explanations share one certificate and one proof check report. In % Answer, each result block MUST be preceded by its query in ?- Goal. form, including results with no displayed variables and unsuccessful queries. Query formatting MAY normalize whitespace and parentheses. Empty sections MUST explain what was not requested. Section grouping MUST NOT change preceding-query explanation context. Malformed or unfinished statements MUST report a source line. Unsupported syntax and runtime operations MUST fail explicitly. The earlier English-like syntax is not supported.