qualia_core_db/modalities/
dl.rs

1use crate::NQuin;
2
3/// Max distinct classes considered in one subsumption query (bounded, zero-heap).
4const DL_MAX_CLASSES: usize = 256;
5
6/// Returns true if `sub_class_hash` is subsumed by `super_class_hash` in the TBox.
7///
8/// Comprehensive: a full transitive-closure search over the `rdfs:subClassOf` **DAG**, so
9/// **multiple inheritance** is handled (a class may have many superclasses — e.g.
10/// `NaturalPerson ⊑ Agent` AND `NaturalPerson ⊑ self:HumanBeing`). Zero-heap (fixed
11/// frontier + visited arrays) and cycle-safe (visited set). The earlier version followed only
12/// the FIRST parent edge per node and silently missed every other inheritance path.
13pub fn check_subsumption_quin(
14    sub_class_hash: u64,
15    super_class_hash: u64,
16    tbox: &[NQuin], // Quins with predicate = q_hash("rdfs:subClassOf")
17) -> bool {
18    if sub_class_hash == super_class_hash {
19        return true;
20    }
21    let mut frontier = [0u64; DL_MAX_CLASSES];
22    let mut visited = [0u64; DL_MAX_CLASSES];
23    let mut fl = 1usize; // frontier length
24    let mut vl = 0usize; // visited length
25    frontier[0] = sub_class_hash;
26
27    while fl > 0 {
28        fl -= 1;
29        let current = frontier[fl];
30        if visited[..vl].contains(&current) {
31            continue;
32        }
33        if vl < DL_MAX_CLASSES {
34            visited[vl] = current;
35            vl += 1;
36        } else {
37            break; // closure exceeds the bound; refuse rather than mis-answer
38        }
39        for quin in tbox {
40            if quin.subject == current {
41                let parent = quin.object;
42                if parent == super_class_hash {
43                    return true;
44                }
45                if fl < DL_MAX_CLASSES && !visited[..vl].contains(&parent) {
46                    frontier[fl] = parent;
47                    fl += 1;
48                }
49            }
50        }
51    }
52    false
53}
54
55// ─── Structural SROIQ constructs (disjointness/clash, roles, cardinality, nominals) ─
56//
57// SCOPE (honest): these are the zero-heap STRUCTURAL constructs of SROIQ — concept disjointness
58// + clash detection (ABox consistency core), role hierarchies + transitivity, qualified
59// cardinality, and nominals — over an ABox/RBox of NQuins. The full ALC/SROIQ model-construction
60// TABLEAU (∃/∀ expansion with individual generation + blocking) is a separate research-grade
61// effort that ALSO conflicts with the zero-heap invariant (a tableau builds a dynamic model tree)
62// — recorded in AUDIT_BOUNDARY_DEFERRALS.md.
63
64/// Are concepts `a` and `b` declared DISJOINT in `disjoint` (symmetric pairs)?
65pub fn concepts_disjoint(a: u64, b: u64, disjoint: &[(u64, u64)]) -> bool {
66    disjoint
67        .iter()
68        .any(|&(c1, c2)| (c1 == a && c2 == b) || (c1 == b && c2 == a))
69}
70
71/// **Clash detection** (ABox consistency core): does an individual asserted to have all of
72/// `types` have a clash — two types that are disjoint, directly or via subsumption (`t1 ⊑ X`,
73/// `t2 ⊑ Y`, `X` disjoint `Y`)? Returns true on a clash (inconsistency). Zero-heap.
74pub fn abox_clash(types: &[u64], disjoint: &[(u64, u64)], tbox: &[NQuin]) -> bool {
75    for (i, &t1) in types.iter().enumerate() {
76        for &t2 in &types[i + 1..] {
77            if concepts_disjoint(t1, t2, disjoint) {
78                return true;
79            }
80            for &(d1, d2) in disjoint {
81                if (check_subsumption_quin(t1, d1, tbox) && check_subsumption_quin(t2, d2, tbox))
82                    || (check_subsumption_quin(t1, d2, tbox)
83                        && check_subsumption_quin(t2, d1, tbox))
84                {
85                    return true;
86                }
87            }
88        }
89    }
90    false
91}
92
93/// **Role hierarchy**: is `sub_role` subsumed by `super_role` (transitively) in the RBox of
94/// `rdfs:subPropertyOf` quins? (Same transitive-closure search as class subsumption.)
95#[inline]
96pub fn role_subsumes(sub_role: u64, super_role: u64, rbox: &[NQuin]) -> bool {
97    check_subsumption_quin(sub_role, super_role, rbox)
98}
99
100/// **Transitive role**: is `role` declared transitive?
101#[inline]
102pub fn is_transitive_role(role: u64, transitive_roles: &[u64]) -> bool {
103    transitive_roles.contains(&role)
104}
105
106/// Count an individual's `role`-successors that are instances of `filler_class` (directly or via
107/// subsumption) — for **qualified cardinality** restrictions. `abox` holds role assertions
108/// `(individual, role, successor)`; `type_assertions` holds `(individual, class)`. Zero-heap.
109pub fn count_qualified_fillers(
110    individual: u64,
111    role: u64,
112    filler_class: u64,
113    abox: &[NQuin],
114    type_assertions: &[(u64, u64)],
115    tbox: &[NQuin],
116) -> usize {
117    let mut count = 0usize;
118    for e in abox {
119        if e.subject == individual && e.predicate == role {
120            let succ = e.object;
121            if type_assertions
122                .iter()
123                .any(|&(s, c)| s == succ && check_subsumption_quin(c, filler_class, tbox))
124            {
125                count += 1;
126            }
127        }
128    }
129    count
130}
131
132/// Qualified MIN cardinality `≥ n R.C` satisfied?
133#[inline]
134pub fn min_cardinality_met(actual: usize, n: usize) -> bool {
135    actual >= n
136}
137
138/// Qualified MAX cardinality `≤ n R.C` satisfied?
139#[inline]
140pub fn max_cardinality_met(actual: usize, n: usize) -> bool {
141    actual <= n
142}
143
144/// **Nominal** `{a}`: a nominal concept has exactly one instance — `a` itself. Is `individual`
145/// the instance of the nominal `{nominal_individual}`?
146#[inline]
147pub fn is_nominal_instance(individual: u64, nominal_individual: u64) -> bool {
148    individual == nominal_individual
149}
150
151#[cfg(test)]
152mod tests {
153    use super::*;
154
155    #[test]
156    fn test_check_subsumption_quin() {
157        let tbox = vec![
158            NQuin {
159                subject: 10,
160                predicate: 0,
161                object: 20,
162                context: 0,
163                metadata: 0,
164                parity: 0,
165            },
166            NQuin {
167                subject: 20,
168                predicate: 0,
169                object: 30,
170                context: 0,
171                metadata: 0,
172                parity: 0,
173            },
174        ];
175
176        assert_eq!(check_subsumption_quin(10, 10, &tbox), true);
177        assert_eq!(check_subsumption_quin(10, 20, &tbox), true);
178        assert_eq!(check_subsumption_quin(10, 30, &tbox), true);
179        assert_eq!(check_subsumption_quin(10, 40, &tbox), false);
180        assert_eq!(check_subsumption_quin(20, 10, &tbox), false);
181    }
182
183    /// Comprehensive: MULTIPLE INHERITANCE + diamond (the old single-edge impl failed these).
184    #[test]
185    fn multiple_inheritance_dag() {
186        let e = |s: u64, o: u64| NQuin {
187            subject: s,
188            predicate: 1,
189            object: o,
190            context: 0,
191            metadata: 0,
192            parity: 0,
193        };
194        let (np, agent, human, moral) = (1u64, 2u64, 3u64, 4u64);
195        let tbox = [
196            e(np, agent),    // NaturalPerson ⊑ Agent       (first parent)
197            e(np, human),    // NaturalPerson ⊑ HumanBeing  (SECOND parent — old impl missed this)
198            e(human, moral), // HumanBeing ⊑ MoralFrame
199            e(agent, moral), // Agent ⊑ MoralFrame          (diamond)
200        ];
201        assert!(check_subsumption_quin(np, agent, &tbox), "via first parent");
202        assert!(
203            check_subsumption_quin(np, human, &tbox),
204            "via SECOND parent (multiple inheritance)"
205        );
206        assert!(
207            check_subsumption_quin(np, moral, &tbox),
208            "transitively via either diamond path"
209        );
210        assert!(
211            !check_subsumption_quin(agent, human, &tbox),
212            "Agent is not a HumanBeing"
213        );
214    }
215
216    #[test]
217    fn disjointness_clash_detection() {
218        let sub = 1u64; // pretend predicate
219        let e = |s: u64, o: u64| NQuin {
220            subject: s,
221            predicate: sub,
222            object: o,
223            context: 0,
224            metadata: 0,
225            parity: 0,
226        };
227        let (human, robot, agent, machine) = (10u64, 20u64, 30u64, 40u64);
228        let tbox = [e(human, agent), e(robot, machine)]; // Human⊑Agent, Robot⊑Machine
229        let disjoint = [(agent, machine)]; // Agent disjoint Machine
230                                           // Direct disjointness.
231        assert!(concepts_disjoint(agent, machine, &disjoint));
232        // An individual that is both Human and Robot clashes (Human⊑Agent, Robot⊑Machine, Agent⊥Machine).
233        assert!(abox_clash(&[human, robot], &disjoint, &tbox));
234        // Human alone, or Human+Agent, is consistent.
235        assert!(!abox_clash(&[human, agent], &disjoint, &tbox));
236    }
237
238    #[test]
239    fn roles_cardinality_nominals() {
240        let sp = 7u64;
241        let e = |s: u64, o: u64| NQuin {
242            subject: s,
243            predicate: sp,
244            object: o,
245            context: 0,
246            metadata: 0,
247            parity: 0,
248        };
249        let (has_mother, has_parent) = (100u64, 200u64);
250        let rbox = [e(has_mother, has_parent)]; // hasMother ⊑ hasParent
251        assert!(role_subsumes(has_mother, has_parent, &rbox));
252        assert!(!role_subsumes(has_parent, has_mother, &rbox));
253        assert!(is_transitive_role(
254            crate::q_hash("role:ancestorOf"),
255            &[crate::q_hash("role:ancestorOf")]
256        ));
257
258        // Qualified cardinality: alice has 2 children who are Students.
259        let role = crate::q_hash("role:hasChild");
260        let student = crate::q_hash("class:Student");
261        let (alice, bob, cara) = (
262            crate::q_hash("ind:alice"),
263            crate::q_hash("ind:bob"),
264            crate::q_hash("ind:cara"),
265        );
266        let mut a1 = NQuin {
267            subject: alice,
268            predicate: role,
269            object: bob,
270            context: 0,
271            metadata: 0,
272            parity: 0,
273        };
274        a1.parity = a1.subject ^ a1.predicate ^ a1.object;
275        let mut a2 = a1;
276        a2.object = cara;
277        a2.parity = a2.subject ^ a2.predicate ^ a2.object;
278        let abox = [a1, a2];
279        let types = [(bob, student), (cara, student)];
280        let n = count_qualified_fillers(alice, role, student, &abox, &types, &[]);
281        assert_eq!(n, 2);
282        assert!(min_cardinality_met(n, 2) && !min_cardinality_met(n, 3));
283        assert!(max_cardinality_met(n, 2) && !max_cardinality_met(n, 1));
284
285        // Nominal {alice} has exactly alice as its instance.
286        assert!(is_nominal_instance(alice, alice));
287        assert!(!is_nominal_instance(bob, alice));
288    }
289}
qualia_core_db/modalities/dl.rs

qualia_core_db/modalities/
dl.rs
