A Logical Framework for Convergent Infinite Computations (HTML Version)

A Logical Framework for Convergent Infinite Computations ¹

Wei Li², Shilong Ma^,2, Yuefei Sui³, and Ke Xu^,2

Department of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100083, CHINA
Institute of Computing Technology, Chinese Academy of Sciences
Beijing 100080, CHINA

Abstract: Classical computations can not capture the essence of infinite computations very well. This paper will focus on a class of infinite computations called convergent infinite computations. A logic for convergent infinite computations is proposed by extending first order theories using Cauchy sequences, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite-length terms defined by Cauchy sequences. We will show that the limit of sequence of first order theories can be defined in terms of distance, similar to the e-N style definition of limits in real analysis. On the basis of infinitary terms, a computation model for convergent infinite computations is proposed. Finally, the interpretations of logic programs are extended by introducing real Herbrand models of logic programs and a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation is given.

Keywords: Infinite Computation, Distance, Limit, Convergent infinite computation.

1.Introduction

The need of studying infinite computations has been emphasized in recent years, e.g., see (Vardi and Wolper, 1994). By infinite computations, one means the computations done by some programs that create non-terminating processes or very long time running processes. For such programs, the computations done by them usually go through infinite sequences of running states (or configurations), unlike finite computations in which only finite sequences of running states are involved.

Furthermore, over computer networks there is a very large family of computations which are carried out very long time (approximately treated as infinite time) and need constantly to interact with other processes and access some huge sets of external data over networks (approximately treated as infinite sets of data). For example, various procedures for knowledge discovery from databases over Internet do such computations.

1.1. Convergent infinite computations
In the above-mentioned family, there is a large class of infinite computations that have the following characteristics: (1) They constantly access some huge sets of external data during the run time, and (2) the infinite sequences of running states, which they go through, are convergent to some certain limits as the time goes to the infinity. Such computations will be called convergent infinite computations in this paper.

In the following, we will focus on convergent infinite computations, and establish a logical framework for them. This requires us to study the computational behaviors from the point of view of analyzing long time changes, because such computations depend fundamentally on the nature of the long time changes and classical computations may not capture their essence well.

As well known, a computation can be expressed by a first order theory. We will give a framework for convergent infinite computations by expressing infinite computations with sequences of first order theories. Our approach is based on the study of the sequences of first order theories and their limits (Li, 1992). The problems of infinite computations are reduced to that of sequences of first order theories and their limits. The concept of limit of a sequence of first order theories in (Li, 1992), different from the previous concepts of the limit involved in computer science and mathematical logic, is used to characterize that some theory is infinitely approached but maybe never is reached.

We will discuss a class of ideal long time changes, i.e., long time changes with some continuous" nature, by extending first order theories and domains using Cauchy sequences. The extension is similar to that of rational numbers to real numbers. We will show that the semantic interpretations of first order theories are enriched by extending domains using Cauchy sequences. In addition, we show that the limit of sequence of first order theories can be defined in terms of distance, similar to the e-N style definition of limits in real analysis.

In sections 2,3 and 4, based on the study on sequences of first order theories and their limits, a logic for convergent infinite computations is proposed by extending first order theories using Cauchy sequences, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite length terms defined by Cauchy sequences. Furthermore, we study the relations between the convergence of theory sequences and the convergence of model sequences to characterize the limits of formal theory sequences from both proof-theoretical and model-theoretical approaches. We give a formal computation model on the infinitary terms in section 5. Finally, the interpretations of logic programs are extended by introducing real Herbrand models of logic programs and a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation is given.

1.2. Comparison with related work

Notation Our notation is standard. The notation in deductive databases follows from Dahr (1997). We use G to denote theories or logic programs, and r to denote the distances between terms, formulas, theories and logic programs. We use w to denote the set of all the natural numbers, i,j,k,m,n to denote the natural numbers, f,g,h to denote functions, p,q to denote predicates, and t,r,s to denote terms, x,y,z to denote variables, j,y to denote the formulas, and R to denote the relations as in relational databases.

2. The Cauchy sequences of terms.

We pay attention to not only the convergent infinite computations which runs in a long run, but also the possible outputs of such computations. To research such outputs of convergent infinite computations, we should have a way to represent such outputs.

