Experimental API

The experimental surface holds capabilities the engine exposes and tests, but whose meaning is not yet a promise. The current member is bounded Why-false: a post-solve exploration of why a ground fact was not derived. Since 0.1.0-alpha.4 it is reachable from the stable header as text; what stays experimental is what a complete exploration is allowed to mean, and the bounds behind it.

Why-false is not the mirror of Why-true

Why-true answers an existential question: at least one derivation exists, so a single retained witness is enough. Why-false answers a universal question: every candidate rule and substitution must fail. Its natural shape is a bounded refutation tree rather than one path.

The current implementation reconstructs that information after a successful solve against the immutable final policy-fact, EDB, and IDB state. It never derives a new fact and never changes the retained Why-true witness.

Shared boundedness, different evidence

Both Why-true and Why-false can return a document with status=truncated. That is a successful explanation API call, not a failed solve. Why-true then emits steps=0 premises=0, with no partial witness; Why-false can retain partial diagnostics and reports named limit-hits. Their symmetry stops at boundedness, not at the meaning or shape of the evidence.

A short C output buffer is a separate error, PAYLOAD_TOO_LARGE, not a truncated document. Allocating more text storage cannot increase the exploration limits. Python prepares the explanation once, reads its text size and renders it into an owned buffer before releasing it; the document is returned unchanged.

For a guided example with both C and Python, a branching diagram and actual output for an allowed user and a blocked user, see Membership, Why-true and Why-false.

Status contract

Since 0.4.0, Why-false and Why-true share the MAELYS-DATALOG-v2 envelope. The second line, document=why-false or document=why-true, identifies the document kind; the first line alone no longer distinguishes them. The next line carries the status:

C and Python entry points

Why-false is exposed by the stable header, as text, with the same buffer contract as Why-true — count first, then render into a buffer the application owns:

#include <maelys/datalog.h>

/* Inside a function with a live result and terms for allow("alice").
 * Requires <stdlib.h> and <stdio.h>. */
size_t required = 0;
maelys_datalog_status_t status = maelys_datalog_result_explain_false_text(
    result, "allow", terms, 1, NULL, 0, &required);
if (status != MAELYS_DATALOG_STATUS_OK) return 1;
if (required == (size_t)-1) return 1;
char *text = malloc(required + 1);
if (text == NULL) return 1;
status = maelys_datalog_result_explain_false_text(
    result, "allow", terms, 1, text, required + 1, &required);
int success = status == MAELYS_DATALOG_STATUS_OK;
if (success) success = fputs(text, stdout) >= 0;
free(text);
return success ? 0 : 1;

The capability is the backend's to declare: backend ABI v3 uses the three explanation_* callbacks and the EXPLAIN_FALSE capability bit. The reference backend declares it; a backend without it answers UNSUPPORTED, outputs untouched.

Prepare once in caller-owned storage

Since 0.4.0, maelys_datalog_result_explanation_storage_requirements() reports the workspace size and alignment. maelys_datalog_result_prepare_explanation() then constructs an opaque explanation in that storage. Read its cached text length with maelys_datalog_prepared_explanation_text_size() and write with maelys_datalog_prepared_explanation_write_text() as often as needed, without repeating the exploration. Finish with maelys_datalog_prepared_explanation_release(). Check every returned status.

The reference backend makes no internal allocation on this path. The caller provides both the workspace and a separate text buffer; it may use fixed application budgets, as in the compiled C reference helper. The prepared handle leases its result until release. The exploration bounds, statuses and output are the same as for the convenience text call above. The Python binding uses this prepared path internally and returns a string; Python/CFFI still allocate their buffers.

Reuse the session workspace

Since 0.4.1, maelys_datalog_result_explain_text_in() combines preparation, measurement, writing and release in one caller-owned call. maelys_datalog_session_explanation_storage_bound() sizes storage once for the reference session.

Since 0.5.0, opt in at session creation with session_config_set_explanation_workspace(config, kinds) in C, or ruleset.prepare(explanations=ExplanationKind.TRUE | ExplanationKind.FALSE) in Python. The existing text methods then reuse the session workspace. Measuring and rendering the same query need only one preparation, with no reference-engine allocation after session creation. Output buffers and Python objects may still allocate. The default session reserves no explanation workspace. See the stable C querying reference for cache lifetime, unreserved kinds and storage errors.

Fixed bounds

The exploration is bounded, and the bounds are not caller-tunable: backend ABI v3 preserves them, so two applications reading the same result get the same document. The reference backend explores at most 128 candidate rules, 4,096 substitutions per rule, depth 10 and 16 retained diagnostics, and accounts the cost of ground string filters separately.

Hitting any of them turns the status to truncated and names the bound on the limit-hits line — none, or a comma-separated subset of the five names.

Obstacles

Each retained diagnostic records the positive supports already found and the first obstacle that prevents that branch from deriving its target.

For this policy:

allow(User) :-
    member(User, Group),
    admin(Group),
    not(blocked(User)).

and these runtime facts:

member("alice", "team").
admin("team").
blocked("alice").

asking why allow("alice") is absent produces this document — engine output of 0.4.0 through the stable API, not a transcription:

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

The failed branch retains its two positive supports and reports blocked("alice") as a negative contradiction at its original body position (body=2). Bindings name variables by their rule-local IR id — the id maelys_datalog_program_rule reports — and the standard grammar maps A–Z to 0–25: Group is 6 and User is 20; anonymous variables start at 26. A variable left unbound prints as ?N.

Canonical diagnostics

Execution may use a safe literal order as variables become bound, but public identity remains independent of optimizer choices. Diagnostics retain original body indices and are ordered canonically by rule, substitution, and obstacle identity. When the diagnostic capacity is smaller than the discovered set, the engine retains the canonical top-k diagnostics rather than the first execution prefix.

This distinction matters for long-lived audit data: an optimizer improvement must not silently redefine an explanation's public identity.

What is promised, and what is not

Promised by the stable header today:

• the entry point and its buffer contract;
• the MAELYS-DATALOG-v2 envelope with document=why-false, status, query, limit-hits with its five names, counters, then per-diagnostic bindings, supports and one obstacle, in canonical order;
• that the exploration is read-only and never derives a fact.

Deliberately not promised:

• that status=complete is a proof of non-derivability — the language specification does not yet define complete finite refutation;
• the values of the bounds, which belong to the backend and may change with the engine;
• that every backend can answer — the capability is optional and a missing one is UNSUPPORTED;
• the structured form behind the text (maelys_datalog_why_false_explanation_t and caller-supplied limits), reachable only through the advanced alpha surface and coupled to engine layout.

Promotion criteria

The text entry point is already in the stable opaque facade. Promoting the meaning of a complete Why-false exploration to a formal absence guarantee requires all of the following:

1. The language specification defines complete finite refutation against the stratified least model.
2. complete and truncated have a versioned, externally testable contract — the text format is fixed (the v2 document envelope since 0.4.0); the semantics of complete are not.
3. An independent conformance oracle checks the explored failed branches.
4. Real consumers demonstrate that the fixed bounds produce useful complete results.

Until then, applications may experiment with Why-false, but persisted data should carry its own schema version and preserve the engine and policy fingerprints used to produce it.

For the supported integration boundary, use the stable C API. For the structured form the reference backend uses underneath, see the advanced alpha API.