Datalog language

Maelys Datalog is a Policy-as-Code language for writing security and authorization rules that are clear, deterministic, and auditable.

This guide explains both its syntax and its semantics through practical examples: not only which forms are accepted, but what facts, rules, negation, comparisons, Why-true and Why-false mean when a policy is evaluated. It follows the normative grammar and semantic constraints while adding the pedagogical context that an ABNF grammar alone cannot provide. For the complete specification, use the Normative specification (ABNF and semantics).

1. Facts and rules

A Maelys Datalog policy has two simple building blocks:

• Facts describe what is known.
• Rules describe what can be derived from those facts.

Here is a complete first policy:

% Alice is a member of the engineering team.
member("alice", "engineering").

% A user has access if they are an engineering member.
has_access(User) :- member(User, "engineering").

The engine derives has_access("alice"). The first line is a policy fact: it is declared in the policy source, so member/2 must be registered as POLICY_FACT. Data supplied for one request is instead an EDB fact, added through the API before solving. Rules derive IDB or QUERY facts.

The three syntax rules

1. A predicate starts with a lowercase letter: member, has_access.
2. A named variable starts with an uppercase letter: User, Document.
3. Every fact or rule ends with a period: .

Strings are UTF-8 text in double quotes, booleans are true or false, and source integers are bounded, non-negative decimals. Use % for a line comment or /* ... */ for a non-nested block comment.

2. Writing rules

Read :- as if, and a comma as and:

eligible(User) :-
    member(User, "engineering"),
    trained(User, true).

This says: derive eligible(User) if that user is an engineering member and has completed training. Variables with the same name refer to the same value inside one rule.

3. Wildcards and alternatives

Anonymous wildcard _

Use _ when a positive fact contains a value that the rule does not need:

has_access(User) :- grant(User, _, _).

Each _ is a fresh anonymous wildcard. It may appear only as a term in a positive body atom—never in a rule head, direct fact, comparison, arithmetic expression, or not(...).

Bounded disjunction or

Lowercase or expresses alternatives between positive atoms:

reachable(X, Y) :- edge(X, Y) or link(X, Y), enabled(Y).

The parser expands this bounded disjunction in lexical order before solving, as if the alternatives had been written as separate rules. That expansion is transparent to the canonical Why-true witness. Uppercase OR is not the operator.

4. Negation and comparisons

Stratified negation

Wrap a fact in not(...) to require its absence:

eligible(User) :-
    member(User, "engineering"),
    not(suspended(User)).

Variables used by negation must be bound by positive atoms in the rule body. They do not have to be bound by the immediately preceding atom. Negation must be stratifiable: recursion through negation is rejected, while positive recursion is supported.

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

Comparisons and arithmetic

Symbols and booleans support = and !=. Integers also support <, <=, >, and >=, with bounded +, -, and * expressions:

priority(User) :-
    score(User, Value),
    Value + 2 >= 10.

As with negation, variables used in comparisons or arithmetic must first be bound by positive body atoms. Overflow and incompatible mixed types are rejected.

Stratified distinct count

We will use the document-ownership vocabulary already introduced in the Quickstart.

Assume the application supplies these request facts:

The policy counts the documents owned by each known user:

document_count(User, N) :-
    user(User),
    count(Document, owns(User, Document), N).

has_multiple_documents(User) :-
    document_count(User, N),
    N >= 2.

Follow the first rule in order:

1. user(User) selects one known user. It first binds User to "alice", then to "mallory".
2. owns(User, Document) selects that user's ownership facts.
3. count keeps the distinct values bound to Document and binds N to their number.

The result is therefore:

Read the aggregate expression

Read count(Document, owns(User, Document), N) from left to right:

• Document — the value to count. Each distinct document contributes once.
• owns(User, Document) — the relation to inspect. At this point User is already bound by user(User), so only that user's ownership facts match.
• N — the result. The aggregate binds this variable to the integer count.

User is the grouping key. The ordinary positive atom user(User) defines the groups before count runs. This is why Mallory receives a count of zero: the group exists even though it has no matching document. A name absent from user/1 is not invented and produces no result.

count counts distinct documents, not repeated facts. Supplying the same owns("alice", "roadmap.pdf") fact more than once still counts that document once. With "roadmap.pdf" and "budget.xlsx", Alice's count is therefore two.

What “stratified” means

count needs a final list of facts before it can return a stable number. Stratified means that the engine can order the rules into layers: a layer that uses count runs only after the relation it counts is complete.

For the document policy, the order is:

• First: collect ownership facts. The request supplies the complete user/1 and owns/2 relations for this solve.
• Then: count. The engine reads the completed owns/2 relation and derives document_count/2.
• Finally: use the number. A later rule reads document_count/2 and derives has_multiple_documents/1.

The dependency moves in one direction:

owns/2 → document_count/2 → has_multiple_documents/1

In practical terms:

• count may read a relation that has already been completed;
• later rules may use the number produced by count;
• that number must not be used to add new facts to the relation being counted.

What would be circular? The following policy is deliberately invalid:

can_read(User, Document) :-
    owns(User, Document).

document_count(User, N) :-
    user(User),
    count(Document, can_read(User, Document), N).

can_read(User, Document) :-
    document_count(User, N),
    delegated(User, Document),
    N < 2.

It creates a loop:

• to calculate document_count/2, the engine first needs every can_read/2 fact;
• to finish can_read/2, the last rule needs document_count/2;
• that rule could add another can_read/2 fact and therefore change the count that enabled it.

There is no safe first layer: the count depends on can_read/2, while can_read/2 also depends on the count. The engine rejects this dependency cycle instead of producing an order-dependent result.

Ordinary recursion is still allowed. For example, a positive recursive reachable/2 relation may run until it produces no new facts. Once that relation is complete, a higher layer may count its destinations. Only a cycle that passes through count is forbidden.

Syntax rules and limits

Start from the expression used above:

count(Document, owns(User, Document), N)

Its three variables have different jobs:

• Document is the value being counted. It must appear in the nested relation, here owns(User, Document). It belongs to the aggregate itself, so the rule cannot reuse Document after the count expression.
• User identifies the group. It is not counted. The earlier positive atom user(User) must bind it before count runs. The engine then performs one count for Alice, one for Mallory, and so on.
• N receives the integer result. It must be a different variable from Document. A later condition such as N >= 2 may use it. If an earlier atom has already bound N, count instead checks whether that integer equals the computed result.

These rules follow from those roles:

• every named variable inside the nested relation, except the value being counted, is a grouping key and must already have a value;
• with no grouping key, the aggregate produces one global count;
• a known group with no matching fact receives zero;
• a group that was never introduced by an earlier positive atom is not created automatically;
• joins and filters belong in an auxiliary relation. Complete that relation first, then count it. For example, derive readable_document(User, Document) from ownership and access rules, then count its Document values.

The count contract:

• one aggregate: distinct count;
• sources made of request facts (EDB), facts written in the policy, or a derived relation (IDB) completed in an earlier layer;
• a separate count for each explicitly bound group, or one global count;
• zero for an existing group whose completed source relation has no match.

What count does not provide:

• streaming counts, sliding windows, or incremental updates between solves;
• partial answers when a configured capacity is exceeded. A capacity error fails the solve, and no result is published.

Each solve therefore counts one complete, bounded snapshot of its input facts.

See the aggregate contract for the normative binding, stratification, capacity, and compatibility rules.

Integer minimum, maximum, and sum

These aggregates have the same three-part shape as count:

operator(Value, source(...), Result)

• Value is the integer selected from each matching source fact.
• source(...) is the completed relation to inspect.
• Result receives the computed integer.

Extend the ownership example with a size for every document. These are request facts supplied by the application:

The policy derives three summaries for every known user:

smallest_document(User, N) :-
    user(User),
    min(Bytes, document_size(User, _, Bytes), N).

largest_document(User, N) :-
    user(User),
    max(Bytes, document_size(User, _, Bytes), N).

total_document_size(User, N) :-
    user(User),
    sum(Bytes, document_size(User, _, Bytes), N).

For Alice, the engine derives:

The two documents of size 12 both contribute to sum because they are two different complete source facts: their document names differ. Repeating the exact same document_size("alice", "roadmap.pdf", 12) fact does not add 12 again, because Datalog relations contain facts as a set. This differs from count(Bytes, document_size("alice", _, Bytes), N), which counts the two distinct projected values 8 and 12 and therefore returns 2.

Empty groups and invalid values

Suppose user("mallory") exists but no document_size fact matches Mallory:

• min and max derive no result for Mallory. An empty set has no smallest or greatest integer, and the engine does not invent a sentinel value.
• sum derives total_document_size("mallory", 0).
• a user absent from user/1 is not a known group, so no summary is derived.

Numeric aggregates accept only integers in the engine's source range, 0..2147483647. A matching symbol or boolean is not converted to an integer. A matching non-integer, or a sum above the maximum, fails the whole solve with INVALID_FIELD; no partial result is published. A later valid snapshot can reuse the prepared session.

Cost and capability boundaries

Let S be the source slice inspected for one aggregate evaluation and M the number of matching facts:

• min and max scan once: O(S);
• count and sum must also establish set semantics: O(S + M log M);
• several aggregates over the same relation perform separate scans. There is no per-group aggregate cache, stream, window, or incremental maintenance API.

Evaluation uses bounded scratch storage and adds no engine allocation for each group. Capacity errors remain solve errors. Support is negotiated independently: count, min, max, and sum each have their own capability. Supporting count does not imply that a custom backend supports the three numeric operators.

5. Why-true explanations

Solving answers whether a ground query is true. For a derived IDB fact, the engine can also return a bounded, canonical Why-true document showing one deterministically selected witness.

This policy declares member/2 as POLICY_FACT and eligible/1 as IDB | QUERY:

member("alice", "engineering").
eligible(User) :- member(User, "engineering").

Querying eligible("alice") produces these exact bytes:

MAELYS-DATALOG-v2
document=why-true
status=complete
steps=1 premises=1
step=0 rule=1 fact="eligible"("alice")
premise=0 body=0 kind=positive origin=policy-fact fact="member"("alice","engineering") parent=-
result-step=0

• complete means the full bounded witness is present.
• truncated means the fact is true but the bounded document cannot contain its complete witness.
• not-derived means no derived IDB witness is represented.

A fact supplied directly as input or declared in the policy does not need a rule to establish it. It can therefore be true without a derived witness. The absence of that witness does not mean the fact is false or the explanation was truncated.

Explanation text may contain application symbols and should be treated as potentially sensitive data. Do not log, persist, or transmit it without an explicit product decision. Why-true provides one witness—not every derivation or a universal proof of authorization. For an absent fact, use the separate Why-false diagnostic described next.

Reading a count witness

The earlier document count example derives has_multiple_documents("alice"). Because membership succeeds, its Why-true document shows how the observed count participates in that derivation:

MAELYS-DATALOG-v2
document=why-true
status=complete
steps=2 premises=4
step=0 rule=1 fact="document_count"("alice",2)
premise=0 body=0 kind=positive origin=edb fact="user"("alice") parent=-
premise=1 body=1 kind=count origin=edb pattern="owns"("alice",?3) projected=?3 value=2 parent=-
step=1 rule=2 fact="has_multiple_documents"("alice")
premise=2 body=0 kind=positive origin=idb fact="document_count"("alice",2) parent=0
premise=3 body=1 kind=comparison-true origin=none lhs=2 op=>= rhs=2 parent=-
result-step=1

The kind=count premise records the completed source relation, the projected variable, and the observed cardinality value=2. It does not list the two documents or prove every member of the counted set. Here ?3 is the engine's serialized identifier for the policy variable Document; it is not a new runtime value.

Reading numeric aggregate witnesses

Why-true records numeric aggregates with kind=min, kind=max, or kind=sum. Like kind=count, each premise identifies the frozen source pattern, projected variable, observed integer and source origin. It records the aggregate result used by the selected derivation; it does not enumerate every matching fact.

6. Why-false explanations

Why-true asks “Which derivation supports this fact?” Why-false asks “What prevented this absent fact from being derived?” Neither is a new Datalog operator. Both describe a successfully evaluated policy: they do not add facts, change the rules, or evaluate the policy again.

Check membership first. A false answer means the ground fact is absent from this policy's model for these inputs—not that it is false in the outside world. An API error is not a false answer.