In description logic, a recursive definition such as X=f(X) may have many solutions, where f is a monotonic operator. By Tarski's theorem, there is a unique least fixed solution A₀ and a unique greatest fixed solution A₁ to the definition. What kinds of description logical properties A₀ should have is a very interesting problem in description logic.

In mathematical analysis, given a continuous function f and a real number x, we cannot compute f(x) directly. Instead, we can approximate f(x) by computing f(x) for some rational number x close enough to x. f(x) can be taken as a result of infinite computations (f(x₁),f(x₂),...,f(x_k),...), where the distance between x and x_k is less than 1/k.

In the following two sections we shall give a logic framework for the convergent infinite computations based on the distance defined on the terms of a language. In this section we shall give the distance on the terms of a language which is basically equivalent to the distance defined on trees. By the defined distance, we extend finite terms to infinitary terms. Such extension is similar to the extension of rational numbers to real numbers, but there are some differences between the two extensions. In the next section we shall give a logic for the infinitary terms.

Before giving the definition of the infinite terms, we first define a distance on the terms of some language.

Let L be a language consisting of constant symbols, variable symbols, predicate symbols and function symbols; the logic connectives: , , $. We shall use c,d,... to denote the constant symbols, x,y,z,... to denote the variable symbols, f,g,h,... the function symbols and p,q,... the predicate symbol.

A string t of symbols in L is a term if

(i) t is a constant symbol c, or

(ii) t is a variable symbol x, or

(iii) t is f(t₁,...,t_n), where f is an n-ary function and t₁,...,t_n are terms.

We call the terms as the finitary terms, denote the set of all the finitary terms by FT_L (we usually omit L when no confusion occurs).

We define a distance on FT. Nienhuys-Cheng (Nienhuys-Cheng, 1997) proposed a distance on terms and formulas. Here, we give a ramified definition of a distance on FT.

Definition 2.1. Let f and g be an n-ary and an n-ary function symbols, respectively. The distance r: FT × FT ® {1/m| mÎ w} is defined as follows.

(i) r(t, t)=0, for any t Î FT.

(ii) If f ¹ g, then r(f(t₁,...,t_n), g(t₁,..., t_n))=1.

(iii) r(f(t₁,..., t_n), f(t₁,...,t_n))=max{r(t_i, t_i)| 1£ i£ n}/max{r(t_i, t_i)| 1£ i£ n}+1.

Definition 2.2. Let t={t_k | k Î w} be an infinite sequence of terms. If for any number m>0, there exists an integer K >0 such that r(t_k, t_j)< 1/m for any k,j ³ K, then t is called a Cauchy term sequence, or simply, a Cauchy sequence, an infinitary term, denoted by t=lim_k®
¥ t_k. Let IT_L, simply IT, be the set of all the Cauchy term sequence in L.

Remark. In what follows, we still use t={t_k | k Î w} to denote a Cauchy sequence t=lim_{k® ¥} t_k when no confusion occurs.

The definition of the distance on terms and formulas is a little different from the one given by Nienhuys-Cheng in that the value which the distance can take has a simple form 1/m for some natural number. Such a distance is used to define the distance between two trees in graph theory. Every term t can be taken as a tree T_t. For example, t=f(t₁,...,t_n), the tree T_t has a root with symbol f and n -many children T_t₁,...,T_{t_n}. We say that two terms t and t are the same to depth m if T_t and T_t are the same to depth m. The distance defined here have the basic properties that the distance defined by Nienhuys-Cheng has. In the following, we give some facts stated as propositions without proofs, since they can be proved easily.

Proposition 2.3. (i) t and t are the same to depth m if and only if r(t,t)£ 1/m.

(ii) Given t with depth m, {t| r(t, t)<1/m }={t}.

Remark. Different from rational numbers, the set of all the finite terms is not dense, but the set of all the infinite terms is dense. This fact is stated by the above proposition. It follows from the proposition that for any term tÎ FT, there is a number m such that for any term t, either t=t or r(t,t)>1/m. Therefore, FT È IT is not connective. This is one of the differences from the extension of rational numbers to real numbers.

Note that given two Cauchy term sequences t={t_k | k Î w} and t={t_k | k Î w}, then {r(t_k,t_k) | k Î w} is a Cauchy sequence of rational numbers, so lim_{k® ¥}r(t_k, t_k) exists.

