Factoidal — RIF Core forward-chaining demo

RIF Core (Rule Interchange Format Core dialect) is a Horn-clause sublanguage standardised by the W3C. The Factoidal implementation covers the operational fragment relevant to RDF: triples, frames, membership (#), and subclass (##) atoms; rules are Forall vars (head :- body) with conjunctive bodies. Equality, built-ins, and the import / dialect-mixing machinery are out of scope.

The engine in RIF.Core.Eval.fst performs naive forward chaining with set semantics. One round = fire every rule once against the current graph; a fuel parameter caps the number of rounds. The saturation lemma (lemma_fixpoint_extends) is proved: forward chaining never removes a triple.

What the engine is not: full RIF (no Core-Plus dialects, no BLD / PRD, no built-ins beyond term equality, no skolemisation, no <Import> resolution). The body translator delegates to SPARQL11.Algebra.eval_bgp, so rule bodies are evaluated as basic graph patterns; this matches the standard operational reading of RIF Core under simple entailment.

Smoke test: RIF.Core.Eval.fst's own program

This runs the exact smoke_input_graph / smoke_program baked into RIF.Core.Eval.fst, saturated live via RIF_Core_Eval.fixpoint in the js_of_ocaml bundle — the same F* function the module's own assert_norm checks exercise at compile time, called fresh in your browser. No user input; a fixed capability probe.

Green rows are derived by forward chaining from the input.

Try your own RIF program

Edit the RIF-XML rules and the Turtle premise data below, then run inference. The Turtle is parsed to N-Quads by the engine's own Turtle parser (Parser.Turtle.fst, via the parseToDatasetJson ABI export already used by the SPARQL demos); the RIF-XML is parsed by Parser.RIFXML.fst; saturation is RIF_Core_Eval.fixpoint — the same live call the smoke test above makes, just with your program and data instead of the fixed one.

Green rows are derived by forward chaining from the input.

What's actually running

• bin/npm-entry/entry_jsoo.ml exports factoidalNpmEntry.rifSmoke() and factoidalNpmEntry.rifEval(rifXml, dataNQuads). Both call RIF_Core_Eval.fixpoint directly (fuel 8 for the smoke program, fuel 100 for custom programs); rifEval additionally calls Parser_RIFXML.parse_rif_program to turn the RIF-XML text into a rif_program first. Neither export re-implements any RIF/SPARQL semantics — they are thin string/JSON glue around F*-extracted functions, per rule #11.
• This page loads factoidal-npm-entry.js (built from that OCaml file by js_of_ocaml) through npm/factoidal/browser.js's loadNpmEntry() — the same Pages-mirrored npm package (docs/npm/factoidal/) the JSON-LD playground loads its bundle from.
• Body atoms are translated to SPARQL BGPs via RIF.Core.Translation; bindings come from SPARQL11.Algebra.eval_bgp inside RIF_Core_Eval.fire_rule. Same evaluator the regular SPARQL demos use. No separate Datalog implementation.
• Termination is fuel-bounded (fixpoint : rdf_graph -> rif_program -> nat -> rdf_graph). The "rounds" figure in the status line is measured by driving RIF_Core_Eval.one_round — the same primitive fixpoint composes internally — until it reports no change; it is orchestration telemetry, not a separate implementation of the saturation logic.
• Saturation lemma: lemma_fixpoint_extends g p fuel establishes graph_subset g (fixpoint g p fuel). Forward chaining is monotone over set-semantics graphs.
• If the bundle at docs/fstar-extracted/factoidal-npm-entry.js predates the RIF exports (or fails to load), this page falls back to a static, clearly-labelled canned rendering of the smoke result and disables the custom-program panel — the same honest-failure discipline the JSON-LD playground uses for unsupported inputs.

Caveat

Parser and algebra spec verified in F*; on-disk backend has unverified OCaml-side optimization layers being migrated back to F* (see fstar-purity-unwind.md). The RIF Core engine itself is pure F* with no assume val holes.

RIF Core is scoped out of the entailment-regime test suite (see docs/claude-rules/scope.md): the four W3C SPARQL 1.1 ent:RIF tests (rif01, rif03, rif04, rif06) are permanent SKIPs, not fails, because RIF Core is "a separate production-rule language layered on RDF, not an entailment regime that fits into a verified SPARQL/OWL-RL closure loop." This demo exists to show the engine works, not to claim those tests pass.