BRICS RS-02-26 M. Korovina: Fixed Points on Abstract Structures without the Equality Test BRICS

Basic Research in Computer Science

Fixed Points on Abstract Structures without the Equality Test

Margarita Korovina BRICS Report Series RS-02-26 ISSN 0909-0878 June 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Margarita Korovina.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/26/

Fixed Points on Abstract Structures without the Equality Test

M. V. Korovina

BRICS^{∗} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract

In this paper we present a study of definability properties of fixed points of effective operators on abstract structures without the equality test. In particular we prove that Gandy theorem holds for the reals without the equality test. This provides a useful tool for dealing with recursive definitions using Σ-formulas.

1 Introduction

The aim of the paper is to present a study of definability properties of fixed points of effective operators on abstract structures without the equality test. The question of definability of fixed points of Σ-operators on abstract structures with equality was first studied in [1, 6, 5]. One of the most fundamental theorems in the area is Gandy theorem which states that the least fixed point of any positive Σ-operator is Σ-definable. This theorem allows us to treat inductive definitions using Σ-formulas. The role of inductive definability as the basic principle of general computability is discussed in [9, 13]. In some case it is natural to consider a structure in the language without equality. For example, in all effective approaches to exact real number computation via concrete representations [7, 8, 14], the equality test is undecidable. This is not surprising, because infinite amount of information must be checked in order to decide that two given numbers are equal.

∗

Basic Research in Computer Science (www.brics.dk),

funded by the Danish National Research Foundation.

Until now there has been no Gandy-type theorem known for such structures. Let us note that in all proofs of Gandy theorem that have been known so far it is the case that even when the definition of a Σoperator does not involve equality, the resulting Σ-formula usually does. In this paper we show that it is possible to overcome this problem. In particular we show that Gandy theorem holds for the real numbers without the equality test.

The concept of Σ-definability is closely related to the generalised computability on an abstract structure [1, 6, 12, 15], in particular on the real numbers [10, 11, 15].

Notions of Σ-definable sets or relations generalise those of computable enumerable sets of natural numbers, and play a leading role in the specification theory that is used in the higher order computation theory on abstract structures.

In this paper we investigate definability of the least fixed points of Σ-operators on abstract structure without the equality test. The organisation of paper is as follows. In Section 2 we introduce basic notations and definitions. We provide the background information necessary to understand of main results. Section 3 presents Gandy theorem for structures without the equality test. In Section 4 we give an application of our result to the real numbers without the equality test. We end with discussion of future work.

2 Background

We start by introducing basic notations and definitions. Let us consider an abstract structure A in a finite language σ_{0} without the equality test.

In order to do any kind of computation or to develop a computability theory one has to work within a structure rich enough for information to be coded and stored. For this purpose we extend the structure A by the set of hereditarily finite sets HF(A).

The idea that the hereditarily finite sets over A form a natural domain for computation is quite classical and is developed in detail in [1, 6].

Note that such or very similar extensions of structures with equality are used in the theory of abstract state machines [2, 3] and in query languages for hierarchic databases [4].

We will construct the set of hereditarily finite sets over the model without equality. This structure permits us to define the natural numbers, and to code and store information via formulas.

We construct the set of hereditarily finite sets, HF(A), as follows:

1. HF_{0}(A) ⇌ A, HF_{n+1}(A) ⇌ P_{ω}(HF_{n}(A)) ∪ HF_{n}(A), where n ∈ ω and for every set B, P_{ω}(B) is the set of all finite subsets of B.

2. HF(A) = ⋃_{n∈ω} HF_{n}(A).

We define HF(A) as the following model:

HF(A) ⇌ ⟨HF(A), U, S, σ_{0}, ∅, ∈⟩ ⇌ ⟨HF(A), σ⟩ ,

where the constant ∅ stands for the empty set, the binary predicate symbol ∈ has the set-theoretic interpretation. Also we add predicates symbols U for urelements (elements from A) and S for sets. Let us denote S(HF(A)) ⇌ HF(A) \ A.

The natural numbers 0, 1, … are identified with the (finite) ordinals in HF(A) i.e. ∅, {∅, {∅}}, …, so in particular, n + 1 = n ∪ {n} and the set ω is a subset of HF(A). We use variables subject to the following conventions:

r, r_{1}, … range over A (urelements),

x, y, z, s, w, f, g, … range over S(HF(A)) (sets),

n, m, l, … range over ω (natural numbers) and

a, b, c … range over HF(A).

We use the same letters to denote elements from the corresponding structures and r̄ to denote r_{1}, …, r_{m}.

The notions of a term and an atomic formula are given in the standard manner.

The set of Δ_{0}-formulas is the closure of the set of atomic formulas under ∧, ∨, ¬, and bounded quantifiers (∃a ∈ s) and (∀a ∈ s), where (∃a ∈ s) Ψ denotes ∃a(a ∈ s ∧ Ψ) and (∀a ∈ s) Ψ denotes ∀a(a ∈ s → Ψ).

The set of Σ-formulas is the closure of the set of Δ_{0} formulas under ∧,∨, (∃a ∈ s), (∀a ∈ s), and ∃.

We are interested in Σ-definability of sets on A^{n} which can be considered as generalisation of recursive enumerability. The analogy of Σdefinable and recursive enumerable sets is based on the following fact.

Consider the structure HF = ⟨HF(∅), ∈⟩ with the hereditarily finite sets over ∅ as its universe and membership as its only relation. In HF the Σ-definable sets are exactly the recursively enumerable sets.

The notion of Σ-definability has a natural meaning also in the structure HF(A).

Definition 2.1 1. A set B ⊆ HF(A) is Σ-definable, if there exists a Σ-formula Φ(a) such that b ∈ B ↔ HF(A) ⊧ Φ(b).

2. A function f : HF(A) → HF(A) is Σ-definable, if there exists a Σ-formula Φ(c, d) such that f(a) = b ↔ HF(A) ⊧ Φ(a, b).

Note that the sets A and ω are Δ_{0}-definable. This fact makes HF(A) a suitable domain for studying subsets of A^{n} and operators of the type

Γ : P(A^{n}) → P(A^{n}).

In the following lemma we introduce some Δ_{0}-definable and Σ-definable predicates that we will use later.

Lemma 2.2 1. The predicates R(a) ⇌ a ∈ A, S(a) ⇌ a is a set, and n ∈ ω are Δ_{0}-definable.

2. The following predicates are Δ_{0}-definable: x = y, x = y ∩ z, x = y ∪ z, x =< y, z >, x = y \ z (recall that all variables x, y, z range over sets).

3. A function f : ω^{n} → ω^{m} is computable if and only if it is Σdefinable.

4. Let F un(g) mean that g is a finite function i.e.

g = {⟨x, y⟩ | for every x there exists a unique y }

then the predicate F un(g) is Δ_{0}-definable.

5. If HF(A) ⊧ F un(g) then the domain of g, denoted by δ_{g}, is Δ_{0}- definable.

Proof. Proofs of all properties are straightforward except (3) which can be found in [6]. □

For finite functions F un(f) let us denote f(x) = y if ⟨x, y⟩ ∈ f. The following proposition states that we have full collection on HF(A).

Proposition 2.3 (Collection.) For every formula Φ the following claim holds. If HF(A) ⊧ (∀a ∈ x) ∃bΦ(a, b) then there is a set z such that

HF(A) ⊧ (∀a ∈ x) (∃b ∈ z) Φ(a, b) ∧ (∀b ∈ z) (∃a ∈ x) Φ(a, b).

Proof. The claim follows from the definition of HF(A). Indeed, if x ∈ HF(A) consists of k elements a_{1}, …, a_{k} and for each of these a_{i} there is an b_{i} such that Φ(a_{i}, b_{i}) holds. Then all b_{1}, …, b_{k} occur in HF_{n}(A) for some n, hence {b_{1}, …, b_{k}} ∈ HF_{n+1}(A). □

3 The least fixed points of effective operators

Now we recall the notion of Σ-operator and prove Gandy theorem for structures without the equality test.

Let Φ(a_{1}, …, a_{n}, P) be a Σ-formula where P occurs positively in Φ and the arity of Φ is equal to n.

We think of Φ as defining a Σ-operator Γ : P(HF(A)^{n}) → P(HF(A)^{n}) given by

Γ(Q) = {ā| (HF(A), Q) ⊧ Φ(ā, P)},

