Transcript Document

Operational Semantics
- An overview
• The language of programs
• The computation mechanism
• Choices and their impact
14 October 2005
Foundations of Logic and Constraint Programming
1
Atoms and Herbrand Bases
-
The basic constructs of programs and queries are atoms (predicates).
Syntacticaly, atoms are similar to functions, but defined over predicate
symbols rather than function symbols.
-
Given

the term universe TUF,V (over variables V and Function symbols F)

a ranked alphabet  of predicate symbols
the term base TB
such that
 ,F,V
is (over , F and V) is the smallest set A of atoms
1. p  A, if p  (0)
2. p(t1,t2, ... ,tn)  A if p  (n) with n  1, and
t1,t2, ... , tn  TUF,V
-
Given the Herbrand Universe, HUF, and the ranked alphabet  of predicate
symbols:
Herbrand Base HB (over  and F) : TB  ,F,V
14 October 2005
Foundations of Logic and Constraint Programming
2
Programs and Queries
-
From atoms, both programs and queries can be constructed.

Query : finite sequence of atoms B1, B2, ..., Bn.

Empty Query : empty sequence of atoms.


An empty query is denoted by □
H  B (definite clause) :
-
H (the clause head) is an atom,
-
B (the clause body) is a query.
H  (unit clause) :
-
The clause body is empty

(Definite) program : finite set of definite and unit clauses

Horn Clause : Clause or a negated query
14 October 2005
Foundations of Logic and Constraint Programming
3
Intuitive Meaning of Clauses and Queries
-
Clauses are obtained from the atoms by connecting them with Boolean
connectives. Hence their intuitive meaning:
-
A clause H  B1, .. , Bn can be understood as the formula
x1, ..., xk (B1  ...  Bn  H); or
x1, ..., xk (B1  ...   Bn  H)
where x1, ... ,xk are the variables occurring in H  B1, .. , Bn.

-
A Unit clause, H , encodes x1, ..., xk H.
A query, A1, ..., An , can be understood as the formula
x1, ...,  xk (A1  ...  An) ; or
 x1, ..., xk (A1  ...   An)
where , x1, ... ,xk are the variables occurring in A1, ..., An.

The empty query, □, is equivalent to true.
14 October 2005
Foundations of Logic and Constraint Programming
4
Queries and Negated Queries
-
Informally, one is interested in assessing whether a query is a logical
consequence of a program. This is indeed equivalent to assess that the
negation of the query is contradictory with the program.
-
Hence





 x1, ...,  xk (A1  ...  An)
 x1, ...,  xk  (A1  ...  An)
 x1, ...,  xk ( A1  ...   An)
 x1, ...,  xk (false   A1  ...   An )
 x1, ...,  xk (false   (A1  ...  An)
 x1, ...,  xk (false  (A1  ...  An)
-
A negated empty query is equivalent to false (since the empty query is
equivalent to true)
-
The computation mechanism of logic programming proves either
 that a query is a logical consequence of the program
 that the negation of the query, together with the program, entails false.
14 October 2005
Foundations of Logic and Constraint Programming
5
What is computed
-
A program P can be understood as a set of axioms.
-
A query Q can be interpreted as the request for finding an instance, Qθ, which
is a logical consequence of P.
-
A successful derivation provides such a θ
(by composition of the substitutions performed at each derivation step)
-
Hence, the derivation is a proof of Qθ (from P)., i.e.
P |- Qθ
14 October 2005
Foundations of Logic and Constraint Programming
6
How it is computed
-
A computation is a sequence of derivation steps.
-
In each step an atom A is selected from the current query and a program
clause H  B is chosen.
-
If A and H are unifiable, and θ is an mgu of A and H, then A is replaced by B
in the query, and θ is applied to the resulting query.
-
The computation is successful if it ends with the empty query.
-
The resulting answer substitution is obtained by composition of the mgus of
each step.
14 October 2005
Foundations of Logic and Constraint Programming
7
SLD-Derivations (proposicional)
-
The schema described assumes that

atoms in the query are selected according to some Selection rule,

derivations are a (Linear) sequence of resolution steps, and that

the clauses in the program are all Definite clauses.
-
The sequence of resolution steps is thus known as an SLD-derivation.
-
In the propositional case (no variables), given
• A program P
• A query A, B, C (where A means it contains zero or more atoms).
• A clause B  B
-

B is the selected atom in the query

The resulting query ( A, B, C ) is called the SLD-resolvent.
The notation A, B, C  A, B, C may be used in this case.
14 October 2005
Foundations of Logic and Constraint Programming
8
SLD-Derivations (example)
-
Given program
1.
2.
3.
4.
5.
6.
7.
-
happy :- sun, holidays.
happy :- snow, holidays.
snow :- cold, winter.
cold :- winter
precipitation :- holidays.
winter.
holidays.
The following is an SLD-derivation of query ?- happy
???????-
14 October 2005
happy
snow, holidays
cold, winter, holidays
winter, winter, holidays
winter, holidays
holidays
□
(clause
(clause
(clause
(clause
(clause
(clause
2)
3)
4)
6)
6)
7)
Foundations of Logic and Constraint Programming
9
SLD-Derivations (non proposicional)
SLD derivations can be extended to first-order predicates (with variables).
Given
•
•
•
•
•
-
A program P
A query A, B, C
A clause c  P
A variant H  B of c, variable disjoint with the query
An mgu θ of B and H
SLD-resolvent of A, B, C and c wrt. B with mgu θ : 
(A, B, C) θ
-
SLD-derivation step : 
(A, B, C) θc (A, B, C) θ
-
input clause:  variant H  B of c,
“clause c is applicable to atom B”
14 October 2005
Foundations of Logic and Constraint Programming
10
SLD-Derivations (example)
Example: Given program
1. add(X,0,X).
2. add(X,s(Y),s(Z)) :- add(X,Y,Z).
the following is an SLD-derivation of query ?-add(s(0),W, s(s(s(0)))).
?-add(s(0),W, s(s(s(0)))).
(Variant a of Clause 2)
{Xa/s(0),W/s(Ya),Za/s(s(0))}
?-add(s(0),Ya, s(s(0))).
(Variant b of Clause 2)
{Xb/s(0),Ya/s(Yb),Zb/s(0))}
?-add(s(0),Yb, s(0)).
(Variant c of Clause 1)
{Xc/s(0) ,Yb/0}
?- □
14 October 2005
Foundations of Logic and Constraint Programming
11
SLD-Derivations (example)
?-add(s(0),W, s(s(s(0)))). (2a) {Xa/s(0),W/s(Ya),Za/s(s(0))}
?-add(s(0),Ya, s(s(0))).
(2b) {Xb/s(0),Ya/s(Yb),Zb/s(0))}
?-add(s(0),Yb, s(0)).
(1c) {Xc/s(0) ,Yb/0}
?- □
-
Composing the substitutions,
(θ 2a) (θ 2b) =
{ Xa/s(0), W/s(s(Yb)), Za/s(s(0)),
Xb/s(0), Ya/s(Yb),
Zb/s(0))
}
(θ 2a) (θ 2b) (θ 1c) =
{Xa/s(0),W/s(s(0)),Za/s(s(0)),
Xb/s(0),Ya/s(0),Zb/s(0)),
Xc/s(0) ,Yb/0
}
the answer W = s(s(0)) is obtained.
14 October 2005
Foundations of Logic and Constraint Programming
12
SLD-Derivations Steps
1. Selection:

Select an atom in the query
2. Renaming:

Rename (if necessary) the clause
3. Instantiation

Instantiate query and cluase by an mgu of the selected atom and the head
of the clause
4. Replacement

Replace the instance of the selected atom by the instance of the body of
the clause
14 October 2005
Foundations of Logic and Constraint Programming
13
SLD-Derivations
- A maximal sequence of SLD-derivation steps
Q0 θ1c1 Q1 θ2c2 Q2 ... Qn θn+1cn+1Qn+1 ...
is an
SLD-derivation of P  {Q0} :
 Q0, Q1, ... , Qn+1, ... are queries, each empty or with one atom selected in it;
 θ1, θ2, ... , θn+1, ... are substitutions;
 c1, c2, ... , cn+1, ... are clause of P;
 For every SLD-derivation step, standardisation apart holds.
14 October 2005
Foundations of Logic and Constraint Programming
14
Standardisation Apart
- Variables in a clause are universally quantified. It is thus important that when a
clause is used a variant of the clause is used with “fresh” variables that have
not been previously “used”.
- This guarantees that the input clause is variable disjoint from the initial query
and from the substitutions and input clauses used at earlier steps.
- Formally:
Var(c’i )  (Var(Q0) j=1..i-1 (Var (θj  Var(c´j )) = 
for i  1, where c’i ( variant of clause Ci  P) is the input clause used in the i-th
SLD-derivation step Qi θi+1ci+1 Qi+1
14 October 2005
Foundations of Logic and Constraint Programming
15
Result of a Derivation
- Let ξ = Q0 θ1c1 Q1 θ2c2 Q2 ... Qn-1 θncn Qn be a finite SLD-derivation.
 ξ is successful : Qn = □
 ξ failed : Qn  □ and no clause is appliucable to any atom of Qn.
- Let ξ be successful.
 Computed Answer Substitution (CAS) of Q0 (w.r.t. ξ)
: ( θ1 θ2 ... θn ) | Var(Q0)
 Computed Instance of Q0 (w.r.t. ξ)
: Q0 θ1 θ2 ... θn
14 October 2005
Foundations of Logic and Constraint Programming
16
Choices
-
A number of choices can be made in any SLD-derivation, namely
1. Choice of the renaming
2. Choice of the mgu
3. Choice of the selected atom
4. Choice of the program clause
-
How do they influence the result?
14 October 2005
Foundations of Logic and Constraint Programming
17
Resultants: What is Proved after a Step
- To assess the impact of the choices, it is conveniente to assess what is
“logically” computed at each derivation step.
- Informally, answer a query Q1, requires answering a subsequent query Q2.
Hence if Q2 is true for some substitution θ so is Q1. More formally,
Resultant Associated with Q1 θ1 Q2 : Implication Q1θ1  Q2
- Consider
 A program P
 A resultant R = Q  A, B, C
 A clause c
 A variant H  B of c, variable disjoint with R
 An mgu θ of B and H
SLD – Resolvent of resultant R and c wrt B with mgu θ :
Q  (A, B, C) θ
SLD – Resultant step :
Q  A, B, C
14 October 2005
 θc
Q  (A, B, C) θ
Foundations of Logic and Constraint Programming
18
Propagation
- Consider an SLD – Derivation
ξ = Q0 θ1c1 Q1 ... Qn θn+1cn+1Qn+1 ...
- Resultantant of level i of ξ, Ri :
Q0 θ1 θ2 ... θi  Qi for i 0
- The resultant Ri describes what is proved wrt to the initial query Q0, after i
derivation steps. In particular
 Nothing has been proved in the begining
R0: Q0  Q0
 The query has been answered, if the derivation is successful
Rn : Q0 θ1 θ2 ... θn if Qn = □ (since □ = true)
14 October 2005
Foundations of Logic and Constraint Programming
19
Resultants: SLD - derivations
- The selected atom of a resultant Q1  Qi is defined as the atom selected in Qi.
Lemma 3.12
- Assume that R θc R1 and R’ θ’c R’1 are two SLD – resultant steps such
that
 R is an instance of R’
 In R and R’ atoms in the same positions are selected
then R1 is an instance of R’1.
Proof: See [Apt97], page 55.
Sketch: If R is an instance of R’, then θ = θ’σ (for some σ) and R = R’ σ.
14 October 2005
Foundations of Logic and Constraint Programming
20
Resultants: SLD - derivations
Example:
- Let us consider
 clause c: q(W,b):- s(W).
 resultant R: p(a,Y) :- q(a,Z), r(Z,Y).
 resultant R’: p(X,Y) :- q(X,Z), r(Z,Y).
 atom q/2 is selected in both resultants .
Now, if atom q/2 is selected in both resultants, it must be
 θ = mgu(q(a,Z), q(W,b)) = {W/a, Z/b}, and from R , c and θ
resultant R1 : p(a,Y) :- s(a), r(b,Y).
 θ’ = mgu(q(X,Z), q(W,b)) = {W/X, Y/b}, and from R’ , c and θ’
resultant R’1 : p(X,Y) :- s(X), r(b,Y).
thus confirming that R1 is an instance of R’1. Moreover, it is
θ = θ’ {X/a} and so R1 = R’1 {X/a}
14 October 2005
Foundations of Logic and Constraint Programming
21
Resultants: SLD-derivations
- A similar result can be obtained for SLD-resolvents
Corollary 3.13
- Assume that Q θc Q1 and Q’ θ’c Q’1 are two SLD–resultant steps such
that
 Q is an instance of Q’
 In R and R’, atoms in the same positions are selected
then Q1 is an instance of Q’1.
Example:
From Q: q(a,Z), r(Z,Y) and Q’: q(X,Z), r(Z,Y) if atom q/2 is
selected in both resolvents, together with clause c: q(W,b):- s(W), then
Q1: s(a), r(b,Y)
14 October 2005
and
Q’1: s(X), r(b,Y)
Foundations of Logic and Constraint Programming
22
Similar SLD-derivations
- Consider two (initial fragments) of SLD – derivations
ξ = Q0 θ1c1 Q1 ... Qn θn+1cn+1Qn+1 ...
ξ’ = Q’0 θ’1c1 Q’1 ... Q’n θ’n+1cn+1Q’n+1 ...
ξ and ξ’ are similar :
 lenght(ξ ) = lenght(ξ’ );
 Q0 and Q’0 are variants,
 in Qi and Q’i atoms in the same positions are selected (for i in 0.. n)
14 October 2005
Foundations of Logic and Constraint Programming
23
A Theorem on Variants
Theorem 3.18:
Consider two similar SLD – derivations ξ and ξ’ . Then for every i  0, the
resultants Ri and R’i of level i of ξ and ξ’, respectively, are variants of each
other.
Proof (by induction):
Base case (i=0) :
R0: Q0  Q0 and R’0: Q’0  Q’0 . But Q0 is a variant of Q’0 (by definition
of similar derivations), hence Q0 is a variant of Q’0.
Induction case (i > i+1) :
Let Ri θi+1ci+1 Ri+1 and R’ i  θ’i+1ci+1 R’i+1. Then
Ri is a variant of R’i (induction hypothesis)
 Ri is an instance of R’i and vice-versa (definition of variant)
 Ri+1 is an instance of R’i+1 and vice-versa (lemma 3.12)
 Ri+1 is a variant of R’i+1 (definition of variant)
14 October 2005
Foundations of Logic and Constraint Programming
24
Answer Substitutions of Similar SLD-derivations
Corollary 3.19:
Consider two similar SLD – derivations of Q0 with computed answers
substitutions θ and σ . Then Q0θ and Q0 σ are variants of each other.
Proof:
If the derivations are successful, then their final resultants are
ξ : Q0θ  □ and ξ ‘: Q0 σ  □ .
By theorem 3.18, Q0θ and Q0 σ are variants.
-
Hence,

Choices of type 1 (choice of a renaming)

Choices of type 2 (choice of an mgu)
do not influence - modulo renaming – on the statement proved by a
successful SLD–derivation.
14 October 2005
Foundations of Logic and Constraint Programming
25
Atom Selection in Queries
-
Let INIT be the set of all initial fragments of all possible SLD-derivations in
which the last query is non-empty.
-
A selection rule, is a function which for every ξ<  INIT yields an occurrence
of an atom in the last query of ξ<
-
An SLD-derivation ξ is via a selection rule R if for every initial fragment ξ< of ξ
ending with a non-empty query Q, R (ξ< ) is the selected atom of Q.
Example:
In Prolog, the rule used is “select the leftmost atom”
14 October 2005
Foundations of Logic and Constraint Programming
26
Switching Lemma
Lemma 3.32
-
Consider an SLD-derivation
ξ = Q0 θ1c1 Q1 ... Qn θn+1cn+1 Qn+1 θn+2cn+2 Qn+2 ...
where
 Qn includes atoms A1 and A2
 A1 is the selected atom of Qn
 A2θn+2 is the selected atom of Qn+1
Then for some Q’n+1, θ’n+1 and θ’n+2 there is an SLD-derivation
ξ’ = Q0 θ1c1 Q1 ... Qn θ’n+1cn+1Q’n+1 θ’n+2cn+2Qn+2 ...
where
 A2 is the selected atom of atoms Qn
 A1 θ’n+1 is the selected atom of Q’n+1
 θ’n+1 θ’n+2 = θn+1 θn+2
Proof: see [Apt97, page 65].
14 October 2005
Foundations of Logic and Constraint Programming
27
Independence of Selection Rule
Theorem 3.33
-
-
Let ξ be a successful SLD-derivation of P  {Q0}. Then for every selection
rule R , there exists a successful SLD-derivation ξ’ of P  {Q0} via R such that

CAS of Q0 (wrt ξ) = CAS of Q0 (wrt ξ’)

ξ and ξ’ are of the same length
Hence, choices of type 3 (choice of a selected atom) have no influence
in case of successful queries.
14 October 2005
Foundations of Logic and Constraint Programming
28
Independence of Selection Rule
Proof Sketch (of Theorem 3.33):
(By induction on the number of derivation steps)
Base case (i=1) :
 If the derivation has only one step, than Q0 has a single atom and any
rule must select it.
Induction case (i > i+1) :
-
Assume that the first i steps of the successful derivation ξ are similar to the
first i steps obtained by using rule R..
-
Assume further that in the i+1th step ξ selects atom A in Qi, whereas rule R
selects atom B.
-
Since B must be selected in some subsequent step j of ξ (i +1  j  n), it is
ξ = Q0 ... Qi[A] θi+1ci+1 Qi+1 ... Qj[B] θj+1cj+1 Qj+1 ... Qn-1  Qn = □
-
Applying the switching lemma j-i times to ξ the successful derivation ξ’ is
obtained
ξ’ = Q0 ... Qi(B) σi+1c’i+1 Q’i+1 (A) ... Q’n -1Qn = □.
for which the first i+1 steps are similar to those obtained by using rule R .
14 October 2005
Foundations of Logic and Constraint Programming
29
SLD-Trees and Search Space
Selection rule R variant independent :
-
For all initial fragments of SLD-derivations that are similar, R chooses the
atom in the same position of the last query.
Examples:

Prolog’s rule “select leftmost atom” in the query is variant
independent.

A selection rule such as “select the rightmost atom with predicate
symbol p with arity k, otherwise select the leftmost atom” is variant
independent

A selection rule such as “select leftmost atom if variable X appears
in the query, otherwise select rightmost atom” is not variant
independent
14 October 2005
Foundations of Logic and Constraint Programming
30
SLD-Trees and Search Space
SLD-Tree for P  {Q} via selection rule R :
-
The branches are SLD-derivations of P  {Q} via R
-
Every node Q with selected atom A has exactly one descenddant for every
clause c of P, which is applicable to A.

This descendant is a resolvent of Q and c wrt A.
SLD-Tree successful :
An SLD-tree that contains the success leaf □.
SLD-Tree finitely failed :
An SLD-tree that is finite and not successfully.
The SLD-Tree via “leftmost selection rule” corresponds to Prolog’s strategy
for searching for solutions..
14 October 2005
Foundations of Logic and Constraint Programming
31
The Branch Theorem
Theorem 3.38
-
Consider an SLD-tree T for P  {Q0} via a variant dependent selection rule R.
Then every SLD-derivation of P  {Q0} via R is similar to a branch in T.
-
Hence, choices of type 4 (choice of a program clause) have no influence
on the search space as a whole.
-
Nevertheless, the same search space can be searched differently by different
strategies. For example,

If an infinite branch is to the “left” of any success node, the “left to right
depth first search” of Prolog does not succeed (no termination).

If the order of the clauses is changed, than it is as if Prolog were “right to
left depth first search”, thus finding the solution (before entering the
endless loop).
14 October 2005
Foundations of Logic and Constraint Programming
32
The Branch Theorem
Proof Sketch (of Theorem 3.38):
-
Let ξ = Q0 Q1  Q2 ... be an SLD derivation of P  {Q0} via R
-
By induction on i  0 , a branch (with nodes Q’0, Q’1, Q’2, ...) in T similar to ξ
should be found:
Base case (i=0) :

Q’0 = Q0 (in particular they are variants).
Induction case (i > i+1) :
-
By induction hypothesis, Q0 ... Qi is similar to Q’0  ... Q’i
-
By definition of T , the existence of Q’i implies the existence of Q’i+1 (apply the
same clause as to Qi ).
-
By variant independence, in Qi and Q’i atoms in the same position are
selected, so Q0 ... Qi+1 is also similar to Q’0  ... Q’i+1..
14 October 2005
Foundations of Logic and Constraint Programming
33