A rule is a horn clause that has one predicate (or more; see below) as a head, and one or more literals in the body. The literals can be 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.
Consider the following example, that has relation A and 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
Relation 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 (x,z) in B, if there is a tuple in (x,y) in A and a tuple (y,z) in B.
For the first rule, variables x and y are grounded, since they show up as variables in the
positive predicate B(x,y). Similiar, the variables x, y, and z are grounded because
they occur in the positive predicates A(x,y) and B(y,z).
However, note that the following example has an ungrounded variable:
.decl fib(idx:number, value:number)
fib(1,1).
fib(2,1).
fib(idx, x + y) :- fib(idx-1, x), fib(idx-2, y), idx <= 10.
.output fib
The reason for this is that variable idx is not bound as an argument of a positive predicate in the body. In the example, variable idx occurrs in the predicates fib(idx-1, x) and fib(idx-2, y) but as arguments of a functor rather than as a direct argument. To make variable idx bound, we can shift the index by one and obtain a program whose variables are grounded:
.decl fib(idx:number, value:number)
fib(1,1).
fib(2,1).
fib(idx+1, x + y) :- fib(idx, x), fib(idx-1, y), idx <= 9.
.output fib
And the program can produce the following output,
---------------
fib
idx value
===============
1 1
2 1
3 2
4 3
5 5
6 8
7 13
8 21
9 34
10 55
===============
Type System
Variables in a rule have no explicit type declaration. Hence,
Soufflé’s typesystem must automatically deduce the type of variables in a rule, depending on how they are used
as arguments in predicates, functors, and constraints. Besides deducing their type, its other task is to check
their appropiate use. Soufflé’s typesystem supports subtypes and union types, e.g., .type A <: B and .type C = A|B that makes the semantics of the typesystem more complex. For example,
.type A <: number
.type B <: number
.type C = A | B
.decl P(x:A)
.decl Q(x:B)
.decl R(x:C)
R(x) :- P(x), Q(x).
In the above example, the type of variable is of type C. The reason is that the right-hand side of the body constraints the variable x such that x must be of type A / B or a supertype of them. The left-hand side constrain the type of variable to type C or a subtype of it. We also refer to grounded variable occurrences in the body of a rule as sources and the variable occurrences in the head of a rule / constraints / negation etc. as sinks. The reason for this is that sources may produce a concrete assignment and the the sinks use as concrete assignment.
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.
Multiple Heads
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).
Disjunction
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 person=owner and Housemate(owner, person) are joined by ; to indicate that either must hold.
Query Plan
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.
Syntax
In the following, we define rule declarations in Soufflé more formally using syntax diagrams and EBNF. The syntax diagrams were produced with Bottlecaps.
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?
Qualified Name
A qualified name is a sequence of identifiers separated by . to disambiguate relations that are instantiated by components.
qualified_name ::= IDENT ( '.' IDENT )*
Atom
An atom consists of a relation name followed by comma-separated arguments in parenthesis.
atom ::= qualified_name '(' ( argument ( ',' argument )* )? ')'
Disjunction
A disjunction is a list of conjunction separated by ‘;’.
disjunction ::= conjunction ( ';' conjunction )*
Conjunction
A conjunctive term is a list of (negated) atoms / constraints / disjunctions separated by ‘,’.
conjunction ::= '!'* ( atom | constraint | '(' disjunction ')' ) ( ',' '!'* ( atom | constraint | '(' disjunction ')' ) )*
Query Plan
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 )* )? ')' )*