Reasoning with N3 · Chapter 7 of 10

Chapter 7

Materialization

materialize writes what a rule set concludes as derived beliefs. Each one rests on its premises and on the rule set, and is retracted the moment any of them goes.

Derived beliefs in one minute

Materialization stands on one verb from the change add-derived-beliefs: Tx::derive(s, p, o, valid, support). It asserts a statement D and, for each supporting statement e, an engine-owned link (D sys:derivedFrom e). The rules that matter here:

• Support cascades. When a support of a live derived statement is retracted, by any operation, the derived statement is retracted in the same transaction, recursively.
• Conjunctive within, disjunctive across. One derivation falls when any of its supports goes. Two derivations of the same content from different supports are two statements, and the content stays live while either stands.
• Idempotent for the same support. Deriving the same content from the same live support set returns the existing statement. A different support set, or an identical fact asserted independently, gives a new statement, so an observed fact never becomes dependent by accident.
• Correcting a support drops what rests on it. Superseding a support retracts its derived statements with kind supersede and does not replay them, since they were computed from the old content.

sys:derivedFrom is engine-owned: you cannot assert it directly. View::dependents, dry runs and max_cascade all follow support links, so “what breaks if I retract this” includes every conclusion drawn from it.

What materialize does

Db::materialize(rule_set, &MaterializeOptions) runs in two phases. Only the second one holds the writer.

1. Check. Classify the rule set. A NonMonotonic, ClockDependent or UntracedPremises rule set fails with N3NotMaterializable { rule, builtin } before anything runs.
2. Snapshot. Take a read view at t₀. Load the scope, as reason does, but leave out statements derived from this rule set’s own live R. They are what is being recomputed.
3. Reason. Run the sweep of chapter 5 over the default unbounded window, or the one you give.
4. Fuse. If an inference fuse fired, fail with N3Contradiction { rule }. Nothing is written.
5. Commit. Open one write transaction and write the conclusions in proof order through derive. Support is the conclusion’s loaded premises, the eids just written for its derived premises, and R. Two layers name where it came from: (D n3:derivedBy rule_set) and (D n3:rule i).
6. Report what was derived, what already existed, what was widened and what was skipped.

Socrates, materialized

use tiramemsu::{MaterializeOptions, TxN3};

// e1 = (v:socrates rdf:type v:Human) was asserted earlier.
db.transact(TxOptions::default(), |tx| { tx.store_rules(v("mortality"), MORTALITY)?; Ok(()) })?;

let report = db.materialize(v("mortality"), &MaterializeOptions::default())?;
println!("reasoned at {}  committed tx {}", report.reasoned_at, report.tx.t);
println!("derived {:?}  existing {:?}", report.derived, report.existing);

Memory now holds a conclusion D = (v:socrates rdf:type v:Mortal) with two support links, (D sys:derivedFrom e1) and (D sys:derivedFrom R), and the label (D n3:derivedBy v:mortality). Here it is, with a second rule set built on top of it:

Conclusions fall with premises and rules

A premise goes. Retract e1. In the same transaction, the link to e1 is retracted because its object is e1. D is retracted because it lost a support. Then D’s other link and its labels go, because their subject is D. All but e1 get kind cascade.

let rep = db.transact(TxOptions::default(), |tx| { tx.retract(e1)?; Ok(()) })?;
// rep.retracted: (e1, Explicit), and with kind Cascade: both support links,
// D, (D n3:derivedBy v:mortality) and (D n3:rule 0)

Correcting e1 with supersede does the same with kind supersede: the corrected fact is replayed, and the conclusion drawn from the old one is not.

A rule goes. Store a new version of v:mortality. That supersedes R, and every conclusion resting on R is retracted with kind supersede in that transaction. The next materialize writes the conclusions of the new version. Retracting R outright retracts them the same way.

There is no window in which old rules’ conclusions sit next to new rules. A conclusion is in memory only while everything it was drawn from is.

Labels are not support

n3:derivedBy and n3:rule say which rule set and which rule produced a conclusion. They are layers on D, for querying. Grounding comes from the sys:derivedFrom links alone. Both are ordinary data, so SPARQL reads them:

PREFIX n3: <urn:tiramemsu:n3:>
# Who is mortal according to v:mortality, and on what grounds?
SELECT ?who ?premise WHERE {
  ?who a v:Mortal ~ ?d .
  ?d n3:derivedBy v:mortality ;
     sys:derivedFrom ?premise .
}

The premises include R itself, so the answer also says which version of the rules was used.

Rule sets layer

A run never loads the conclusions of its own rule set. Conclusions of other rule sets are ordinary statements, so rule sets build on each other:

v:mortality

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Human } => { ?x a v:Mortal }.

v:lifespans

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Mortal } => { ?x v:has v:lifespan }.

Materialize v:mortality, then v:lifespans. The second conclusion, D2 in the figure, has D among its supports. Retract e1 and both fall. Materialize v:mortality again and nothing changes. Order matters: run the lower rule set first.

Re-running and widening

Materialization is idempotent. Run it twice with no other writes and the second run reports every conclusion as existing. Its commit asserts nothing.

A conclusion’s interval can grow. Say the facts are valid [2020, 2024), and a first run used the window [2020, 2022). It wrote a conclusion for [2020, 2022). A second run without a window finds the same content from the same support over [2020, 2024). It supersedes the stored conclusion to the hull of the two intervals and reports it as widened. The support links are replayed, so the conclusion still rests on the same statements.

• Same content and support, interval contained in the stored one: existing.
• Same content and support, interval overlapping or touching without being contained: widened to the hull.
• Same content, different support: a separate statement, another episode or another derivation.

Intervals grow across runs and never shrink. A conclusion that stops holding is not narrowed. It loses a support and is retracted.

Invented nodes

A blank node in a rule head invents a node (chapter 2). Written naively, every run would invent a new one, and Bob would collect a new anonymous manager each time.

v:staffing

@prefix v: <urn:tiramemsu:v:>.

{ ?x a v:Employee } => { ?x v:manager _:m }.

Materialization turns each blank node into a node found or created by upsert_derived(n3:skolem, "<R eid>/<rule>/<label>", support). The key is built from the rule set’s statement, the rule index and eyeron’s deterministic witness name, so the same firing gives the same key. The key statement is itself derived from the firing’s support. As a result:

• Run it twice for v:bob and both runs use the same node for _:m. The second asserts nothing.
• Retract (v:bob rdf:type v:Employee) and the key goes with the conclusions about the node. The node itself, like everything, is never deleted. It is simply no longer used.

Snapshot, then commit

Reasoning can take a while. The writer is single, and holding it for a reasoning run would block every other write. So materialize reasons on a read view taken at t₀, outside the writer, and holds the writer only for the commit. The report carries reasoned_at = t₀.

Between the two, another writer may retract a premise. At commit time, a conclusion whose support is no longer live is skipped, together with everything that depends on it, and listed in stale_support. The run does not fail, and the other conclusions are written. Run materialize again to catch up.

Previewing and bounding

• dry_run reports what would be derived, existing and widened, and commits nothing.
• require_complete refuses to commit a run that stopped at a limit, failing with Incomplete. Without it, a partial run writes what it found, all of it sound.
• QueryBudget bounds the loading and the commit. eyeron’s own limits bound reasoning. Cancellation is checked between segments.

let preview = db.materialize(v("mortality"), &MaterializeOptions {
    dry_run: true,
    require_complete: true,
    ..MaterializeOptions::default()
})?;

tm materialize memory.db urn:tiramemsu:v:mortality --dry-run
tm materialize memory.db urn:tiramemsu:v:mortality --valid-during 1577836800000..1893456000000 --require-complete

One proof per conclusion

eyeron returns one proof for each conclusion in each segment, even when the conclusion follows in several ways. A stored conclusion therefore rests on one of its possible supports. That is sound: everything it rests on is live. If that support goes while another remains, the conclusion is retracted, and the next materialize derives it again from the other support.

The report