-
Notifications
You must be signed in to change notification settings - Fork 211
High Level AST Transformations
The purpose of this transformation is to allow for intermediate results of an aggregate query to be computed and saved in an auxiliary table. Without this transformation, it is not possible to write aggregates with complex bodies that rely on outer scope groundings.
An aggregate will undergo materialisation when it has a complex body. A body is considered complex when it contains more than one literal. This is an example of an aggregate which has a complex body.
B(x) :- A(n), x = sum z : { C(z), z < 10 }.
This rule will be transformed into
B(x) :- A(n), x = sum z : agg_rel_0(z).
agg_rel_0(z) :- C(z), z < 10.
The head of the new relation agg_rel_0 contains any free or bound variable occurring in the body of the aggregate condition. If a variable in the aggregate body is grounded from the outside scope, the grounding atom is copied over into the synthesised relation agg_rel_k. For example,
B(x) :- A(n), x = sum y : { C(y), y < n }.
will become
B(x) :- A(n), x = sum y : agg_rel_0(y, n).
agg_rel_0(y, n) :- C(y), y < n, A(n).
This is because A(n) is required to give the variable n the appropriate grounding.
To see that this transformation is correct, we need to check that a rule that is transformed by MaterializeAggregationQueries remains semantically equivalent.
B(n, x) :- A(n), x = sum z : { ..., z < n }.
B'(n, x) :- A(n), x = sum z : C(a, z, n).
C(a, z, n) :- ..., z < n, A(n).
B is the original relation, B' is the transformed relation and C is the materialised aggregate relation. a is a free variable occurring in the body of C, n is a term that requires grounding from the outer scope.
B is semantically equivalent to B'.
Let B(n, x) evaluate to true. Then A(n) is true, and x = sum z : { ..., z < n }. Then in B', C(a, z, n) is true exactly when { ..., z < n } is true since A(n) is true. Therefore the aggregate results are equal, and B'(n, x) is true.
Let B(n, x) evaluate to false. Then A(n) is false or the aggregate result does not equal x. If A(n) is false, then B'(n, x) is false since B' contains this predicate. If A(n) is true but the aggregate result does not equal x, then maybe the aggregate result for B' is x. But we know that since A(n) is true, the aggregate body truth value and the C truth value coincide, so it is not possible for the aggregate values to differ. Therefore B'(n, x) is false.
Therefore the truth values of B' and B coincide. Therefore B and B' are semantically equivalent.