Definition 2.4. Given two Cauchy term sequences t={t_k | k Î w} and t={t_k | k Î w}, we define the distance r(t,t)=lim_{k® ¥} r(t_k, t_k). t and t are equivalent, denoted by tº t, if r(t,t)=0.

Proposition 2.5. º is an equivalence relation on FTÈ IT.

Proposition 2.6. For any set AÍ FT and infinitary term tÎ IT, if for any number m there is a term tÎ A with r(t,t)£ 1/m then there is a Cauchy term sequence tÍ A such that tº t.

We define the substitutions as in the first order logic.

Proposition 2.7. Given a finite term t(x), let Q₁={x/r₁}, Q₂={x/r₂} be any two substitutions. Let m be the least such that x occurs in the depth m of t, then

r(t(x)Q₁, t(x)Q₂)=

r(r₁,r₂)

Therefore, given any finitary term t, {tQ_k} is a Cauchy sequence if and only if {Q_k} is a Cauchy sequence, where {Q_k} is a Cauchy sequence if {y_k} is a Cauchy sequence and Q_k={x/y_k} for every k.

Notice that for some infinitary term t(x), t(r)º t(r) for any terms r and r. For example, given an infinitary term t(x)={t_k(x) | k Î w} with one variable such that m_k tends to infinity, as k tends to infinity, where m_k is the least depth at which x occurs in t_k, e.g., t_k(x)=f^k(x) for some function symbol f, then r(t(r),t(r))=0 for any terms r and r. In another words, when t is some infinitary term satisfying certain conditions then substituting any terms results in equivalent terms.

3. A logic system L_IT for the infinitary terms

Given a language L, let FT and IT be the sets defined as in the last section. We use L to denote the first order logic on L. We assume two basic axioms on syntax:

(3.1) The classes of variables, function symbols, predicate symbols, constant symbols are all disjoint.

(3.2) The different variables are not equal.

An atomic formula of L_IT is in one of the following forms:
(3.3) t₁º t₂, where t₁,t₂Î TERM.
(3.4) p(t₁,...,t_n), where p is an n-ary predicate symbol and t₁,...,t_nÎ TERM.

The formulas of L_IT are defined as in the first order logic. We assume that the axioms and the rules of inference of L_IT are those in the first order logic.

The interpretations of L_IT is defined on a structure N which is constructed from a pre-structure M, and M is a universe of an interpretation of L.

A pre-structure M for L_IT is a pair M=< M,hñ such that M is a nonempty set; h is a function with dom(h)Í L; h(c) Î M; h(f): Mⁿ® M if f is an n -ary function symbol; and h(p)Í Mⁿ if p is an n-ary predicate symbol.

An assignment in M is a function s such that if x is a variable symbol then s(x) Î M. Given an assignment s and a finitary term t, we can define s(t) inductively: if t=c then s(t)=h(c); if t=x then s(t)=s(x); and if t=f(t₁,...,t_n) then s(t)=h(f)(s(t₁),...,s(t_n)).

Just as extending the rational numbers to the real numbers, we extend a pre-structure M to a structure N=á N,hñ, where

where s is an assignment and ~ is an equivalence relation on N defined as follows: Let a={a_k}, and a_k=s(t_k) for every k, and t={t_k}, we denote a=s(t). Given any two a={a_k} and b={b_k}, a~ b if there are t, tÎ IT and an assignment s such that tº t, a=s(t) and b=s(t). We call N an algebraically closed extension of M.

For any n-ary predicate symbol p, h(p)Í Nⁿ such that h(p)Ç Mⁿ=h(p). For any n-ary function symbol f, h(f)é Mⁿ=h(f), and for any a₁,...,a_nÎ N, h(f)(a₁, ...,a_n)={h(f)(a_1k,...,a_nk): kÎ w}.

We interpret the terms and formulas in N as in the classical first order logic. Given an assignment s and a term t, we can define s(t) inductively: if t is finitary then s(t) is defined as above; if t=f(t₁,...,t_n) and t₁={t_1k},...,t_n={t_nk} Î TERM then s(t)={s(f(t_1k,...,t_nk)): kÎ w}.

The truth value of a formula j under an assignment s is defined inductively. j is true in N under an assignment s, denoted by á N,sñ|= j, if

