Reasoning with N3 · Chapter 10 of 10

Chapter 10

Time leaves the store

Chapters 4 and 5 asked what follows as of a transaction and at an instant. This short chapter takes the same two clocks out of tiramemsu, as RDF 1.2 that any RDF 1.2 tool can read, with the views you already know.

Why not plain N-Triples

A rule sees a view: the statements live as of some transaction, valid at some instant. Plain tm export writes one such view, the live statements now, and nothing else. The ids are gone, so a layer about a statement has nothing to point at. Retracted statements are gone, so chapter 4's "what did we believe then" cannot be asked again elsewhere. The intervals are gone, so chapter 5's pointwise semantics has nothing to work on.

Every statement, with its clocks

tm export --format sg-nt12 writes every statement as an RDF 1.2 reifier, with its lifetime and its valid interval:

tm export memory.db --format sg-nt12

stmt:3 rdf:reifies <<( v:alice v:worksAt v:acme )>> .
stmt:3 tm:txAdded 3 .
stmt:3 tm:validFromMs 1577836800000 .      # 2020-01-01
stmt:3 tm:validToMs 1640995200000 .        # 2022-01-01

This is shortened: in the file, IRIs are written in full and numbers are typed xsd:integer. Then comes the triple itself, v:alice v:worksAt v:acme. It is written only if the statement is live in the view of the export, which you choose with the same flags as tm query:

The reifiers are the same in every view. A reader can always see that Alice's job ended in 2022 and was recorded in transaction 3, even in a view where the job is not asserted.

Conclusions travel too, their reasons do not

A materialized conclusion from chapter 7 is a statement like any other, so it is exported with its clocks. Its sys:derivedFrom links are engine bookkeeping and stay behind, like every sys: statement. Outside the store, a conclusion is a fact with a lifetime. To know why it holds, ask tiramemsu: View::dependents, or tm reason --proof.

Two names for valid time

In rules and queries, tm:validFrom and tm:validTo are xsd:dateTime values (chapter 9). The export writes epoch milliseconds under names of its own, tm:validFromMs and tm:validToMs, so the two never mix. A rule run over an exported file has to compare milliseconds.

A format with a proof

The format is defined by LeanRDF, which proves in Lean that its decoder is exact:

• a file that decodes is exactly the export of a well-formed set of statements;
• decoding an export gives back the statements.

tiramemsu writes LeanRDF's canonical form, and LeanRDF's tests decode tiramemsu's recorded exports and reproduce them byte for byte. The articles Taking memory out whole and An export with a proof tell both halves.