rify/
rule.rs

1//! Defines a human frendly-ish logical rule representation [Rule].
2
3use crate::common::inc;
4use crate::reasoner::{Instantiations, Quad};
5use crate::translator::Translator;
6use alloc::collections::BTreeMap;
7use alloc::collections::BTreeSet;
8use core::fmt::Debug;
9use core::fmt::Display;
10
11#[derive(Clone, Debug, PartialEq, Eq)]
12/// The reasoner's rule representation.
13/// It is is optimized machine use, not human use. Comprehending and writing these rules directly
14/// is difficult for humans.
15/// [Rule] is the human friendly representation.
16/// A [Rule] can be converted to a [LowRule] via the [Rule::lower].
17/// We hide the lowered rule representation from the user of this library.
18/// Interfaces like [crate::prove::prove], [crate::validate::validate], and [crate::infer::infer]
19/// accept [Rule] as input and lower to this representation before passing it to the reasoner.
20///
21/// Invariants held:
22///   unbound names may not exists in `then` unless they exist also in `if_all`
23// TODO: find a way to make fields non-public to protect invariant
24pub(crate) struct LowRule {
25    pub if_all: Vec<Quad>,    // contains locally scoped names
26    pub then: Vec<Quad>,      // contains locally scoped names
27    pub inst: Instantiations, // partially maps the local scope to some global scope
28}
29
30#[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)]
31#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
32pub enum Entity<Unbound, Bound> {
33    Unbound(Unbound),
34    Bound(Bound),
35}
36
37impl<Unbound, Bound> Entity<Unbound, Bound> {
38    pub fn as_unbound(&self) -> Option<&Unbound> {
39        match self {
40            Entity::Unbound(s) => Some(s),
41            Entity::Bound(_) => None,
42        }
43    }
44
45    pub fn as_bound(&self) -> Option<&Bound> {
46        match self {
47            Entity::Unbound(_) => None,
48            Entity::Bound(s) => Some(s),
49        }
50    }
51}
52
53#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone)]
54#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
55/// A human friendly-ish logical rule representation. Each rule represents an
56/// if-then statement (implication relationship). Statements in the rule
57/// may contain constants and/or variables. Constants are represented as [Entity::Bound].
58/// Variables are represented as [Entity::Unbound].
59///
60/// So that rules remain turing-incomplete, an invariant is upheld:
61/// Unbound entities may not exists in the `then` clause unless they exist also in the `if_all`
62/// clause.
63pub struct Rule<Unbound, Bound> {
64    if_all: Vec<[Entity<Unbound, Bound>; 4]>,
65    then: Vec<[Entity<Unbound, Bound>; 4]>,
66}
67
68impl<'a, Unbound: Ord + Clone, Bound: Ord> Rule<Unbound, Bound> {
69    /// This constructor ensures that any unbound element in `then` also exists somewhere
70    /// in `if_all`. If this is not the case the rule is invalid and the function will return
71    /// `Err`. Otherwise it will return `Ok`.
72    pub fn create(
73        if_all: Vec<[Entity<Unbound, Bound>; 4]>,
74        then: Vec<[Entity<Unbound, Bound>; 4]>,
75    ) -> Result<Self, InvalidRule<Unbound>> {
76        let unbound_if = if_all.iter().flatten().filter_map(Entity::as_unbound);
77        let unbound_then = then.iter().flatten().filter_map(Entity::as_unbound);
78
79        for th in unbound_then.clone() {
80            if !unbound_if.clone().any(|ifa| ifa == th) {
81                return Err(InvalidRule::UnboundImplied(th.clone()));
82            }
83        }
84
85        Ok(Self { if_all, then })
86    }
87
88    /// Converts [Rule] to [LowRule]. As part of the conversion
89    /// this function uses `translator` to convert bound entities to
90    /// the usize representation. If the rule contains any bound entity for which the translator
91    /// contains no translation this function will return `Err`. Otherwise it will return `Ok`.
92    pub(crate) fn lower(&self, tran: &Translator<Bound>) -> Result<LowRule, NoTranslation<&Bound>> {
93        // There are three types of name at play here.
94        // - human names are represented as Entities
95        // - local names are local to the rule we are creating. they are represented as usize
96        // - global names assigned by Translator. they are represented as usize
97
98        // assign local names to each human name
99        // local names will be in a continous range from 0.
100        // smaller local names will represent unbound entities, larger ones will represent bound
101        let mut next_local = 0usize;
102        let unbound_map: BTreeMap<&Unbound, usize> = assign_ids(
103            self.if_all.iter().flatten().filter_map(Entity::as_unbound),
104            &mut next_local,
105        );
106        let bound_map = assign_ids(
107            self.iter_entities().filter_map(Entity::as_bound),
108            &mut next_local,
109        );
110        debug_assert!(
111            bound_map.values().all(|bound_local| unbound_map
112                .values()
113                .all(|unbound_local| bound_local > unbound_local)),
114            "unbound names are smaller than bound names"
115        );
116        debug_assert_eq!(
117            (0..next_local).collect::<BTreeSet<usize>>(),
118            unbound_map
119                .values()
120                .chain(bound_map.values())
121                .cloned()
122                .collect(),
123            "no names slots are wasted"
124        );
125        debug_assert_eq!(
126            next_local,
127            unbound_map.values().chain(bound_map.values()).count(),
128            "no duplicate assignments"
129        );
130
131        // gets the local name for a human_name
132        let local_name = |entity: &Entity<Unbound, Bound>| -> usize {
133            match entity {
134                Entity::Unbound(s) => unbound_map[s],
135                Entity::Bound(s) => bound_map[s],
136            }
137        };
138        // converts a human readable restriction list to a list of locally scoped machine oriented
139        // restrictions
140        let to_requirements = |hu: &[[Entity<Unbound, Bound>; 4]]| -> Vec<Quad> {
141            hu.iter()
142                .map(|[s, p, o, g]| {
143                    [
144                        local_name(&s),
145                        local_name(&p),
146                        local_name(&o),
147                        local_name(&g),
148                    ]
149                    .into()
150                })
151                .collect()
152        };
153
154        Ok(LowRule {
155            if_all: to_requirements(&self.if_all),
156            then: to_requirements(&self.then),
157            inst: bound_map
158                .iter()
159                .map(|(human_name, local_name)| {
160                    let global_name = tran.forward(human_name).ok_or(NoTranslation(*human_name))?;
161                    Ok((*local_name, global_name))
162                })
163                .collect::<Result<_, _>>()?,
164        })
165    }
166}
167
168impl<'a, Unbound: Ord, Bound> Rule<Unbound, Bound> {
169    /// List the unique unbound names in this rule in order of appearance.
170    pub(crate) fn cononical_unbound(&self) -> impl Iterator<Item = &Unbound> {
171        let mut listed = BTreeSet::<&Unbound>::new();
172        self.if_all
173            .iter()
174            .flatten()
175            .filter_map(Entity::as_unbound)
176            .filter(move |unbound| listed.insert(unbound))
177    }
178}
179
180impl<'a, Unbound, Bound> Rule<Unbound, Bound> {
181    pub fn iter_entities(&self) -> impl Iterator<Item = &Entity<Unbound, Bound>> {
182        self.if_all.iter().chain(self.then.iter()).flatten()
183    }
184
185    pub fn if_all(&self) -> &[[Entity<Unbound, Bound>; 4]] {
186        &self.if_all
187    }
188
189    pub fn then(&self) -> &[[Entity<Unbound, Bound>; 4]] {
190        &self.then
191    }
192}
193
194#[derive(Clone, Debug, PartialEq, Eq)]
195#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
196pub enum InvalidRule<Unbound> {
197    /// Implied statements (part of the "then" property) must not contain unbound symbols that do
198    /// not exist in the other side of the expression.
199    ///
200    /// Examples of rules that would cause this error:
201    ///
202    /// ```customlang
203    /// // all statements are true
204    /// -> (?a, ?a, ?a)
205    ///
206    /// // conditional universal statement
207    /// (<sun> <enabled> <false>) -> (?a <color> <black>)
208    /// ```
209    UnboundImplied(Unbound),
210}
211
212impl<Unbound: Debug> Display for InvalidRule<Unbound> {
213    fn fmt(&self, fmtr: &mut core::fmt::Formatter<'_>) -> Result<(), core::fmt::Error> {
214        Debug::fmt(self, fmtr)
215    }
216}
217
218#[cfg(feature = "std")]
219impl<Unbound> std::error::Error for InvalidRule<Unbound> where InvalidRule<Unbound>: Debug + Display {}
220
221#[derive(Debug, Eq, PartialEq)]
222/// The rule contains terms that have no corresponding entity in the translators target universe.
223pub struct NoTranslation<T>(T);
224
225// assign a unique id to each unique element in the input
226// starts counting with the current next_id. As ids are assigned
227// the next_id value is incremented so it always reperesents the next available id
228fn assign_ids<T: Ord>(inp: impl Iterator<Item = T>, next_id: &mut usize) -> BTreeMap<T, usize> {
229    let mut ret: BTreeMap<T, usize> = BTreeMap::new();
230    for unbound in inp {
231        ret.entry(unbound).or_insert_with(|| inc(next_id));
232    }
233    ret
234}
235
236#[cfg(test)]
237mod test {
238    use super::Entity::{Bound, Unbound};
239    use super::*;
240    use core::iter::FromIterator;
241
242    #[test]
243    fn similar_names() {
244        // test rule
245        // (?a <a> <b>) ->
246        // ?a should be a separate entity from <a>
247
248        let rule = Rule::<&str, &str> {
249            if_all: vec![[Unbound("a"), Bound("a"), Unbound("b"), Unbound("g")]],
250            then: vec![],
251        };
252        let trans: Translator<&str> = ["a"].iter().cloned().collect();
253        let rr = rule.lower(&trans).unwrap();
254
255        // ?a != <a>
256        assert_ne!(rr.if_all[0].s.0, rr.if_all[0].p.0);
257    }
258
259    #[test]
260    fn lower() {
261        // rules: (?a parent ?b) -> (?a ancestor ?b)
262        //        (?a ancestor ?b) and (?b ancestor ?c) -> (?a ancestor ?c)
263
264        let trans: Translator<&str> = ["parent", "ancestor"].iter().cloned().collect();
265
266        {
267            let rulea = Rule::<u16, &str> {
268                if_all: vec![[Unbound(0xa), Bound("parent"), Unbound(0xb), Unbound(0xc)]],
269                then: vec![[Unbound(0xa), Bound("ancestor"), Unbound(0xb), Unbound(0xc)]],
270            };
271
272            let re_rulea = rulea.lower(&trans).unwrap();
273            let keys = [
274                re_rulea.if_all[0].s.0,
275                re_rulea.if_all[0].p.0,
276                re_rulea.if_all[0].o.0,
277                re_rulea.if_all[0].g.0,
278                re_rulea.then[0].s.0,
279                re_rulea.then[0].p.0,
280                re_rulea.then[0].o.0,
281                re_rulea.then[0].g.0,
282            ];
283            let vals: Vec<Option<&str>> = keys
284                .iter()
285                .map(|local_name| {
286                    re_rulea
287                        .inst
288                        .get(*local_name)
289                        .map(|global_name| trans.back(*global_name).unwrap().clone())
290                })
291                .collect();
292            assert_eq!(
293                &vals,
294                &[
295                    None,
296                    Some("parent"),
297                    None,
298                    None,
299                    None,
300                    Some("ancestor"),
301                    None,
302                    None,
303                ]
304            );
305
306            let ifa = re_rulea.if_all;
307            let then = re_rulea.then;
308            assert_ne!(ifa[0].p.0, then[0].p.0); // "parent" != "ancestor"
309            assert_eq!(ifa[0].s.0, then[0].s.0); // a == a
310            assert_eq!(ifa[0].o.0, then[0].o.0); // b == b
311        }
312
313        {
314            let ruleb = Rule::<&str, &str> {
315                if_all: vec![
316                    [Unbound("a"), Bound("ancestor"), Unbound("b"), Unbound("g")],
317                    [Unbound("b"), Bound("ancestor"), Unbound("c"), Unbound("g")],
318                ],
319                then: vec![[Unbound("a"), Bound("ancestor"), Unbound("c"), Unbound("g")]],
320            };
321
322            let re_ruleb = ruleb.lower(&trans).unwrap();
323            let keys = [
324                re_ruleb.if_all[0].s.0,
325                re_ruleb.if_all[0].p.0,
326                re_ruleb.if_all[0].o.0,
327                re_ruleb.if_all[0].g.0,
328                re_ruleb.if_all[1].s.0,
329                re_ruleb.if_all[1].p.0,
330                re_ruleb.if_all[1].o.0,
331                re_ruleb.if_all[1].g.0,
332                re_ruleb.then[0].s.0,
333                re_ruleb.then[0].p.0,
334                re_ruleb.then[0].o.0,
335                re_ruleb.then[0].g.0,
336            ];
337            let vals: Vec<Option<&str>> = keys
338                .iter()
339                .map(|local_name| {
340                    re_ruleb
341                        .inst
342                        .get(*local_name)
343                        .map(|global_name| trans.back(*global_name).unwrap().clone())
344                })
345                .collect();
346            assert_eq!(
347                &vals,
348                &[
349                    None,
350                    Some("ancestor"),
351                    None,
352                    None,
353                    None,
354                    Some("ancestor"),
355                    None,
356                    None,
357                    None,
358                    Some("ancestor"),
359                    None,
360                    None,
361                ]
362            );
363
364            let ifa = re_ruleb.if_all;
365            let then = re_ruleb.then;
366            assert_ne!(ifa[0].s.0, ifa[1].s.0); // a != b
367            assert_ne!(ifa[0].o.0, then[0].o.0); // b != c
368
369            // "ancestor" == "ancestor" == "ancestor"
370            assert_eq!(ifa[0].p.0, ifa[1].p.0);
371            assert_eq!(ifa[1].p.0, then[0].p.0);
372
373            assert_eq!(ifa[0].s.0, then[0].s.0); // a == a
374            assert_eq!(ifa[1].o.0, then[0].o.0); // b == b
375        }
376    }
377
378    #[test]
379    fn lower_no_translation_err() {
380        let trans = Translator::<&str>::from_iter(vec![]);
381
382        let r = Rule::create(
383            vec![[Unbound("a"), Bound("unknown"), Unbound("b"), Unbound("g")]],
384            vec![],
385        )
386        .unwrap();
387        let err = r.lower(&trans).unwrap_err();
388        assert_eq!(err, NoTranslation(&"unknown"));
389
390        let r = Rule::<&str, &str>::create(
391            vec![],
392            vec![[
393                Bound("unknown"),
394                Bound("unknown"),
395                Bound("unknown"),
396                Bound("unknown"),
397            ]],
398        )
399        .unwrap();
400        let err = r.lower(&trans).unwrap_err();
401        assert_eq!(err, NoTranslation(&"unknown"));
402    }
403
404    #[test]
405    fn create_invalid() {
406        use Bound as B;
407        use Unbound as U;
408
409        Rule::<&str, &str>::create(vec![], vec![[U("a"), U("a"), U("a"), U("a")]]).unwrap_err();
410
411        // Its unfortunate that this one is illegal but I have yet to find a way around the
412        // limitation. Can you figure out how to do this safely?
413        //
414        // if [super? claims [minor? mayclaim pred?]]
415        // and [minor? claims [s? pred? o?]]
416        // then [super? claims [s? pred? o?]]
417        //
418        // The problem is that "then" clauses aren't allowed to create new entities. A new entity is
419        // needed in order to state that last line. Example:
420        //
421        let ret = Rule::<&str, &str>::create(
422            vec![
423                // if [super? claims [minor? mayclaim pred?] g?]
424                [U("super"), B("claims"), U("claim1"), U("g")],
425                [U("claim1"), B("subject"), U("minor"), U("g")],
426                [U("claim1"), B("predicate"), B("mayclaim"), U("g")],
427                [U("claim1"), B("object"), U("pred"), U("g")],
428                // and [minor? claims [s? pred? o?] g?]
429                [U("minor"), B("claims"), U("claim2"), U("g")],
430                [U("claim2"), B("subject"), U("s"), U("g")],
431                [U("claim2"), B("predicate"), U("pred"), U("g")],
432                [U("claim2"), B("object"), U("o"), U("g")],
433            ],
434            vec![
435                // then [super? claims [s? pred? o?] g?]
436                [U("super"), B("claims"), U("claim3"), U("g")],
437                [U("claim3"), B("subject"), U("s"), U("g")],
438                [U("claim3"), B("predicate"), U("pred"), U("g")],
439                [U("claim3"), B("object"), U("o"), U("g")],
440            ],
441        );
442        assert_eq!(ret, Err(InvalidRule::UnboundImplied("claim3")));
443
444        // Watch out! You may think that the following is a valid solution, but it's not.
445        //
446        // DANGEROUS, do not use without further consideration:
447        //
448        // ```
449        // if [super? claims c1?]
450        // and [c1? subject minor?]
451        // and [c1? predicate mayclaim]
452        // and [c1? object pred?]
453        //
454        // and [minor? claims c2?]
455        // and [c2? subject s?]
456        // and [c2? predicate pred?]
457        // and [c2? object o?]
458        //
459        // then [super? claims c2?]
460        // ```
461        //
462        // This is potentially dangerously incorrect because c2? may have any number of other
463        // subjects, predicates, or objects. Consider if the following were premises:
464        //
465        // ```
466        // [alice claims _:c1]
467        // [_:c1 subject s?]
468        // [_:c1 predicate mayclaim]
469        // [_:c1 object maysit]
470        //
471        // [bob claims _:c2]
472        // [_:c2 subject charlie]
473        // [_:c2 predicate maysit]
474        // [_:c2 predicate owns]
475        // [_:c2 object chair]
476        // ```
477        //
478        // With these premises, it can be proven that [alice claims [charlie owns chair]]
479        // even though alice only intendend to let [alice claims [charlie maysit chair]]
480        //
481        // Question: Is it possible to guard against these tricky premises?
482    }
483
484    #[test]
485    fn serde() {
486        #[derive(Debug, serde::Serialize, serde::Deserialize, PartialEq, Eq)]
487        enum Term {
488            Blank(String),
489            Iri(String),
490            Literal {
491                value: String,
492                datatype: String,
493                #[serde(skip_serializing_if = "Option::is_none")]
494                language: Option<String>,
495            },
496            DefaultGraph,
497        }
498
499        let jsonrule = serde_json::json![{
500            "if_all": [
501                [
502                    { "Unbound": "pig" },
503                    { "Bound": { "Iri": "https://example.com/Ability" } },
504                    { "Bound": { "Iri": "https://example.com/Flight" } },
505                    { "Bound": "DefaultGraph" },
506                ],
507                [
508                    { "Unbound": "pig" },
509                    { "Bound": { "Iri": "http://www.w3.org/1999/02/22-rdf-syntax-ns#type" } },
510                    { "Bound": { "Iri": "https://example.com/Pig" } },
511                    { "Bound": "DefaultGraph" },
512                ],
513            ],
514            "then": [
515                [
516                    { "Bound": { "Iri": "did:dock:bddap" } },
517                    { "Bound": { "Iri": "http://xmlns.com/foaf/spec/#term_firstName" } },
518                    {
519                        "Bound": {
520                            "Literal": {
521                                "value": "Gorgadon",
522                                "datatype": "http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral",
523                            },
524                        },
525                    },
526                    { "Bound": "DefaultGraph" },
527                ],
528            ],
529        }];
530
531        let rule = Rule::<String, Term> {
532            if_all: vec![
533                [
534                    Entity::Unbound("pig".to_string()),
535                    Entity::Bound(Term::Iri("https://example.com/Ability".to_string())),
536                    Entity::Bound(Term::Iri("https://example.com/Flight".to_string())),
537                    Entity::Bound(Term::DefaultGraph),
538                ],
539                [
540                    Entity::Unbound("pig".to_string()),
541                    Entity::Bound(Term::Iri(
542                        "http://www.w3.org/1999/02/22-rdf-syntax-ns#type".to_string(),
543                    )),
544                    Entity::Bound(Term::Iri("https://example.com/Pig".to_string())),
545                    Entity::Bound(Term::DefaultGraph),
546                ],
547            ],
548            then: vec![[
549                Entity::Bound(Term::Iri("did:dock:bddap".to_string())),
550                Entity::Bound(Term::Iri(
551                    "http://xmlns.com/foaf/spec/#term_firstName".to_string(),
552                )),
553                Entity::Bound(Term::Literal {
554                    value: "Gorgadon".to_string(),
555                    datatype: "http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral".to_string(),
556                    language: None,
557                }),
558                Entity::Bound(Term::DefaultGraph),
559            ]],
560        };
561
562        assert_eq!(
563            &serde_json::from_value::<Rule::<String, Term>>(jsonrule.clone()).unwrap(),
564            &rule
565        );
566        assert_eq!(
567            &jsonrule,
568            &serde_json::to_value::<Rule::<String, Term>>(rule).unwrap()
569        );
570    }
571}
rify/rule.rs

rify/
rule.rs
