IA008: Computational Logic
3. Prolog and Databases
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
∀¯x[p(¯s) ← q0(¯t0) ∧ ⋅⋅⋅ ∧ qn−1(¯tn−1)]
where ¯x are the variables appearing in the formula.
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 formulae
∀¯x[P(¯s) ← Q0(¯t0) ∧ ⋅⋅⋅ ∧ Qn−1(¯tn−1)])
• goal φ(¯x) = R0(¯u0) ∧ ⋅⋅⋅ ∧ Rm−1(¯um−1)
Evaluation strategy
Use resolution to check for which values of ¯x the union Π ∪ {¬φ(¯x)}
is unsatisfiable.
Remark
As we are dealing with a set of Horn formulae, we can use linear
resolution. 吀he variant used by Prolog-interpreters is called
SLD-resolution.
SLD-resolution
▸ Current goal: ¬ψ0 ∨ ⋅⋅⋅ ∨ ¬ψn−1
▸ If n = 0, stop.
▸ Otherwise, find a formula ψ ← θ0 ∧ ⋅⋅⋅ ∧ θm−1 from Π such that
ψ0 and ψ can be unified.
▸ If no such formula 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 rules:
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
q1, q2,!, q3, q4 r fail
q2,!, q3, q4 success
!, q3, q4
q4
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
LH8302 Prague Frankfurt 240
OA1472 Vienna Warsaw 300
UA0870 London Washington 800
…
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.
吀he active domain of a database is the set of elements appearing in
some relation.
Example
In the previous table, the active domain contains:
LH8302, OA1472, UA0870, 240, 300, 800,
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
吀heorem
Relational Algebra = First-Order Logic
Expressive Power
吀heorem
Relational Algebra = First-Order Logic
Proof
(≤) s ↦ s∗
such that s = { ¯a A ⊧ s∗
(¯a)}
Expressive Power
吀heorem
Relational Algebra = First-Order Logic
Proof
(≤) s ↦ s∗
such that s = { ¯a A ⊧ s∗
(¯a)}
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
吀heorem
Relational Algebra = First-Order Logic
Proof
(≥) φ ↦ φ∗
such that φ∗
= { ¯a A ⊧ φ(¯a)}
Expressive Power
吀heorem
Relational Algebra = First-Order Logic
Proof
(≥) φ ↦ φ∗
such that φ∗
= { ¯a A ⊧ φ(¯a)}
R(xu0 ,...,xun−1 )∗
= π0,...,m−1(σu0,m+0⋯σun−1,m+n−1
(All × ⋅⋅⋅ × All × R))
(xi = xj)∗
= σij(All × ⋅⋅⋅ × All)
(φ ∧ ψ)∗
= φ∗
∩ ψ∗
(φ ∨ ψ)∗
= φ∗
∪ ψ∗
(¬φ)∗
= All × ⋅⋅⋅ × All ∖ φ∗
(∃xiφ)∗
= π0,...,i−1,n,i+1,...,n−1(φ∗
× All)
Query Evaluation
Conjunctive query
φ(¯x) = ∃¯y[R0(¯z0) ∧ ⋅⋅⋅ ∧ Rn−1(¯zn−1)] for ¯z0,..., ¯zn−1 ⊆ ¯x¯y
Query Evaluation
Conjunctive query
φ(¯x) = ∃¯y[R0(¯z0) ∧ ⋅⋅⋅ ∧ Rn−1(¯zn−1)] for ¯z0,..., ¯zn−1 ⊆ ¯x¯y
Relational Algebra
π¯u[R0 × ⋅⋅⋅ × Rn−1]
Query Evaluation
Conjunctive query
φ(¯x) = ∃¯y[R0(¯z0) ∧ ⋅⋅⋅ ∧ Rn−1(¯zn−1)] for ¯z0,..., ¯zn−1 ⊆ ¯x¯y
Relational Algebra
π¯u[R0 × ⋅⋅⋅ × Rn−1]
Query Optimisation
π¯u[R0 ij ⋅⋅⋅ kl Rn−1] (works if φ is ‘tree-shaped’)
Constraint Satisfaction Problem (CSP)
Given structures A, B, does there exists a homomorphism A → B?
Constraint Satisfaction Problem (CSP)
Given structures A, B, does there exists a homomorphism A → B?
Example
φ(x) = ∃y∃z[E(x,y) ∧ E(x,z) ∧ R(x,y,z)]
A
B
x
y
z
E
E
R
Constraint Satisfaction Problem (CSP)
Given structures A, B, does there exists a homomorphism A → B?
Example
φ(x) = ∃y∃z[E(x,y) ∧ E(x,z) ∧ R(x,y,z)]
A
B
x
y
z
E
E
R
Complexity
In general the problem is NP-complete, but there are subclasses
where it is in P.
Datalog
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
吀he 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
吀he 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 0
Example
path(X,Y) ← edge(X,Y)
path(X,Y) ← path(X,Z) ∧ path(Z,Y)
A stage 1
Example
path(X,Y) ← edge(X,Y)
path(X,Y) ← path(X,Z) ∧ path(Z,Y)
A stage 2
Example
path(X,Y) ← edge(X,Y)
path(X,Y) ← path(X,Z) ∧ path(Z,Y)
A stage 3
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 0 ∅
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 0 ∅
stage 1 (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 0 ∅
stage 1 (k,0,k)
stage 2 (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 0 ∅
stage 1 (k,0,k)
stage 2 (k,0,k), (k,1,k + 1)
stage 3 (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 0 ∅
stage 1 (k,0,k)
stage 2 (k,0,k), (k,1,k + 1)
stage 3 (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
吀heorem
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.