ogar-elk: the EL subsumption closure as the third factfinder - #253
Conversation
`ogar-obo` and `ogar-ro` say what is ASSERTED. Nothing said what FOLLOWS.
This closes that gap with the smallest calculus that does the job.
Three rules over ABI-shaped (classid, identity) addresses:
R1 reflexivity A ⊑ A
R2 transitivity A ⊑ B , B ⊑ C ⟹ A ⊑ C
R3 merge-soundness closing C ∪ S introduces no A ≡ B absent from C
Two questions, no others: does `A ⊑ B` follow, and is adding a set of axioms
to an existing closure sound.
UNGRADED BY CONSTRUCTION. An EL entailment is a fact — it follows necessarily
or it does not — so nothing here is scored, ranked or weighted. The thinking
that consumes these facts lives one layer out and this crate is unfazed by it.
ADDRESSES, NEVER A FILE. It never parses an ontology, resolves a CURIE, or
reads a label. Reasoning over the addressed form is the whole point of having
addressed it; a reasoner reaching back for the source document would
re-introduce the coupling the bake exists to remove.
R3 IS WHY THIS IS A CRATE and not a transitive-closure helper. Two
independently authored sources can each be internally consistent and still
disagree about a relation's DIRECTION. Merging them then derives A ⊑ B and
B ⊑ A for classes neither source calls equivalent — and that cycle is the
disagreement made mechanical. It is found at ANY distance, including cycles
that close through a chain no pairwise comparison would think to check.
`merge` does not mutate: it returns a verdict splitting axioms into
corroborating / enriching / conflicting, so a caller decides after seeing it.
Silence is reported as enrichment, never as disagreement — the distinction
that separates "the other source is denser" from "the other source is wrong".
THE BOUNDARY IS DELIBERATE AND NAMED. No existential restrictions, no role
composition, no bottom propagation, no conjunction/disjunction/complement.
Each becomes necessary the moment a typed cross-angle predicate enters the
closure, and at that point the correct move is to wrap a full reasoner, not to
grow this file. The concrete hazard it guards: without role composition,
walking subsumption and part-of together derives FALSE ancestors — `A part_of
B` with `B ⊑ C` does NOT give `A ⊑ C`. `Closure::from_asserted` therefore takes
a `Subsumption` type rather than raw pairs, so a mixed edge set cannot be fed
in by accident.
The depth guard is reported (`depth_cap`) rather than silent, so a caller can
tell "not entailed" from "the walk stopped" — different answers that must not
be conflated.
Zero-dependency, forbid(unsafe_code), clippy -D warnings clean. 8 tests, each
carrying the input that would falsify it: transitivity paired with a
must-NOT-entail case, the depth cap proven to bind AND to release, cycles
proven detected AND absent on a non-trivial acyclic graph, the merge verdict
proven to discriminate all three outcomes, and a pre-existing cycle proven not
to be blamed on an innocent merge.
DISCOVERY-MAP: D-ELK-FACTFINDER appended.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_72a7f898-54a5-4b2a-9bc4-f9dbd4004728) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d0067fa76c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| #[derive(Debug, Clone, Default)] | ||
| pub struct Closure { |
There was a problem hiding this comment.
Because Default is derived, Closure::default() sets depth_cap to zero rather than DEFAULT_DEPTH_CAP. Any caller that builds an empty closure with this public trait and then calls extended gets a graph whose walks never inspect an edge, so non-reflexive entailments are always false and even a two-node cycle is reported as sound; implement Default manually or route it through from_asserted.
Useful? React with 👍 / 👎.
| let mut introduced: Vec<ClassAddr> = merged | ||
| .equivalence_cycles() | ||
| .into_iter() | ||
| .filter(|c| !pre.contains(c)) | ||
| .collect(); |
There was a problem hiding this comment.
When the base already contains two separate cycles, merging edges that join those strongly connected components in both directions introduces new equivalences between every class in the two components. However, every affected class is already in pre, so this filter removes them all and is_sound() incorrectly returns true; R3 requires comparing the pre/post mutual-reachability pairs or SCC partition rather than only the set of classes participating in some cycle.
Useful? React with 👍 / 👎.
| while let Some((node, depth)) = queue.pop_front() { | ||
| if depth >= self.depth_cap { | ||
| continue; | ||
| } |
There was a problem hiding this comment.
For any entailment path or cycle longer than the configured cap (65 edges with the default), this branch silently discards the remaining frontier, causing entails to return false and merge potentially to report a cyclic merge as sound. The depth_cap() getter only exposes the configured number and cannot tell a caller whether a particular walk was truncated, so these results are indistinguishable from complete negative answers; return truncation status or remove the cap, since seen already makes traversal of a finite cyclic graph terminate.
Useful? React with 👍 / 👎.
1 participant
ogar-obosays what is harvested.ogar-rosays which relation. Neither says what follows. This is the third factfinder.Three rules, over addresses
Two questions and no others: does
A ⊑ Bfollow, and is adding a set of axioms to an existing closure sound.Ungraded by construction. An EL entailment is a fact — it follows necessarily or it does not — so nothing here is scored, ranked or weighted. The thinking that consumes these facts lives one layer out.
Addresses, never a file. Input is
(classid, identity). The crate never parses an ontology, resolves a CURIE, or reads a label. Reasoning over the addressed form is the point of having addressed it; reaching back for the source document would re-introduce the coupling the bake exists to remove.Why R3 makes this a crate rather than a transitive-closure helper
Two independently authored sources can each be internally consistent and still disagree about a relation's direction. Merging them derives
A ⊑ BandB ⊑ Afor classes neither source calls equivalent — and that cycle is the disagreement made mechanical. It is found at any distance, including cycles closing through a chain no pairwise comparison would think to check.mergedoes not mutate. It returns a verdict splitting axioms into corroborating / enriching / conflicting, so a caller decides after seeing it. Silence is reported as enrichment, never as disagreement — the distinction between "the other source is denser" and "the other source is wrong".Proven on a real corpus, not only on unit tests
Wired to a consumer's baked 68,797-row spine and a second independently authored hierarchy:
The 4 are two genus/species pairs the two sources model in opposite directions — a bounded, hand-reviewable list rather than a statistic. An independent pairwise method found the same pairs; the two agree.
The boundary is deliberate and named in the crate doc
No existential restrictions, no role composition, no bottom propagation, no conjunction/disjunction/complement. Each becomes necessary the moment a typed cross-angle predicate enters the closure — and at that point the correct move is to wrap a full reasoner (
whelk-rs), not to grow this file.The concrete hazard that boundary guards: without role composition, walking subsumption and part-of together derives FALSE ancestors (
A part_of BwithB ⊑ Cdoes not giveA ⊑ C).Closure::from_assertedtherefore takes aSubsumptiontype rather than raw pairs, so a mixed edge set cannot be fed in by accident.The depth guard is reported (
depth_cap) rather than silent, so a caller can tell "not entailed" from "the walk stopped".Hygiene
Zero-dependency,
forbid(unsafe_code),clippy -D warningsclean,cargo fmtclean. 8 tests, each carrying the input that would falsify it — transitivity paired with a must-NOT-entail case, the depth cap proven to bind and to release, cycles proven detected and absent on a non-trivial acyclic graph, the merge verdict proven to discriminate all three outcomes, and a pre-existing cycle proven not to be blamed on an innocent merge.docs/DISCOVERY-MAP.md:D-ELK-FACTFINDERappended.Generated by Claude Code