Tiramemsu

Reasoning with N3 · Chapter 6 of 10

Chapter 6

Rule sets as memory

Rules are knowledge too. A stored rule set is one statement, so it has history like a fact, it is corrected like a fact, and it can be the reason a conclusion exists.

Storing a rule set

A rule set is named by any IRI, say v:mortality. Tx::store_rules(rule_set, n3) parses the text and, if it parses, writes one statement:

R = (v:mortality n3:source "…the N3 text…")

where n3: is urn:tiramemsu:n3:. That is all a rule set is: a node with one live n3:source statement.

use tiramemsu::TxN3;   // brings store_rules into scope

const MORTALITY: &str = r#"@prefix v: <urn:tiramemsu:v:>.
{ ?x a v:Human } => { ?x a v:Mortal }."#;

db.transact(TxOptions::default(), |tx| {
    let r = tx.store_rules(v("mortality"), MORTALITY)?;   // the eid of R
    println!("rule set statement {r}");
    Ok(())
})?;

store_rules returns the eid of R. Three cases:

Text that does not parse fails with N3Parse { line, message } and leaves no trace. A broken rule set never reaches memory.

From the command line:

tm rules put  memory.db urn:tiramemsu:v:mortality mortality.n3
tm rules show memory.db urn:tiramemsu:v:mortality

Reasoning with a stored rule set

Rules::Stored(rule_set) reads the live n3:source of the rule set in the reasoning view and runs it. The proofs then name the rule set. If the view has no live source for it, the run fails with UnknownRuleSet.

let r = db.now().reason(Rules::Stored(v("mortality")), &ReasonOptions::default())?;
assert_eq!(r.conclusions[0].proof.rule_set, Some(v("mortality")));

let none = db.now().reason(Rules::Stored(v("nothing")), &ReasonOptions::default());
assert!(matches!(none, Err(Error::UnknownRuleSet { .. })));

Because the source is read from the view, an as_of view runs the version believed then. Chapter 4 showed the timeline.

Rule history is a query

Rule sets are ordinary statements, so SPARQL and Cypher read them like anything else. Every version of a rule set, with the transaction that stored it:

PREFIX n3: <urn:tiramemsu:n3:>
SELECT ?text ?t WHERE {
  v:mortality n3:source ?text ~ ?r .
  ?r tm:txAdded ?t
} ORDER BY ?t

Run it on db.history() to see retracted versions too. Each edit links the new version to the old one with sys:supersedes, so ?r sys:supersedes+ ?old walks the edit chain. Put an author and a reason on the transaction that stores a rule set and the rules carry their own changelog.

Namespaces: n3: and tm:

The two prefixes look alike and behave differently:

The monotonicity check

Parsing a rule set also classifies it, by looking at the builtins in its rule bodies:

ClassWhenreasonmaterialize
Monotonicnone of the builtins belowrunsruns
NonMonotonic { rule, builtin }a body uses log:notIncludes, log:collectAllIn or log:forAllInrunsrefused
ClockDependent { rule, builtin }a body uses time:localTime or tm:nowrunsrefused
UntracedPremises { rule, builtin }a body uses list:map, whose proof does not name the facts it readrunsrefused

The classification names the first offending rule by index and the builtin. For example, this rule set is NonMonotonic, naming rule 0 and log:notIncludes:

unmanaged.n3

@prefix v: <urn:tiramemsu:v:>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

{ ?x a v:Employee. ?SCOPE log:notIncludes { ?x v:manager ?m } } => { ?x a v:Unmanaged }.

View::rule_set_info(rule_set) reports the class, the number of rules and the predicates the bodies use, which are also the predicates pruning will load:

let info = db.now().rule_set_info(&v("unmanaged"))?;
// info.monotonicity == NonMonotonic { rule: 0, builtin: "log:notIncludes" }
// info.rules        == 1
// info.predicates   == [rdf:type, v:manager]

Why materialization refuses them

A stored conclusion stays true because of its supports. Each support is a live statement, and when any of them is retracted the conclusion is retracted too. That covers everything a monotonic rule depends on: things that are there.

A non-monotonic rule also depends on things that are not there. “Bob is unmanaged” rests on the absence of a manager. When the manager is asserted tomorrow, nothing is retracted, so nothing would retract the stored conclusion. It would stay, wrong, and look grounded. A clock-dependent rule has the same problem with time: “overdue” was true when written and is false after the deadline moves, with no retraction in between.

The design considered two ways around this, diffing runs and accepting stale results, and chose neither. Materialization is for rules whose conclusions the cascade can keep honest. For the rest, reason answers on demand, on any view, and nothing goes stale because nothing is stored.

Split rule sets by concern

Every conclusion a rule set produced rests on its statement R. Editing the rule set supersedes R, so every one of those conclusions is retracted in the same transaction, and the next materialize writes the new ones. That is what keeps them honest, and also what makes a big rule set expensive to touch. Keep rule sets small and focused: one for employment, one for trust, one for team structure. Recipe 6 shows how to see the cost of an edit before you make it.