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. Termination on this demo is by exhaustion of new productions (4 rounds for the smoke program below) rather than fuel cutoff.

What the engine is not: full RIF (no Core-Plus dialects, no BLD / PRD, no built-ins beyond term equality, no skolemisation). 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.

Input graph

RDF triples (Turtle-style, read-only)

@prefix ex:   <ex:> .
@prefix rdf:  <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

ex:alice   rdf:type        ex:Student .
ex:Student rdfs:subClassOf ex:Person  .
ex:Person  rdfs:subClassOf ex:Agent   .

RIF Core program

Two rules (read-only)

// Rule 1: subClassOf transitivity
Forall ?x ?y ?z (
  ?x rdfs:subClassOf ?z :-
    And ( ?x rdfs:subClassOf ?y
          ?y rdfs:subClassOf ?z )
)

// Rule 2: rdf:type propagation up the class hierarchy
Forall ?o ?c ?d (
  ?o # ?d :-
    And ( ?o # ?c
          ?c rdfs:subClassOf ?d )
)

Ready (static smoke output).

Saturated graph

Click Run inference to render the saturated graph.

What's actually running

The triples and rules above are encoded in RIF.Core.Eval.fst as smoke_input_graph and smoke_program; the saturation result smoke_saturated is computed at module-init when the JS bundle (factoidal.js) loads. The static button reads pre-canned output from the F* source; it stays in sync because the smoke values themselves are assert_norm-checked at compile time.
RIF_Core_Eval joined the js_of_ocaml link line in this commit. Until Js_of_ocaml.Js.export bindings are wired up (a small factoidal_rif_jsoo.ml shim), JS code cannot construct fresh graphs and call fixpoint directly. The "Live re-run" button is pre-disabled and feature-gates that follow-on work.
Body atoms are translated to SPARQL BGPs via RIF.Core.Translation; bindings come from SPARQL11.Algebra.eval_bgp. Same evaluator the regular SPARQL demos use. No separate Datalog implementation.
Termination is fuel-bounded (fixpoint : rdf_graph -> rif_program -> nat -> rdf_graph). Convergence ends the loop early when a round produces no new triple. Fuel = 8 in the smoke run; actual rounds to fixpoint = 4.
Saturation lemma: lemma_fixpoint_extends g p fuel establishes graph_subset g (fixpoint g p fuel). Forward chaining is monotone over set-semantics graphs.

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.