Skip to content

perf(infer): reason over the ontology at load, and skip sameAs rules that cannot fire - #417

Merged
EthanThatOneKid merged 1 commit into
mainfrom
infer-tbox-vocabulary
Oct 20, 2026
Merged

EthanThatOneKid merged 1 commit into
mainfrom
infer-tbox-vocabulary

Conversation

@EthanThatOneKid

Copy link
Copy Markdown
Collaborator

What

Two changes to applyInference (src/wiki/infer.ts). Each leaves the inferred closure identical.

  1. engine.load() gets only the ontology. load() is the engine's preprocessing pass: it closes the rules over the vocabulary it's given, then infer() runs the data through. We passed the whole graph as the vocabulary, so the instance data was reasoned over twice. Now isOntologyTriple selects RDFS/OWL axioms, class and property declarations, and list cells. Annotations, sameAs, and differentFrom stay in the data.
  2. The nine rules whose premise reads owl:sameAs are dropped when no sameAs can arise. Eyeling evaluates owl:sameAs as a builtin that scans every fact (evalOwlSameAsBuiltin), and eq-rep-s/p/o call it once per triple, so inference was O(n²) even on graphs that derive nothing. mayDeriveSameAs keeps those rules whenever an asserted triple mentions a term that some rule needs in order to conclude owl:sameAs: sameAs, NamedIndividual (the ruleset declares sameAs reflexive via prp-rp), Nothing (closed under NamedIndividual), functional or inverse-functional properties, hasKey, or max (qualified) cardinality. No rule concludes any of these terms, which I checked by scanning every rule conclusion in the baked ruleset. The rules are found by shape, and the count is checked at load, the same way dt-eq is, so a re-bake that changes them fails loudly.

Parity

The closure matches main triple for triple (the harness is in the session record, not committed):

Corpus Asserted Closure Equality rules main This PR
Synthetic OWL 2 RL (restrictions, chains, hasKey, functional props, sameAs on classes, a disjointness inconsistency) 76 350 kept 375 ms 129 ms
Same, with every sameAs trigger removed 59 263 dropped 124 ms 60 ms
tests/fixtures/micro 38 159 dropped 136 ms 49 ms
docs wiki (docs/wiki.yml) 717 832 dropped 1.9 s 183 ms
wazootech/memory 1,074 1,189 dropped 1.7 s 171 ms
bench:shacl fixture, 10³ 1,041 1,156 dropped 771 ms 59 ms
bench:shacl fixture, 10⁴ 10,040 10,155 dropped 41.2 s 410 ms

A scratch patch of Eyeling's builtin, using its existing predicate index, also made infer() linear (8,005 quads: 6.9 s → 0.56 s) with identical output once the per-run inconsistency-report IRIs are normalized. That confirms the diagnosis. It isn't part of this PR; we don't own Eyeling (see wazootech/reasoner#1).

Benchmark (deno task bench:shacl, #416), full wiki check

Quads main This PR Peak RSS
1,007 2.2 s 0.7 s 203 MB
10,006 45.1 s 1.6 s 441 MB
100,007 timeout (> 20 min) 8.8 s 1,058 MB
1,000,017 not run 92.7 s 3,656 MB

At 10⁶, loadGraph takes 61 s and SHACL validation 28 s. SHACL result counts match the validator-only cases at every size (4 / 24 / 194 / 2,078). Measured on Windows with 1.4–3.5 GB of RAM free.

Not fixed

Graphs that do mention one of those terms still go through Eyeling's quadratic sameAs builtin. The fix for that is our own reasoner (wazootech/reasoner#1).

Checks

deno task check, lint, fmt:check, test (581 passed, 1 ignored), and the docs wiki's fmt --check, lint --strict, check --strict, and render --check all pass. The docs' embedded SPARQL results are unchanged. New: tests/infer_test.ts covers ontology classification, the sameAs trigger terms, sameAs substitution with an asserted sameAs, sameAs derived from a functional property, and axioms applying with the equality rules dropped.

Refs #414

🤖 Generated with Claude Code

…that cannot fire

Two changes to applyInference, each with an identical closure:

- engine.load() gets only the ontology triples (RDFS/OWL axioms, class and
  property declarations, list cells), not the whole graph. load() closes the
  rules over its vocabulary, so passing every triple reasoned over the
  instance data twice.
- When no asserted triple mentions a term that can introduce owl:sameAs
  (sameAs, NamedIndividual, Nothing, functional or inverse-functional
  properties, hasKey, max (qualified) cardinality), the nine rules whose
  premise reads owl:sameAs are dropped. Eyeling evaluates owl:sameAs as a
  builtin that scans every fact, and eq-rep-* call it once per triple, which
  made inference quadratic even when nothing was derived.

Full `wiki check` on the bench:shacl fixture: 10^4 quads 45.1 s -> 1.6 s,
10^5 from over 20 minutes to 8.8 s, 10^6 in 92.7 s.

Refs #414

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@EthanThatOneKid
EthanThatOneKid merged commit 17c4ea0 into main Oct 20, 2026
14 checks passed
@EthanThatOneKid
EthanThatOneKid deleted the infer-tbox-vocabulary branch October 20, 2026 19:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant