A Logical Framework for Convergent Infinite
Computations 1

arXiv:cs/0105020v3 [cs.LO] 7 Feb 2002

†

Wei Li†2 , Shilong Ma†,2 , Yuefei Sui‡3 , 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 ǫ − 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
1

The research is supported by the National 973 Project of China under the grant number
G1999032701 and by the National Science Foundation of China.
2
Email: {liwei, slma, kexu}@nlsde.buaa.edu.cn.
3
Email: suiyyff@sina.com.

1

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 ǫ − 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
1. In the infinitary logic (Vardi and Wolper, 1994) and (Abiteboul, Vardi and
Vianu, 1995) there are formulas of infinite length, but there is no term of
infinite length. We give a logic for the terms of infinite length and discuss
the convergence problem of logical theory sequences. The logic for the terms
of infinite length is different from the infinite logic in expressiveness and logic
properties. For example, being finite can be expressed in the infinite logic, and
2

a fix point of a monotonic function in a complete lattice can be expressed in
the logic for the infinite length terms. The compactness theorem does not hold
in the infinite logic, but does in the logic for the terms of infinite length.
2. In real machines (Blum, Shub and Smale, 1989, 1998) and analytic machines
(Chadzelek and Hotz, 1999), a computation model for real numbers is established to characterize continuous computations. We discuss the computation
problem on the terms of infinite length (strings of infinite length over an infinite
alphabet) to characterize “continuous” symbolic computations.
3. To study the approximation problem of inductive logic programming and machine learning, the distance of Herbrand interpretations is discussed (NienhuysCheng, 1997, 1998). The approximation concept in this paper, similar to the
approximation concept in real analysis, is more general, and is used to characterize that some theory is infinitely approached but may never be reached.
Usually, the approximation sequences are non-monotonic. The semantic interpretations of first order theories are enriched by extending Herbrand universe
to real Herbrand universe using Cauchy sequences.
Notation Our notation is standard. The notation in deductive databases follows
from Dahr (1997). We use Γ to denote theories or logic programs, and ρ to denote
the distances between terms, formulas, theories and logic programs. We use ω 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, ϕ, ψ 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 A0 and a unique greatest fixed solution A1 to the definition.
What kinds of description logical properties A0 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 (x1 ), f (x2 ), ..., f (xk ), ...), where the distance between x and
1
xk is less than .
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
3

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 (t1 , ..., tn ), where f is an n-ary function and t1 , ..., tn are terms.
We call the terms as the finitary terms, denote the set of all the finitary terms by
FTL (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, respec1
| m ∈ ω is defined as follows.
tively. The distance ρ : FT × FT →
m
(i) ρ(t, t) = 0, for any t ∈ FT.
(ii) If f 6= g, then ρ(f (t′1 , ..., t′n′ ), g(t1 , ..., tn )) = 1.
max{ρ(t′i , ti ) | 1 ≤ i ≤ n′ }
(iii) ρ(f (t′1 , ..., t′n′ ), f (t1 , ..., tn′ )) =
.
max{ρ(t′i , ti ) | 1 ≤ i ≤ n′ } + 1
Definition 2.2. Let t = {tk | k ∈ ω} be an infinite sequence of terms. If for
1
for any
any number m > 0, there exists an integer K > 0 such that ρ(tk , tj ) <
m
k, j ≥ K, then t is called a Cauchy term sequence, or simply, a Cauchy sequence,
an infinitary term, denoted by t = lim tk . Let ITL , simply IT, be the set of all the
k→∞

Cauchy term sequence in L.
Remark. In what follows, we still use t = {tk | k ∈ ω} to denote a Cauchy
sequence t = lim tk when no confusion occurs.
k→∞

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
1
a simple form
for some natural number. Such a distance is used to define the
m
distance between two trees in graph theory. Every term t can be taken as a tree
Tt . For example, t = f (t1 , ..., tn ), the tree Tt has a root with symbol f and n-many
children Tt1 , ..., Ttn . We say that two terms t and t′ are the same to depth m if Tt and
Tt′ are the same to depth m. The distance defined here have the basic properties
4

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.
1
Proposition 2.3. (i) t and t′ are the same to depth m if and only if ρ(t, t′ ) ≤ .
m


1
′
′
(ii) Given t with depth m, t | ρ(t, t ) <
= {t}.
m
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
1
is a number m such that for any term t′ , either t′ = t or ρ(t′ , t) > . Therefore,
m
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 ∈ ω} and t = {tk |
k ∈ ω}, then {ρ(tk , t′k ) | k ∈ ω} is a Cauchy sequence of rational numbers, so
lim ρ(tk , t′k ) exists.

