eyekind

eyekind — reasoning you can see.

A standalone, dependency-free Python rule language with forward and backward reasoning and checkable proofs.

Playground · Examples · Example decks · Specification · Conformance suite (run it in your browser) · PyPI

Most software computes an answer and the reasoning evaporates. eyekind makes a different bargain: an answer can arrive together with the reasoning that supports it, in a form another program can check. You write facts and rules; eyekind draws conclusions, and every conclusion can come with a proof that a separate checker verifies against your program.

• The idea in a few lines
• Run it
• Writing programs
• Proofs, and what checking one means
• Checking the translation
• From Python
• The examples
• What is deliberately absent
• The name

The idea in a few lines

from eyekind import *

fact(human('socrates'))
implies(human(X), mortal(X))

A fact and a rule. eyekind concludes mortal('socrates'). Ask for the reasoning and you get a document that names the fact it used, the rule it applied, and the substitution that connects them:

mortal('socrates')

clause(1, fact(human('socrates')))
clause(2, implies(human(X), mortal(X)))

step(mortal('socrates'), clause(2), {'X': 'socrates'}, [human('socrates')])
step(human('socrates'), clause(1), {}, [])

That proof is itself Python, one expression per line, and a checker that never consults the reasoner re-establishes every step against the program. Save the two lines above, with their import, as socrates.py and try it:

python -m eyekind --proof socrates.py | python -m eyekind --check-proof - socrates.py

The checker prints a report ending in verdict('checked'). The certificate for a ten-thousand-step derivation works exactly the same way.

What a checked derivation adds is a place for disagreement to land. When a conclusion is wrong, there are only three possibilities, and a proof tells you which: the inference was invalid, the rule did not say what you meant, or the input fact was wrong. A checked proof settles the first, so you can spend your attention on the other two.

Run it

Python 3.9 or newer. No dependencies, no build step. From the root of a checkout:

python -m eyekind examples/socrates.py
python -m eyekind --proof examples/socrates.py
python -m eyekind --proof examples/socrates.py | python -m eyekind --check-proof - examples/socrates.py
./test

./test runs every test, one numbered line each: the unit tests, the examples (each must reproduce its saved output, proof and report), and the conformance suite, in process and through the command line. ./test examples runs one section, and ./test -k skolem only the tests that mention skolem.

To use eyekind from anywhere, install it; an editable install keeps using the checkout, so your edits take effect at once:

pip install -e .
eyekind --proof examples/socrates.py
python examples/socrates.py --proof

Once eyekind is installed, a program is also a script: python program.py runs it with the same options as eyekind program.py. Run eyekind --help for the full command line, which SPEC §14 describes.

Or in the browser: the playground edits, runs and checks any example, with eyekind running in the page through Pyodide. To run it from a checkout, serve it (python -m http.server) and open /playground/.

Writing programs

A program is a Python module that starts with from eyekind import * and states clauses with these calls:

A premise joins its goals with &, and so can a forward rule's conclusion: implies(p(X) & q(X), r(X) & s(X)). A conclusion is never true or false: query(...) and contradiction(...) say those, and proofs show them that way.

Data that is not a program. Everything eyekind writes, conclusions, proofs and check reports, is a document: plain expressions, one per line, with no from eyekind import * and no fact(...) around them, so it cannot be imported. facts_from reads such a document as data and states each expression as a fact. It never executes the text, so it is also the safe way to take in data you do not trust; a data file written as a program would run as Python code. It is what lets one run reason over another, as audited-grants reasons over its own check report:

facts_from('data.py')                                 # a file of expressions such as score('ann', 3)
facts_from(text=check_report(result.proof_report))    # or text, such as another run's report

The two kinds of rule compose. A forward rule's body may call backward definitions, and a backward goal may use facts that forward reasoning established, so you let knowledge accumulate and then ask a focused question:

from eyekind import *

fact(parent('alice', 'bob'))
fact(parent('bob', 'carol'))

implies(parent(X, Y), ancestor(X, Y))
implies(ancestor(X, Y) & parent(Y, Z), ancestor(X, Z))

implied_by(related(X, Y), ancestor(X, Y))
implied_by(related(X, Y), ancestor(Y, X))

query(related('alice', 'carol'))

With nothing asked, a run prints the facts it derived; query(...) asks the program's own questions, and --goal "Goal" asks from outside instead.