Follow one failed branch

Reuse the membership idea, with a suspension check. For this independent example, declare member/2 and suspended/1 as EDB, and eligible/1 as IDB | QUERY, before loading this policy:

eligible(User) :-
    member(User, Group),
    not(suspended(User)).

Supply these runtime facts through the API, rather than appending them to the policy source:

member("alice", "engineering").
member("mallory", "engineering").
suspended("mallory").

A failed branch retains supports already found and one obstacle that stops that branch. Here the obstacle is an existing suspension, not a missing membership. If several rules can derive the same fact, inspecting one failed branch is not enough to conclude absence; the membership query remains authoritative.

Read the diagnostic

For eligible("mallory"), the Why-false document is:

MAELYS-DATALOG-v2
document=why-false
status=complete
query="eligible"("mallory") origin=none
summary=none
limit-hits=none candidate-rules=1 substitutions=1 diagnostics=1 filter-cost=0
diagnostic=0 rule=1 depth=0 target="eligible"("mallory")
binding=6 value="engineering"
binding=20 value="mallory"
support=0 body=0 origin=edb fact="member"("mallory","engineering")
obstacle=negative-contradicted body=1 origin=edb pattern="suspended"("mallory")

• support=0 records the membership that already works.
• negative-contradicted identifies the suspension that prevents this rule from succeeding. body=1 is the second body literal, using zero-based positions.
• binding=6 and binding=20 identify the rule-local variables Group and User; they are not user IDs or source line numbers.
• limit-hits=none means this diagnostic exploration hit no reported bound.

Other obstacles include a positive premise with no matching fact (positive-no-match), a false comparison (comparison-false), a recursive branch without base support (recursive-no-base-support), or a ground string filter that does not match (filter-false). These are diagnostic categories, not instructions to remove a security condition or invent a missing fact.

Reading a count mismatch

Return to the document count example. Alice owns two distinct documents, so the ground query document_count("alice", 3) is absent. Its Why-false document reports the mismatch between the requested value and the completed count:

MAELYS-DATALOG-v2
document=why-false
status=complete
query="document_count"("alice",3) origin=none
summary=none
limit-hits=none candidate-rules=1 substitutions=1 diagnostics=1 filter-cost=0
diagnostic=0 rule=1 depth=0 target="document_count"("alice",3)
binding=13 value=3
binding=20 value="alice"
support=0 body=0 origin=edb fact="user"("alice")
obstacle=count-mismatch body=1 origin=edb observed=2 expected=3 projected=?3 pattern="owns"("alice",?3)

observed=2 expected=3 explains why this particular ground fact is absent; it is not an engine error. As with every Why-false diagnostic, the membership query remains authoritative and the diagnostic remains bounded.

Reading numeric aggregate failures

Why-false distinguishes two situations:

• a non-empty aggregate whose computed value differs from the ground query uses min-mismatch, max-mismatch, or sum-mismatch, with observed and expected values;
• an empty source for min or max uses min-empty or max-empty. There is no sum-empty obstacle because an empty sum succeeds with zero.

A non-integer match or overflowing sum is different: it fails the solve with INVALID_FIELD, so there is no successful result from which to request a Why-false document.

Both explanations are bounded, but they are not mirror images

Why-false bounds candidate rules, substitutions, recursion depth, retained diagnostics and filter work. These bounds limit how much of the explanation can be explored and reported; they do not change whether the queried fact is present in the evaluated policy. A truncated explanation therefore does not replace the membership answer with an unknown answer.

Both documents share the MAELYS-DATALOG-v2 envelope. The second line, document=why-true or document=why-false, identifies the kind of explanation. For integration details and error handling, see the explanation API documentation.

7. Where to go next

• Quickstart — run a complete policy lifecycle.
• Rulesets concepts — how a policy source written in this language becomes the parsed program the solver consumes.
• Concepts — the engine's vocabulary, policy, input, solve, and query model.
• C Stable API — explicit engine ownership and native integration.
• Python binding — query and explain from the unified 0.10.0 package.
• WebAssembly API — use the same engine and Why-true contract in JavaScript.
• Normative specification — source ABNF, Why-true ABNF, semantics, and conformance material.