Merge pull request #14 from docknetwork/open-ended

implement open-ended reasoning

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "rify"
-version = "0.6.0"
+version = "0.7.0"
 authors = [
   "Andrew Dirksen <[email protected]>",
   "Sam Hellawell <[email protected]>"

README.md

@@ -8,7 +8,7 @@ Rify is a [forward chaining](https://en.wikipedia.org/wiki/Forward_chaining) [in
 
 It accepts conjunctive rules with limited expressiveness so reasoning is bounded by `O(n^k)` in both memory and in computation where n is the number of nodes in the input RDF dataset.
 
-Reasoning generates a proof which can be used to quickly verify the result pragmatically.
+Given premises and target statement[s], rify can generate a proof which can be used to quickly verify the result programatically.
 
 Logical rules are defined as if-then clauses. Something like this:
 
@@ -48,11 +48,11 @@ Rify doesn't care whether its input and output is valid rdf. For example, it wil
 
 # Use
 
-Two functions are central to this library: `prove` and `validate`.
+Three functions are central to this library: `prove`, `validate`, and `infer`.
 
-```rust
-// Example use of `prove`
+## prove
 
+```rust
 use rify::{
     prove,
     Entity::{Unbound, Bound},
@@ -96,13 +96,13 @@ assert_eq!(
 );
 ```
 
-```rust
-// Example use of `validate`
+# validate
 
+```rust
 use rify::{
     prove, validate, Valid,
     Rule, RuleApplication,
-	Entity::{Bound, Unbound}
+    Entity::{Bound, Unbound}
 };
 
 // same as above
@@ -131,6 +131,43 @@ let Valid { assumed, implied } = validate::<&str, &str>(
 // quads in `implied` are also true.
 ```
 
+## infer
+
+```rust
+use rify::{infer, Entity::{Unbound, Bound}, Rule};
+
+// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
+let awesome_score_axiom = Rule::create(
+    vec![
+        // if someone is awesome
+        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
+        // and they have some score
+        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
+    ],
+    vec![
+        // then they must have an awesome score
+        [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]
+    ],
+).expect("invalid rule");
+
+let mut facts = vec![
+    ["you", "score", "unspecified", "default_graph"],
+    ["you", "is", "awesome", "default_graph"]
+];
+
+let new_facts = infer::<&str, &str>(&facts, &[awesome_score_axiom]);
+facts.extend(new_facts);
+
+assert_eq!(
+    &facts,
+    &[
+        ["you", "score", "unspecified", "default_graph"],
+        ["you", "is", "awesome", "default_graph"],
+        ["you", "score", "awesome", "default_graph"],
+    ],
+);
+```
+
 # Recipes
 
 In addition to normal cargo commands like `cargo test` and `cargo check` the `./justfile`

bindings/js_wasm/binding_tests/test.js

@@ -1,4 +1,4 @@
-import { prove, validate } from 'rify';
+import { prove, validate, infer } from 'rify';
 import { expect } from 'chai';
 
 // poor man's replacement for jest because making jest work with webpack+wasm is problematic
@@ -232,6 +232,30 @@ tests([
     // After verifying all the assumptions in the proof are true, we know that the
     // quads in valid.implied are true with respect to the provided rules.
   }],
+
+  ['Example from doctest for infer actually runs.', () => {
+    // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
+    let awesome_score_axiom = {
+      if_all: [
+        [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }],
+        [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }],
+      ],
+      then: [
+        [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }]
+      ],
+    };
+    let facts = [
+      ["you", "score", "unspecified", "default_graph"],
+      ["you", "is", "awesome", "default_graph"],
+    ];
+    let new_facts = infer(facts, [awesome_score_axiom]);
+    facts = facts.concat(new_facts);
+    expect(facts).to.deep.equal([
+      ["you", "score", "unspecified", "default_graph"],
+      ["you", "is", "awesome", "default_graph"],
+      ["you", "score", "awesome", "default_graph"],
+    ]);
+  }],
 ]);
 
 /// catch whichever error is emitted by when cb is called and return it

bindings/js_wasm/package.json

@@ -5,7 +5,7 @@
     "Sam Hellawell <[email protected]>"
   ],
   "description": "RDF reasoner that operates on RIF-like conjunctive rules. Outputs a machine\nreadable proof of some claim which can be cheaply verified.\n",
