RFD 0094: Rule-body reads of a completed undefined companion

State: committed

Question

How may a rule body select tuples that the well-founded model leaves unknown without observing a relation before its fixpoint converges?

Context

The evaluator stores a head R as two disjoint extents: definitely true tuples in R, and well-founded-undefined tuples in $undefined::R. The read plane already exposes both. The surface R(args) is unknown was parsed but discarded, which silently changed the question to definite membership in R.

Companion names are generated, not rule heads. Without an explicit dependency, the stratifier may schedule a companion consumer before the component that produces it. Incremental maintenance also cannot use a delta path that omits the whole-program companion-producing pass.

Decision

R(arguments) is unknown lowers to a positive read of $undefined::<resolved R>. The dependency graph treats that companion read as a strict completion dependency on R: a consumer in another component is scheduled after R converges. A read in the same recursive component is refused with OE1441; no in-progress undefined extent is observable.

is not unknown, payload-binding is unknown(x), and path-headed x is unknown remain refused. They require, respectively, a finite complement domain, payload semantics, or a predicate identity. Multi-valued both / ambiguous / timeout outcomes remain OE1349.

Programs containing a companion read use full recomputation for mutation maintenance. This preserves incremental/full-recompute equality until the incremental circuit represents companion production directly.

Rationale

The lower-component restriction gives the qualifier its literal set meaning using the existing WFS result. It neither collapses unknown to false nor exposes an intermediate approximation. A dedicated dependency kind distinguishes this completion requirement from aggregation, so recursive use is not mislabeled as OE1317.

Alternatives

Continuing to refuse all uses preserves safety but leaves an already-materialized extent inaccessible to rules. Treating the companion as an ordinary base relation can evaluate too early. General recursive truth-value reflection needs pair-valued recursive semantics and remains outside this decision.

Consequences

The derivation semantic epoch advances because accepted artifacts and their materialized projections change. Parser, elaboration, stratification, evaluator, runtime, and maintainer tests must cover definite, false, unknown, recursive refusal, and mutation parity.

Open questions

Native incremental companion maintenance and recursive truth-value reflection remain separate work.