Nothing to declare. A name the program uses without defining it is a variable when it starts with a capital or an underscore, like X or _Rest, and a predicate otherwise, like parent. Python's builtins keep their meaning in ordinary Python code, so a program can compute with int, getattr or sorted; inside a statement such as fact(type('socrates', 'human')) a builtin name is a predicate, except for the few a program computes with there: print, range, len, list, dict, set, tuple, str, enumerate, zip, sorted, reversed, isinstance, open, repr, chr, ord, iter, any, all, map and filter, and builtins beginning with an uppercase letter. A program that wants one of those as a predicate says so, range = preds('range'). A call of an undeclared predicate on its own, such as a misspelled fcat(p(1)), states nothing, so eyekind stops with an error instead of ignoring it.

Terms are Python values. An atom is a string, 'socrates'; a number is an int of any size or a finite float; a list is a list, and [H, *T] has head H and tail T; a compound term is a call, parent('alice', 'bob'); and _ is a fresh variable at every occurrence. Goals join with & (and), | (or) and ~ (not), alongside call, once and findall. Python reads & and | before comparisons, so write (X > 1) & (Y < 2); a chained comparison such as X > 1 & Y < 2 stops the program with an explanation instead of meaning something else.

Numbers are Python's. Integers are exact and unbounded, so the Fibonacci example computes F(10000), a 2,090-digit integer, exactly. An expression means what it means in Python: 4 / 2 is 2.0, // and % are floor division and modulo, round rounds half to even. 1 and 1.0 do not unify, yet compare exactly. Infinity and NaN are rejected, including overflowing float literals such as 1e999 in programs, goals and documents. A result that is not a finite real number stops the run rather than becoming a value.

The primitives (unify, is_, eq, comparisons, type tests, functor, univ, atom_concat and the rest) are listed in SPEC §5, and the arithmetic functions in SPEC §6. Everything else, such as membership, mapping or graph traversal, is written as ordinary clauses.

Domains get representations, not syntax. eyekind has no built-in notion of RDF or of anything else: IRIs, typed literals, triples and quoted graphs are just terms, such as literal(V, lang(L)) or triple(S, P, O). A forward head may contain variables its body never binds, and then says that something exists. Each such unknown becomes a Skolem function of the activation: implies(person(X), has_parent(X, P)) concludes has_parent('ann', skolem(2, 'P', ['ann'])), the P of rule 2 for Ann. The same activation always gives the same term, in any round and any run, which keeps conclusions deduplicated, and a different one a different term, so two unknowns never pass for one.

Proofs, and what checking one means

A proof holds claims, the source clauses it displays, and one inference record per step. The checker establishes seven conditions:

Two properties make this worth more than a log. The checker follows the certificate: it never calls the reasoner to fill a gap, so a missing step fails the check rather than being quietly re-derived. The source is the authority: the clauses a proof displays cannot override the program, so you cannot smuggle a rule into a proof, nor pad it with steps no claim needs.

The report is Python data too, so one program's evidence is material another program can reason over, with facts_from('report.py'):

condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

Failures appear as failed(N) outcomes with failure(Condition, Conclusion, Detail) facts, an invalid proof gives verdict(failed(N)) and exit code 2, and --json gives the same report as JSON. Proofs are parsed as data and never executed. Simple lines use a direct reader; other syntax uses Python's ast module, with the same accepted terms, so checking a proof from someone else runs none of their code. Every proof eyekind generates is checked before it is returned.

Why negation and aggregation are safe

A negation (~G) concludes something from what is not there, and a collection (findall(T, G, L)) from everything that is there. Both are only right once nothing more can be derived: a fact added later would make an earlier absence false, or a collected list incomplete. eyekind guards them in four ways.

Ask only once the answer is final. When it loads a program, eyekind works out which clauses each body goal depends on. A dependency is closed when the goal sits inside ~ or findall. Every clause gets a rank, at least that of everything it depends on, plus one across a closed dependency, and forward rules run rank by rank, each to its fixpoint. By the time a rule asks ~already_received(P) or collects findall(X, p(X), L), every rule that could still produce such a fact has finished. A program with no such ranking is rejected with "unstratified negation or collection dependency":

implies(~q, p)
implies(p, q)     # p needs q to be absent, yet p yields q: rejected

Positive cycles, such as transitive closure, are fine. Ranks compare whole terms rather than predicate names, so t(X, 'type', Y) and t(X, 'status', Y) can sit at different ranks, which matters when everything is a triple. A goal that is a variable, reachable from a forward rule, is rejected, because nobody can tell what it depends on.

Negate only what is bound. The variables of ~G must be bound when it is solved. With a variable, as in ~p(X), the question would quietly become "is there no X at all?", so eyekind stops with an error instead. Bind the variables first: applicant(P), income(P, I), I < 2500, ~already_received(P). When "no value at all" is what you mean, say so with _: ~q(X, _) holds when q(X, Y) has no solution for any Y.

Say what was taken on trust. A search that found nothing cannot be proved the way a derivation can. So a proof records each negation as an 'absent' step and each collection as a 'collected' step, the report lists them as obligation('absent', 'theory_scoped', Goal), and the verdict is checked_with_obligations rather than checked. Theory-scoped says what the claim is: absent according to this program, a closed-world assumption made visible. --strict-proof rejects any proof that leans on one.

Refute them when the evidence allows. The checker cannot prove an obligation, but it can catch one out (C6). An absence fails when a fact of the program, a step of the proof or a recomputed primitive is a solution after all, and a collection fails when such a solution is missing from its list. A valid proof with obligations is valid conditional on them, and the report says which they are.

Checking the translation

A checked proof shows that the conclusions follow from the program. It cannot show that the program says what the law, the policy or the textbook says; the person who knows the source has to judge that. What eyekind can do is point at the parts of a program that make no difference to its conclusions, because those are where a translation is most likely to be decorative, incomplete or untested:

from eyekind import *

fact(p('a'))
fact(q('b'))
implied_by(s(X), q(X))
fact(z('c'))
implies(p('a') & ~s('a'), 'ok')

$ eyekind --unused program.py
unused(line(4), fact(q('b')))
unused(line(5), implied_by(s(X), q(X)))
unused(line(6), fact(z('c')))

A clause is listed when no conclusion's proof uses it. A negation or a collection may consult a clause without its proof recording that search, as ~s('a') consults q('b') and the rule for s; for each such clause eyekind leaves it out, runs the program again, and lists it only when the conclusions stay the same. The example programs research-portal.py and package-holiday.py list no clauses.

From Python

from eyekind import check_proof, load_text, run

socrates = load_text("""
from eyekind import *
fact(human('socrates'))
implies(human(X), mortal(X))
""")
result = run(socrates, goal='mortal(X)', proof=True)
print(result.answers)                                  # ["mortal('socrates')"]
print(result.bindings)                                 # [{'X': "'socrates'"}]
print(check_proof(socrates, result.proof)['valid'])    # True

load('program.py', ...) loads program files and load_text(source) source text. run() returns a Result with answers, bindings, inferred, stdout, proof, proof_report, stats and halt_code; options are goal, goals, proof, max_depth (1000000), max_iterations (1000 per stratum) and max_inferences (1000000), and exceeding a bound raises EyekindError rather than return a partial result. check_report(report) formats a report and read_term(text) reads a term back. A goal given as text reads a bare name as a variable, so a goal with no arguments is written p() or 'p'.

The examples

The example collection is 63 complete programs, each with its conclusions, proof and C1-C7 report saved beside it (examples/output/, examples/proof/, examples/check/), and a card deck that explains it for a wide audience.

These are meant to be edited: change a fact, run it, look at what changed. Because the artifacts are saved, you can see exactly what your change did:

./test                                                       # every test, one numbered line each
python tools/update_examples.py                              # regenerate artifacts after an intended change
python conformance/run.py                                    # the conformance suite of SPEC.md

What is deliberately absent

Cut, conditional commitment, mutable databases, attributed variables, constraint libraries, tabling, and filesystem or network built-ins. Several of these omissions are load-bearing: without cut and without a mutable database, a derivation is a function of the program and its input, which is what makes a certificate meaningful. A program is free to use Python to compute its clauses (read a CSV, loop over a range), but once stated a clause is a term, and reasoning over it calls no Python code of yours. Undefined predicates fail, under the closed-world convention. How the engine itself works is described in SPEC Appendix C.

Begin with one question and a few facts. Give the relationships names, write the rules you already believe, and let the program show you what they imply. The first unexpected answer is often worth the most, because it points at a specific rule or assumption to revisit.

The name

eyekind joins a p, from the Prolog its reasoning comes from, to eye, after the EYE family of reasoners it belongs to. And said aloud it sounds like py: in eyekind everything, from the rules and the data to the proofs and the check reports, is done in Python.

License

MIT