owl_dl_core/
transform.rs

1//! Structural transformation (Tseitin-style fresh-name introduction).
2//!
3//! ## Scope in Phase 1 v0
4//!
5//! This module is a **deliberate stub**. It exposes a stable
6//! [`transform`] function that the Phase 1 pipeline (`nnf -> told ->
7//! definitions -> absorb -> transform`) can call today, even though the
8//! current body is the identity. Phase 4 will fill it in.
9//!
10//! ## Why deferred
11//!
12//! Tseitin-style transformation introduces fresh atomic class names for
13//! complex sub-concepts that recur frequently — converting axioms like
14//! `A ⊑ ∃R.(C ⊓ D ⊓ E)` into `A ⊑ ∃R.X` plus `X ≡ C ⊓ D ⊓ E`. The
15//! tableau then labels nodes with the fresh `X` instead of carrying the
16//! conjunction.
17//!
18//! For the **standard tableau** we picked in strategy v2 §3.2, two
19//! pre-existing pieces of work already do most of what Tseitin buys:
20//!
21//! 1. [`crate::ConceptPool`] interns every distinct sub-expression to
22//!    a single [`crate::ConceptId`]. Logical equality is O(1) integer
23//!    comparison; sub-concept sharing is automatic.
24//! 2. [`crate::absorb`] converts most `⊤ ⊑ φ` axioms into triggers —
25//!    `ConceptRule` / `NominalRule` / `RoleRule` — that fire only when
26//!    needed, regardless of the structural complexity of φ.
27//!
28//! [`crate::Definitions`] (lazy unfolding) handles the remaining
29//! case where keeping a named atom in labels is preferable to expanding
30//! it.
31//!
32//! ## Phase 4 plan
33//!
34//! When this is revisited:
35//!
36//! - Walk every `ConceptId` reachable from the absorbed `TBox`.
37//! - Identify sub-expressions appearing in `N ≥ k` distinct contexts.
38//! - Synthesize a fresh class IRI in a `_TS_n` namespace, add to the
39//!   vocabulary, and emit a [`crate::Definitions`] entry binding it to
40//!   the body.
41//! - Rewrite the absorbed `TBox` to use the fresh name in place of the
42//!   original sub-expression.
43//!
44//! Implementation will live here, with the existing [`transform`] entry
45//! point evolving to do the work (or returning a richer struct that
46//! also carries the new vocabulary / definition entries).
47
48use crate::absorb::AbsorbedTBox;
49
50/// Phase 1 v0: identity. See module-level docs for what Phase 4 will
51/// add.
52#[must_use]
53pub fn transform(tbox: AbsorbedTBox) -> AbsorbedTBox {
54    tbox
55}
56
57#[cfg(test)]
58mod tests {
59    use super::*;
60    use crate::ConceptPool;
61    use crate::absorb::{AbsorbedTBox, ConceptRule};
62    use crate::ir::ClassId;
63
64    #[test]
65    fn identity_preserves_concept_rules() {
66        let mut pool = ConceptPool::new();
67        let a = pool.atomic(ClassId::new(0));
68        let input = AbsorbedTBox {
69            concept_rules: vec![ConceptRule {
70                trigger: ClassId::new(1),
71                conclusion: a,
72            }],
73            ..AbsorbedTBox::default()
74        };
75        let cloned = input.clone();
76        let output = transform(input);
77        assert_eq!(output, cloned);
78    }
79
80    #[test]
81    fn identity_preserves_empty_tbox() {
82        let output = transform(AbsorbedTBox::default());
83        assert_eq!(output, AbsorbedTBox::default());
84    }
85}
owl_dl_core/transform.rs

owl_dl_core/
transform.rs
