IA���: Computational Logic
�. Prolog
Achim Blumensath blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Prolog
Prolog
Syntax
A Prolog program consists of a sequence of statements of the form
p(¯s). or p(¯s) − q0(¯t0), . . . , qn−1(¯tn−1).
p, qi relation symbols,¯s, ¯ti tuples of terms.
Semantics
p(¯s) − q0(¯t0), . . . , qn−1(¯tn−1).
corresponds to the implication
p(¯s) ← ∃¯y[q0(¯t0) ∧ ⋅⋅⋅ ∧ qn−1(¯tn−1)]
where ¯y are all the variables that do not appear in ¯s.
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) − father_of(X, Y).
parent_of(X, Y) − mother_of(X, Y).
sibling_of(X, Y) − parent_of(Z, X), parent_of(Z, Y).
ancestor_of(X, Y) − father_of(X, Z), ancestor_of(Z, Y).
Interpreter
On input
p0(¯s0), . . . , pn−1(¯sn−1).
the program finds all values for the variables satisfying the
conjunction
p0(¯s0) ∧ ⋅⋅⋅ ∧ pn−1(¯sn−1) .
Example
?- sibling_of(sam, tina).
Yes
?- sibling_of(X, Y).
X = sam, Y = tina
Execution
Input
▸ program Π (set of Horn clauses)
▸ goal φ( ¯X) = ψ0(¯X) ∧ ⋅⋅⋅ ∧ ψn−1(¯X)
Evaluation strategy
▸ transform ¬φ = ¬ψ0 ∨ ⋅⋅⋅ ∨ ¬ψn−1 into a clause;
▸ use resolution to check for which values of ¯X the union
Π ∪ {¬φ(¯X)} is unsatisfiable.
Remark
As we are dealing with a set of Horn clauses, we can use linear
resolution. The variant used by Prolog-interpreters is called
SLD-resolution.
SLD-resolution
▸ Current goal: ¬ψ0 ∨ ⋅⋅⋅ ∨ ¬ψn−1
▸ If n = 0, stop.
▸ Otherwise, find a clause ψ′
← ϑ0 ∧ ⋅⋅⋅ ∧ ϑm−1 from Π such that ψ0
and ψ′
can be unified.
▸ If no such clause exists, backtrack.
▸ Otherwise, resolve them to produce the new goal
τ(¬ϑ0) ∨ ⋅⋅⋅ ∨ τ(¬ϑm−1) ∨ σ(¬ψ1) ∨ ⋅⋅⋅ ∨ σ(¬ψn−1) .
(σ, τ is the most general unifier of ψ0 and ψ′
.)
Implementation
Use a stack machine that keeps the current goal on the stack.
(→ Warren Abstract Machine)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
unifier X = tina, Y = sam
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
unifier X = tina, Y = sam
new goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
unifier X = Z, Y = tina
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
unifier X = Z, Y = tina
new goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
fails
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
fails
backtrack to ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
unifier X = Z, Y = tina
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
unifier X = Z, Y = tina
new goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
unifier Z = peter
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
unifier Z = peter
new goal ¬parent_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
unify with father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
unify with father_of(peter, sam)
new goal empty
Search tree
sibling_of(tina, sam)
parent_of(Z, tina), parent_of(Z, sam)
mother_of(Z, tina), parent_of(Z, sam) father_of(Z, tina), parent_of(Z, sam)
fail parent_of(peter, sam)
mother_of(peter, sam) father_of(peter, sam)
fail success
Caveats
Prolog-interpreters use a simpler (and unsound) form of unification
that ignores multiple occurrences of variables. E.g. they happily unify
p(x, f (x)) with p(f (y), f (y)) (equating x = f (y) for the first x and
x = y for the second one).
Caveats
Prolog-interpreters use a simpler (and unsound) form of unification
that ignores multiple occurrences of variables. E.g. they happily unify
p(x, f (x)) with p(f (y), f (y)) (equating x = f (y) for the first x and
x = y for the second one).
It is also easy to get infinite loops if you are not careful with the
ordering of the clauses:
edge(c,d).
path(X,Y) :- path(X,Z),edge(Z,Y).
path(X,Y) :- edge(X,Y).
produces
?- path(X,Y).
path(X,Z), edge(Z,Y).
path(X,U), edge(U,Z), edge(Z,Y).
path(X,V), edge(V,U), edge(U,Z), edge(Z,Y).
...
Example: List processing
append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).
?- append([a,b], [c,d], X).
X = [a,b,c,d]
?- append(X, Y, [a,b,c,d])
X = [], Y = [a,b,c,d]
X = [a], Y = [b,c,d]
X = [a,b], Y = [c,d]
X = [a,b,c], Y = [d]
X = [a,b,c,d], Y = []
Example: List processing
reverse(Xs, Ys) :- reverse_(Xs, [], Ys).
reverse_([], Ys, Ys).
reverse_([X|Xs], Rs, Ys) :- reverse_(Xs, [X|Rs], Ys).
reverse([a,b,c], X)
reverse_([a,b,c], [], X)
reverse_([b,c], [a], X)
reverse_([c], [b,a], X)
reverse_([], [c,b,a], X)
X = [c,b,a]
Example: Natural language recognition
sentence(X,R) :- noun(X, Y), verb(Y, R).
sentence(X,R) :- noun(X, Y), verb(Y, Z), noun(Z, R).
noun_phrase(X, R) :- noun(X, R).
noun_phrase(['a' | X], R) :- noun(X, R).
noun_phrase(['the' | X], R) :- noun(X, R).
noun(['cat' | R], R).
noun(['mouse' | R], R).
noun(['dog' | R], R).
verb(['eats' | R], R).
verb(['hunts' | R], R).
verb(['plays' | R], R).
Cuts
Control backtracking using cuts:
p − q0, q1, !, q2, q3.
When backtracking across a cut !, directly jump to the head of the rule
and assume it fails. Do not try other rules.
Example
s ← p
s ← t
p ← q1, q2, !, q3, q4
p ← r
r
q1
q2
q3
s
p t
q, q, !, q, q r fail
q, !, q, q success
!, q, q
q
fail
Negation
Problem
If we allow negation, the formulae are no longer Horn and
SLD-resolution does no longer work.
Possible Solutions
▸ Closed World Assumption
If we cannot derive p, it is false (Negation as Failure).
▸ Completed Database
p ← q0, . . . , p ← qn is interpreted as the stronger statement
p ↔ q0 ∨ ⋅⋅⋅ ∨ qn.
Examples
Being connected by a path of non-edges:
q(X,X).
q(X,Y) :- q(X,Z), not(p(Z,Y)).
Implementing negation using cuts:
not(A) :- A, !, fail.
not(A).
Some cuts can be implemented using negation:
p :- a, !, b. p :- a, b.
p :- c. p :- not(a), c.
Databases
Databases
Definition
A database is a set of relations called tables.
Example
flight from to price
LH���� Prague Frankfurt ���
OA���� Vienna Warsaw ���
UA���� London Washington ���
…
Formal Definitions
We treat a database as a structure A = ⟨A, R0, . . . , Rn⟩ with
▸ universe A containing all entries and
▸ one relation Ri ⊆ A × ⋅⋅⋅ × A per table.
The active domain of a database is the set of elements appearing in
some relation.
Example
In the previous table, the active domain contains:
LH����, OA����, UA����, ���, ���, ���,
Prague, Frankfurt,Vienna,Warsaw, London,Washington
Queries
A query is a function mapping each database to a relation.
Example
Input: database of direct flights
Output: table of all flight connections possibly including stops
In Prolog: database flight, query connection.
flight('LH8302', 'Prague', 'Frankfurt', 240).
flight('OA1472', 'Vienna', 'Warsaw', 300).
flight('UA0870', 'London', 'Washington', 800).
connection(From, To) :- flight(X, From, To, Y).
connection(From, To) :flight(X,
From, T, Y), connection(T, To).
Relational Algebra
Syntax
▸ basic relations
▸ boolean operations ∩, ∪, ∖, All
▸ cartesian product ×
▸ selection σij
▸ projection πu0...un−1
Examples
▸ π1,0(R) = {(b, a) (a, b) ∈ R }
▸ π0,3(σ1,2(E × E)) = {(a, c) (a, b), (b, c) ∈ E }
Relational Algebra
Syntax
▸ basic relations
▸ boolean operations ∩, ∪, ∖, All
▸ cartesian product ×
▸ selection σij
▸ projection πu0...un−1
Examples
▸ π1,0(R) = {(b, a) (a, b) ∈ R }
▸ π0,3(σ1,2(E × E)) = {(a, c) (a, b), (b, c) ∈ E }
Join
R ij S = σij(R × S)
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Proof
(≤)
R∗
= R(x0, . . . , xn−1)
(s ∩ t)∗
= s∗
∧ t∗
(s ∪ t)∗
= s∗
∨ t∗
(s ∖ t)∗
= s∗
∧ ¬t∗
All∗
= true
(s × t)∗
= s∗
(x0, . . . , xm−1) ∧ t∗
(xm, . . . , xm+n−1)
σij(s)∗
= s∗
∧ xi = xj
πu0,...,un−1 (s)∗
= ∃¯y[s∗
(¯y) ∧ ⋀
i<n
xi = yui ]
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Proof
(≥)
R(xu0 , . . . , xun−1 )∗
= π¯v(R × All × ⋅⋅⋅ × All)
vi =
⎧⎪⎪
⎨
⎪⎪⎩
k if i = uk
n + i otherwise
(xi = xj)∗
= σij(All × ⋅⋅⋅ × All)
(φ ∧ ψ)∗
= φ∗
∩ ψ∗
(φ ∨ ψ)∗
= φ∗
∪ ψ∗
(¬φ)∗
= All × ⋅⋅⋅ × All ∖ φ∗
(∃xiφ)∗
= π0,...,i−1,n,i+1,...,n−1(φ∗
× All)
Datalog
Simplified version of Prolog developped in database theory:
▸ no function symbols,
▸ no cut, no negation, etc.
A datalog program for a database A = ⟨A, R0, . . . , Rn⟩ is a set of Horn
formulae
p0(¯X) ← q0,0( ¯X, ¯Y) ∧ ⋅⋅⋅ ∧ q0,m0 (¯X, ¯Y)
pn(¯X) ← qn,0(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ qn,mn ( ¯X, ¯Y)
where p0, . . . , pn are new relation symbols and the qij are either
relation symbols from A, possibly negated, or one of the new
symbols pk (not negated).
Datalog queries
The query defined by a datalog program
p0(¯X) ← q0,0( ¯X, ¯Y) ∧ ⋅⋅⋅ ∧ q0,m0 (¯X, ¯Y)
pn(¯X) ← qn,0(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ qn,mn ( ¯X, ¯Y)
maps a database A to the relations p0, . . . , pn defined by these
formulae.
Evaluation strategy
▸ Start with empty relations p0 = ∅, . . . , pn = ∅.
▸ Apply each rule to add new tuples to the relations.
▸ Repeat until no new tuples are generated.
Note
The relations computed in this way satisfy the Completed Database
assumption.
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example: Arithmetic
Add(x, y, z) ← y = 0 ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y = 0 ∧ z = 0
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage � ∅
Example: Arithmetic
Add(x, y, z) ← y = 0 ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y = 0 ∧ z = 0
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage � ∅
stage � (k, 0, k)
Example: Arithmetic
Add(x, y, z) ← y = 0 ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y = 0 ∧ z = 0
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage � ∅
stage � (k, 0, k)
stage � (k, 0, k), (k, 1, k + 1)
Example: Arithmetic
Add(x, y, z) ← y = 0 ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y = 0 ∧ z = 0
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage � ∅
stage � (k, 0, k)
stage � (k, 0, k), (k, 1, k + 1)
stage � (k, 0, k), (k, 1, k + 1), (k, 2, k + 2)
Example: Arithmetic
Add(x, y, z) ← y = 0 ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y = 0 ∧ z = 0
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage � ∅
stage � (k, 0, k)
stage � (k, 0, k), (k, 1, k + 1)
stage � (k, 0, k), (k, 1, k + 1), (k, 2, k + 2)
⋯
stage n (k, 0, k), (k, 1, k + 1),…, (k, n − 1, k + n − 1)
⋯
Complexity
Theorem
For databases A = ⟨A, ¯R, ≤⟩ equipped with a linear order ≤, a query Q
can be expressed as a Datalog program if, and only if, it can be
evaluated in polynomial type.