k→∞

Definition 2.4. Given two Cauchy term sequences t′ = {t′k | k ∈ ω} and
t = {tk | k ∈ ω}, we define the distance ρ(t, t′ ) = lim ρ(tk , t′k ). t and t′ are equivalent,
k→∞

denoted by t′ ≡ t, if ρ(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
1
then there is a Cauchy term
number m there is a term t′ ∈ A with ρ(t, t′ ) ≤
m
′′
′′
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 Θ1 = {x/r1 }, Θ2 = {x/r2 } be
any two substitutions. Let m be the least such that x occurs in the depth m of t,
then
1
.
ρ(t(x)Θ1 , t(x)Θ2 ) =
1
m+
ρ(r1 , r2 )
Therefore, given any finitary term t, {tΘk } is a Cauchy sequence if and only if {Θk }
is a Cauchy sequence, where {Θk } is a Cauchy sequence if {yk } is a Cauchy sequence
and Θk = {x/yk } 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) = {tk (x) | k ∈ ω} with one variable such that
mk tends to infinity, as k tends to infinity, where mk is the least depth at which x
occurs in tk , e.g., tk (x) = f k (x) for some function symbol f , then ρ(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 LIT for the infinitary terms
5

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 LIT is in one of the following forms:
(3.3) t1 ≡ t2 , where t1 , t2 ∈ TERM.
(3.4) p(t1 , ..., tn ), where p is an n-ary predicate symbol and t1 , ..., tn ∈ TERM.
The formulas of LIT are defined as in the first order logic. We assume that the
axioms and the rules of inference of LIT are those in the first order logic.
The interpretations of LIT 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 LIT is a pair M =< M, hi such that M is a nonempty
set; h is a function with dom(h) ⊆ L; h(c) ∈ M ; h(f ) : M n → M if f is an n-ary
function symbol; and h(p) ⊆ M n 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 (t1 , ..., tn ) then
s(t) = h(f )(s(t1 ), ..., s(tn )).
Just as extending the rational numbers to the real numbers, we extend a prestructure M to a structure N = hN, h′ i, where
N = {{ak } : ∃t ∈ IT∃s∀k(ak = s(tk ))}/ ≃,
where s is an assignment and ≃ is an equivalence relation on N defined as follows:
Let a = {ak }, and ak = s(tk ) for every k, and t = {tk }, we denote a = s(t). Given
any two a = {ak } and b = {bk }, 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 n such that h′ (p) ∩ M n = h(p). For
any n-ary function symbol f, h′ (f )⌈M n = h(f ), and for any a1 , ..., an ∈ N, h′ (f )(a1 ,
..., an ) = {h(f )(a1k , ..., ank ) : k ∈ ω}.
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 (t1 , ..., tn ) and t1 = {t1k }, ..., tn = {tnk } ∈ TERM
then s(t) = {s(f (t1k , ..., tnk )) : k ∈ ω}.
The truth value of a formula ϕ under an assignment s is defined inductively. ϕ
is true in N under an assignment s, denoted by hN , si |= ϕ, if
(3.5) s(t1 ) ≃ s(t2 ) if ϕ = t1 ≡ t2 ,
(3.6) (s(t1 ), ..., s(tn )) ∈ h(p) if ϕ = p(t1 , ..., tn ),
(3.7) hN , si 6|= ψ if ϕ = ¬ψ,
(3.8) hN , si |= ψ and hN , si |= θ if ϕ = ψ ∧ θ,
(3.9) there is an a ∈ N such that hN , si |= ψ(a) if ϕ = ∃xψ(x).
6

A sentence ϕ is satisfied in N , denoted by N |= ϕ, if hN , si |= ϕ for any
assignment s. Given a set Γ of sentences in LIT , N is a model of Γ if for every
ϕ ∈ Γ, N |= ϕ.
Proposition 3.1. (1) LIT has stronger expressive power than the first order
logic.
(2) LIT 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 LIT by t = {f k (a) | k ∈ ω}, and f (t) = t,
where f 1 (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
LIT 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 = (t1 , ..., tn )
if lim rk = t implies lim f (rk ) = f (t). f is syntactically-continuous if f is syntacticallyk→∞

k→∞

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 = (t1 , ..., tn )
if there is a number m such that for any finitary term tuple r = (r1 , ..., rn ), ρ(r, t) <
1
implies p(r) = p(t).
m
We now define the continuity in semantics. Given a pre-structure M, let N =
hN, hi be its algebraically closed extension. Let p be an n-ary predicate symbol.
h(p) is continuous at (t1 , ..., tn ) in N under assignment s if
s(p(t1 , ..., tn )) = lim s(p(t1k , ..., tnk )).
k→∞

h(p) is continuous in N under s if h(p) is continuous at every (t1 , ..., tn ) in N under
assignment s.
7

Let f be an n-ary function symbol. h(f ) is continuous at (t1 , ..., tn ) in N under
assignment s if
s(f (t1 , ..., tn )) = lim s(f (t1k , ..., tnk )).
k→∞

h(f ) is continuous in N under s if h(f ) is continuous at every (t1 , ..., tn ) 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
Lc which is an extension of LIT . In LIT , for any predicate p and infinitary term t,
if p(t) is true under some interpretation then there is a rational number δ > 0 such
that for every finitary term s with ρ(s, t) < δ, p(s) is true under the interpretation.
We show that such an axiomatized logic Lc is sound and complete.
Lc has the following axioms
1
for
(4.1) If p(t) for t ∈ TERM then there is a rational number δ > 0 of form
m
some m such that for any r ∈ FT, ρ(r, t) ≤ δ implies p(r).
Given a set Γ of formulas (theory), a proof of Γ is a sequence {ϕ1 , ..., ϕm } of
formulas such that for every 1 ≤ i ≤ m, either ϕi is an axiom, or ϕi ∈ Γ or deducted
from two precedent formulas in the list by the inference rules. A sentence ϕ is a
theorem of Γ, denoted by Γ ⊢ ϕ, if there is a proof {ϕ1 , ..., ϕm } of Γ such that
ϕ = ϕm .
A sentence ϕ is valid in a structure N , denoted by N |= ϕ, if hN , si |= ϕ for
any assignment s. We say that ϕ is a logical consequence of Γ if for every structure
N , N |= Γ implies N |= ϕ.
Theorem 4.2(The Soundness Theorem). Given any formula ϕ and a theory Γ,
if Γ ⊢ ϕ then Γ |= ϕ.
It can be verified routinely.
Theorem 4.3(The Completeness Theorem). Given any sentence ϕ, if ϕ |= ψ
then ϕ ⊢ ψ. Combining the soundness theorem, we have the following
Γ ⊢ ϕ ⇔ Γ |= ϕ.
Proof. We firstly prove the following model existence theorem. A theory is
consistent if Γ 6⊢⊥ .
Claim 4.4. If Γ is consistent then Γ has a model.
The proof of the Claim. Let Γ0 = {σ : Γ ⊢ σ} be a theory given by Γ. Any model
of Γ0 is a model of Γ.
Let Γ′ be a conservative extension of Γ0 defined as in the first order logic, with
language L′ such that for every sentence σ ≡ ∃xϕ(x) there is a constant cσ ∈ L′ − L
and an axiom ∃xϕ(x) → ϕ(cσ ) such that distinct σ’s yield distinct cσ ’s. Then Γ′ is
a conservative extension of Γ0 .
8

Considering axiom 4.1, we prove that for any predicate p and infinitary term t,
1
if Γ′ ⊢ p(t) then there is a rational number δ of form
such that for any finitary
m
′
term r with ρ(r, t) < δ, Γ ∪ {p(r)} is consistent. For the contradiction, assume that
1
and Γ′ ⊢ ¬p(rm ).
Γ′ ⊢ p(t) and for any m there is a term rm such that ρ(t, rm ) <
m
There are two cases:
Case 4.1. t does not contain any c ∈ L′ − L. Since Γ′ ⊢ p(t), there is a finite
set Φ ∪ Ψ of sentences such that Φ ⊆ Γ and every sentence σ ∈ Ψ has the form
∃xϕ(x) → ϕ(c) for some c ∈ L′ −L. Without loss of generality, assume that Ψ = {σ}.
Then
Φ, σ ⊢ p(t);
Φ ⊢ σ → p(t);
Φ ⊢ (∃xϕ(x) → ϕ(y)) → p(t);
Φ ⊢ ∀y[(∃ϕ(x) → ϕ(y)) → p(t)];
Φ ⊢ (∃xϕ(x) → ∃yϕ(y)) → p(t);
Φ ⊢ p(t),
where y is a variable that does not occur in p(t) and Φ. Similarly, for any m, there is
a set Φm ∪ Ψm of sentences such that Φm ⊆ Γ, Ψm ∩ Γ = ∅ and Φm ∪ Ψm ⊢ ¬p(rm ).
If rm does not contain c ∈ L′ − L then by the same discussion as above, Γ ⊢ ¬p(rm ).
If rm does contain some c ∈ L′ − L then
Φ, σm ⊢ ¬p(rm );
Φ ⊢ σm → ¬p(rm );
either Φ ⊢ ∃xϕ(x) → ¬p(rm ) or Φ ⊢ ¬ϕ(c) → ¬p(rm ).
The latter case is reduced to the former case, since ϕ(c) ∈ Γ′ only if ∃xϕ(x) ∈ Γ.
′ ∈ TERM
Hence, Γ ⊢ ¬p(rm ). Since c does not occur in Γ, hence, there is an rm
L
′
′
such that Γ ⊢ ¬p(rm ) and rm ≡ rm .
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 Γ ⊢ p(t) and there is a sequence
′ } of finitary terms in L such that for every m, ρ(r , t) < 1 and
{rm } or {rm
m
m
Γ ⊢ ¬p(rm ). So Γ is inconsistent, a contradiction.
At this moment, we extend Γ′ to Γ′′ such that for every predicate p and infinitary
term t ∈ TERML′ , if Γ′ ⊢ p(t) then find the least δ, and enumerate p(r) in Γ′′ for
any r ∈ TERML′ with ρ(r, t) < δ. By the above discussion, Γ′′ is consistent. Then
construct the maximal consistent extension of Γ′′ into Γ′′′ .
By the maximum of Γ′′′ , we know that for any n-ary predicate symbol p and
terms t1 , ..., tn , either p(t1 , ..., tn ) ∈ Γ′′′ or ¬p(t1 , ..., tn ) ∈ Γ′′′ .
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
h(f )(t1 , ..., tn ) = f (t1 , ..., tk );
9

and for every predicate symbol p, we define a relation
(t1 , ..., tn ) ∈ h(p) ⇒ Γ′′′ ⊢ p(t1 , ..., tn );
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,
t ∼ s ⇔ Γ′′′ ⊢ t ≡ s.
By the maximum of Γ′′′ , we can prove that ∼ is an equivalence relation on M, and
satisfies the following claim: ti ∼ si for every 1 ≤ i ≤ n imply h(p)(t1 , ..., tn ) ⇔
h(p)(s1 , ..., sn ), and h(f )(t1 , ..., tn ) ∼ h(f )(s1 , ..., sn ). 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 (t1 , ..., tn ) then [t] = h(f )([t1 ], ..., [tn ]).
It is routine to show that for any sentence ϕ ∈ Γ′′′ , N |= ϕ if and only if Γ′′′ ⊢ ϕ.
✷
Remarks 4.5. (i) Given any infinitary t, if there is a δ > 0 such that for every
finitary s, d(s, t) < δ 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 δ > 0, there is an term s such that
ρ(s, t) < δ and ¬p(s). That is, we do not require that for every infinitary term t, if
p(t) then there is a δ > 0 such that for any (finitary or infinitary) term s, ρ(s, t) < δ
implies p(s).
5. A computation model on the infinitary terms
Corresponding to the logic LIT , 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
A
{e} 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 ϕ to denote a Turing
computable function from FT to FT such that ϕ is continuous, i.e., for any Cauchy
term sequences t and s, t ≡ s implies that {ϕ(tn ) : n ∈ ω} ≡ {ϕ(sn ) : n ∈ ω}.
Definition 5.1. A function f : TERM → TERM is computable if there is
a Turing computable and continuous function ϕ : FT → FT such that for every
t ∈ TERM,
f (t) =

(

{ϕ(tn ) : n ∈ ω} if {ϕ(tn ) : n ∈ ω} is a Cauchy term sequence
undefined
otherwise,

where t ≡ {tn : n ∈ ω}.
Such defined computable functions on TERM are not equivalent to the partial
recursive operators from 2ω to 2ω . We know that an operator E : 2ω → 2ω is partially
recursive if there is a Turing machine {e} such that for any α ∈ 2ω ,
E(α)(n) = {e}α (n)
10

for every n ∈ ω.
A computable function f on TERM is equivalent to the partially computable
operator E, since for any α ∈ 2ω ,
f (α)(n) = {e}(α⌈n),
where α⌈n is a restriction of α up to n, and we take every infinitary term as a
function from ω 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 ϕ : Q → Q to denote a continuous function, i.e., for any two Cauchy
sequences x and y on Q, x ≡ y implies {ϕ(xn ) : n ∈ ω} ≡ {ϕ(yn ) : n ∈ ω} if
x = {xn ∈ Q : n ∈ ω} and y = {yn ∈ Q : n ∈ ω}.
Definition 5.3. A function f : R → R is computable if there is a Turing
computable and continuous function ϕ on Q such that for any x ∈ R,
f (x) =

(

{ϕ(xn ) : n ∈ ω} if {ϕ(xn ) : n ∈ ω} is a Cauchy term sequence
undefined
otherwise,

where x ≡ {xn : n ∈ ω}.
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) = ex = 1 + x +

xn
x2 x3
+
+ ··· +
+ ···
2!
3!
n!

is a computable function on the real numbers. Because for any n ∈ ω, x′ ∈ Q,
ϕ(n, x′ ) =


 1

if n = 0

′n
 ϕ(n − 1, x′ ) + x
n!

11

otherwise

is computable, since ϕ(n, x′ ) can be defined recursively by the recursive function
x′n
g(n, y ′ , x′ ) = y ′ +
, where y ′ ∈ Q. Hence, for any real number x, f (x) = y, where
n!
y = {yn : n ∈ ω}, and yn = ϕ(n, xn ).
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 ϕ(x) = lim f (n, x⌈n). Namely,
n→∞
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(t1 , ..., tn ) for t1 , ..., tn ∈ TERM is called a real atom, where p is an n-ary predicate
symbol. Define
RHU = IT,
RHB = {p(t1 , ..., tn ) | p is an n-predicate symbol, t1 , ..., tn ∈ 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 Γ if it is a real Herbrand interpretation under which
all sentences of the theory Γ are true.
Example 6.3. Let a be a constant symbol, f a unary function symbol, E(x, y) :
x = y and Γ = {∃xE(x, f (x))}, then Γ has no Herbrand model. But, Γ has a real
Herbrand model {E(b̃, f (b̃))} over RHU , where b̃ is the infinitary term {f k (a) | k ∈
ω}.

12

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 ← q1 , ..., qm is called a rule;
is called a fact, if m = 0; and a goal, if q is empty. We shall use γ to denote a
clause. q is called the rule head, denoted by head(γ) and q1 , ..., qm is called the rule
body, denoted by body(γ). A logic program, denoted by Γ, is a set of clauses. Γ may
contain infinitely many clauses. A clause γ is Horn if γ 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 Γ is any
subset I of the real Herbrand base I ⊆ RHB. Given a logic program Γ, a real
Herbrand interpretation I is a real Herbrand model of Γ if for any substitution Θ
and a clause γ, body(γ)Θ ⊆ I implies head(γ)Θ ∈ 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 ∈ ω} by f ∞ (a). Consider the logic program Γ = {p(f (x)) ← p(x)}. Then, Γ has
a real Herbrand model {p(f ∞ (a))}.
Let Γ be a Horn program and define a mapping fΓ : 2RHB → 2RHB by
fΓ (A) = {head(γ)Θ | γ ∈ Γ, body(γ)Θ ⊆ A},
where Θ is any substitution.
Proposition 6.6. (van Emden and Kowalski) If Γ is a Horn program then fΓ is
monotonic and finitary. Moreover, fΓω is the least real Herbrand model of Γ, where
fΓω is the least fixpoint of fΓ : fΓ0 = ∅, fΓ1 = fΓ (∅), ..., fΓn+1 = fΓ (fΓn ), ...
We define a sequence of models {Mk } convergent if {Mk } is a Cauchy sequence,
namely, for any number m > 0, there is a K such that for any j, k ≥ K, ρ(Mk , Mj ) <
1
. We say that M is the limit of a Cauchy sequence {Mk }, denoted by M = lim Mk ,
k→∞
m
if M = {p ∈ RHB | ∃{pk } = p∀k(pk ∈ Mk )}.
Lemma 6.7. Given a Cauchy sequence {Mk } of structures, if M = lim Mk
k→∞

then lim ρ(Mk , M ) = 0.
k→∞

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 {Γk } of Horn logic programs, we say that
limk→∞ Γk =

∞ \
∞
[

i=1 j=i

13

Γj

is the lower limit of {Γk }, and
limk→∞ Γk =

∞ [
∞
\

Γj

i=1 j=i

is the upper limit of {Γk }. If limk→∞ Γk = limk→∞ Γn then we say that the (settheoretic) limit of {Γk } exists (or {Γk } is convergent) and denote it by LIMk→∞ Γk .
Obviously, if Γ = LIMk→∞ Γk exists, then Γ 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 Γ1 , Γ2 , · · · , Γk , · · ·, Γ = LIMk→∞ Γk exists. Let Mk be the least model of
Γk for k = 1, 2, · · ·. The problem is if M = lim Mk exists and is a real Herbrand
k→∞

model of Γ = LIMk→∞ Γ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 Π, assume that every clause
π : p ← p1 , · · · , pm in Π has the following property: for every i if t is a term in pi ,
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 γ satisfying assumption 6.9, by Proposition 2.7, we have the
following
Proposition 6.10. Given any clause γ and two substitutions Θ1 , Θ2 , we have
that
ρ(head(γ)Θ1 , head(γ)Θ2 ) ≤ ρ(body(γ)Θ1 , body(γ)Θ2 ).
Corollary 6.11. Given an sequence {Θn } of substitutions and a formula γ, if
{body(γ)Θn } is a Cauchy sequence then {head(γ)Θn } is a Cauchy sequence.
Remark: Let ϕ : body(γ) 7→ head(γ), the above proposition can be rewritten as
ρ(ϕ(body(γ))Θ1 , ϕ(body(γ))Θ2 ) ≤ ρ(body(γ)Θ1 , body(γ)Θ2 ),
which is an analogoue to the Lipschitz condition in dynamical systems
ρ(f (x1 ), f (x2 )) ≤ mρ(x1 , x2 ),
where m is a constant. Here for our proposition m is taken to be 1.
Theorem 6.12. Given a convergent sequence {Γk } of Horn logic programs. Let
Mk be the least real Herbrand model of Γk for every k. Then {Mk } is a Cauchy
sequence. Moreover, let Γ = LIMk→∞ Γk and M = lim Mk , then M is a real
k→∞

Herbrand model of Γ.
14

Proof. We prove that M is a real Herbrand model of Γ, that is, given any clause
γ ∈ Γ and substitution Θ such that body(γ)Θ ∈ M, then head(γ)Θ ∈ M.
If γ is a fact of Γ then there is a K such that for any k ≥ K, γ ∈ Γk and q =
γ ∈ Mk . Hence, there is a Cauchy sequence qk such that qk ∈ Mk and q = lim qk .
k→∞

If γ ∈ Γ is not a fact then, without loss of generality, let q ′ = body(γ)Θ ∈ M.
Then there is a Cauchy seqence {qk′ } and a K such that qk′ ∈ Mk , γ = γk for any
k ≥ K and q ′ = lim qk′ . There is a Cauchy sequence {Θk } of substitutions such
k→∞

that qk′ = body(γk )Θk for every k. Hence, {head(γk )Θk } is a Cauchy sequence, and
head(γk )Θk ∈ Mk for every k, and head(γ)Θ = lim head(γk )Θk ∈ M.
k→∞

Given any q in the least real Herbrand model of Γ, we want to show that there is
a Cauchy sequence {qk } such that qk ∈ Mk for sufficiently large k and q = lim qk .
k→∞

Let M ′ be the least real Herbrand model of Γ. 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 ∈ ω} by f ∞ (a).
Let {Γk } be as follows:
Γ1 = {p(f (x)) ← p(x), p(f (a))},
Γ2 = {p(f (x)) ← p(x), p(f 2 (a))},
···
.
k
Γk = {p(f (x)) ← p(x), p(f (a))},
..
.
where f k (a) = f (f k−1 (a)), f 1 (a) = f (a). Then we have
M1 = fΓω1 = {p(f (a)), p(f 2 (a)), · · · , p(f n (a)), · · ·},
M2 = fΓω2 = {p(f 2 (a)), p(f 3 (a)), · · · , p(f n (a)), · · ·},
···
ω
Mk = fΓk = {p(f k (a)), p(f k+1 (a)), · · ·},
..
.
and
M = lim Mk = {p(f ∞ (a))}.
k→∞

Now we have
Γ = LIMk→∞ Γk = {p(f (x)) ← p(x)},
Therefore, lim Mk |= LIMk→∞ Γk . That is, lim Mk is a real Herbrand model of
k→∞

k→∞

LIMk→∞ Γk .

15

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
ǫ − 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:
[1] Abiteboul, S., Vardi, M. Y. and Vianu, V., Computing with Infinitary Logic.
Theoretical Computer Science 149(1):101-128 (1995)
[2] Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics, NorthHolland, Amsterdam, 1984.
[3] Blum, L., Shub, M. and Smale, S., On a Theory of Computation and Complexity
over the Real Numbers: NP-completeness, Recursive Function and Universal
Machines, Bull. (New Series) Amer. Math. Soc. 21(1), 1989, 1-46.
[4] Blum, L., Cucker, F., Shub, M. and Smale, S., Complexity and Real Computation, Springer-Verlager, 1998.
[5] Chadzelek, T. and Hotz, G., Analytic Machines, Theoretical Computer Science,
219, 1999, 151-167.
[6] Dahr, M., Deductive Databases: Theory and Applications, International Thomson Computer Press, 1997.
[7] Jaffar, J., ”Efficient Unification over Infinite Terms”, New Generation Computing vol. 2 no. 3, 1984, pp. 207-219
[8] Li, W., An Open Logic System, Science in China (Scientia Sinica) (series A),
10(1992)(in Chinese), 1103-1113.
[9] Li, W., A Logical Framework for Evolution of Specifications, in: Programming
Languages and Systems, (ESOP’94), LNCS 788, Sringer-Verlag, 1994, 394-408.
[10] Lloyd, J. W., Foundations of Logic Programming, Springer-Verlag, Berlin,
1987.

16

[11] Nienhuys-Cheng, S. H., Distance between Herbrand Interpretations: A Measure for Approximations to a Target Concept, Proceedings of the 7th International Workshop on Inductive Programming, LNAI, Springer-Verlag, 1997.
[12] Nienhuys-Cheng, S. H., Distances and limits on Herbrand Interpretations,
Proceedings of the 8th International Workshop on Inductive Programming,
LNAI, Springer-Verlag, 1998.
[13] Tulipani, S., Decidability of the existential theory of infinite terms with subterm
relation. Information and Computation, 108(1):1-33, January 1994.
[14] van Emden, M. H. and Kowalski, R. A., The semantics of predicate logic as a
programming language, J. Association for Computing Machinary 23(4)(1976),
733-742.
[15] Vardi, M. Y. and Wolper, P., Reasoning About Infinite Computations. Information and Computation 115(1):1-37 (1994).

17

