A rule is a definite horn clause that has one or more predicates as a head, and one or more literals in the body. The literals are predicates, negated predicates, or constraints. All variables of a rule must be grounded, i.e., a variable must occur at least once as an argument of a positive predicate in the body of a rule. Soufflé permits arithmetic and string functors assuming that their arguments are grounded.
B with two number attributes.
.decl A, B(x:number, y:number) // declaration of relation B .input A // read A B(x,y) :- A(x,y). // rules of relation B B(x,z) :- A(x,y), B(y,z). .output B
B has two rules:
B(x,y) :- A(x,y). and
B(x,y) :- A(x,y), B(y,z). The first rule says, there is a tuple in
B if this tuple shows up in
A. The second rule says there is a tuple
B, if there is a tuple in
A and a tuple
Binding of Variables
The variables deduce their types from their bindings. A variable receives values from positive predicates in the body of a rule. TBD: Explain the information flow in a rule (what is a a source / sink) and type checking.
Negation in Rules
A rules of the form
CanRenovate(person, building) :- Owner(person, building), !Heritage(building).
expresses the rule that an owner can renovate a building with the condition that the building is not classified as heritage. Thus the literal “Heritage(building)” is negated (via “!”) in the body of the rule. Not all negations are semantically permissible. For example,
A(x) :- ! B(x). B(x) :- ! A(x).
is a circular definition. One cannot determine if anything belongs to the relation “A” without determining if it belongs to relation “B”. But to determine if it is a “B” one needs to determine if the item belongs to “A”. Such circular definitions are forbidden. Technically, rules involving negation must be stratifiable.
Negated literals do not bind variables. For example,
A(x,y) :- R(x), !S(y).
is not valid as the set of values that “y” can take is not clear. This can be rewritten as,
A(x,y) :- R(x), Scope(y), !S(y).
where the relation “Scope” defines the set of values that “y” can take.
Rules can have multiple heads:
A(x,y), C(x,y) :- B(x,y).
which is syntactic sugar for
A(x,y) :- B(x,y). C(x,y) :- B(x,y).
A rule of the form
LivesAt(person, building) :- Owner(owner, building), ( person=owner ; Housemate(owner, person) ).
expresses the rule that a person lives in a building if they are the owner, or a housemate of the owner. Thus the conditions
Housemate(owner, person) are joined by
; to indicate that either must hold.
Rules may have qualifiers, which are used to change the execution behavior / semantics.
Qualifiers are used to set a query plan for a rule. The qualifer
.plan let’s the programmer chose a query plan for a rule.
A rule has one or more heads followed by symbol
:- and a disjunctive term. A query plan is optional for a rule.
rule ::= atom ( ',' atom )* ':-' disjunction '.' query_plan?
A qualified name is a sequence of identifiers separated by
. to disambiguate relations that are instantiated by components.
qualified_name ::= IDENT ( '.' IDENT )*
An atom consists of a relation name followed by comma-separated arguments in parenthesis.
atom ::= qualified_name '(' ( argument ( ',' argument )* )? ')'
A disjunction is a list of conjunction separated by ‘;’.
disjunction ::= conjunction ( ';' conjunction )*
A conjunctive term is a list of (negated) atoms / constraints / disjunctions separated by ‘,’.
conjunction ::= '!'* ( atom | constraint | '(' disjunction ')' ) ( ',' '!'* ( atom | constraint | '(' disjunction ')' ) )*
A query plan gives for each version of a rule a permutation. The permutation dictates the execution order in the loop nest.
query_plan ::= '.plan' NUMBER ':' '(' ( NUMBER ( ',' NUMBER )* )? ')' ( ',' NUMBER ':' '(' ( NUMBER ( ',' NUMBER )* )? ')' )*