LeanRDF

Statement graphs

leanrdf-statements (directory statements/, import LeanRDFStatements, namespace LeanRDF.Statements) models tiramemsu's bitemporal statement records. The book chapter explains the ideas. The example below is compiled with the tests, as statements/StatementsTests/Guide.lean.

From Lean

import LeanRDFStatements

open LeanRDF LeanRDF.Statements

def ex (n : String) : IRI := ⟨"http://example.org/" ++ n⟩
def e1 : Record := { eid := 1, s := .term (.iri (ex "FRA")), p := ex "route",
                     o := .term (.iri (ex "LHR")), txAdded := 1 }
def e2 : Record := { eid := 2, s := .eid 1, p := ex "distance",
                     o := .term (.lit (.typed "655" xsdInteger)), txAdded := 2 }

def sg : StatementGraph := (StatementGraph.ofList? [e1, e2]).toOption.getD .empty

#guard sg.check == []                               -- well formed
#guard (sg.toRDF {}).size == 6                      -- the view `now`: 2 reifiers, 2 clocks, 2 base triples
#guard sg.kernel == [1, 2]
#guard (sg.quote 2).toOption.map (·.toNTriples) == some
  "<<( <<( <http://example.org/FRA> <http://example.org/route> <http://example.org/LHR> )>> <http://example.org/distance> \"655\"^^<http://www.w3.org/2001/XMLSchema#integer> )>>"
#guard decode {} (sg.toRDF {}) matches .ok _

The API

NameWhat it is
Record, Node, StatementGraphrecords, a term or an eid, a sorted list of records with distinct eids (ofList?)
WellFormed, check, violationsdecidable well-formedness; check lists (eid, violation) pairs
View, TxSel, ValidSel, Record.livenow, asOf t, history, plus unfiltered or at ms
StatementGraph.toRDF vthe reifier export; mem_toRDF, toRDF_wellFormed
decode v gExcept String StatementGraph; decode_toRDF, toRDF_decode
kernel, isClosed, isAcyclicthe export kernel and its deciders; mem_kernel_iff, kernel_greatest, isClosed_iff, isAcyclic_iff
criterion, criterion_uniquethe paper's direct_export_iff on LeanRDF types
history_closed, history_cycle, history_kernelhistory closure under tiramemsu's write rules
quotethe quoting view on the kernel; quote_sound, quotes_injective', bgp_view'
readRecords, Record.toJsonLineJSON lines in and out

The vendored abstract development is in LeanRDFStatements.Abstract (namespace StatementExport).

Records as JSON lines

One record per line. Terms use N-Triples 1.2 syntax, and a reference is {"eid": n}. Times are integers: transaction numbers, and valid time in epoch milliseconds.

{"eid": 1, "s": "<http://example.org/FRA>", "p": "<http://example.org/route>", "o": "<http://example.org/LHR>", "txAdded": 1}
{"eid": 2, "s": {"eid": 1}, "p": "<http://example.org/distance>", "o": "\"655\"^^<http://www.w3.org/2001/XMLSchema#integer>", "txAdded": 2, "txRetracted": 4}

The export format

For each record e, with every reference to eid n written as <urn:tiramemsu:stmt:n>:

TripleWhen
stmt:e rdf:reifies <<( s p o )>>always
stmt:e tm:txAdded Nalways
stmt:e tm:txRetracted N, tm:validFromMs N, tm:validToMs Nwhen the record has them
s p owhen the record is live in the view

tm: is urn:tiramemsu:tm:, and every clock is an xsd:integer. The output is canonical RDF 1.2 N-Triples. Valid time uses tm:validFromMs and tm:validToMs because tiramemsu's own tm:validFrom and tm:validTo are xsd:dateTime virtual predicates; v0.3.0 used those names, and v0.3.1 renamed them.

Checking tiramemsu's export

tiramemsu writes this format itself:

tm export memory.db --format sg-nt12 --history > memory.nt
cd statements && lake exe leanrdf-sg decode ../memory.nt --history

decode accepts a file only if it is exactly the export of a well-formed statement graph (toRDF_decode). statements/StatementsTests/data/tm/ holds exports recorded from tiramemsu's tests. lake test checks that each one decodes in its view and exports back byte for byte, and scripts/statements-tm-record.sh TIRAMEMSU records them again.

Limits