Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

implement open-ended reasoning #14

Merged
merged 11 commits into from
Apr 12, 2021
Merged

implement open-ended reasoning #14

merged 11 commits into from
Apr 12, 2021

Conversation

bddap
Copy link
Contributor

@bddap bddap commented Mar 16, 2021

This pr adds a new function. infer

infer doesn't have a goal in mind like prove does.
Unlike validate, infer thinks for itself. It generates its own conclusions.
infer is an open minded individual who won't stop until it groks its universe in full.

:)

@bddap bddap changed the title [WIP] implement open-ended reasoning implement open-ended reasoning Mar 25, 2021
}
}

/// Attempt to forward translate a quad.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

would be really useful for future maintainers to have a high level comment of what forward means
(even if it seems redundant from translator.rs)

btw does forward mean find the index of each of s,p,o, and g ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in 55978e7

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Translator is a bi-directional dictionary from one language to another. One language is T and the other is usize.

forall t in T
  if trans.forward(t) == Some(u)
  then trans.back(u) == Some(t)

btw does forward mean find the index of each of s,p,o, and g ?

If you want to call members of the second language (usize) indices then sure.
The fact that they are indices is an implementation detail. Translator currently looks like this:

pub struct Translator<T> {
    widdershins: Box<[T]>,
}

But a less efficient version of Translator might look like this:

pub struct Translator<T> {
    widdershins: BtreeMap<usize, T>,
    deosil: BtreeMap<T, usize>,
}

src/common.rs Outdated
)
}

/// Reverse of forward.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same as above

and does this mean replace each index with the actual corresponding item ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in 55978e7

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

and does this mean replace each index with the actual corresponding item ?

yes? I think? See above comment.

@@ -19,6 +27,87 @@ where
ret
}

#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I realize I should have pointed that out in the previous PR,

Could you add doc-comments for both highlighting the difference between Rule, LowRule, LowRuleApplication, and what it means to lower()/raise() a rule and why it's used ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On it.

Unrelated observation, lower is kinda doing two separate things here. It both changes the way the rule is represented, and it translates elements from T to usize. Maybe lower simplified in the future by separating the two steps. The refactor would be a little tricky though.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in 55978e7

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Still need to add docs for LowRuleApplication. Will do.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done 26debb6

@@ -184,4 +186,75 @@ mod tests {
let expected: [[&str; 4]; 0] = [];
assert_eq!(&inferences, &expected);
}

#[test]
fn sum_of_consecutive_ints_is_odd() {
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for adding this.

@nmrshll
Copy link
Contributor

nmrshll commented Apr 12, 2021

Thanks for the explanations and comments.
Looks good to merge now I would say.

@bddap
Copy link
Contributor Author

bddap commented Apr 12, 2021

Tagged and pushed changes to https://www.npmjs.com/package/rify and https://crates.io/crates/rify

@bddap bddap merged commit ce92942 into master Apr 12, 2021
@bddap bddap deleted the open-ended branch April 12, 2021 18:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants