�
�
�
�
163
Supported Model Semantics
interpretations and if function symbols are present, then the absence of local
variables is equivalent to a program being of finite type.
5.4.5 Proposition Let P be a normal logic program of finite type, and let
T be a local consequence operator for P . Then T is continuous in Q.
Proof: Let I ∈ I P be an interpretation, let G 2 = G(A, t i ) be a subbasic
neighbourhood of T (I) in Q, and note that G 2 is the set of all K ∈ I P
such that K(A) = t i . We need to find a neighbourhood G 1 of I such that
T (G 1 ) ⊆ G 2 . Since P is of finite type, the set B A is finite. Hence, the set G 1 =
B∈B A
G(B, I(B)) is a finite intersection of open sets and is therefore open.
Since each K ∈ G 1 agrees with I on B A , we obtain T (K)(A) = T (I)(A) = t i
for each K ∈ G 1 by locality of T . Hence, T (G 1 ) ⊆ G 2 .
•
Now, if P is not of finite type, but we can ensure by some other property
of P that the, possibly infinite, intersection B∈B A G(B, I(B)) is open, then
the above proof will carry over to programs which are not of finite type, but
satisfy the propert we seek. Alternatively, we would like to be able to disregard
the infinite intersection entirely under conditions which ensure that we have
to consider finite intersections only, as in the case of a program of finite type.
The following definition is, therefore, quite a natural one to make.
5.4.6 Definition Let P be a logic program, and let T be a consequence
operator on I P . We say that T is (P -)locally finite for A ∈ B P and I ∈ I P if
there exists a finite subset S = S(A, I) ⊆ B A such that we have T (J)(A) =
T (I)(A) for all J ∈ I P which agree with I on S. We say that T is (P -)locally
finite if it is locally finite for all A ∈ B P and all I ∈ I P .
Obviously, any locally finite consequence operator is local. Conversely, a
local consequence operator for a program of finite type is locally finite. This
follows from the observation that, for a program of finite type, the sets B A ,
for any A ∈ B P , are finite. But a much stronger result holds.
5.4.7 Theorem A local consequence operator is locally finite for all A ∈ B P
and some I ∈ I P if and only if it is continuous at I in Q.
Proof: Let T be a locally finite consequence operator, let I ∈ I P , let A ∈ B P ,
and let G 2 = G(A, T (I)(A)) be a subbasic neighbourhood of T (I) in Q. Since
T is locally finite, there is a finite set S ⊆ B A such that T (J)(A) = T (I)(A) for
all J ∈ B∈S G(B, I(B)). By finiteness of S, the set G 1 =
G(B, I(B))
B∈S
is an open neighbourhood of I, and by the choice of S we have T (G 1 ) ⊆ G 2 ,
and this suffices for continuity of T at I.
For the converse, assume that T is continuous at I in Q, and let A ∈ B P
be chosen arbitrarily. Then G 2 = G(A, T (I)(A)) is a subbasic open neighbourhood of T (I), so that, by continuity of T , there exists a basic open neighbourhood G 1 = G(B 1 , I(B 1 )) ∩ · · · ∩ G(B k , I(B k )) of I with T (G 1 ) ⊆ G 2 . In
�
�
�
163
Supported Model Semantics
interpretations and if function symbols are present, then the absence of local
variables is equivalent to a program being of finite type.
5.4.5 Proposition Let P be a normal logic program of finite type, and let
T be a local consequence operator for P . Then T is continuous in Q.
Proof: Let I ∈ I P be an interpretation, let G 2 = G(A, t i ) be a subbasic
neighbourhood of T (I) in Q, and note that G 2 is the set of all K ∈ I P
such that K(A) = t i . We need to find a neighbourhood G 1 of I such that
T (G 1 ) ⊆ G 2 . Since P is of finite type, the set B A is finite. Hence, the set G 1 =
B∈B A
G(B, I(B)) is a finite intersection of open sets and is therefore open.
Since each K ∈ G 1 agrees with I on B A , we obtain T (K)(A) = T (I)(A) = t i
for each K ∈ G 1 by locality of T . Hence, T (G 1 ) ⊆ G 2 .
•
Now, if P is not of finite type, but we can ensure by some other property
of P that the, possibly infinite, intersection B∈B A G(B, I(B)) is open, then
the above proof will carry over to programs which are not of finite type, but
satisfy the propert we seek. Alternatively, we would like to be able to disregard
the infinite intersection entirely under conditions which ensure that we have
to consider finite intersections only, as in the case of a program of finite type.
The following definition is, therefore, quite a natural one to make.
5.4.6 Definition Let P be a logic program, and let T be a consequence
operator on I P . We say that T is (P -)locally finite for A ∈ B P and I ∈ I P if
there exists a finite subset S = S(A, I) ⊆ B A such that we have T (J)(A) =
T (I)(A) for all J ∈ I P which agree with I on S. We say that T is (P -)locally
finite if it is locally finite for all A ∈ B P and all I ∈ I P .
Obviously, any locally finite consequence operator is local. Conversely, a
local consequence operator for a program of finite type is locally finite. This
follows from the observation that, for a program of finite type, the sets B A ,
for any A ∈ B P , are finite. But a much stronger result holds.
5.4.7 Theorem A local consequence operator is locally finite for all A ∈ B P
and some I ∈ I P if and only if it is continuous at I in Q.
Proof: Let T be a locally finite consequence operator, let I ∈ I P , let A ∈ B P ,
and let G 2 = G(A, T (I)(A)) be a subbasic neighbourhood of T (I) in Q. Since
T is locally finite, there is a finite set S ⊆ B A such that T (J)(A) = T (I)(A) for
all J ∈ B∈S G(B, I(B)). By finiteness of S, the set G 1 =
G(B, I(B))
B∈S
is an open neighbourhood of I, and by the choice of S we have T (G 1 ) ⊆ G 2 ,
and this suffices for continuity of T at I.
For the converse, assume that T is continuous at I in Q, and let A ∈ B P
be chosen arbitrarily. Then G 2 = G(A, T (I)(A)) is a subbasic open neighbourhood of T (I), so that, by continuity of T , there exists a basic open neighbourhood G 1 = G(B 1 , I(B 1 )) ∩ · · · ∩ G(B k , I(B k )) of I with T (G 1 ) ⊆ G 2 . In