where for every set B, P(B) is the set of all subsets of B.

Since the predicate symbol P occurs only positively we have that the corresponding operator Γ is monotone i.e. for any sets from A ⊆ B follows Γ(A) ⊆ Γ(B).

By monotonicity, the operator Γ has the least (w.r.t. inclusion) fixed point which can be described as follows.

We start from the empty set and apply operator Γ until we reach the fixed point:

Γ^{0} = ∅, Γ^{n+1} = Γ(Γ^{n}), Γ^{γ} = ∪_{n<γ}Γ^{n},  (1)

where γ is a limit ordinal.

One can easily check that the sets Γ^{n} form an increasing chain of sets: Γ^{0} ⊆ Γ^{1} ⊆ . . .. By set-theoretical reasons, there exists the least ordinal γ such that Γ(Γ^{γ}) = Γ^{γ}. This Γ^{γ} is the least fixed point of the given operator Γ.

In order to study the least fixed points of arbitrary Σ-operators (without equality test), we first consider Σ-operators of the type

Γ : P(S(HF(A))^{n}) → P(S(HF(A))^{n}).

Then we will show how the least fixed points of arbitrary Σ-operators can be constructed using the least fixed points of such operators. Note that, as S(HF(A)) is closed under pairing, S(HF(A))^{n} ⊆ S(HF(A)) for n > 0. Moreover, S(HF(A))^{n} is a Σ-definable subset of HF(A). So, without loss of generality we can consider the case n = 1.

Let us formulate some properties of Σ-operators which we will use below. The following proposition states that each element from the value of a Σ-operator on a Σ-set can be obtained as an element of the value of this operator on a finite subset of the set.

Proposition 3.1 If Q is a Σ-definable subset of S(HF(A)) and w ∈ Γ(Q) then there exists p ∈ S(HF(A)) such that p ⊆ Q and w ∈ Γ(p).

Proof. We prove the proposition for the more general case where we allow parameters from S(HF(A)) to occur into the formula defining our operator.

Let Φ(b̄, x, P) be a Σ-formula defining our operator Γ, where b̄ = b_{1}, …, b_{n} are parameters from S(HF (A)). And let Q be a Σ-definable subset of S(HF (A)) and w ∈ Γ(Q). We need to prove that there exists p ∈ S(HF (A)) such that p ⊆ Q and w ∈ Γ(p).

We prove the claim by induction on the structure of Φ.

If Φ(b̄,x, P) ⇌ P (x) and (HF(A), Q) ⊧ P (w) then the set p ⇌ {w} is a required one.

If Φ is an atomic formula which does not contain P then the set p ⇌ ∅ is a required one.

For the induction step let us consider all possible cases.

1. Suppose Φ(b̄, x, P) ⇌ (∀a ∈ b_{j}) Ψ(a, b̄, x, P) and

(HF(A), Q) ⊧ (∀a ∈ b_{j}) Ψ(a, b̄, w, P).

By induction hypothesis,

(HF(A), Q) ⊧ (∀a ∈ b_{j}) ∃s (Ψ(a, b̄, w, P))_{t∈s}^{P (t)} ∧ s ⊆ Q.

Using Proposition 2.3, we find an element q such that

(HF(A), Q) ⊧ (∀a ∈ b_{j}) (∃s ∈ q) ((Ψ(a, b̄, w, P))_{t∈s}^{P (t)} ∧ s ⊆ Q) ∧
(∀s ∈ q) (∃a ∈ b_{j}) ((Ψ(a, b̄, w, P))_{t∈s}^{P (t)} ∧ s ⊆ Q) .

Let p ⇌ ∪q.

By definition, for all a ∈ b_{j} there exists s ⊆ p such that

(HF(A), s) ⊧ (Ψ(a, b̄, w, P))_{t∈s}^{P (t)} .

So we have

(HF(A), p) ⊧ Ψ(a, b̄, w, P) for all a ∈ b_{j}.

In other words,

(HF(A), p) ⊧ (∀a ∈ b_{j}) Ψ(a, b̄, x, P).

By construction the set p is a required one.

2. The case Φ(b̄, x, P) ⇌ (∃a ∈ b_{j}) Ψ(a, b̄, x, P) is similar to the case above.

