1:
2: \documentstyle[amssymb,twoside]{article}
3: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4: %TCIDATA{OutputFilter=Latex.dll}
5: %TCIDATA{LastRevised=Wednesday, January 23, 2002 21:49:04}
6: %TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
7: %TCIDATA{Language=American English}
8:
9: \renewcommand{\baselinestretch}{1}
10: \renewcommand{\arraystretch}{1}
11: \textheight=19.3cm
12: \textwidth=12.2cm
13: \renewcommand{\aa}{\underline}
14: \newcommand{\oo}{\overline}
15: \newcommand{\lfp}{\rm lfp}
16: \newcommand{\bigland}{\bigwedge}
17: \newcommand{\biglor}{\bigvee}
18: \newcommand{\LIM}{{\rm LIM}}
19: \newcommand{\dlim}{\ddd\lim}
20: \newcommand{\rt}{\rightarrow}
21: \newcommand{\ddd}{\displaystyle}
22: \newcommand{\Lim}{{\rm Lim}}
23: \newcommand{\Cn}{{\rm Cn}}
24: \newcommand{\<}{\langle}
25: \renewcommand{\>}{\rangle}
26: \input{tcilatex}
27:
28: \begin{document}
29:
30:
31: \begin{center}
32: {\Large {\bf The Limits of Horn Logic Programs}} \footnote{{\small The
33: project is supported by the National 973 Project of China under the grant
34: number G1999032701 and the National Science Foundation of China.}}\\[0.5cm]
35: {Shilong Ma$^{\dag }$\footnote[2]{{\small Email: \{slma,
36: kexu\}@nlsde.buaa.edu.cn.}}, Yuefei Sui$^{\ddag }$\footnote[3]{{\small %
37: Email: suiyyff@sina.com.}}, and Ke Xu$^{\dag ,2}$}\\[0pt]
38: {\ {}$^{\dag }$ Department of Computer Science \\[0pt]
39: Beijing University of Aeronautics and Astronautics\\[0pt]
40: Beijing 100083, China}\\[0pt]
41: {\ {}$^{\ddag }$ Institute of Computing Technology, Academia Sinica \\[0pt]
42: Beijing 100080, China}
43: \end{center}
44:
45: \bigskip
46:
47: \begin{minipage}{11cm}
48: {\small\footnotesize {\bf Abstract}: \ Given a sequence $\{\Pi_n\}$ of Horn logic
49: programs, the limit $\Pi$ of $\{\Pi_n\}$ is the set of the clauses such that
50: every clause in $\Pi$ belongs to almost every $\Pi_n$ and every clause in
51: infinitely many $\Pi_n$'s belongs to $\Pi$ also. The limit program $\Pi$ is still Horn but may be infinite.
52: In this paper, we consider if
53: the least Herbrand model of the limit of a given Horn logic program
54: sequence $\{\Pi_n\}$ equals the limit of the least Herbrand models of each logic program $\Pi_n$.
55: It is proved that this property is not true in general but holds if under an assumption which can
56: be syntactically checked and be satisfied by a
57: class of Horn logic programs. Thus, under this assumption we can approach the least Herbrand model of
58: the limit $\Pi$ by the sequence of the least Herbrand models of each finite program $\Pi_n$.
59: We also prove that if a finite Horn logic program
60: satisfies this assumption, then the least Herbrand model of this program is
61: recursive. Finally, by use of the concept of stability from dynamical systems,
62: we prove that this assumption is exactly a sufficient condition to guarantee
63: the stability of fixed points for Horn logic programs.
64:
65: {\bf Keywords:} Logic Program, Horn Theory, Herbrand Model, Limit, Stability,
66: \linebreak Decidability.}
67: \end{minipage}
68:
69: \bigskip
70:
71: \noindent{\bf 1.Introduction}
72:
73: \smallskip
74:
75: As time goes by, the knowledge of the human being is increasing
76: exponentially. The amount of information on the Internet is doubled in
77: several months. So it becomes more and more important to discover useful
78: knowledge in massive information. There have been several data mining tools
79: to find useful knowledge from very large databases. If the knowledge found
80: by a data mining tool is taken as a theory at the current time, we assume
81: that the theory is consistent. As the knowledge increases, the theories
82: should also be updated. Thus we get a sequence of theories $\Pi _{1},\Pi
83: _{2},\cdots ,\Pi _{n},\cdots $. This procedure may never stop, i.e. maybe
84: there does not exist a natural number $k$ such that $\Pi _{k}=\Pi
85: _{k+1}=\cdots $. For example, if we restrict the theories to Horn logic
86: programs, then there exists some Herbrand interpretation $I$ such that we
87: will never find a finite program $\Pi $ whose least Herbrand model $M=I,$
88: because that the set of Herbrand interpretations is uncountable while the
89: set of finite programs is only countable$^{[8]}$. So sometimes we need to
90: consider some kind of limit of theories and discover what kind of knowledge
91: is true in the limit.
92:
93: Formally introducing limits of sequences of first order theories into logic
94: and computer science, and using theory versions as approximations of some
95: formal theories in convergent infinite computations are independent
96: contributions by Li in 1992. Li$^{[5],[6],[7]}$ first defined the limits of
97: first order theories, and thereon gave a formal system of the inductive
98: logic. Precisely, given a sequence $\{\Pi _{n}\}$ of the first order
99: theories $\Pi _{n}$'s, the limit $\Pi =\displaystyle\lim_{n\rightarrow
100: \infty }\Pi _{n}$ is the set of the sentences such that every sentence in $%
101: \Pi $ belongs to almost every $\Pi _{n},$ and every sentence in infinitely
102: many $\Pi _{n}$'s belongs to $\Pi $ also. The limit does not always exist
103: for any sequence of the first order theories.
104:
105: We shall consider the limits of the logic programs in terms of their
106: Herbrand models, and focus on the Horn logic programs. There are two reasons
107: for us to focus on the Horn logic programs. Firstly, the Horn logic programs
108: are used as a main representation method of knowledge in the knowledge
109: engineering. Every knowledge base must have the ability to reason, and the
110: reasoning in a Horn logic program is feasible. Secondly, the Horn logic
111: programs have the least Herbrand model$^{[10]}$, since the meet of any two
112: Herbrand models of a Horn logic program is a Herbrand model of this Horn
113: logic program.
114:
115: For a sequence $\{\Pi _{n}\}$ of finite Horn logic programs, if the limit $%
116: \Pi $ of $\{\Pi _{n}\}$ exists then $\Pi $ is a Horn logic program but it
117: may be infinite. To discover what is true in $\Pi $,\ it is crucial to
118: compute the least Herbrand model of $\Pi $. Then, the problem is: {\sl How to
119: construct the least Herbrand models of such Horn logic programs}?
120:
121: We know that for every finite $\Pi _{n}$, the least Herbrand model can be
122: constructed. Therefore, one may naturally wonder if the least Herbrand model
123: of $\Pi $ can be approached by the sequence of the least Herbrand models of $%
124: \Pi _{n}$. Let $M_{n}$ and $M$ be the least Herbrand models of $\Pi _{n}$
125: and $\Pi $ respectively. Namely, we hope to have
126: $$
127: M=\displaystyle\lim_{n\rightarrow \infty }M_{n}.\eqno(\ast )
128: $$%
129: In another form, ${\bf M}(\displaystyle\lim_{n\rightarrow \infty }\Pi _{n})=%
130: \displaystyle\lim_{n\rightarrow \infty }{\bf M}(\Pi _{n}),$ where ${\bf M}$
131: is taken as an operator which maps a Horn logic program to the least
132: Herbrand model of the logic program.
133:
134: In this paper, we prove that $(\ast )$ holds for a class of Horn logic
135: programs. Thus, if $\{\Pi _{n}\}$ is a sequence of finite Horn logic
136: programs in this class and $\Pi =\displaystyle\lim_{n\rightarrow \infty }\Pi
137: _{n}$ exists, then we can approach the least Herbrand model of $\Pi $ by the
138: sequence of the least Herbrand models of each program $\Pi _{n}$.
139:
140: The paper is arranged as follows. In section 2, we will give the basic
141: definitions in logic programs, and the fixpoint semantics of Horn logic
142: programs. In section 3, we will give two examples to show that $(\ast )$ is
143: not true in general but holds for some Horn logic programs. In section 4, we
144: will prove that $(\ast )$ is true under an assumption which can be syntactically
145: checked and easily satisfied, and if a finite Horn
146: logic program satisfies this assumption then the least Herbrand model of
147: this program is recursive. In section 5, by use of the concept of stability
148: from dynamical systems, we will prove that the assumption in section 4 is
149: exactly a sufficient condition to guarantee the stability of fixed points
150: for Horn logic programs.
151:
152: Our notation follows from Dahr's book$^{[2]}.$ We use $\Pi $ to denote a
153: logic program, $p,q$ atoms, $\pi $ a clause and $\Theta $ a substitution. $%
154: I,J$ denote subsets of Herbrand bases, or interpretations; $n,m,r,s,N$
155: denote the natural numbers. \bigskip
156:
157: \noindent {\bf 2. The basic definitions}
158:
159: \smallskip
160:
161: Let the base (language) $L$ consist of finite sets of constant symbols,
162: variable symbols, function symbols and predicate symbols. A term or formula
163: is {\it ground}\ if there is no variable in it. Let $TE_{L}$ be the set of
164: all terms in $L$, and $TG_{L}$ of all the ground terms in $L.$ A {\it literal%
165: } is an atom or the negation of an atom. An atom is called a {\it positive}
166: literal whereas a negated atom is called a {\it negative} literal. A clause $%
167: \pi :p_{1}\vee \cdots \vee p_{r}\leftarrow q_{1},\cdots ,q_{s}$ is called a
168: {\it rule}\thinspace\ if $r\geq 1$ and $s\geq 1;$ a {\it fact}\thinspace\ if
169: $r\geq 1$ and $s=0;$ and a {\it goal}\thinspace\ if $r=0$ and $s\geq 1.\
170: p_{1}\vee \cdots \vee p_{r}$ is called the {\it rule head}, denoted by $%
171: head(\pi ),$ and $q_{1},\cdots ,q_{s}$ is called the {\it rule body},
172: denoted by $body(\pi ).$ Every $q_{i}$ is called a {\it subgoal.} We assume
173: that the clauses are closed, i.e., every clause is a closed formula with
174: universal quantification on variables in the formula, for example, $%
175: p(x)\leftarrow q(x)$ means that $\forall x[p(x)\leftarrow q(x)].$ A {\it %
176: logic program}\ is a set of clauses in some base $L.$
177:
178: {\bf Definition 2.1.} A clause $\pi :p_{1}\vee \cdots \vee p_{r}\leftarrow
179: q_{1},\cdots ,q_{s}$ is called {\it Horn clause} if $r\leq 1$ and every
180: subgoal is an atom. A logic program $\Pi $ is {\it Horn}\ if every formula
181: in $\Pi $ is a Horn clause.
182:
183: The {\it Herbrand universe} $U_L$ of a logic program in $L$ is the set of
184: all ground terms in $L.\ HB_L$ denotes the set of all the ground atoms in $%
185: L, $ called the {\it Herbrand base}.
186:
187: {\bf Definition 2.2.} A {\it Herbrand interpretation}\ of a logic program $%
188: \Pi$ is any subset $I$ of $HB.$ A Herbrand interpretation $I$ of $\Pi$ is a
189: {\it Herbrand model of} $\Pi$ if every clause is satisfied under $I.$
190: %Let $\Pi$ be a set of clauses; $S$ has a model if and only if $S$ has a Herbrand model.
191: A Herbrand model $I$ of a logic program $\Pi$ is called {\it minimal} if
192: there exists no subset $I^{\prime}\subseteq I$ that is a model for $\Pi;$
193: {\it least model} if $I$ is the unique minimal model of $\Pi.$
194:
195: {\bf Theorem 2.3}. ([10]) Let $\Pi $ be a Horn program and let $HM(\Pi )$
196: denote the set of all Herbrand models of $\Pi .$ Then the model intersection
197: property holds, i.e., $\displaystyle\bigcap_{W\in HM(\Pi )}W$ is a Herbrand
198: model of $\Pi .$
199:
200: \bigskip
201:
202: Let $S$ be a nonempty set and $\wp (S)$ be the power set of $S.$ Then $(\wp
203: (S),\subseteq )$ be a complete lattice. A mapping $f:\wp (S)\rightarrow \wp
204: (S)$ is {\it monotonic}\ if for all element $a,b\in \wp (S),\ a\subseteq b$
205: implies $f(a)\subseteq f(b);$ $f$ is {\it finitary}\ if $f(\bigcup_{n=0}^{%
206: \infty }a_{n})\subseteq \bigcup_{n=0}^{\infty }f(a_{n})$ for every infinite
207: sequence $a_{0}\subseteq a_{1}\subseteq \cdots ;\ f$ is {\it continuous}\ if
208: it is monotonic and finitary.
209:
210: {\bf Definition 2.4.} A subset $a\subseteq \wp(S)$ is called a {\it %
211: pre-fixpoint}\ if $f(a)\subseteq a;$ a {\it post-fixpoint}\ if $a\subseteq
212: f(a);$ and a {\it fixpoint}\ if $a=f(a).$
213:
214: Let $f:\wp(S)\rightarrow \wp(S)$ be a monotonic mapping. Then $f$ has a
215: least fixpoint ${\rm lfp(f).}$ Define by induction on $n$ the following
216: elements of $\wp(S):$
217: \[
218: \begin{array}{rl}
219: f^0 & =\emptyset; \\
220: f^1 & =f(\emptyset)=f(f^0); \\
221: f^{n+1} & =f(f^n).%
222: \end{array}%
223: \]
224: Let $f^\omega=\bigcup_{n=0}^\infty f^n.$
225:
226: {\bf Theorem 2.5}(Kleene).\ Let $f:\wp (S)\rightarrow \wp (S)$ be a
227: continuous mapping. Then ${\rm lfp(f)=f^{\omega }.}$
228:
229: \bigskip
230:
231: In 1992, Li$^{[5]}$ defined the limit of a theory sequence using the
232: standard set-theoretic definition of limit. By this definition, given a
233: sequence $\{\Pi _{n}\}$ of logic programs, we say that
234: \[
235: \overline{\displaystyle\lim }_{n\rightarrow \infty }\Pi _{n}=\displaystyle%
236: \bigcap_{i=1}^{\infty }\displaystyle\bigcup_{j=i}^{\infty }\Pi _{j}
237: \]%
238: is the upper limit of $\{\Pi _{n}\},$ and
239: \[
240: \underline{{\displaystyle\lim }}_{n\rightarrow \infty }\Pi _{n}=\displaystyle%
241: \bigcup_{i=1}^{\infty }\displaystyle\bigcap_{j=i}^{\infty }\Pi _{j}
242: \]%
243: is the lower limit of $\{\Pi _{n}\}.$ It follows from the definition of
244: limits that given a sequence $\{\Pi _{n}\}$ of logic programs, a clause
245: belongs to the upper limit iff it belongs to infinitely many $\Pi _{n}$'s,
246: and a clause belongs to the lower limit iff it belongs to almost every $\Pi
247: _{n}$. It is not hard to prove that $\underline{\displaystyle\lim }%
248: _{n\rightarrow \infty }\Pi _{n}\sqsubseteq \overline{\displaystyle\lim }%
249: _{n\rightarrow \infty }\Pi _{n}$. If $\overline{\displaystyle\lim }%
250: _{n\rightarrow \infty }\Pi _{n}=\underline{\displaystyle\lim }_{n\rightarrow
251: \infty }\Pi _{n}$ then we say that the (set-theoretic) limit of $\{\Pi
252: _{n}\} $ exists and denote it by $\displaystyle\lim_{n\rightarrow \infty
253: }\Pi _{n}.$
254:
255: \bigskip
256:
257: \noindent{\bf 3. The limits of the Horn logic programs}
258:
259: \smallskip
260:
261: Let $\Pi $ be a logic program. We define a mapping $f_{\Pi
262: }:2^{HB}\rightarrow 2^{HB}$ by, for any $I\in 2^{HB},$
263: \[
264: f_{\Pi }(I)=\{head(\pi )\Theta :\pi \in \Pi \ \&\ \exists \Theta \lbrack
265: body(\pi )\Theta \subseteq I]\}.
266: \]
267:
268: {\bf Proposition 3.1}([10]).\ If $\Pi $ is a Horn logic program then $f_{\Pi
269: }$ is monotonic and finitary. Moreover, $f_{\Pi }^{\omega }$ is the least
270: model of $\Pi .$
271:
272: \bigskip
273:
274: We hope to prove the following statement:
275:
276: $(3.1)$\ \ Given a sequence $\{\Pi_n\}$ of the Horn logic programs, let $M_n$
277: be the least model of $\Pi_n.$ If $\Pi=\displaystyle\lim_{n\rightarrow
278: \infty} \Pi_n$ exists then $\Pi$ is a Horn logic program. Let $M$ be the
279: least model of $\Pi,$ then $M=\displaystyle\lim_{n\rightarrow \infty} M_n.$
280:
281: The Claim $(3.1)$ does not hold for all Horn logic programs. Let us take a
282: look at the following example.
283:
284: \bigskip
285:
286: {\bf Example 3.2.}\ Assume that there are one function symbol $f,$ one
287: predicate symbol $p$ and one constant symbol $a$ in $L.$ Let $\{\Pi _{n}\}$
288: be defined as follows:
289: \[
290: \begin{array}{rl}
291: \Pi _{1} & =\{p(x)\leftarrow p(f(x)),p(f(a))\}, \\
292: \Pi _{2} & =\{p(x)\leftarrow p(f(x)),p(f^{2}(a))\}, \\
293: & \cdots \\
294: \Pi _{n} & =\{p(x)\leftarrow p(f(x)),p(f^{n}(a))\},%
295: \end{array}%
296: .
297: \]%
298: where $f^{(n)}(a)=f(f^{(n-1)}(a)),f^{1}(a)=f(a).$ Then we have
299: \[
300: \begin{array}{rl}
301: f_{\Pi _{1}}^{\omega } & =\{p(a),p(f(a))\}, \\
302: f_{\Pi _{2}}^{\omega } & =\{p(a),p(f(a)),p(f^{2}(a))\}, \\
303: & \cdots \\
304: f_{\Pi _{n}}^{\omega } & =\{p(a),p(f(a)),\cdots ,p(f^{n}(a))\},%
305: \end{array}%
306: \]%
307: and
308: \[
309: \displaystyle\lim_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega
310: }=\{p(a),p(f(a)),\cdots ,p(f^{n}(a)),\cdots \}.
311: \]%
312: But
313: \[
314: \Pi =\displaystyle\lim_{n\rightarrow \infty }\Pi _{n}=\{p(x)\leftarrow
315: p(f(x))\},
316: \]%
317: and
318: \[
319: f_{\Pi }^{\omega }=\emptyset .
320: \]%
321: Therefore, $f_{\Pi }^{\omega }\neq \displaystyle\lim_{n\rightarrow \infty
322: }f_{\Pi _{n}}^{\omega }.$
323:
324: \bigskip
325:
326: For some other Horn logic programs, the Claim $(3.1)$ is true. Let us take a
327: look at the following example.
328:
329: {\bf Example 3.3.}\ Assume that there are one function symbol $f,$ one
330: predicate symbol $p$ and one constant symbol $a$ in $L.$ Let $\{\Pi _{n}\}$
331: be defined as follows:
332: \[
333: \begin{array}{rl}
334: \Pi _{1} & =\{p(f(x))\leftarrow p(x),p(f(a))\}, \\
335: \Pi _{2} & =\{p(f(x))\leftarrow p(x),p(f^{2}(a))\}, \\
336: & \cdots \\
337: \Pi _{n} & =\{p(f(x))\leftarrow p(x),p(f^{n}(a))\},%
338: \end{array}%
339: .
340: \]%
341: where $f^{n}(a)=f(f^{n-1}(a)),f^{1}(a)=f(a).$ Then we have
342: \[
343: \begin{array}{rl}
344: f_{\Pi _{1}}^{\omega } & =\{p(f(a)),p(f^{2}(a)),\cdots ,p(f^{m}(a)),\cdots
345: \}, \\
346: f_{\Pi _{2}}^{\omega } & =\{p(f^{2}(a)),p(f^{3}(a)),\cdots
347: ,p(f^{m}(a)),\cdots \}, \\
348: & \cdots \\
349: f_{\Pi _{n}}^{\omega } & =\{p(f^{n}(a)),p(f^{n+1}(a)),\cdots \},%
350: \end{array}%
351: \]%
352: and
353: \[
354: \displaystyle\lim_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }=\emptyset .
355: \]%
356: Now we have
357: \[
358: \Pi =\displaystyle\lim_{n\rightarrow \infty }\Pi _{n}=\{p(f(x))\leftarrow
359: p(x)\},
360: \]%
361: and
362: \[
363: f_{\Pi }^{\omega }=\emptyset .
364: \]%
365: Therefore, $f_{\Pi }^{\omega }=\displaystyle\lim_{n\rightarrow \infty
366: }f_{\Pi _{n}}^{\omega }.$
367:
368: \bigskip \bigskip
369:
370: \noindent{\bf 4. The main theorems}
371:
372: \smallskip
373:
374: Example 3.2 shows that the Claim $(3.1)$ does not hold for all Horn logic
375: programs. In general cases, we have the following property.
376:
377: {\bf Lemma 4.1.} For any base $L,$ given any sequence $\{\Pi _{n}\}$ of the
378: Horn logic programs in $L,$ if $\Pi =\displaystyle\lim_{n\rightarrow \infty
379: }\Pi _{n}$ exists then $\underline{\displaystyle\lim }_{n\rightarrow \infty
380: }f_{\Pi _{n}}^{\omega }$ is a Herbrand model of $\Pi .$ Therefore, $f_{\Pi
381: }^{\omega }\subseteq \underline{\displaystyle\lim }_{n\rightarrow \infty
382: }f_{\Pi _{n}}^{\omega }.$
383:
384: {\sl Proof.} To show that $f_{\Pi }^{\omega }\subseteq \underline{%
385: \displaystyle\lim }_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega },$ let $p$
386: be a ground atom $\in f_{\Pi }^{\omega },$ we prove the claim by induction
387: on $m$ such that $p\in f_{\Pi }^{m+1}-f_{\Pi }^{m}.$ There are two cases:
388:
389: Case 1. $p\in f_{\Pi }^{1}.$ Then $[p\leftarrow ]\in \Pi .$ Hence, for
390: almost every $n,[p\leftarrow ]\in \Pi _{n},$ so $p\in f_{\Pi
391: _{n}}^{1}\subseteq f_{\Pi _{n}}^{\omega }.$ Hence, $p\in \underline{%
392: \displaystyle\lim }_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }.$
393:
394: Case 2. $p\in f_{\Pi }^{m+1}-f_{\Pi }^{m}.$ By the definition of $f_{\Pi },$
395: there is a clause $\pi \in \Pi $ and a substitution $\Theta $ such that $%
396: body(\pi )\Theta \subseteq f_{\Pi }^{m}$ and $p=head(\pi )\Theta .$ By the
397: induction assumption, $body(\pi )\Theta \in \underline{\displaystyle\lim }%
398: _{n\rightarrow \infty }f_{\Pi _{n}}^{\omega },$ i.e., there is an $N_{0}$
399: such that for any $n\geq N_{0},$ $body(\pi )\Theta \subseteq f_{\Pi
400: _{n}}^{\omega }.$ Since $\pi \in \Pi ,$ then $\pi \in \Pi _{n}$ for almost
401: every $n.$ Let $N_{1}$ be the least such that for any $n\geq N_{1},\ \pi \in
402: \Pi _{n}.$ Let $N=\max \{N_{0},N_{1}\}.$ Hence, by the same substitution $%
403: \Theta ,$ $p=head(\pi )\Theta \in f_{\Pi _{n}}^{\omega }$ for any $n\geq N.$
404: \hfill$\Box $
405:
406: \bigskip
407:
408: Example 3.2 and lemma 4.1 indicate that to make the Claim $(3.1)$ hold, we
409: have to put some conditions on Horn logic programs.
410:
411: {\bf Assumption 4.2.} \ Given a Horn logic program $\Pi $, assume that every
412: clause $\pi :p\leftarrow p_{1},\cdots ,p_{m}$ in $\Pi $ has the following
413: property: for every $i$ if $t$ is a term in $p_{i}$, then $t$ is also in $p$.
414:
415: Nienhuys-Cheng$^{[9]}$ used the above condition to discuss a metric on the
416: set of Herbrand interpretations for finite Horn logic programs. As we know,
417: in a constrained clause, it is usually assumed that every variable occurring
418: in the body of a clause also occurs in its head. In fact, assumption 4.2 can
419: be syntactically checked in polynomial time and easily satisfied. For example, suppose that there are one
420: function symbol $f,$ one predicate symbol $p$ and one constant symbol $a$ in the base $L$.
421: It is easy to verify that there are infinitely many clauses satisfying this
422: assumption, e.g. $\pi _{k}=p(f^{k}(x))\leftarrow p(x)$, where $k=1,2,\cdots $%
423: . Based on this fact, we can conclude that there is an uncountable number of
424: infinte Horn logic programs satisfying assumption 4.2.
425:
426: By the definition of the limits and the assumption that every $\Pi _{n}$ is
427: Horn, it is easily verified that $\Pi =\displaystyle\lim_{n\rightarrow
428: \infty }\Pi _{n}$ is Horn. Under assumption 4.2, we shall prove the
429: following theorem.
430:
431: {\bf Theorem 4.3.} Let $L$ be a base consisting of infinitely many constant
432: symbols, function symbols and finitely many predicate symbols. Given a
433: sequence $\{\Pi _{n}\}$ of Horn logic programs in $L$, if $\Pi =\displaystyle%
434: \lim_{n\rightarrow \infty }\Pi _{n}$ exists and there is an $N$ such that $%
435: \Pi _{n}$ satisfies assumption 4.2 for every $n\geq N$, then $\displaystyle%
436: \lim_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }$ exists and $f_{\Pi
437: }^{\omega }=\displaystyle\lim_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }.$
438:
439: {\sl Proof.} We first prove that $\overline{\displaystyle\lim }%
440: _{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }\subseteq f_{\Pi }^{\omega }$.
441: Assume that $p\in \overline{\displaystyle\lim }_{n\rightarrow \infty }f_{\Pi
442: _{n}}^{\omega },$ then there is an infinite sequence $n_{i},i=1,2,\cdots ,$
443: such that for every $n_{i},p\in f_{\Pi _{n_{i}}}^{\omega }.$ Then by the
444: definition, for every $n_{i},$ there is a proof of $p$ from the facts of $%
445: \Pi _{n_{i}}.$ We define a proof tree $T$ of $p$ as follows such that every
446: node $\alpha $ of $T$ is associated with a set of atoms, denoted by $%
447: P(\alpha ).$ Let $\lambda $ be the root of $T,$ assume that $P(\lambda
448: )=\{p\}.$ For every clause $\pi \in \bigcup_{n=N}^{\infty }\Pi _{n}$ with
449: head $p,$ there is a node $\alpha \in T$ such that $\alpha $ is a child of $%
450: \lambda $ and $P(\alpha )=body(\pi ).$ For every node $\alpha \in T,$ if
451: there is a clause $\pi ^{\prime }\in \bigcup_{n=N}^{\infty }\Pi _{n}$ such
452: that $head(\pi ^{\prime })\in P(\alpha ),$ there is a child $\beta $ of $%
453: \alpha $ such that $P(\beta )=body(\pi ^{\prime })$ (if $\pi $ is a fact
454: then $P(\beta )=\emptyset $).
455:
456: We construct a subtree $T^{\prime }$ of $T$ as follows: let $\lambda \in
457: T^{\prime },$ and let $\alpha $ be a child of $\lambda $ such that $%
458: p\leftarrow P(\alpha )$ is used to deduce $p$, by the assumption, such an $%
459: \alpha $ does exist, then set $\alpha \in T^{\prime };$ and for any node $%
460: \alpha ^{\prime }\in T^{\prime }$ and $p^{\prime }\in P(\alpha ^{\prime }),$
461: let $\beta $ be the child of $\alpha ^{\prime }$ such that $p^{\prime
462: }\leftarrow P(\beta )$ is used to deduce $p^{\prime }$, then set $\beta \in
463: T^{\prime }.$
464:
465: We now prove that $T$ has only finitely many such subtrees. To do this, we
466: only need to show that $T$ is finite. Every ground atom has a tree structure
467: and the depth of the tree can be considered as the {\it level} of the atom$%
468: ^{[9]}$. By assumption 4.2, the level of an atom in $T$ is not smaller than
469: that of any atom in its children. Hence, the level of every atom in $T$ is
470: not greater than that of $p$, i.e. the levels of atoms in $T$ are finite.
471: Also by assumption 4.2, every function symbol or constant symbol appearing
472: in the nodes of $T$ also appears in $p$. Note that there are only finitely
473: many predicate symbols. Thus $T$ is finite and so we are done.
474:
475: It follows from the above analysis that there is a subtree $T^{\prime }$ of $%
476: T$ such that $T^{\prime }$ belongs to infinitely many $\Pi _{n}$'s. By the
477: definition of the limits, we have%
478: \[
479: T^{\prime }\subseteq \displaystyle\lim_{n\rightarrow \infty }\Pi _{n}.
480: \]%
481: There is an $N_{0}$ and a $K$ such that for every $n\geq N_{0},\ T^{\prime
482: }\in f_{\Pi _{n}}^{K}.$ So $p\in f_{\Pi }^{K},$ i.e., $p\in f_{\Pi }^{\omega
483: }$. Note that $p\in \overline{\displaystyle\lim }_{n\rightarrow \infty
484: }f_{\Pi _{n}}^{\omega }$. Thus $\overline{\displaystyle\lim }_{n\rightarrow
485: \infty }f_{\Pi _{n}}^{\omega }\sqsubseteq f_{\Pi }^{\omega }$. By lemma 4.1,
486: $f_{\Pi }^{\omega }\subseteq \underline{\displaystyle\lim }_{n\rightarrow
487: \infty }f_{\Pi _{n}}^{\omega }$. Recall that $\underline{\displaystyle\lim }%
488: _{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }\sqsubseteq \overline{%
489: \displaystyle\lim }_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }$. So, we get
490:
491: \[
492: \underline{\displaystyle\lim }_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega }=%
493: \overline{\displaystyle\lim }_{n\rightarrow \infty }f_{\Pi _{n}}^{\omega
494: }=f_{\Pi }^{\omega }.
495: \]%
496: This completes the proof. \hfill$\Box $
497:
498: \medskip
499:
500: The following discussion will point out an interesting decidability result
501: on the least Herbrand models related to the above main theorem. As we know,
502: given a finite Horn logic program, the least Herbrand model of this program
503: is in genreral non-recursive$^{[1]}$. In what follows, we will prove that
504: for finite Horn logic programs satisfying assumption 4.2, their least
505: Herbrand models are recursive. More precisely, we have the following theorem.
506:
507: {\bf Theorem 4.4.} Given a finite Horn logic program $\Pi $, if $\Pi $
508: satisfies assumption 4.2, then the least Herbrand model of $\Pi $ is
509: recursive.
510:
511: {\sl Proof.} For any ground atom $p$, using the clauses in $\Pi $, we can
512: construct a tree $T$ with $p$ as the root node by the same method as in the
513: proof of theorem 4.3. As previously shown, if $\Pi $ satisfies assumption
514: 4.2, then $T$ is finite. Note that $T$ contains all the possible proof trees
515: for $p$ from $\Pi $. So we can decide in finite time whether $p$ is provable
516: from $\Pi $. Equivalently, it is decidable whether $p$ is in the least
517: Herbrand model of $\Pi $. This completes the proof. \hfill $\Box $
518:
519: \bigskip
520:
521: \noindent {\bf 5. The stability of fixed points for Horn logic programs}
522:
523: \smallskip
524:
525: For a Horn logic program $\Pi $, the Herbrand models of this program are
526: also the fixed points of the mapping $f_{\Pi }$. In the study of dynamical
527: systems, the concept of stability is of great importance to characterize the
528: properties of fixed points. Intuitively, the stability of a fixed point of a
529: differential equation means that if the initial solution is sufficiently
530: close to the fixed point then the solution will remain close to the fixed
531: point thereafter$^{[3]}$. There are many ways to formalize this concept
532: mathematically which are similar but not the same. A classical concept for
533: the stability of fixed points defined by Lyapounov is as follows$^{[3]}$:
534:
535: A fixed point $X$ of $F:{\Bbb R}^{m}\rightarrow {\Bbb R}^{m}$ is {\it stable}
536: if for all $\epsilon >0$ there exists $\delta (\epsilon )$ such that
537:
538: \[
539: \left| F^{n}(x_{0})-X\right| <\epsilon \text{ \ \ \ for }n=1,2,\cdots ,
540: \]%
541: for all $x_{0}$ such that $\left| x_{0}-X\right| <\delta (\epsilon )$, where
542: $x_{n}=F^{n}(x_{0})$ is defined iteratively by $x_{n+1}=F(x_{n})$.
543:
544: To discuss the stability of fixed points for Horn logic programs, it is
545: essential to define a distance between Herbrand interpretations. Fitting$%
546: ^{[4]}$ was the first to introduce metric methods to logic programming. [4]
547: defined a metric on the set of Herbrand interpretations by level mappings
548: and studied the fixed point semantics for some logic programs using the
549: Banach contraction theorem. Nienhuys-Cheng$^{[9]}$ used the depth of an
550: expression tree for the level mapping and discussed this mapping and the
551: induced metric.
552:
553: {\bf Definition 5.1.} \ ([9]) Let $HB$ be the Herbrand base of a logical
554: language. A level mapping is a function $\parallel :HB\rightarrow {\Bbb N}$
555: (natural numbers). We use $\left| A\right| $ to denote $\parallel \left(
556: A\right) $, i.e. the image of $A$. It is called the {\it level} of $A$.
557:
558: Given a level mapping $\parallel $ we can define a metric on the set of all
559: Herbrand interpretations as follows: $d(I,I)=0$ for every interpretation $I$%
560: . If $I\neq J$, then $d(I,J)=1/2^{n}$ if $I$ and $J$ differ on some ground
561: atom of level $n$, but agree on all ground atoms of lower level$^{[4]}$,
562: i.e. $A\in I\cap J$ for all $\left| A\right| \leq n-1$ $\wedge $ $A\in I\cup
563: J$ and there is an $A\in I\vartriangle J$ such that $\left| A\right| =n$.
564:
565: {\bf Theorem 5.2.} \ ([4]) The function $d$ defined above is a metric on the
566: set of all Herbrand interpretations $2^{HB}$.
567:
568: {\bf Lemma 5.3.} \ ([4]) The metric space $\left( 2^{HB},d\right) $ is
569: complete.
570:
571: {\bf Definition 5.4.} \ ([9]) Every ground atom has a tree structure and the
572: depth can be considered as the level of the atom. Thus we have a level
573: mapping $\parallel :HB\rightarrow {\Bbb N}$. Let $d$ be the distance on the
574: set of Herbrand interpretations induced by this level mapping.
575:
576: For a Horn logic program $\Pi $, the mapping $f_{\Pi }$ is from the set of
577: Herbrand interpretations to the set of Herbrand interpretations. In this
578: paper, we will use the above metric to study the fixed points of Horn logic
579: programs. First, if a Horn logic program $\Pi $ satisfies assumption 4.2,
580: then the mapping $f_{\Pi }$ has the following property.
581:
582: {\bf Lemma 5.5.} \ ([9]) Given a Horn logic program $\Pi $, if $\Pi $\
583: satisfies assumption 4.2, then $d(f_{\Pi }(I),f_{\Pi }(J))$ $\leq d(I,J)$
584: for all $I,J\in 2^{HB}$.
585:
586: Given a Horn logic program $\Pi ,$ if there is a constant $c:0\leq c<1$ such
587: that $d(f_{\Pi }(I),f_{\Pi }(J))$ $<c\cdot d(I,J)$ for all $I,J\in 2^{HB}$,
588: then the mapping $f_{\Pi }$ is called a {\it contraction}. In such a case,
589: we know, by the Banach contraction theorem, that $f_{\Pi }$ has a unique
590: fixed point. For a Horn logic program $\Pi $ satisfying assumption 4.2, in
591: many cases the mapping $f_{\Pi }$ may be a contraction, e.g. $\Pi
592: =\{p(f(x))\leftarrow p(x),p(f(a))\}$, but not in general, e.g. $\Pi
593: =\{p(x)\leftarrow p(x),p(f(a))\}$ which has more than one fixed point such
594: as $\{p(f(a))\}$ and $\{p(a),p(f(a))\}$.
595:
596: We can now define and discuss the stability of fixed points for Horn logic
597: programs.
598:
599: {\bf Definition 5.6.} \ For a Horn logic program $\Pi $, a fixed point $J$
600: of $f_{\Pi }:2^{HB}\rightarrow 2^{HB}$ is {\it stable} if for all $\epsilon
601: >0$ there exists $\delta (\epsilon )$ such that
602:
603: \[
604: d(f_{\Pi }^{n}(I),J)<\epsilon \text{ \ \ \ for }n=1,2,\cdots ,
605: \]%
606: for all interpretations $I$ such that $d(I,J)<\delta (\epsilon )$.
607:
608: From the above definition, we can prove that the fixed points of Horn logic
609: programs satisfying assumption 4.2 are stable. That is to say, we have the
610: following theorem.
611:
612: {\bf Theorem 5.7.} Given a Horn logic program $\Pi $, if $\Pi $ satisfies
613: assumption 4.2, and $J$ is a fixed point of $f_{\Pi }$, then $J$ is a stable
614: fixed point.
615:
616: {\sl Proof.} To prove that $J$ is a stable fixed point, by definition 5.6,
617: we have to show that for any $\epsilon >0$ there exists $\delta (\epsilon )$
618: such that
619:
620: \[
621: d(f_{\Pi }^{n}(I),J)<\epsilon \text{ \ \ \ for }n=1,2,\cdots ,
622: \]%
623: for all interpretations $I$ such that $d(I,J)<\delta (\epsilon )$.
624:
625: Let $\delta (\epsilon )=\epsilon $. We can now prove the above inequality by
626: induction on $n$. When $n=0$, it is trivial to see that the inequality
627: holds. Assume that for $n=k$, the inequality also holds, i.e.
628:
629: \[
630: d(f_{\Pi }^{k}(I),J)<\epsilon .\text{ \ \ }
631: \]%
632: When $n=k+1$, applying lemma 5.2 yields
633:
634: \[
635: d(f_{\Pi }^{k+1}(I),J)=d(f_{\Pi }^{k+1}(I),f_{\Pi }^{k+1}(J))\leq d(f_{\Pi
636: }^{k}(I),J)<\epsilon \text{,}
637: \]%
638: as required. \hfill$\Box $
639:
640: \smallskip
641:
642: By theorem 5.7, it is easy to see that in example 3.3, the least Herbrand
643: model $M=\emptyset $ of the program $\Pi =\{p(f(x))\leftarrow p(x)\}$ is a
644: stable fixed point. But in example 3.2 where assumption 4.2 is not
645: satisfied, we can prove by contradiction that the least Herbrand model $%
646: M=\emptyset $ of the program $\Pi =\{p(x)\leftarrow p(f(x))\}$ is not a
647: stable fixed point. Suppose that $M=\emptyset $ is a stable fixed point. By
648: definition 5.6, for $\epsilon =1/8$, there exists a constant $\delta >0$
649: such that
650:
651: \[
652: d(f_{\Pi }^{n}(I),M)<\frac{1}{8}\text{ \ \ \ for }n=1,2,\cdots ,
653: \]%
654: for all interpretations $I$ such that $d(I,M)<\delta $. Let $%
655: I_{0}=\{p(f^{k}(a))\}$ where $k\in {\Bbb N}$ and $2^{k}>1/\delta $. Then we
656: have
657:
658: \[
659: d(I_{0},M)=\frac{1}{2^{k+2}}<\frac{1}{2^{k}}<\delta ,
660: \]%
661: and $f_{\Pi }^{k}(I_{0})=\{p(a)\}$. So $d(f_{\Pi }^{k}(I_{0}),M)=1/4$, which
662: contradicts the assumption that $d(f_{\Pi }^{n}(I_{0}),M)<1/8$ for $%
663: n=1,2,\cdots ,$ and thus completes the proof.
664:
665: \smallskip
666:
667: Theorems 4.3, 5.7 and examples 3.2, 3.3 show that there seems to exist some
668: connections between the limit of Horn logic programs and the stability of
669: fixed points for Horn logic programs. As mentioned above, a stable fixed
670: point is one where a small perturbation will not grow but remain close to
671: the fixed point even after an infinite number of iterations. So from this
672: point of view we can understand that if the least Herbrand model of a Horn
673: logic program is a stable fixed point, then this model may be approached by
674: a sequence of least Herbrand models.
675:
676: \bigskip
677:
678: \noindent {\bf 6. Conclusion}
679:
680: \smallskip
681:
682: Assume that the base $L$ contains infinitely many constant symbols, function
683: symbols and finitely many predicate symbols. Given a sequence $\{\Pi _{n}\}$
684: of Horn logic programs, suppose that the limit $\Pi $ of $\{\Pi _{n}\}$
685: exists, we studied if the least Herbrand model of $\Pi $ is equal to the
686: limit of the least Herbrand models of each $\Pi _{n}$. It was shown by some
687: examples that in general, this property is not true. Further studies proved
688: that the property holds if Horn logic programs satisfy an assumption that can be syntactically
689: checked and easily satisfied. This
690: result implies that for an infinite Horn logic program satisfying the
691: assumption, the least Herbrand model of this program can be approached by a
692: sequence of least Herbrand models of finite programs. We also discussed the
693: decidability of least Herbrand models for Horn logic programs satisfying the
694: assumption. It is proved that the least Herbrand models of these programs
695: are recursive. More interestingly, using the concept of stability from
696: dynamical systems, we proved that the assumption is exactly a sufficient
697: condition to ensure the stability of fixed points for Horn logic programs.
698: Finally, we hope that more general conditions could be found for the property to hold
699: and the main ideas and results of this paper could be
700: extended to more general logic programs in the future.
701:
702: \bigskip
703:
704: \noindent{\bf References:}
705:
706: \begin{description}
707: \item \lbrack 1] Apt, K., Logic Programming, in J. Leeuwen (eds.), {\it %
708: Handbook of Theoretical Computer Science}, Elsevier Science, 1990, Chapter
709: 10.
710:
711: \item {[2]} Dahr, M., {\it Deductive Databases: Theory and Applications},
712: International Thomson Computer Press, 1997.
713:
714: \item \lbrack 3] Drazin, P. G., {\it Nonlinear Systems, }Cambridge
715: University Press, 1992.
716:
717: \item \lbrack 4] Fitting M., Metric methods, Three examples and a Theorem,
718: {\it J. of Logic Programming}, 21(1994):113-127.
719:
720: \item {[5]} Li, W., An Open Logic System, {\it Science in China} (Scientia
721: Sinica) (series A), 10(1992)(in Chinese), 1103-1113.
722:
723: \item {[6]} Li, W., A Logical Framework for Evolution of Specifications, in:
724: {\it Programming Languages and Systems,}\ (ESOP'94), LNCS 788,
725: Sringer-Verlag, 1994, 394-408.
726:
727: \item {[7]} Li, W., A logical Framework for Inductive Inference and Its
728: rationality, in N. Fu (eds.), {\it Advanced Topics in Artificial
729: Intelligence,} LNAI 1747, Springer, 1999.
730:
731: \item \lbrack 8] Nienhuys-Cheng, S. H., Distance between Herbrand Interpretations:
732: A Measure for Approximations to a Target Concept, in: {\it Proc. of the 7th International
733: Workshop on Inductive Logic Programming}, LNAI 1297, Springer, 1997,
734: 213-226.
735:
736: \item {[9]} Nienhuys-Cheng, S. H., Distances and Limits on Herbrand
737: Interpretations, in: {\it Proc. of the 8th International Workshop on Inductive
738: Programming}, LNAI 1446, Springer, 1998, 250-260.
739:
740: \item {[10]} van Emden, M. H. and Kowalski, R. A., The Semantics of
741: Predicate Logic as a Programming Language, {\it J. Association for Computing
742: Machinary} 23(4)(1976), 733-742.
743: \end{description}
744:
745: \end{document}
746: