Function canrun::goals::not

pub fn not(goal: impl Goal) -> Not

Create a Goal that only succeeds if the sub-goal is proved to always fail.

This is implented using my interpretation of Negation as failure. When created, it will exhaustively run the sub-goal. If every possible iteration fails, it assumes that no additional facts can change the result and so marks the outer goal as a success. If any result state is a success, it adds a constraint that will continue checking until the sub-goal has no unresolved variables or open constraints. At this point, if it succeeds at least once, the outer Not will fail.

Examples

use canrun::{State, Query, LVar, all, any, unify, not};

let x = LVar::new();
let goal = all![
    any![unify(x, 1), unify(x, 2)],
    not(unify(x, 1)),
];
let results: Vec<_> = goal.query(x).collect();
assert_eq!(results, vec![2]);

Caveats

This is a somewhat recurring complication in the logic programming world, and I can’t claim a very deep understanding of the space. I have not yet found this approach to yield incorrect results, but, well… proving a negative is hard!

Performance considerations

This goal will do a speculative fork of the outer state in an attempt to search for success states. It will short circuit as soon as one is found, but this could be a lot of computation depending on the complexity of the outer state.

A not() that depends on unresolved variables should work correctly, but will require adding a constraint watch on these variables. If they are only resolved within branches of a fork, this could involve a lot of repeating forking before the not() is able to conclusively prove or disprove the sub-goal.

All of this is not to discourage usage, but just to say that you should try to keep them relatively simple and as precise as possible.