3. Suppose Φ(b̄, x, P) ⇌ ∃aΨ(a, b̄, x, P) and

(HF(A), Q) ⊧ Ψ(b′, b̄, w, P).

By induction hypothesis, there exists p_{0} ⊆ Q such that p_{0} ∈ S(HF(A)) and

(HF(A), p_{0}) ⊧ Ψ(b′, b̄, w, P).

The set p ⇌ p_{0} is a required one.

4. Suppose Φ(b̄, x, P) ⇌ Ψ_{1}(b̄, x, P) ∧ Ψ_{2}(b̄, x, P) and

(HF(A), Q) ⊧ Ψ_{1}(b̄, w, P) ∧ Ψ_{2}(b̄, w, P).

By induction hypothesis, there exist p_{1} ⊆ Q and p_{2} ⊆ Q such that p_{1} ∈ S(HF(A)), p_{2} ∈ S(HF(A)) and

(HF(A), p_{1}) ⊧ Ψ_{1}(b̄, w, P)

and

(HF(A), p_{2}) ⊧ Ψ_{2}(b̄, w, P).

The set p ⇌ p_{1} ∪ p_{2} is a required one.

5. The case Φ(b̄, x, P) ⇌ Ψ_{1}(b̄, x, P)∨Ψ_{2}(b̄, x, P) is similar to the case above. □

Proposition 3.2 Let Γ : P(S(HF(A))) → P(S(HF(A))) be a Σ-operator. The relation x ∈ Γ(y) is Σ-definable.

Proof. Let Φ(z, P) be a Σ-formula which defines the operator Γ. Suppose x ∈ Γ(y). By definition,

x ∈ {z| (HF(A), y) ⊧ Φ(z, P)}.

It means that

(HF(A), y) ⊧ Φ(x, P).

So we have

(HF(A)) ⊧ (Φ(x, P))_{t∈y}^{P (t)} .

It is easy to see that the relation x ∈ Γ(y) is defined by Σ-formula Φ(x, P)_{t∈y}^{P (t)}. □

Now we are ready to prove Gandy theorem for Σ-operators of the type

Γ : P(S(HF(A))) → P(S(HF(A))).

Theorem 3.3 Let Γ : P(S(HF(A))) → P(S(HF(A))) be a Σ-definable operator. Then the least fixed-point of Γ is Σ-definable.

Proof. We will prove that the least fixed point of the operator Γ is Γ^{ω}, where Γ^{ω} is defined as follows: Γ^{0} = ∅, Γ^{n} = Γ(Γ^{n−1}) for a finite ordinal n, and Γ^{ω} = ⋃_{m<ω} Γ^{m}.

Let us show Σ-definability of Γ^{n} for every finite ordinal n.

For this purpose we introduce the following family of finite functions:

X_{0} = < ∅, ∅ >,
X_{n} = {f|F un(f) and δ_{f} = n + 1, f(0) = ∅, f is monotonic

and for any m ≤ n the following is true:f(m) ⊆ ⋃_{l<m} Γ(f(l)}

where n > 0.

From the definitions X_{n} and Γ it follows that X_{n} is Σ-definable for all n ∈ ω, moreover there exists a Σ-formula ψ(n, x) such that

HF(A) ⊧ ψ(n, x) ↔ x ∈ X_{n}.

Below we will use the following useful properties of the families X_{n}:

1. Let w be a finite subset of X_{n}. Let us define f^{∗}(m) ⇌ ∪_{f∈w}f(m) for all m ≤ n. Then f^{∗} ∈ X_{n}.

2. If f ∈ X_{n} and m ≤ n. Then f ↾ (m + 1) ∈ X_{m}.

3. Let f ∈ X_{m} and m ≤ n.

Define a function

f^{∗}(l) = \{ \begin{matrix}f(l), & if l ≤ m \\ f(m), & if m < l ≤ n. \end{matrix}

Then f^{∗} ∈ X_{n}.

4. Let f ∈ X_{n} and b ∈ Γ(f(m)) where m ≤ n.

Define a function

f^{∗}(l) = \{ \begin{matrix}f(l), & if l ≤ n \\ \{b\}, & if l = n + 1. \end{matrix}

Then f^{∗} ∈ X_{n+1}.

Using these properties let us show that:

x ∈ Γ^{n} iff HF(A) ⊧ ∃f (f ∈ X_{n} ∧ x ∈ f(n))  (2)

by induction on n. For n = 0 we have Γ^{n} = ∅ and therefore (2) holds. Assume that (2) holds for n let us prove that (2) holds for n + 1. To prove from left to right let us consider x ∈ Γ^{n+1} = Γ(Γ^{n}). By

induction hypothesis we have that x_{1} ∈ Γ^{n} iff ∃g (g ∈ X_{n} ∧ x_{1} ∈ g(n)) . So the set Γ^{n} is Σ-definable. By Proposition 3.1 it follows that there exists y ∈ S(HF(A)) such that y ⊆ Γ^{n} and x ∈ Γ(y). By induction hypothesis and the condition y ⊆ Γ^{n},

HF(A) ⊧ (∀z ∈ y) ∃g (g ∈ X_{n} ∧ z ∈ g(n)) .

Using Proposition 2.3, we find an element w such that

HF(A) ⊧ (∀z ∈ y) (∃g ∈ w) (g ∈ X_{n} ∧ z ∈ g(n)) ∧
(∀g ∈ w) (∃z ∈ y) (g ∈ X_{n} ∧ z ∈ g(n)) .

Starting from the finite subset w ⊆ X_{n}, we define the function g_{0} as follows:

g_{0}(l) = ∪_{g∈w}g(l), l ≤ n.

By Property (1) of X_{n} which is mentioned above, g_{0} ∈ X_{n}. It is easy to check the following inclusion y ⊆ g_{0}(n). Indeed, if z ∈ y then there exists g ∈ w such that z ∈ g(n) ⊆ g_{0}(n).

Define a function

f(l) = \{ \begin{matrix}g_{0}(l), & if l ≤ n \\ \{x\}, & if l = n + 1. \end{matrix}

From Property (4) of X_{n} follows that f ∈ X_{n+1} and moreover x ∈ f(n+1) holds by the definition of f. So f is a required one.

To prove from right to left let us suppose there exists f such that (f ∈ X_{n+1} ∧ x ∈ f(n + 1)) . By the definition of X_{n+1}, x ∈ Γ(f(m)) for some m ≤ n.

Let us check the inclusion : f(m) ⊆ Γ^{m}. For this purpose we consider f_{1} = f ↾ (m+1). From Property (2) of X_{m} follows that f_{1} ∈ X_{m}. So, for all y ∈ f_{1}(m) we have HF(A) ⊧ ∃f (f ∈ X_{m} ∧ y ∈ f(m)) . By induction it means that f_{1}(m) = f(m) ⊆ Γ^{m}.

The operator Γ is monotone, so we have

x ∈ Γ(f(m)) ⊆ Γ(Γ^{m}) ⊆ ⋃_{m<n+1} Γ(Γ^{m}) = Γ^{n+1}.

Thus we have proven that Γ^{n} is Σ-definable for all n ∈ ω. Consequently,

x ∈ Γ^{ω} ↔ ∃n∃f (f ∈ X_{n} ∧ x ∈ f(n))  (3)

is Σ-definable.

To check that Γ^{ω} is a fixed point i.e. Γ(Γ^{ω}) ⊆ Γ^{ω} let us consider x ∈ Γ(Γ^{ω}). From (3) it follows that Γ^{ω} is Σ-definable. From Proposition 3.1 it follows that there exists y ∈ S(HF(A)) such that y ⊆ Γ^{ω} and x ∈ Γ(y). It is easy to check that y ⊆ Γ^{m} for some m ∈ ω. From this we have that x ∈ Γ(Γ^{m}) ⊆ Γ^{ω}. By monotonicity of Γ, the set Γ^{ω} is the least fixed point. So the least fixed point of the operator Γ is Σ-definable. □

Now we consider arbitrary Σ-operators on the structure A without the equality test.

Theorem 3.4 Let Γ : P(HF(A)^{n}) → P(HF(A)^{n}) be an arbitrary Σoperator. Then the least fixed-point of Γ is Σ-definable.

Proof.

Without loss of generality let us consider the case n = 1. For simplicity of notation, we will give the construction only for that case, since the main ideas are already contained here. Let Φ(r, P) define the operator Γ. We construct a new Σ-operator F : P(S(HF(A))) → P(S(HF(A))) such that

r ∈ Γ^{n} ⟷ ∃x (x ∈ F^{n} ∧ r ∈ x) .

For this purpose we define the following formula with a new unary predicate symbol Q:

Ψ(x, Q) = (∀r ∈ x) (Φ(r, P))_{∃yQ(y)∧t∈y}^{P (t)} .

It is easy to see that Ψ induces a Σ-operator F given by

F (D) = {x|(HF(A), D) ⊧ Ψ(x, Q)}.

Let us show that

r ∈ Γ^{n} ↔ ∃x(x ∈ F^{n} ∧ r ∈ x)  (4)

by induction on n. For n = 0 we have Γ^{n} = F^{n} = ∅ and therefore (4) holds.

Assume that (4) holds for n let us prove that (4) holds for n + 1. In other words we need to prove that

\begin{matrix}(HF(A), Γ^{n}) ⊧ Φ(r, P) ↔ \\ (HF(A), F^{n}) ⊧ ∃x (r ∈ x ∧ (∀r′ ∈ x) (Φ(r′, P))_{∃yQ(y)∧t∈y}^{P (t)}) . \end{matrix}

Since the first formula does not contain Q and the second formula does not contain P it is sufficient to consider one structure (HF(A), Γ^{n}, F^{n}) and prove that

(HF(A), Γ^{n}, F^{n}) ⊧ Φ(r, P) ↔

(HF(A), Γ^{n}, F^{n}) ⊧ ∃x (r ∈ x ∧ (∀r′ ∈ x) (Φ(r′, P))_{∃yQ(y)∧t∈y}^{P (t)}) .

To prove from left to right let us consider r ∈ HF(A) such that

(HF(A), Γ^{n}, F^{n}) ⊧ Φ(r, P).

Consider the formula (Φ(r, P))_{∃yQ(y)∧t∈y}^{P (t)} then by induction hypothesis we have that

(HF(A), Γ^{n}, F^{n}) ⊧ ∀r′ (P (r′) ↔ ∃x(x ∈ Q ∧ r′ ∈ x))  (5)

and therefore (by replacement lemma) we have

(HF(A), Γ^{n}, F^{n}) ⊧ (Φ(r, P))_{∃yQ(y)∧t∈y}^{P (t)} .

Now it is easy to check that

(HF(A), Γ^{n}, F^{n}) ⊧ ∃x (r ∈ x ∧ (∀r′ ∈ x) (Φ(r′, P))_{∃yQ(y)∧t∈y}^{P (t)})

taking x = {r}.

To prove from right to left let us consider r ∈ HF(A) such that

(HF(A), Γ^{n}, F^{n}) ⊧ ∃x (r ∈ x ∧ (∀r′ ∈ x) (Φ(r′, P))_{∃yQ(y)∧t∈y}^{P (t)}) .

From this we have that

(HF(A), Γ^{n}, F^{n}) ⊧ (Φ(r, P))_{∃yQ(y)∧t∈y}^{P (t)}

and from (5) (by replacement lemma) we obtain that

(HF(A), Γ^{n}, F^{n}) ⊧ Φ(r, P).

Now from Theorem 3.3 it follows that the least fixed point of the operator F is Σ-definable and therefore the the least fixed point of the operator Γ is also Σ-definable.

□

4 The least fixed points of effective operators on the real numbers without the equality test

In this section we consider the standard model of the real numbers ⟨IR, 0, 1, +, ·, −, <⟩, denoted also by IR, where +, · and − are regarded as the usual arithmetic operations on the reals. We use the language of strictly ordered rings, so the predicate < occurs positively in formulas. This allows us to consider Σ-definability as generalisation of computable enumerability. Indeed, in all effective approaches to exact real number computation via concrete representations, we need only finite amount of information in order to show that one given number is less than another one. The following is an immediate corollary of Theorem 3.4.

Corollary 4.1 Let Γ : P(HF(IR)^{n}) → P(HF(IR)^{n}) be an arbitrary Σ– operator. Then the least fixed-point of Γ is Σ-definable.

5 Future work

One of the applications of Gandy theorem in the case of structures with equality is that it allows us to define universal Σ-predicates. It leads to a topological characterisation of Σ-relations on IR. Thus the sets B ⊆ IR^{n} that are Σ-definable in HF(IR) with equality are exactly the effective unions of semialgebraic sets.

We think that Gandy theorem can be used in this way for the structures without equality, but for this we need more evolved arguments. Also we think that it is possible to show that the sets B ⊆ IR^{n} that are Σ-definable in HF(IR) without equality are exactly the effective unions of open semialgebraic sets.

References

[1] J. Barwise, Admissible sets and structures, Berlin, Springer-Verlag, 1975.

[2] A. Blass, Y. Gurevich and S. Shelah, Choiceless Polynomial Time, Pure and Applied logic, N 100, 1999, pages 141–187.

[3] A. Blass, Y. Gurevich, Background, Reserve and Gandy Machines, Proceedings of CSL’2000, LNCS N 1862, 2000, pages 1–17.

[4] E. Dahlhaus, J. A. Makowsky, Query languages for hierarchic databases, Information and computation, N 101, 1992, pages 1–32.

[5] R. Gandy, Inductive definitions, Generalized Recursion Theory, Amsterdam: North-Holland, 1974, pages 265–300.

[6] Yu. L. Ershov, Definability and computability, Plenum, New York, 1996.

[7] H. Freedman and K. Ko, Computational complexity of real functions, Theoret. Comput. Sci. , v. 20, 1982, pages 323–352.

[8] A. Grzegorczyk, On the definitions of computable real continuous functions, Fund. Math., N 44, 1957, pages 61–71.

[9] P. G. Hinman, Recursion on abstract structures, Handbook of Computability Theory, Elsevier, 1999, pages 317–359.

[10] M. Korovina, O. Kudinov, Characteristic Properties of Majorant-Computability over the Reals, Proc. of CSL’98, LNCS, 1584, 1999, pages 188–204.

[11] M. Korovina, O. Kudinov, Semantic Characterisations of Second-Order Computability over the real Numbers, Proc. of CSL’01, LNCS 2142, 2001, pages 160–173.

[12] Y. N. Moschovakis, Abstract first order computability, Trans. Amer. Math. Soc., v. 138, 1969, pages 427–464.

[13] Y. N. Moschovakis, Elementary Induction on Abstract Structure, North-Holland, 1974.

[14] M. B. Pour-El, J. I. Richards, Computability in Analysis and Physics, Springer-Verlag, 1988.

[15] J. V. Tucker, J. I. Zucker, Computable functions and semicomputable sets on many-sorted algebras, Handbook of Logic in Computer Science, v. 5, Oxford University Press, Oxford, 2000, pages 397–525.

Recent BRICS Report Series Publications

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002. 14 pp. Appears in Ésik and Ingólfsdóttir, editors, Preliminary Proceedings of the Workshop on Fixed Points in Computer Science, FICS ’02, (Copenhagen, Denmark, July 20 and 21, 2002), BRICS Notes Series NS-02-2, 2002, pages 58–61.

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp. Appears in Antonín and Mayr, editors, 4th International Workshop on Verification of Infinite-State Systems, INFINITY ’02 Proceedings, ENTCS 68(6), 2002, 18 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis for Dynamic XML. May 2002. 13 pp.

RS-02-23 Antonio Di Nola and Laurenţiu Leuştean. Compact Representations of BL-Algebras. May 2002. 25 pp.

RS-02-22 Mogens Nielsen, Catuscia Palamidessi, and Frank D. Valencia. On the Expressive Power of Concurrent Constraint Programming Languages. May 2002. 34 pp. Appears in Pfenning, editor, 4th International Conference on Principles and Practice of Declarative Programming, PPDP ’02 Proceedings, 2002, pages 156–157.

RS-02-21 ZoltánÉsik and Werner Kuich. Formal Tree Series. April 2002. 66 pp.

RS-02-20 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers (Preliminary Version). April 2002. 56 pp.

RS-02-19 Stephen L. Bloom and Zoltán Ésik. An Extension Theorem with an Application to Formal Tree Series. April 2002. 51 pp. Appears in Blute and Selinger, editors, Category Theory and Computer Science: 9th International Conference, CTCS ’02 Proceedings, ENTCS 69, 2003 under the title Unique Guarded Fixed Points in an Additive Setting.