Related work

The Theory page explains algorithms and implementation guarantees. This page places Maelys beside related work; it is not a performance ranking or a claim of research priority.

Datalog foundations

Least-fixpoint evaluation, semi-naive evaluation, stratification, join ordering and provenance all predate Maelys. Maelys combines these foundations in a bounded embedded C evaluator. The contribution described here is a concrete implementation and its tested contracts, not a new general-purpose Datalog semantics.

For the mathematical background, see Abiteboul, Hull and Vianu's Foundations of Databases and the Theory bibliography.

Maelys and Soufflé

Soufflé is a high-performance Datalog system with a strong focus on static program analysis. Its research includes synthesis of analyzers, compilation, indexing, specialized data structures, scalable provenance and join optimization. See its publications, provenance documentation and join-optimizer work.

Maelys reuses classical ideas also present in Soufflé, but targets a different integration contract: bounded memory, explicit failure, deterministic results and explanation limits inside an application. It embeds an evaluator rather than synthesizing a large native analyzer. These priorities describe its design; they do not establish a speed or memory advantage over Soufflé without a comparable experiment.

The shared subject is Datalog, not identical execution or explanation algorithms. Maelys Why-true exports one retained witness graph, with ancestors before descendants and shared parents emitted once. It is neither every possible derivation nor a guarantee of the smallest proof.

Why and why-not provenance: PUG

Lee, Ludäscher and Glavic's PUG framework explains answers and missing answers for first-order queries with negation through graph-based provenance and query rewriting.

That is relevant prior work for the question “why is this fact absent?”. It does not imply that Maelys implements PUG or inherits its guarantees. Maelys Why-false performs its own bounded exploration against a completed result, retains obstacles, and explicitly reports truncation. Its diagnostic cannot alter the membership decision. See the Why-false design and tests.

Security languages: Binder

John DeTreville's Binder (2002) uses communicating logic programs to express distributed security statements, including certificates and delegation.

Binder is a useful precedent for logic-based authorization. Maelys is an embedded evaluation kernel, not an implementation of Binder's distributed trust model. The application supplies the vocabulary, trusted policy and request facts, then interprets successful queries as decisions.

Authorization tokens: Biscuit

Biscuit combines signed bearer tokens, offline attenuation and a Datalog-derived authorization language. Attenuation lets a holder add restrictions without gaining rights or contacting the issuer.

Maelys does not supply that token protocol or cryptographic delegation model. Its policy fingerprints identify material and execution configuration; a digest alone does not authenticate an author. Token transport, trust and authorization workflow remain the application's responsibility. This is a difference in scope, not evidence that one system is more secure.

What Maelys contributes here

Maelys's engineering contribution is the combination of bounded evaluation, explicit failure, reusable preparation and auditable explanation contracts in one C runtime:

• explanation truncation is separate from decision correctness;
• native event-window publication preserves committed inputs and results after a rejected push;
• optional workspace reuse separates preparation from repeated formatting;
• source, policy and execution identities serve distinct audit purposes.

Each claim has its own scope and test evidence on the Theory page. None requires attributing established algorithms to the project or claiming a universal first.