(3.5) s(t₁)~ s(t₂) if j=t₁º t₂,
(3.6) (s(t₁),...,s(t_n))Î h(p) if j=p(t₁,...,t_n),
(3.7) á N,sñ ¬ |=y if j= y,
(3.8) á N,sñ|= y and á N,sñ|= q if j= y q,
(3.9) there is an aÎ N such that á N,sñ|= y(a) if j= $ xy(x).

A sentence j is satisfied in N, denoted by N|= j, if á N,sñ|= j for any assignment s. Given a set G of sentences in L_IT, N is a model of G if for every jÎ G, N|= j.

Proposition 3.1. (1) L_IT has stronger expressive power than the first order logic.
(2) L_IT is complete and compact.
Proof. (1) Let L be the language consisting of one function symbol f and one constant symbol c. The fixed point of a function f, which cannot be expressed in the first order logic, can be expressed in L_IT by t={f^k(a)| kÎ w}, and f(t)=t, where f¹(a)=f(a), f^k+1(a)=f(f^k(a)).

(2) Just by the completeness and compactness of first order logic, we have that L_IT is complete and compact.

Remarks: (1) The fixed point is expressed actually by infinitly many terms. The main point is that we can state some properties about the infinitary terms, just as extending the rational numbers to the real numbers in analysis.

(2) There is some research on the infinitary terms, e.g., Jaffar(1984) and Tulipani (1994). Those studies focus on the algebraically structural or discrete properties of the infinitary terms. Instead, we take the whole finite or infinite terms as a continuum and focus on their continuous and analytic properties.

4. The continuity of predicates and functions

The continuous function is a very important notion in mathematical analysis. By the definition of the assignments, the predicate symbols and function symbols under the interpretation have some continuous properties. We shall give a formal definition of the continuity of the predicate and function symbols in syntax and semantics.

Given an n-ary function symbol f, f is syntactically-continuous at t=(t₁,...,t_n) if lim_{k® ¥} r_k=t implies lim_{k® ¥} f(r_k)=f(t). f is syntactically-continuous if f is syntactically-continuous at every t. By the definition of the distance, we have the following

Proposition 4.1. Every function symbol f is syntactically-continuous.

Given an n-ary predicate symbol p, p is syntactically-continuous at t=(t₁,...,t_n) if there is a number m such that for any finitary term tuple r=(r₁,...,r_n), r(r,t)<1/m implies p(r)=p(t).

We now define the continuity in semantics. Given a pre-structure M, let N=á N,hñ be its algebraically closed extension. Let p be an n-ary predicate symbol. h(p) is continuous at (t₁,...,t_n) in N under assignment s if

s(p(t₁,...,t_n))=

lim

k® ¥

s(p(t_1k,...,t_nk)).

h(p) is continuous in N under s if h(p) is continuous at every (t₁,...,t_n) in N under assignment s.

Let f be an n-ary function symbol. h(f) is continuous at (t₁,...,t_n) in N under assignment s if

s(f(t₁,...,t_n))=

lim

k® ¥

s(f(t_1k,...,t_nk)).

h(f) is continuous in N under s if h(f) is continuous at every (t₁,...,t_n) in N under assignment s.

By the definition of the assignment, every h(f) is continuous.

We now focus on the continuity of the predicate symbols and give a logic system L_c which is an extension of L_IT. In L_IT, for any predicate p and infinitary term t, if p(t) is true under some interpretation then there is a rational number d>0 such that for every finitary term s with r (s,t)<d, p(s) is true under the interpretation. We show that such an axiomatized logic L_c is sound and complete.

L_c has the following axioms

(4.1) If p(t) for tÎ TERM then there is a rational number d>0 of form 1/m for some m such that for any rÎ FT, r(r,t)£ d implies p(r).

Given a set G of formulas (theory), a proof of G is a sequence {j₁,...,j_m} of formulas such that for every 1£ i£ m, either j_i is an axiom, or j_iÎ G or deducted from two precedent formulas in the list by the inference rules. A sentence j is a theorem of G, denoted by G|- j, if there is a proof {j₁,...,j_m} of G such that j=j_m.

A sentence j is valid in a structure N, denoted by N|= j, if á N,sñ|= j for any assignment s. We say that j is a logical consequence of G if for every structure N, N|= G implies N|= j.

Theorem 4.2(The Soundness Theorem). Given any formula j and a theory G, if G|- j then G|= j.
It can be verified routinely.

Theorem 4.3(The Completeness Theorem). Given any sentence j, if j |= y then j|- y. Combining the soundness theorem, we have the following

Proof. We firstly prove the following model existence theorem. A theory is consistent if G¬ |-^.

Claim 4.4. If G is consistent then G has a model.
The proof of the Claim. Let G₀={s: G|- s} be a theory given by G. Any model of G₀ is a model of G.

Let G be a conservative extension of G₀ defined as in the first order logic, with language L such that for every sentence sº $ xj(x) there is a constant c_sÎ L- L and an axiom $ xj(x)® j(c_s) such that distinct s's yield distinct c_s's. Then G is a conservative extension of G₀.

Considering axiom 4.1, we prove that for any predicate p and infinitary term t, if G|- p(t) then there is a rational number d of form 1/m such that for any finitary term r with r(r,t)<d, GÈ {p(r)} is consistent. For the contradiction, assume that G|- p(t) and for any m there is a term r_m such that r(t,r_m)<1/m and G|- p(r_m). There are two cases:

Case 4.1. t does not contain any cÎ L- L. Since G|- p(t), there is a finite set FÈ Y of sentences such that F Í G and every sentence sÎ Y has the form $ xj(x) ® j(c) for some cÎ L- L. Without loss of generality, assume that Y={s}. Then

F, s|- p(t);

F|- s® p(t);

F|- ($ xj(x)® j(y))® p(t);

F|- " y[($ j(x)® j(y))® p(t)];

F|- ($ xj(x)® $ yj(y))® p(t);

F|- p(t),

where y is a variable that does not occur in p(t) and F. Similarly, for any m, there is a set F_mÈ Y_m of sentences such that F_mÍ G, Y_mÇ G=Ø and F_mÈ Y_m|- p(r_m). If r_m does not contain cÎ L- L then by the same discussion as above, G|- p(r_m). If r_m does contain some cÎ L- L then

F, s_m|- p(r_m);

F|- s_m® p(r_m);

either F|- $ x j(x)® p(r_m) or F|- j(c)® p(r_m).

The latter case is reduced to the former case, since j(c)Î G only if $ xj(x)Î G. Hence, G |- p(r_m). Since c does not occur in G, hence, there is an r_mÎ TERM_L such that G|- p(r_m) and r_mº r_m.

Case 4.2. t does contain a constant symbol cÎ L- L. The discussion is the same as the second part of case 4.1.

Combining the above discussion, we have that G|- p(t) and there is a sequence {r_m} or {r_m} of finitary terms in L such that for every m, r(r_m,t)<1/m and G|- p(r_m). So G is inconsistent, a contradiction.

At this moment, we extend G to G such that for every predicate p and infinitary term tÎ TERM_L, if G|- p(t) then find the least d, and enumerate p(r) in G for any rÎ TERM_L with r(r,t)<d. By the above discussion, G is consistent. Then construct the maximal consistent extension of G into G.

By the maximum of G, we know that for any n-ary predicate symbol p and terms t₁,...,t_n, either p(t₁,...,t_n)Î G or p(t₁,...,t_n)Î G.

We construct a pre-model M as follows: let M={tÎ L: t is closed}, and for every function symbol f we define a function

(t₁,...,t_n)Î h(p) Þ G

|- p(t₁,...,t_n);

and for every constant symbol c we define h(c)=c.

We define an equivalence relation ~ on M such that for any t,sÎ M,

By the maximum of G, we can prove that ~ is an equivalence relation on M, and satisfies the following claim: t_i~ s_i for every 1£ i£ n imply h(p)(t₁,...,t_n)Û h(p)(s₁,...,s_n), and h(f)(t₁,...,t_n)~ h(f)(s₁,...,s_n). Hence, ~ is a congruence with respect to the basic relations and functions.

We define another structure N= M/~. We shall use [t] to denote the equivalence class containing t. By the induction on t we can prove that i) if tº c then [t]=[c]; and ii) if t=f(t₁,...,t_n) then [t]=h(f)([t₁],...,[t_n]).

It is routine to show that for any sentence jÎ G, N|= j if and only if G|- j.

