This may happen on the first request due to CSS mimetype issues. Try clearing your browser cache and refreshing.

--- a/doc/source/logic_tricks.txt +++ b/doc/source/logic_tricks.txt @@ -27,6 +27,7 @@ /description format: rest encoding: utf8 + initialheaderlevel: 2 output-encoding: utf8 include: yes /restindex @@ -35,7 +36,7 @@ Logic Tricks =================================== -This describes how to accomplish different logic operations with rules. +This describes how to accomplish different logic operations with rules_. X OR Y =========== @@ -43,21 +44,21 @@ For example: check for text_x($arg) OR test_y($arg). Create a separate subgoal for the OR case, let's call it ``or_goal``. Then use -a separate rule for each OR clause:: - - or_goal_test_x: +a separate rule_ for each OR clause:: + + or_goal_test_x use or_goal($arg) when test_x($arg) - or_goal_test_y: + or_goal_test_y use or_goal($arg) when test_y($arg) Then you'd use ``or_goal($arg)`` where you wanted the *OR* clause. -This can go on for any number of OR-ed clauses by just adding more rules for +This can go on for any number of OR-ed clauses by just adding more rules_ for ``or_goal``. IF X THEN Y @@ -66,19 +67,19 @@ For example: if test_x($arg) then test_y($arg). What this means is that test_y($arg) must be true if test_x($arg) is true. -But if test_x($arg) is not true, then test_y($arg) doesn't matter and ``if +But if test_x($arg) is not true, then test_y($arg) doesn't matter so ``if test_x($arg) then test_y($arg)`` is true. -Create a new subgoal, let's call it ``if_x_then_y``. Use two rules:: - - if_x_then_y_if: +Create a new subgoal, let's call it ``if_x_then_y``. Use two rules_:: + + if_x_then_y_if use if_x_then_y($arg) when test_x($arg) # if this fails, the next rule will be used special.claim_goal() # don't use any other rules for if_x_then_y test_y($arg) # if this fails, the next rule will not be used, so if_x_then_y will fail. - if_x_then_y_else: + if_x_then_y_else use if_x_then_y($_) # this rule is only used if test_x($arg) fails NOT X @@ -89,25 +90,28 @@ You have to be careful about *not* logic because it can mean different things. In this example, if we try ``not test_x($arg)`` and ``$arg`` is unbound what should happen? Should it generate all of the different values for ``$arg`` -for which ``test_x($arg)`` fails? This generally isn't very practical! +for which ``test_x($arg)`` fails? This generally isn't very practical +computationally! The other interpretation is that there is **no** possible binding for ``$arg`` that makes ``test_x($arg)`` true. In this example, ``not test_x($arg)`` would then be false, because there is some ``$arg`` value that makes ``test_x($arg)`` true. -This second interpretation can be implemented by creating a new subgoal, let's -say ``not_test_x`` and using a pair of rules:: - - not_test_x_fail: - use not_test_x($arg) - when - test_x($arg) # if there is any way for test_x($arg) to be true - special.claim_goal() # don't use any other rules for not_test_x - check False # and cause this rule to fail, which causes the not_test_x goal to fail - - not_test_x_success: - use not_test_x($_) # this rule only runs if test_x($arg) fails, above +This second interpretation can be done using the notany_ clause. This can +be used in both `forward chaining`_ and `backward chaining`_ rules_:: + + your_rule + use your_goal($arg) + when + .. + notany + test_x($arg) + .. + +Note that notany_ will only temporarily bind `pattern variables`_ while it +runs, but not leave any of these bindings in place (for the following premise) +after it's finished. Notany_ always fails on backtracking_. EXISTS X SUCH THAT Y =============================================================== @@ -124,16 +128,84 @@ FOR ALL X, Y =============================================================== -For example: for all $x from generate_x($x), test_y($x) is true - -Use the forall clause:: +FOR ALL X, Y succeeds +----------------------- + +For example: for all $x from generate_x($x); test_y($x) succeeds + +Use the forall_ clause:: forall generate_x($x) require test_y($x) -Note that all pattern variable bindings done in the forall clause are undone -before the next clause is run. - -This always fails on backtracking. +Note that all `pattern variables`_ bound in the forall_ clause are unbound +before the premise following the forall_ is run. In this example, this +means that ``$x`` would not be bound to a value following the forall_ clause. +You can use `python premises`_ to capture the bindings of `pattern variables`_ +in the forall_ clause and make them available to the premises following the +forall_:: + + python x_list = [] + forall + generate_x($x) + require + test_y($x) + python x_list.append($x) + $xs = tuple(x_list) + +Note that ``x_list`` is a python variable -- not a `pattern variable`_! It is +moved back to `pattern variable`_ ``$xs`` in the final line so that the +following premises can access it. + +Forall_ always fails on backtracking_. Consider these two techniques:: + + forall_technique + use solve_list($x_list, $x_answers) + when + python x_answers = [] + forall + $x in $x_list + require + solve($x, $x_ans) + python x_answers.append($x_ans) + $x_answers = tuple(x_answers) + +and:: + + recursive_technique_done + use solve_list((), ()) + + recursive_technique_more + use solve_list(($x1, *$x_rest), ($ans1, *$ans_rest)) + when + solve($x1, $ans1) + solve_list($x_rest, $ans_rest) + +The first technique will only find the first solution and then fail on +backtracking_ (if the invoking goal doesn't like the first solution). +But the second technique will find other solutions on backtracking_. + + +FOR ALL X, Y fails +----------------------- + +For example: for all $x from generate_x($x), not test_y($x) + +In this case, just use the notany_ clause:: + + notany + generate_x($x) + test_y($x) + +.. _backtracking: overview/rules/backward_chaining.html#backtracking +.. _backward chaining: overview/rules/backward_chaining.html +.. _forall: krb_syntax/bc_rule.html#forall +.. _forward chaining: overview/rules/forward_chaining.html +.. _notany: krb_syntax/bc_rule.html#notany +.. _pattern variable: krb_syntax/pattern.html#pattern-variable +.. _pattern variables: `pattern variable`_ +.. _python premises: krb_syntax/python_premise.html +.. _rule: overview/rules/index.html +.. _rules: rule_