-  "version": "0.6.0",
+  "version": "0.7.0",
   "license": "MIT OR Apache-2.0",
   "repository": {
     "type": "git",

bindings/js_wasm/src/js_wasm_test.rs

@@ -11,6 +11,7 @@ type ProofInput = Vec<RuleApplication<String>>;
 /// with the actual interface
 fn _types_correct(r: RulesInput, c: ClaimsInput, p: ProofInput) -> ProofInput {
     super::validate_(r.clone(), p).unwrap();
+    super::infer_(c.clone(), r.clone()).unwrap();
     super::prove_(c.clone(), c, r).unwrap()
 }
 

bindings/js_wasm/src/lib.rs

@@ -134,6 +134,44 @@ pub fn validate_(
     Ok(valid)
 }
 
+/// Make all possible true inferences given input premises and rules. This is open-ended reasoning.
+///
+/// ```js
+/// // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
+/// let awesome_score_axiom = {
+///   if_all: [
+///     [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }],
+///     [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }],
+///   ],
+///   then: [
+///     [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }]
+///   ],
+/// };
+/// let facts = [
+///   ["you", "score", "unspecified", "default_graph"],
+///   ["you", "is", "awesome", "default_graph"],
+/// ];
+/// let new_facts = infer(facts, [awesome_score_axiom]);
+/// facts = facts.concat(new_facts);
+/// expect(facts).to.deep.equal([
+///   ["you", "score", "unspecified", "default_graph"],
+///   ["you", "is", "awesome", "default_graph"],
+///   ["you", "score", "awesome", "default_graph"],
+/// ]);
+/// ```
+#[wasm_bindgen]
+pub fn infer(premises: Box<[JsValue]>, rules: Box<[JsValue]>) -> Result<JsValue, JsValue> {
+    Ok(ser(&infer_(deser_list(&premises)?, deser_list(&rules)?)?))
+}
+
+pub fn infer_(
+    premises: Vec<[String; 4]>,
+    rules: Vec<RuleUnchecked>,
+) -> Result<Vec<[String; 4]>, Error> {
+    let rules = RuleUnchecked::check_all(rules)?;
+    Ok(rify::infer::<String, String>(&premises, &rules))
+}
+
 #[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone, serde::Serialize, serde::Deserialize)]
 pub enum Entity {
     Unbound(String),

src/common.rs

@@ -1,3 +1,11 @@
+use crate::reasoner::Quad;
+use crate::rule::Rule;
+use crate::translator::Translator;
+use crate::Entity;
+use crate::RuleApplication;
+use alloc::collections::BTreeMap;
+use core::fmt::Debug;
+
 /// Increment argument then return previous value.
 ///
 /// ```nocompile
@@ -19,6 +27,101 @@ where
     ret
 }
 
+#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
+/// A proof element that has yet to be translated to a presentable form.
+///
+/// [crate::prove::prove] function does not immediately convert LowRuleApplication's to
+/// [RuleApplication]'s. Rather, it converts only the LowRuleApplication's it is going to return
+/// to the caller.
+pub struct LowRuleApplication {
+    pub rule_index: usize,
+    pub instantiations: BTreeMap<usize, usize>,
+}
+
+impl LowRuleApplication {
+    /// Translate to a higher representation [RuleApplication]. The higher representation is
+    /// portable to other machines as long as those machines assume the same rule list.
+    /// This lower representation is not portable.
+    ///
+    /// Panics
+    ///
+    /// This function will panic if:
+    ///   - an unbound item from originial_rule is not instatiated by self
+    ///   - or there is no translation for a global instatiation of one of the unbound entities in
+    ///     original_rule.
+    pub fn raise<Unbound: Ord, Bound: Ord + Clone>(
+        &self,
+        original_rule: &Rule<Unbound, Bound>,
+        trans: &Translator<Bound>,
+    ) -> RuleApplication<Bound> {
+        let mut instantiations = Vec::new();
+
+        // unbound_human -> unbound_local
+        let uhul: BTreeMap<&Unbound, usize> = original_rule
+            .cononical_unbound()
+            .enumerate()
+            .map(|(i, a)| (a, i))
+            .collect();
+
+        for unbound_human in original_rule.cononical_unbound() {
+            let unbound_local: usize = uhul[unbound_human];
+            let bound_global: usize = self.instantiations[&unbound_local];
+            let bound_human: &Bound = trans.back(bound_global).unwrap();
+            instantiations.push(bound_human.clone());
+        }
+
+        RuleApplication {
+            rule_index: self.rule_index,
+            instantiations,
+        }
+    }
+}
+
+/// Attempt to forward translate a quad.
+/// This is a helper function. It translates all four element of a quad, calling
+/// [Translator::forward] for each element. If any element has no translation
+/// this function will return `None`.
+pub fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad> {
+    let [s, p, o, g] = key;
+    Some(
+        [
+            translator.forward(s)?,
+            translator.forward(p)?,
+            translator.forward(o)?,
+            translator.forward(g)?,
+        ]
+        .into(),
+    )
+}
+
+/// Reverse of [forward].
+/// [forward] translates each element from `T` to `usize`. This function translates each element
+/// from `usize` to `T`. If any element has no translation this function will return `None`.
+pub fn back<T: Ord>(translator: &Translator<T>, key: Quad) -> Option<[&T; 4]> {
+    let Quad { s, p, o, g } = key;
+    Some([
+        translator.back(s.0)?,
+        translator.back(p.0)?,
+        translator.back(o.0)?,
+        translator.back(g.0)?,
+    ])
+}
+
+/// list with repetition all bound vertices of rules and all verticies of premises
+pub fn vertices<'a, 'b, 'c, Bound, Unbound>(
+    premises: &'a [[Bound; 4]],
+    rules: &'b [Rule<Unbound, Bound>],
+) -> impl Iterator<Item = &'c Bound>
+where
+    'a: 'c,
+    'b: 'c,
+{
+    rules
+        .iter()
+        .flat_map(|rule| rule.iter_entities().filter_map(Entity::as_bound))
+        .chain(premises.iter().flatten())
+}
+
 #[cfg(test)]
 mod test_util {
     use core::fmt::Debug;