Transcript Document

Declarative Semantics
- An overview
• Algebras (semantics for terms)
• Interpretations (semantics for programs)
• Soundness of SLD-Resolution
• Completeness of SLD-Resolution
• Least Herbrand Models
• Computing least Herbrand Models
17 October 2006
Foundations of Logic and Constraint Programming
1
Algebras
Informally, an algebra assigns values of constants and functions to elements of a
certain domain (for example, the usual algebra for the natural numbers N, assigns
to function +(3,1)) the value 4 ). More formally
-
Given a set of Variables V , and a ranked alphabet F of function symbols,
An algebra J for F (or F-algebra or pre-interpretation for F) consists of:
1. domain : non-empty set D
2. Assignment of a mapping
fJ : Dn  D
to every f F (n) (with n  0)
-
State σ over D : mapping σ : V  D
-
Extension of σ to TUF,V :
σ: TUF,V  D such that for every f F (n)
σ(f(t1, ... , tn)) = fJ (σ(t1), ... , σ(tn))
17 October 2006
Foundations of Logic and Constraint Programming
2
Interpretations
Informally, an interpretation assigns true or false to predicates over its arguments,
which are elements of a domain (or terms pre-interpreted by an algebra). For
example, (+(3,1), 2) is true in the usual interpretation of /2). More formally
-
Given a ranked alphabet F of function symbols, and a ranked alphabet  of
predicate symbols
-
An interpretation I for F and  consists of:
1. Algebra J for F (with domain D)
2. Assignment of a relation
pI  D  D  ... D
to every p   (n) (with n  0)
n
-
Note: Given a predicate p with n arguments in D, this definition is equivalent
to mapping the predicate into
• true if the n-tuple is a member of in the relation pI
• false if the n-tuple is not a member of the relation pI
17 October 2006
Foundations of Logic and Constraint Programming
3
Interpretations
Let Padd be the” add-program”
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
I1, I2, I3, I4, I5 and I6 are all legitimate (if not all “conventional”) interpretations for
the sets F = {0,s/1} and  = {add/3}
-
I1 : DI1 = N, 0I1 = 0, sI1(n) = n+1 f.e. n N
addI1 = {(m,n,m+n) | m, n N }
Note: This is the usual interpretation where terms are interpreted to
numbers and add is “addition”
-
I2 : DI2 = N, 0I2 = 0, sI2(n) = n+1 f.e. n N
addI2 = {(m,n,m*n) | m, n N }
Note: In this interpretation, “addition is in fact multiplication”.
-
I3 : DI3 = HU{s,0}, 0I3 = 0, sI3(t) = s(t) f.e. t  HU{s,0},
addI3 = {(sm(0), sn(0), sm+n(0),) | m, n N }
Note: This is the interpretation of addition in the Peano algebra for integers.
17 October 2006
Foundations of Logic and Constraint Programming
4
Interpretations
Let Padd be the” add-program”
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
-
I4 : DI4 = HU{s,0}, 0I4 = 0, sI4(t) = s(t) f.e. t  HU{s,0},
addI4 = { }
Note: In this interpretation, “Peano numbers cannot be added”.
-
I5 : DI5 = HU{s,0}, 0I5 = 0, sI5(t) = s(t) f.e. t  HU{s,0},
addI5 = (HU{s,0} )3
Note: In this interpretation, “anything goes”, since any triple of terms is in the
model.
-
I6 : DI6 = {0,1} 0I6 = 0, sI6(n) = n f.e. n  { 0,1}
addI6 = {(m,n,n) | m, n { 0,1}
Note: in this interpretation for a boolean domain, s is the identity function,
and add “selects of the second argument”.
17 October 2006
Foundations of Logic and Constraint Programming
5
Logical Truth (1)
- Expression E : E is an atom, query, clause or resultant
- Given an expression E, an interpretation I and a state σ
E true in I under σ, written I |= σ E
:
By case analysis on E:

I |= σ p(t1, ... , tn)
: (σ(t1), ... , σ(tn)) pI
(atom)

I |= σ A1, ... , An
: I |= σ A1, ... , I |= σ An
(query)

I |= σ A ← B
: if I |= σ B then I |= σ A
(clause)

I |= σ A ← B
: if I |= σ B then I |= σ A
(resultant)
17 October 2006
Foundations of Logic and Constraint Programming
6
Logical Truth (2)
- Given an expression E, and an interpretation I:
Let x1, ... , xk be the variables occurring in E

x1, ... , xk E
: Universal closure of E (abreviated E)

x1, ... , xk E
: Existential closure of E (abreviated  E)

I |= E
: if I |= σ E for every state σ

I |=  E
: if I |= σ E for some state σ

When I |= E we say that
•
I is a model of E; or
•
E is true in I.
17 October 2006
Foundations of Logic and Constraint Programming
7
Logical Truth (3)
- Given sets of expressions S and T, and an interpretation I:

I is a model of S (written I |= S )
: I |= E for every E S

T is a semantic (or logical) consequence of S, (written S |= T )
: every model of S is a model of T
- Given a program P, a query Q0 and a substitution 

|
var(Q0)
is a correct answer substitution of Q0
: P |= Q0 

Q0 is a correct instance of Q0
: P |= Q0 
17 October 2006
Foundations of Logic and Constraint Programming
8
Models (Example)
Let Padd be the” add-program”
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
- I1 : DI1 = N, 0I1 = 0, sI1(n) = n+1 ; addI1 = {(m,n,m+n) | m, n N }
- I1 |= Padd as I1 |= c for every clause c of Padd and state σ : V  N. In fact
(i) (σ(0), σ(x), σ(x))  add I1 ; and
(ii) if (σ(M), σ(N), σ(K))  add I1 then (σ(M)+1, σ(N), σ(K)+1)  add I1
- I2 : DI2 = N, 0I2 = 0, sI2(n) = n+1 ; addI2 = {(m,n,m*n) | m, n N }
- I2 | Padd . To check this let σ(M) = 1. Then I2 |σ add(0,M,M) since
(σ(0), σ(M), σ(M)) = (0,1,1)  addI2 (in other words, 0*1  1)
- I3 : DI3 = HU{s,0}, 0I3 = 0, sI3(t)=s(t) ; addI3={(sm(0),sn(0),sm+n(0),)|m,n N }
- I3 |= Padd like for I1. Since the domain D is the Herbrand Universe of terms,
this interpretation is a (least) Herbrand Model.
17 October 2006
Foundations of Logic and Constraint Programming
9
Models (Example)
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
- I4 : DI4 = HU{s,0}, 0I4 = 0, sI4(t) = s(t) f.e. t  HU{s,0}, addI4 = { }
- I4 | Padd . To check this let σ(M) = 1. Then I4 |σ add(0,M,M) since
(σ(0), σ(M), σ(M)) = (0,1,1)  addI4 = { }.
- I5 : DI5 = HU{s,0}, 0I5 = 0, sI5(t) = s(t) f.e. t  HU{s,0}, addI5 = (HU{s,0} )3
- I5 |= Padd as any triple, (σ(0), ỤỴ(M), σ(M)) or (s(σ(M)), σ(N)), s(σ(K)),
belongs to addI5. Since DI5 is the Herbrand Universe, I5 is a Herbrand
Model. However, it is not a least model, since addI5 includes more
triples than strictly necessary (addI2  addI5)
- I6 : DI6 = {0,1} 0I6 = 0, sI6(n) = n; addI6 = {(m,n,n) | m, n { 0,1}
- I6 |= Padd . Like for I1.
(i) (σ(0), σ(x), σ(x))  add I6 ; and
(ii) if (σ(M), σ(N), σ(K))  add I6 then (σ(M), σ(N), σ(K))  add I6
17 October 2006
Foundations of Logic and Constraint Programming
10
Semantic Consequences (Example)
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
- Padd |= add(0,x,x)
- For every interpretation I, if I |= Padd then I |= Padd since add(0,x,x) 
Padd.
- Padd |= add(s(0),x,s(x))
- For every interpretation I, if I |= Padd then
(i) I |= add(0,x,x) ; and
(ii) I |= add(s(0),x,s(x)) ← add(0,x,x).
- Hence, I |= add(s(0),x,s(x)) .
- Padd | add(x,0,x)
- Consider interpretation I6, (that selects the second element). Although
I6 |= Padd as seen before, it is
I6 | add(x,0,x) for state σ(x) = 1, as (σ(x),σ(0),σ(x)) = (1,0,1) addI6.
17 October 2006
Foundations of Logic and Constraint Programming
11
Towards Soundness of SLD-Resolution (1)
- Lemma 4.3 (i)
- Let Q c Q’ be an SLD-derivation step and Q ← Q’ the resultant associated
with it. Then
c |= Q ← Q’
Proof.
- Let Q = A, B, C with selected atom B. Let H ← B be the input clause c , and
Q’ = (A,B,C) . Then
c |= H ← B
(variant of c)
implies c |= H  ← B 
(instance)
implies c |= B  ← B 
( unifies B and H)
implies c |= (A,B,C)  ← (A,B,C) 
(unchanged “context” : A, C)
17 October 2006
Foundations of Logic and Constraint Programming
12
Towards Soundness of SLD-Resolution (2)
Lemma 4.3 (ii)
Let  be an SLD-derivation of P  {Q0}. For i  0 let Ri be the resultant of level i
of . Then
P |= Ri
Proof. Let  = Q0 1 Q1 ... Qn n+1 Qn+1. The proof is by induction on n.
- i = 0: R0 = Q0 ← Q0 = “true”. Hence, P |= R0.
- i = 1: R1 = Q01← Q1 . By Lemma 4.3(i) it is P |= R1.
- i ~> i+1: Assume that P |= Ri and Qii+1 ← Qi+1
- Let Qi i+1 ← Qi+1 and Ri = Q0 1 2 ... , i ← Qi; Then
- Ri+1 = Ri i+1 = Q0 1 2 ... , i+1 ← Qi+1.
- Hence, by Lemma 4.3 (i) and the induction hipothesis, it is P |= Ri+1.
17 October 2006
Foundations of Logic and Constraint Programming
13
Soundness of SLD-Resolution
Theorem 4.4
If there exists a successful SLD-derivation of P  {Q0 } with CAS (computed
answer substitution)  , then
P |= Q0 
Proof.
Let  = Q0 1 Q1 ... Qn-1 n □ be a successful SLD-derivation. Lemma 4.3(ii)
applied to the resultant of level n of  implies
P |= Q0 1... n
and Q0 1... n = Q0 (1... n | Var(Q0)) = Q0.
- This theorem thus guarantees that the answers computed by a successful
derivation are logical consequences of the program.
- The converse result, is the object of the completeness theorem.
17 October 2006
Foundations of Logic and Constraint Programming
14
Intuitive Meaning of Queries
- To prepare the addressing of completeness, the next corollary simply states that
if an SLD-derivation exists, then the program implies the existential closure of
the query (some instance of the query).
Corollary 4.5
If there exists a successful SLD-derivation of P  {Q0} then P |= Q0.
Proof.
Theorem 4.4. implies P |= Q0  for some CAS . Now,
P |= Q0 .
- implies for every interpretation I: I |= P, then I |= Q0 ,
- implies for every interpretation I: I |= P, then I |= (Q0 )
- implies for every interpretation I: I |= P, then I |= Q0
- implies P |= Q0
17 October 2006
Foundations of Logic and Constraint Programming
15
Towards Completeness of SLD-Resolution
- To assess completeness of SLD-Resolution it is convenient to characterise the
set of sintactically derivable queries. For this purpose the concepts of term
models and implication trees are defined.
- The main idea is to interpret the set of functional symbols into “themselves”,
rather, avoinding their mapping into a different domain. For example, instead of
a mapping such as
- “0”  0,”s(0)”  1, “s(s(0))”  2, ... a term interpretation/model will adopt
- “0”  0, “s(0)”  s(0), “s(s(0))”  s(s(0)), ...
- Formally, for an expression E, and a set of expressions S
- inst(E) : set of all instances of E
- inst(S) : set of all instances of all elements E  S
- ground(E) : set of all ground instances of E
- ground(S) : set of all ground instances of all elements E  S
17 October 2006
Foundations of Logic and Constraint Programming
16
Term Models
For a set of variables V, function symbols F and predicate symbols 
-
The term algebra J for F is defined as follows:
1. Domain D = TUF,V
2. Mapping fJ: (TUF,V)n  TUF,V assigned to every f  F(n) with
fJ(t1, ... , tn) : f(t1, ... , tn)
A term interpretation I for F and  consists of:
1. A term algebra for F
2. I  TB,,F,V (set of atoms that are true; equivalently it can be seen as an
assignment of a relation pI  (TUF,V)n to every p  (n)).
A term model I of a set S of expressions
: a term interpretation I that is a model of S
17 October 2006
Foundations of Logic and Constraint Programming
17
Herbrand Models
The Herbrand algebra J for F is defined for ground terms as follows:
1. Domain D = HUF
2. Mapping fJ: (HUF)n  HUF assigned to every f  F(n) with
fJ(t1, ... , tn) : f(t1, ... , tn)
A Herbrand interpretation I for F and  consists of:
1. Herbrand algebra for F
2. I  HB,,F (set of ground atoms that are true; equivalently it can be seen as an
assignment of a relation pI  (HUF)n to every p  (n)).
A Herbrand model I of a set S of expressions
: a Herbrand interpretation I that is a model of S
A least Herbrand model I of a set S of expressions
: I is a Herbrand model of S and I  I’ for all Herbrand Models I’ of S
17 October 2006
Foundations of Logic and Constraint Programming
18
Implication Trees
An implication tree T with respect to program P
:
-
T is a finite tree
-
The nodes of T are atoms
-
If A is a node with direct descendants B1, ... , Bn then there must be some
A ← B1, ... , Bn  inst(P).
-
If A is a leaf, then A ←  inst(P).
-
B is a ground implication tree wrt. Program P
:
B is an implication tree wrt P and all nodes are ground atoms.
17 October 2006
Foundations of Logic and Constraint Programming
19
Implication Trees (Example)
Let Padd be the” add-program”,
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
and n  N, V be a set of variables and t  TU{s,0},V.
Let T =
add(sn(0), t, sn(t))
add(sn-1(0), t, sn-1(t))
add(s(0), t, s(t))
Then
add(0, t, t)
-
T is an implication tree wrt. Padd.
-
If additionally t  HU{s,0}, then T is a ground implication tree.
17 October 2006
Foundations of Logic and Constraint Programming
20
Implication Trees (Example)
Let Pmult be the” multiply-program”,
mult(0,X,0).
mult(s(M),N, K):- mult(M,N,Z), add(Z,N,K).
and n  N, V be a set of variables and t  TU{s,0},V. . Let T =
mult(s(s(0)),s(0),s(s(0)))
mult(s(0),s(0),s(0))
mult(0,s(0),0)
add(0,s(0),s(0))
add(s(0),s(0),s(s(0)))
add(0,s(0),s(0))
Then
-
T is an implication tree wrt. Padd.
-
T is also a ground implication tree.
17 October 2006
Foundations of Logic and Constraint Programming
21
Implication Trees and Term Models
Lemma 4.7
Consider term interpretation I, atom A and program P
•
I |= A iff inst (A)  I
•
I |= A iff for every A ← B1, ... , Bn  inst(P), {B1, ... , Bn}  I implies A  I.
Lemma 4.12
The term interpretation
C (P) : {A | A is the root of some implication tree wrt. P}
is a model of P.
17 October 2006
Foundations of Logic and Constraint Programming
22
Ground Implication Trees and Herbrand Models
Lemma 4.26
Consider Herbrand interpretation I, atom A and program P
•
I |= A iff ground (A)  I
•
I |= A iff for every A ← B1, ... , Bn  ground(P), {B1, ... , Bn}  I implies A  I.
Lemma 4.28
The Herbrand interpretation
M(P) : {A | A is the root of some ground implication tree wrt. P}
is a model of P.
17 October 2006
Foundations of Logic and Constraint Programming
23
Implication Trees (Example)
Let Padd be the” add-program” below and V a set of variables.
add(0,M,M).
add(s(M),N,s(K)):- add(M,N,K).
The term interpretation
C (P) = {add(sn(0), t, sn(t)) | n  N, t  TU{s,0},V }
= {add(sn(0), sm(v), sm+n(v)) | n,m  N, v  V  {0} }
is a model of Padd.
The Herbrand interpretation
M(P) = {add(sn(0), t, sn(t)) | n  N, t  HU{s,0} }
= {add(sn(0), sm(0), sm+n(0)) | n,m  N}
is a model of Padd.
17 October 2006
Foundations of Logic and Constraint Programming
24
Answer Substitutions
Let Padd be the” add-program” below and the query Q = add(s(0), u, s(u))
add(0,M1,M1).
add(s(M2),N,s(K)):- add(M2,N,K).
•
 = {u / s(s(v))}is a correct answer substitution of Q, since
Padd |= Q = add(s(0), s(s(V)), s(s(s(V)))) .
-
However, there is no SLD-derivation leading to Q. In fact, query Q leads to
the following SLD-derivation of Padd  {Q}
add(s(0), u, s(u)) 1 add(0, u, u )  2 □
where 1 = {M2/0, N/u, K/u} and 2 = {u/M1}. Hence,
h = 1 2 | {u} = {u/M1} is the Computed Answer Substitution (CAS) of Q.
-
Hence, Qh is more general than Q (since  = h {M1/s(s(v) ), and CAS are
more general than specific correct answer substitutions. Nevertheless, are
there always CAS, possibly more general, for every correct answer?
-
The completeness result for SLD-resolution ensures this.
17 October 2006
Foundations of Logic and Constraint Programming
25
Completeness of SLD-Resolution (Implication Trees)
First, a convenient lemma is obtained that relates SLD-resolution with
implication trees.
-
Query Q is n-deep
:
every atom in Q is the root of an implication tree, and n is the total number of
nodes in these trees.
Lemma 4.15
Suppose Q is n-deep for some n  0. Then for every selection rule R there
exists a successful SLD-derivation of P {Q} with CAS h such that Qh is more
general than Q.
Proof. By induction on n (see [Apt97], pg 84)
17 October 2006
Foundations of Logic and Constraint Programming
26
Completeness of SLD-Resolution (1)
Theorem 4.13
Suppose  is a correct answer substitution of Q. Then for every selection rule
R there exists a successful SLD-derivation of P {Q} with CAS h such that Qh
is more general than Q.
Proof. Let Q = A1, ... , Am. Then
 correct answer substitution of A1, ... , Am
 P |= A1, ... , Am
 for every interpretation I: if I |= P then I |= A1, ... , Am
 C(P) |= A1, ... , Am (since C(P) |= P, by Lemma 4.12)
 inst(Ai)  C(P) for every i  1, ..., m
 Ai  C(P) for every i  1, ..., m
 A1, ... , Am is n-deep for some n  0 (by definition of C(P) ).
 claim (by Lemma 4.15)
17 October 2006
Foundations of Logic and Constraint Programming
27
Completeness of SLD-Resolution (2)
The completeness of SLD-resolution is often regarded as the guarantee of
obtaining a successful SLD-derivation for any query whose existential closure
is implied by the program.
Corollary 4.16
Suppose P |=  Q. Then there exists a successful SLD-derivation of P {Q}.
Proof. P |=  Q
 P |= Q for some substitution 
  is a correct answer substitution of Q
 Claim (by Theorem 4.13)
-
However, it is interesting to characterise, beforehand, the set of queries whose
existential closure is implied by the program. This is the goal of the declarative
semantics for logic programs.
17 October 2006
Foundations of Logic and Constraint Programming
28
Least Herbrand Models
This set of queries is in fact the least Herbrand model of P. First we define it.
Theorem 4.29
M(P)† is the least Herbrand model of P.
Proof. Let IH be some Herbrand model of P and let A M(P). We prove A  IH by
induction on the number i of nodes in the ground implication tree wrt. P with
root A. Then M(P)  IH.
i = 1:
A is a leaf
 A ←  ground(P)
 IH |= A (since IH |= P)
 A  IH
i ~> i+1:
A has direct descendants B1, ... , Bn (roots of subtrees)
 A ← B1, ... , Bn  ground(P) and B1, ... , Bn  I (Herbrand Interpretation)
 A ← B1, ... , Bn  ground(P) and IH |= B1, ... , Bn
 IH |= A (since IH |= P)
 A  IH
†(M(P) as defined in slide 23)
17 October 2006
Foundations of Logic and Constraint Programming
29
Ground Equivalence
Now we characterise the set of ground atoms implied by a program.
Theorem 4.30
For every ground atom A : P |= A iff M(P) |= A
Proof.
 : P |= A and, from Lemma 4.28, M(P) |= P. Then it must be M(P) |= A.
 : Show that for all A M(P), every interpretation I: I |= P implies I |= A. Let
us consider Herbrand interpretation IH = {A | A ground atom and I |= A}. Then,
I |= P
 I |= A ← B1, ... , Bn for all A ← B1, ... , Bn  ground(P)
 if I |= B1, ... , Bn then I |= A for all A ← B1, ... , Bn  ground(P)
 if B1  IH, ... , Bn  IH, then A  IH, for all A ← B1, ... , Bn  ground(P)
 IH |= P (by Lemma 4.26; thus IH is a Herbrand model)
 For all A M(P), it is A  IH , (IH |= A) as M(P) is the least Herbrand Model.
 Hence, I |= A (by definition of IH, A  IH implies A  IH).
17 October 2006
Foundations of Logic and Constraint Programming
30
Complete Partial Orderings
-
Once proven that the least Herbrand models are the set of ground atoms
implied by logic programs, it is interesting to specify alternative forms of
characterising these least Herbrand models.
Let (A,  ) be a partial ordering (i.e. reflexive, antisimmetric and transitive)
•
a is the least element of X A
:
a  X, a  x for all x X
•
a is the least upper bound of X A (notation a = X )
:
a  A , x  a for all x  X and a is the least such element of A
•
(A,  ) is a complete partial ordering (cpo) contains a least element
:
• A contains a least element
• For every increasing sequence ao  a1  a2 ... of elements of A, the set
X = { a0, a1, a2, ...} has a least upper bound.
17 October 2006
Foundations of Logic and Constraint Programming
31
Some Properties of Operators
Let (A,  ) be a complete partial ordering 
•
Operator T: A  A is monotonic
:
I  J implies T(I)  T(J)
•
Operator T: A  A is finitary
:
for every infinite sequence I0  I1  ...
 ∞n=0 T (In) exists and T (∞n=0 In)  ∞n=0 T(In)
•
Operator T: A  A is continuous
:
T is monotonic and finitary
•
I is a pre-fixpoint of T :
•
I is a fixpoint of T :
17 October 2006
T(I)  I
T(I) = I
Foundations of Logic and Constraint Programming
32
Iterating of Operators
Let (A, ) be a CPO, T: A A and I A
• T↑0(I) : I
• T↑(n+1)(I) : T(T↑n(I) )
• T↑w (I) : ∞n=0 (T↑n(I) )
T↑a : T↑a () (for a = 0, 1, 2, ... , w)
By the definition of a CPO:
• If the sequence T↑0(I) , T↑1(I) , T↑2(I) , ... is increasing, then T↑w (I) exists
Theorem 4.22
If T is a continuous operator on a CPO, then T↑w exists and is the least prefixpoint of T and the least fixpoint of T.
17 October 2006
Foundations of Logic and Constraint Programming
33
Consequence Operator TP
Consider CPO ({I | I Herbrand Interpretation}, ).
Let P be a program and I a Herbrand interpretation. Then
•
TP(I) : {A | A ← B1, ... , Bn  ground(P) , B1, ... , Bn  I}
Lemma 4.33
(i) TP is finitary
(i) TP is monotonic
•
In “practice”, the Tp operator is useful to obtain (least) Herbrand Models with
a bottom-up procedure.
17 October 2006
Foundations of Logic and Constraint Programming
34
Consequence Operator TP: Example (1)
happy ← summer, warm
warm ← sunny
sunny ←
summer ←
TP↑0 = 
TP↑1 = {sunny, summer}
TP↑2 = {sunny, summer, warm}
TP↑3 = {sunny, summer, warm, happy}
...
TP↑w = {sunny, summer, warm, happy}
17 October 2006
is the fixpoint
Foundations of Logic and Constraint Programming
35
Consequence Operator TP: Example (2)
happy ← summer, warm
warm ← sunny
sunny ←
summer ←
-
Notice that if I is some “incomplete model” of P, then the consequence
operator adds new atoms to I. For example, let
I = {summer, sunny}
then
J = TP(I) = {summer, sunny, warm}
and
TP(I)  I
17 October 2006
Foundations of Logic and Constraint Programming
36
Consequence Operator TP: Example (3)
num(0) ←
num(s(x)) ← num(x).
TP↑0 = 
TP↑1 = {num(0)}
% 0 is the 1st number
TP↑2 = {num(sk(0))}
...
0k<2
% 0, 1 are the first 2 numbers
where s0(0) = 0
TP↑i = {num(sk(0))}
...
0k<i
% 0, ..., i -1 are the first i numbers
TP↑w (I)= {num(sk(0))}
0k
% fixpoint
17 October 2006
Foundations of Logic and Constraint Programming
37
Consequence Operator TP: Example (4)
num(0) ←
num(s(x)) ← num(x).
sum(0,z,z) ← num(z)
sum(s(x),y,s(z)) ← sum(x,y,z).
TP↑0=
TP↑1={num(0}
TP↑2={num(0}, num(s(0)),sum(0,0,0)}
TP↑3={num(sk(0)),sum(si(0),sj(0),si+j(0))} 0  k < 2, 0  i < 1, 0  j < i
...
TP↑i={num(sk(0)),sum(si(0),sj(0),si+j(0))} 0  k < i, 0  i < i-1, 0  j< i
...
TP↑w={num(sk(0)),sum(si(0),sj(0),si+j(0))} 0  k, 0  i, 0  j fixpoint
17 October 2006
Foundations of Logic and Constraint Programming
38
TP characterization
Lemma 4.32
A Herbrand Interpretation I is a model of P iff
TP (I)  I
Proof.
I |= P
iff for every A ← B1, ... , Bn  ground(P) :
{B1, ... , Bn}  I implies A  I (by Lemma 4.26)
iff for every ground atom A :
A  TP (I) implies A  I
iff
TP (I)  I
17 October 2006
Foundations of Logic and Constraint Programming
39
Characterization Theorem
Theorem 4.31
The following sets are equal
•
M(P)
(i)
•
= least Herbrand model of P
(ii)
•
= least pre-fixpoint of P
(iii)
•
= least fixpoint of P
(iv)
•
= TP↑w
(v)
•
= {A | A is a ground atom, P |= A}
(vi)
17 October 2006
Foundations of Logic and Constraint Programming
40
Success Sets
The success set of a program P
:
{A | A is a ground atom,  sucessful SLD-derivation of P  {A} }
Theorem 4.37
For a ground atom A, the following are equivalent 
 M(P) |= A
(i)
•
(ii)
P |= A
 Every SLD-tree for P  {A} is successful
(iii)
 A is in the success set of P
(iv)
17 October 2006
Foundations of Logic and Constraint Programming
41