Remarks 4.5. (i) Given any infinitary t, if there is a d>0 such that for every finitary s, d(s,t)<d implies p(s), it is possible that p(t). (ii) Given any infinitary term t, if p(t) then it is possible that for any d>0, there is an term s such that r(s,t)<d and p(s). That is, we do not require that for every infinitary term t, if p(t) then there is a d>0 such that for any (finitary or infinitary) term s, r(s,t)<d implies p(s).

5. A computation model on the infinitary terms

Corresponding to the logic L_IT, we give a formal computation model on the infinitary terms.
We shall use {e} for natural number e to denote the e-th Turing machine, and {e}^A to denote the e-th Turing machine with oracle A. Here, {e} can be taken as a function defined on the finitary terms of a language L. Not every Turing computable function on FT induces a function on TERM. We shall use j to denote a Turing computable function from FT to FT such that j is continuous, i.e., for any Cauchy term sequences t and s, tº s implies that {j(t_n): nÎ w} º {j(s_n): nÎ w}.
Definition 5.1. A function f:TERM® TERM is computable if there is a Turing computable and continuous function j :FT® FT such that for every tÎ TERM,

f(t)=

ì
í
î

{j (t_n):nÎ w }	if {j(t_n): nÎ w} is a Cauchy term sequence
undefined	otherwise,

where tº {t_n:nÎ w }.

Such defined computable functions on TERM are not equivalent to the partial recursive operators from 2^w to 2^w. We know that an operator E: 2^w® 2^w is partially recursive if there is a Turing machine {e} such that for any a Î 2^w,

for every nÎ w.

A computable function f on TERM is equivalent to the partially computable operator E, since for any aÎ 2^w,

where aé n is a restriction of a up to n, and we take every infinitary term as a function from w to FT.

Hence, the computable functions on TERM are something between partially computable functions (Turing computable functions) and partially computable operators. Namely,

Theorem 5.2. There is a computable function on TERM which is not a partially computable function. And every computable function on TERM is a partially computable operator.

Generally, we can define computable functions on any continuous (and algebraically closed) ring R in a similar way.

A ring R is continuous if there is a subset Q of R such that R is the algebraical closure of Q and Q is countable and metric. By the definition of the Cauchy sequences on Q, we assume that the definition of the Cauchy sequences on Q can be extended to the Cauchy sequences on R such that every Cauchy sequence of R is equal to some element x in R, and every Cauchy sequence on R has an equivalent Cauchy sequence on Q. We can define Turing computable functions on Q as usual. Not every Turing computable functions on Q can induce a function on R. We shall use j: Q® Q to denote a continuous function, i.e., for any two Cauchy sequences x and y on Q, xº y implies {j(x_n): nÎ w} º {j(y_n): nÎ w} if x={x_nÎ Q: nÎ w} and y={y_nÎ Q: nÎ w}.

Definition 5.3. A function f:R® R is computable if there is a Turing computable and continuous function j on Q such that for any xÎ R,

f(x)=

ì
í
î

{j (x_n):nÎ w }	if {j (x_n):nÎ w } is a Cauchy term sequence
undefined	otherwise,

where xº {x_n:nÎ w }.

For example, Let Q be the set of the rational numbers. Then R is the set of the real numbers. For any xÎ R, function

f(x)=e^x=1+x+

x²

x³

+··· +

xⁿ

+···

j(n,x

ì
ï
í
ï
î

if n=0

j(n-1,x

otherwise

is computable, since j(n,x) can be defined recursively by the recursive function g(n,y,x)=y+xⁿ/n!, where yÎ Q. Hence, for any real number x, f(x)=y, where y={y_n: nÎ w}, and y_n=j(n, x_n).

Both definitions of the computable functions on any continuous ring R are different from the BSS definition. In fact, both the definitions make taking limits as the computable processes, since j(x)=lim_{n® ¥} f(n,xé n). Namely,

Theorem 5.4. There is a computable function f on TERM or any continuous ring R which is not BSS-computable.

Chadzelek and Hotz(1999) defined the analytic machines which are defined on the real numbers and the rational numbers, and in which the infinite computations are allowed. The computable functions defined here is different from the analytic machines in the following point: a computable function defined by an analytic machine produces an infinite sequence of outputs after input; and the computable functions defined here produce infinite sequences of outputs only after infinite sequence of inputs, and for every input, the computation terminates.

6. The real Herbrand model of Horn logic programs

In this section, we will extend the Herbrand base (universe) to the real Herbrand base (universe) in which infinitary terms can occur, and extend the interpretations of the logic programs by introducing real Herbrand models of logic programs. Then, we will give a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation.

Definition 6.1. A Cauchy term sequence is called a real Herbrand term, and p(t₁,...,t_n) for t₁,...,t_nÎ TERM is called a real atom, where p is an n-ary predicate symbol. Define

RHU=IT,

RHB={p(t₁,...,t_n)| p is an n-predicate symbol, t₁,...,t_nÎ RHU}.

RHU and RHB are called a real Herbrand universe and a real Herbrand base, respectively.

Definition 6.2. (Real Herbrand interpretation and real Herbrand model) I Í RHB is called a real Herbrand interpretation, and M is called a real Herbrand model of a first order theory G if it is a real Herbrand interpretation under which all sentences of the theory G are true.

Example 6.3. Let a be a constant symbol, f a unary function symbol, E(x, y): x=y and G={$ x E(x, f(x))}, then G has no Herbrand model. But, G has a real Herbrand model {E( b, f( b))} over RHU, where b is the infinitary term {f^k(a) | k Î w}.

There are many interesting properties for real Herbrand models of first order theories. But here, we will focus on Horn logic programs, not general first order theories. We will show how to compute a real Herbrand model of some Horn logic programs using convergent infinite computation.

In the following, we recall the basic definitions in logic programming. A literal is an atom or the negation of an atom. An atom is called a positive literal whereas a negated atom is called a negative literal. A clause q ¬ q₁,...,q_m is called a rule; is called a fact, if m=0; and a goal, if q is empty. We shall use g to denote a clause. q is called the rule head, denoted by head(g) and q₁,...,q_m is called the rule body, denoted by body(g). A logic program, denoted by G, is a set of clauses. G may contain infinitely many clauses. A clause g is Horn if g has at most one positive literal. A logic program is Horn if every its clause is Horn.

Definition 6.4. A real Herbrand interpretation of a logic program G is any subset I of the real Herbrand base IÍ RHB. Given a logic program G, a real Herbrand interpretation I is a real Herbrand model of G if for any substitution Q and a clause g, body(g)Q Í I implies head(g)Q Î I.

Example 6.5. Suppose that there are one function symbol f, one predicate symbol p and one constant symbol a in L. We denote the infinitary term {f^k(a) | k Î w} by f^¥(a). Consider the logic program G={p(f(x))¬ p(x)}. Then, G has a real Herbrand model {p(f^¥(a))}.

Let G be a Horn program and define a mapping f_G: 2^RHB® 2^RHB by

(A)={head(g)Q| gÎ G, body(g)Q Í A},

where Q is any substitution.

Proposition 6.6. (van Emden and Kowalski) If G is a Horn program then f_G is monotonic and finitary. Moreover, f_G^w is the least real Herbrand model of G, where f_G^w is the least fixpoint of f_G: f_G⁰=Ø, f_G¹=f_G(Ø),..., f_Gⁿ⁺¹=f_G(f_Gⁿ),...

We define a sequence of models {M_k} convergent if {M_k} is a Cauchy sequence, namely, for any number m>0, there is a K such that for any j,k³ K, r(M_k,M_j)<1/m. We say that M is the limit of a Cauchy sequence {M_k}, denoted by M=lim_k®¥M_k, if M={pÎ RHB| $ {p_k}=p" k(p_kÎ M_k)}.

Lemma 6.7. Given a Cauchy sequence {M_k} of structures, if M=lim_{k® ¥} M_k then lim_{k® ¥} r(M_k,M)=0.

In 1992, Li defined the limit of first order theory sequences in a set-theoretic way(Li, 1992). For Horn logic programs, we can defined such limits.

Definition 6.8. Given a sequence {G_k} of Horn logic programs, we say that

lim

k® ¥

G_k=

i=1

j=i

G_j

lim

k® ¥

G_k=

i=1

j=i

G_j

is the upper limit of {G_k}. If lim_{k® ¥} G_k =lim_{k® ¥} G_n then we say that the (set-theoretic) limit of {G_k} exists (or {G_k} is convergent) and denote it by LIM_k® ¥ G_k.

Obviously, if G=LIM_k® ¥ G_k exists, then G is still a Horn logic program (possibly, an infinite length Horn logic program).

Problem: We concern the following problem: Given a sequence of Horn logic programs G₁, G₂, ···, G_k, ···, G=LIM_k®¥G_k exists. Let M_k be the least model of G_k for k=1, 2, ···. The problem is if M=lim_{k® ¥} M_k exists and is a real Herbrand model of G=LIM_k®¥ G_k?

The above problem does not have solutions for all sequences of Horn logic programs. To solve it we have to put some conditions on Horn logic programs. We assume that

Assumption 6.9. Given a Horn logic program P , assume that every clause p :p¬ p₁,··· ,p_m in P has the following property: for every i if t is a term in p_i, then t is also in p.

By Assumption 6.9, we would like to establish some sufficient condition for the above problem. We first give a fact that can be proved easily.

Given such a clause g satisfying assumption 6.9, by Proposition 2.7, we have the following

Proposition 6.10. Given any clause g and two substitutions Q₁,Q₂, we have that

Corollary 6.11. Given an sequence {Q_n} of substitutions and a formula g, if {body(g)Q_n} is a Cauchy sequence then {head(g)Q_n} is a Cauchy sequence.

Remark: Let j: body(g)|® head(g), the above proposition can be rewritten as

where m is a constant. Here for our proposition m is taken to be 1.

Theorem 6.12. Given a convergent sequence {G_k} of Horn logic programs. Let M_k be the least real Herbrand model of G_k for every k. Then {M_k} is a Cauchy sequence. Moreover, let G=LIM_k®¥ G_k and M=lim_k®¥ M_k, then M is a real Herbrand model of G.

Proof. We prove that M is a real Herbrand model of G, that is, given any clause gÎ G and substitution Q such that body(g)QÎ M, then head(g)QÎ M.

If g is a fact of G then there is a K such that for any k³ K, gÎ G_k and q=gÎ M_k. Hence, there is a Cauchy sequence q_k such that q_kÎ M_k and q=lim_{k® ¥} q_k.

If gÎ G is not a fact then, without loss of generality, let q'=body(g)Q Î M. Then there is a Cauchy seqence {q'_k} and a K such that q'_kÎ M_k, g=g_k for any k³ K and q'=lim_{k® ¥} q'_k. There is a Cauchy sequence {Q_k} of substitutions such that q'_k=body(g_k)Q_k for every k. Hence, {head(g_k)Q_k} is a Cauchy sequence, and head(g_k)Q_kÎ M_k for every k, and head(g)Q=lim_{k® ¥} head(g_k)Q_k Î M.

Given any q in the least real Herbrand model of G, we want to show that there is a Cauchy sequence {q_k} such that q_kÎ M_k for sufficiently large k and q=lim_{k® ¥} q_k. Let M' be the least real Herbrand model of G. We prove the claim by induction on n, the step at which q enters M'. The proof is similar to the discussion given above.

Example 6.13. Assume that there are one function symbol f, one predicate symbol p and one constant symbol a in L. We denote the infinitary term {f^k(a) | k Î w} by f^¥(a).

Let {G_k} be as follows:

G₁	={p(f(x))¬ p(x),p(f(a))},
G ₂	={p(f(x))¬ p(x),p(f²(a))},
	···
G_k	={p(f(x))¬ p(x),p(f^k(a))},
· · ·

M₁=f

G₁

={p(f(a)),p(f²(a)),··· ,p(fⁿ(a)),··· },

M₂=f

G₂

={p(f²(a)),p(f³(a)),··· ,p(fⁿ(a)),··· },

···

M_k=f

G_k

={p(f^k(a)),p(f^k+1(a)),··· },

·
·
·

Therefore, lim_{k® ¥}M_k |= LIM_k® ¥ G_k. That is, lim_{k® ¥}M_k is a real Herbrand model of LIM_k® ¥ G_k.

7. Conclusions

We focus on a class of infinite computations. First order theories are extended by using Cauchy sequences, and then a logic for convergent infinite computations is proposed, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite-length terms defined by Cauchy sequences. We show that the limit of sequence of first order theories can be defined in terms of distance, similar to the e -N style definition of limits in real analysis. On the basis of infinitary terms, a computation model for convergent infinite computations is proposed. Finally, the interpretations of logic programs are extended by introducing real Herbrand models of logic programs and a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation is given.

References: