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:
- New rule set.
Ris asserted. - Same text again. The existing statement is returned. Nothing is superseded, nothing is written.
- Different text. The live
n3:sourceis superseded by the new text. The old version is retracted with kindsupersedeand stays in history.
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:
n3:(urn:tiramemsu:n3:) holds ordinary stored data:n3:sourceon rule sets, and the labelsn3:derivedBy,n3:ruleandn3:skolemthat materialization writes (chapter 7).tm:(urn:tiramemsu:tm:) is reserved for virtual predicates such astm:contentandtm:now. They are computed for a run and cannot be written.
The monotonicity check
Parsing a rule set also classifies it, by looking at the builtins in its rule bodies:
| Class | When | reason | materialize |
|---|---|---|---|
Monotonic | none of the builtins below | runs | runs |
NonMonotonic { rule, builtin } | a body uses log:notIncludes, log:collectAllIn or log:forAllIn | runs | refused |
ClockDependent { rule, builtin } | a body uses time:localTime or tm:now | runs | refused |
UntracedPremises { rule, builtin } | a body uses list:map, whose proof does not name the facts it read | runs | refused |
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.