Compound Premise Syntax
There are three kinds of compound premises. These can be used in both forward-chaining rules and backward-chaining rules, but the nested premises within each of these are restricted to the kind of premises legal for that kind of rule: fc_premise for forward-chaining rules, and bc_premise for backward-chaining rules.
compound_premise ::= first_premise
| forall_premise
| notany_premise
First Premise
The first premise is used to prevent backtracking from finding subsequent solutions to a set of premises. The first premise always fails on backtracking (but does do backtracking within the nested premises).
first_premise ::= ['!'] 'first' premise
| ['!'] 'first' NL
INDENT
{premise NL}
DEINDENT
The ! option can only be used in backward-chaining rules.
When used within backward-chaining rules, the nested premises may include any type of plan_spec.
Forall Premise
The forall premise forces backtracking within the nested premises to process all of the possible solutions found before the forall succeeds. After the first success, the forall fails on backtracking.
forall_premise ::= 'forall' NL
INDENT
{premise NL}
DEINDENT
[ 'require' NL
INDENT
{premise NL}
DEINDENT ]
The premises within the require clause are tried for each solution found to the forall clause. If these fail for any solution, then the entire forall premise fails. Thus, the forall only succeeds if the require premises are true for all solutions generated within the forall clause. Thus, the forall clause may be read: "Forall X, require Y".
The forall always succeeds if the require clause is omitted (even if no solutions are found to the nested premises). This can be used in conjunction with python_statements to gather a list of results.
See Notes on Forall and Notany Premises and Examples, below.
Notany Premise
The notany premise only succeeds if no solution can be found to the nested premises. Notany always fails on backtracking.
notany_premise ::= 'notany' NL
INDENT
{premise NL}
DEINDENT
See Notes on Forall and Notany Premises and Examples, below.
Notes on Forall and Notany Premises
- All pattern variable bindings made during the execution of a forall or notany premise are undone before the premises following the forall or notany are run. Thus, forall and notany can be used to test values produced by prior premises; but to generate values for subsequent premises the values must be captured in Python variables within the forall or notany clause before the pattern variables are unbound (see Computing a Value for Each Generated Value, below).
- When used within backward-chaining rules, the only plan_spec allowed in nested premises is the as clause.
Examples
- Finding the First Solution From a Set of Values
- Testing Every Generated Value
- Computing a Value for Each Generated Value
- Iterating on Tuples
- Computing Values for All Generated Values that Pass a Test
These examples use the following subgoals:
- generate_x($x) generates multiple solutions (as $x) that will be looped over
- test_x($x) does some test on $x
- compute_y($x, $y) takes $x as input and computes a $y value
Finding the First Solution From a Set of Values
If you want the first $x that passes the test_x($x) test, you have two options:
generate_x($x) test_x($x) ...
And:
first
generate_x($x)
test_x($x)
...
The difference is that the first example will find other $x values that pass test_x($x) on backtracking, while the second example will stop after the first value is found and fail on backtracking.
Testing Every Generated Value
There are two general cases. You might want to verify that test_x($x) succeeds for all generated $x values:
forall
generate_x($x)
require
test_x($x)
Note
While $x is set and used within the forall premise to transfer values from the generate_x($x) goal to the test_x($x) goal, it is no longer set afterwards and can not be referenced in the premises following the forall premise.
The second case that you might want to verify is that test_x($x) fails for every generated $x value:
forall
generate_x($x)
require
notany
test_x($x)
Or, more simply:
notany
generate_x($x)
test_x($x)
Computing a Value for Each Generated Value
If you want a tuple of computed $y values for all of the $x values:
python y_list = []
forall
generate_x($x)
require
compute_x($x, $y)
python y_list.append($y)
$y_list = tuple(y_list)
This will only succeed if compute_y succeeds for every $x value.
If you want to skip over $x values that compute_y fails on, you might try:
python y_list = []
forall
generate_x($x)
compute_x($x, $y)
python y_list.append($y)
$y_list = tuple(y_list)
But note that if compute_y computes multiple solutions for a single $x value on backtracking, you would end up including all of these solutions in your $y_list. To only get the first computed value for each $x value:
python y_list = []
forall
generate_x($x)
first
compute_x($x, $y)
python y_list.append($y)
$y_list = tuple(y_list)
Iterating on Tuples
A simple common case of generate_x is when you are computing values for each element of a tuple:
python y_list = []
forall
$x in $x_list
require
compute_x($x, $y)
python y_list.append($y)
$y_list = tuple(y_list)
This can also be done by creating a new subgoal that recurses on $x_list. If you call the new subgoal compute_list, you would use it like this:
compute_list($x_list, $y_list)
And define it like this:
compute_list_done
use compute_list((), ())
compute_list_step
use compute_list(($x, *$x_rest), ($y, *$y_rest))
when
compute_y($x, $y)
compute_list($x_rest, $y_rest)
Important
Note that there is an important difference between these two examples if compute_y may find alternate $y values for any given $x value on backtracking.
The first example will only generate one $y_list. If that $y_list doesn't work for subsequent premises, the forall fails on backtracking, so no overall solution will be found.
The second example will not fail in this situation, but will produce all possible combinations of solutions to compute_y for each $x on backtracking until a resulting $y_list satisfies the subsequent premises so that an overall solution is found.
Computing Values for All Generated Values that Pass a Test
Finally, if you want to gather only the computed $y values for $x values that pass test_x($x):
python y_list = []
forall
generate_x($x)
test_x($x)
require
compute_x($x, $y)
python y_list.append($y)
$y_list = tuple(y_list)