BRICS RS-03-23 M. Korovina: Recent Advances in Σ-definability over Continuous Data Types BRICS

Basic Research in Computer Science

Recent Advances in Σ-definability over Continuous Data Types

Margarita Korovina BRICS Report Series RS-03-23 ISSN 0909-0878 June 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, 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/03/23/

Recent Advances in Σ-definability over Continuous Data Types^{∗}

Margarita Korovina

June, 2003

Abstract

The purpose of this paper is to survey our recent research in computability and definability over continuous data types such as the real numbers, real-valued functions and functionals. We investigate the expressive power and algorithmic properties of the language of Σ-formulas intended to represent computability over the real numbers. In order to adequately represent computability we extend the reals by the structure of hereditarily finite sets. In this setting it is crucial to consider the real numbers without equality since the equality test is undecidable over the reals. We prove Engeler’s Lemma for Σ-definability over the reals without the equality test which relates Σ-definability with definability in the constructive infinitary language L_{ω_{1}ω}. Thus, a relation over the real numbers is Σ-definable if and only if it is definable by a disjunction of a recursively enumerable set of quantifier free formulas. This result reveals computational aspects of Σ-definability and also gives topological characterisation of Σ-definable relations over the reals without the equality test. We also illustrate how computability over the real numbers can be expressed in the language of Σ-formulas.

1 Introduction

Study of computability properties of continuous objects such as reals, real-valued functions and functionals is one of the fundamental areas of Computer Science motivated by applications from Engineering; where the vast majority of objects are of a continuous nature. The classical theory of computation, which works with discrete structures, is not suitable for formalisation of computations that operate on realvalued data. Since computational processes are discrete in their nature and objects we consider are continuous, formalisation of computability of such objects is already a challenging research problem. This has resulted in various concepts of computability over continuous data types [4, 6, 12, 11, 15, 18, 22, 27, 26, 32, 37]. If we consider the case of the real numbers there are at least two main nonequivalent models of computability. The first one is related to abstract finite machines and schemes of computations (e.g. [4, 16, 31, 29, 35] ) where real numbers are considered as basic entities which can be added, multiplied, divided or compared in a single step, and computations are finite processes. In this approach equality is usually used as a basic relation, consequently a computable function can be discontinuous. It differs from the situation in concrete computability over the reals, particularly, in computable analysis. The second model ( e.g. [6, 12, 11, 15, 18, 22, 32, 37]) is closely related to computable analysis. In this approach real numbers are given by appropriate representations and computations are infinite processes which produce approximations to the results. This model is more satisfying conceptually, conforming to our intuition of reals, but depends on representations of the reals. In some cases it is not clear which representations are preferable. In this paper we survey the logical approach to computability on continuous structures, which have been first proposed in [27, 26]. On the one hand, the logical approach agrees with the second model mentioned above (i.e. mathematical intuition), on the other hand it does not depend on representations of reals.

∗This research was partially supported by the Danish Natural Science Research Council, Grant no. 21-02-0474.

In order to introduce the logical approach to computability over continuous data types we consider the following problems.

1. Which data structures are suitable for representing continuous objects?

2. Which logical language is appropriate to express computability on continuous data types?

3. Can we treat inductive definitions using this language?

4. What is the expressive power of this language?

In this paper we represent continuous data types by suitable structures without the equality test. This is motivated by the following natural reason. In all effective approaches to exact real number computation via concrete representations [15, 18, 32], the equality test is undecidable. This is not surprising, because an infinite amount of information must be checked in order to decide that two given real numbers are equal. 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 a structure 𝔸 by the set of hereditarily finite sets HF(𝔸). The idea that the hereditarily finite sets over 𝔸 form a natural domain for computation is discussed in [1, 14, 33]. Note that such or very similar extensions of structures are used in the theory of abstract state machines [3, 2], in query languages for hierarchic databases [7], and in Web-like databases [33].

In order to express computability on continuous data types we use the language of Σ-formulas. This approach is based on definability and has the following beneficial features.

• Notions of Σ-definable sets or relations generalise those of computable enumerable sets of natural numbers.

• It does not depend on representations of elements of structures.

• It is flexible: sometimes we can change the language of the structure to obtain appropriate computability properties.

• We can employ model theory to study computability.

• One can treat inductive definitions using Σ-formulas.

• Formulas can be seen as a suitable finite representation of the relations they define.

Now we address problems 3-4, listed above, regarding the language of Σ-formulas. These problems are closely related to the well-known Gandy’s Theorem which states that the least fixed point of any positive Σ-operator is Σ-definable. Gandy’s Theorem was first proven for abstract structures with the equality test (see [1, 14, 17]). In our setting it is important to consider structures without the equality test. Let us note that in all known proofs of Gandy’s Theorem so far, it is the case that even when the definition of a Σ-operator does not involve equality, the resulting Σ-formula usually does. Only recently we have shown in [25, 24] that it is possible to overcome this problem. In particular we have proved that Gandy’s Theorem holds for abstract structures without the equality test. The following several applications of Gandy’s Theorem demonstrate its significance. One of them is that we can treat inductive definitions using Σ-formulas. The role of inductive definability as a basic principle of general computability is discussed in [20, 30]. It is worth noting that for finite structures the least fixed points of definable operators give an important and well studied logical characterisation of complexity classes [10, 21, 36]. For infinite structures fixed point logics are also studied e.g. [8]. In the case of the real numbers, as in the case of discrete structures, inductive definitions allow us to define universal Σ-predicates. Another application is that Gandy’s Theorem can be used to reveal algorithmic aspects of Σ-definability.

In order to investigate algorithmic aspects of Σ-definability over the reals without the equality test we use a suitable fragment of the constructive infinite language L_{ω_{1}ω} [1, 34]. Certain fragments of constructive L_{ω_{1}ω} have been used to study the expressive power of formal approaches to computability such as search computability [30], ’While’-computability [35], ∀-recursiveness [28], dynamic logics [19] and fixed-point logics [10]. We show that a relation over the real numbers is Σ-definable if and only if it is definable by a disjunction of a recursively enumerable set of quantifier free formulas. Let us note that the proof of the ’if’ direction follows from Engeler’s Lemma for Σ-definability, which have been recently proved for the reals without equality in [23], and the proof of the ’only if’ direction uses methods based on Gandy’s Theorem. It is worth noting that both of the directions of this characterisation are important. Engler’s Lemma gives us an effective procedure which generates quantifier free formulas approximating Σ-relations. The converse direction provides tools for descriptions of the results of effective infinite approximating processes by finite formulas. For an illustration of the concepts of the logical approach, we consider computability on the real numbers. We show that computability of continuous objects, i.e. real numbers, real-valued functions, can be characterised by finite Σ-formulas.

The structure of this paper is as follows. In Section 2 we recall the notion of Σ-definability. In Section 3 we show that we can treat inductive definitions using Σ-formulas. Section 4 introduces a certain fragment of the constructive infinite logic. In Section 5 we present a characterisation of the expressive power of Σ-definability on the reals without the equality test. Section 6 illustrates how computability on the real numbers can be expressed in the language of Σ-formulas. We conclude with a discussion of future work.

2 Σ-definability over the Real Numbers

2.1 Basic Definitions and Notions

We start by introducing basic notations and definitions. Let us consider an abstract structure 𝔸 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 𝔸 by the set of hereditarily finite sets HF(𝔸).

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

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

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(𝔸), as follows:

1. HF_{0}(𝔸) ⇌ 𝔸,

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

3. HF(𝔸) ⇌ ⋃_{n∈ω} HF_{n}(𝔸).

We define HF(𝔸) as the following model:

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

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(𝔸)) ⇌ HF(𝔸) \ 𝔸.

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

r, x, y, z, … range over 𝔸 (urelements),

i, j, k, l, m, n, … range over ω (natural numbers),

α, β, κ, … range over HF(∅),

f, g, p, q, s, t, u, v, w, … range over S(HF(𝔸)) (sets),

L, M, N, R, X, Y, Z, … range over 𝔸^{∗} (nonempty finite sets over 𝔸),

A, B, C, D, U, V, W, … range over HF(𝔸^{∗}) (finite sets which do not contain elements of 𝔸 as members) and

a, b, c, d, k, … range over HF(𝔸). Different sorts for variables can been seen as a syntactic sugar, which can be eliminated, since, as we will see below, structures 𝔸, 𝔸^{∗}, HF(𝔸^{∗}), ω, HF(n) are Δ_{0}- definable subsets of 𝔸. We use the same letters as for variables to denote elements from the corresponding structures.

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(𝔸).

Definition 2.1 1. A relation B ⊆ HF(𝔸)^{n} is Δ_{0} (Σ)-definable, if there exists a Δ_{0} (Σ)-formula Φ(ā) such that

b̄ ∈ B ↔ HF(𝔸) ⊧ Φ(b̄).

2. A function f : HF(𝔸)^{n} → HF(𝔸)^{m} is Δ_{0} (Σ)-definable, if there exists a Δ_{0} (Σ)-formula Φ(c̄, d̄) such that

f(ā) = b̄ ↔ HF(𝔸) ⊧ Φ(ā, b̄).

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

Γ : P(𝔸^{n}) → P(𝔸^{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 ∈ 𝔸, S(a) ⇌ a is a set, and n ∈ ω are Δ_{0}-definable.

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

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

4. Every B ⊂ IN^{n} is recursively enumerable if and only if it is Σ-definable.

5. All arithmetic operations on ordinals are Σ-definable.

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

g = {⟨u, v⟩ | for every u there exists a unique v }

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

7. If HF(𝔸) ⊧ 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 [14]. □

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

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

HF(𝔸) ⊧ (∀a ∈ u) (∃b ∈ t) Φ(a, b) and
HF(𝔸) ⊧ (∀b ∈ t) (∃a ∈ u) Φ(a, b).

Proof. The claim follows from the definition of HF(𝔸). Indeed, if u ∈ HF(𝔸) 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}(𝔸) for some n, hence {b_{1}, …, b_{k}} ∈ HF_{n+1}(𝔸). □

Proposition 2.4 (Σ-reflection principle) Every Σ-formula Φ(ā) is equivalent to a formula of the type ∃uΨ(u, ā), where Ψ is a Δ_{0}-formula.

2.2 The least fixed points of effective operators

Now we recall the notion of Σ-operator and prove Gandy’s 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(𝔸)^{n}) → P(HF(𝔸)^{n})

given by

Γ(Q) = {ā| (HF(𝔸), 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 the equality test), we first consider Σ-operators of the type

Γ : P(S(HF(𝔸))^{n}) → P(S(HF(𝔸))^{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(𝔸)) is closed under pairing, S(HF(𝔸))^{n} ⊆ S(HF(𝔸)) for n > 0. Moreover, S(HF(𝔸))^{n} is a Σ-definable subset of HF(𝔸). 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 2.5 If Q is a Σ-definable subset of S(HF(𝔸)) and w ∈ Γ(Q) then there exists p ∈ S(HF(𝔸)) such that p ⊆ Q and w ∈ Γ(p).

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

Let Φ(b̄, u, 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̄,u, P) ⇌ P (u) and (HF(𝔸), 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̄, u, P) ⇌ (∀a ∈ b_{j}) Ψ(a, b̄, u, P) and

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

By induction hypothesis,

(HF(𝔸), 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

\begin{matrix}(HF(𝔸), 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) . \end{matrix}

Let p ⇌ ∪q.

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

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

So we have

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

In other words,

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

By construction the set p is a required one.

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

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

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

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

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

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

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

(HF(𝔸), 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(𝔸)), p_{2} ∈ S(HF(𝔸)) and

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

and

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

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

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

Proposition 2.6 Let Γ : P(S(HF(𝔸))) → P(S(HF(𝔸))) be a Σ-operator. The relation u ∈ Γ(v) is Σ-definable.

Proof. Let Φ(t, P) be a Σ-formula which defines the operator Γ. Suppose u ∈ Γ(v). By definition,

u ∈ {t| (HF(𝔸), v) ⊧ Φ(t, P)}.

It means that

(HF(𝔸), v) ⊧ Φ(u, P).

So we have

(HF(𝔸)) ⊧ (Φ(u, P))_{t∈v}^{P (t)} .

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

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

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

Theorem 2.7 Let Γ : P(S(HF(𝔸))) → P(S(HF(𝔸))) 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:

𝒳_{0} = < ∅, ∅ >,
𝒳_{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 𝒳_{n} and Γ it follows that 𝒳_{n} is Σ-definable for all n ∈ ω, moreover there exists a Σ-formula ψ(n, u) such that

HF(𝔸) ⊧ ψ(n, u) ↔ u ∈ 𝒳_{n}.

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

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

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

3. Let f ∈ 𝒳_{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^{∗} ∈ 𝒳_{n}.

4. Let f ∈ 𝒳_{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^{∗} ∈ 𝒳_{n+1}.

Using these properties let us show that:

u ∈ Γ^{n} iff HF(𝔸) ⊧ ∃f (f ∈ 𝒳_{n} ∧ u ∈ 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 an element u ∈ Γ^{n+1} = Γ(Γ^{n}). By induction hypothesis we have that u_{1} ∈ Γ^{n} iff ∃g (g ∈ 𝒳_{n} ∧ u_{1} ∈ g(n)) . So the set Γ^{n} is Σ-definable. By Proposition 2.5 it follows that there exists v ∈ S(HF(𝔸)) such that v ⊆ Γ^{n} and u ∈ Γ(v). By induction hypothesis and the condition v ⊆ Γ^{n},

HF(𝔸) ⊧ (∀t ∈ v) ∃g (g ∈ 𝒳_{n} ∧ t ∈ g(n)) .

Using Proposition 2.3, we find an element w such that

HF(𝔸) ⊧ (∀t ∈ v) (∃g ∈ w) (g ∈ 𝒳_{n} ∧ t ∈ g(n)) ∧
(∀g ∈ w) (∃t ∈ v) (g ∈ 𝒳_{n} ∧ t ∈ g(n)) .

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

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

By Property (1) of 𝒳_{n} which is mentioned above, g_{0} ∈ 𝒳_{n}. It is easy to check the following inclusion v ⊆ g_{0}(n). Indeed, if t ∈ v then there exists g ∈ w such that t ∈ g(n) ⊆ g_{0}(n). Define a function

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

From Property (4) of 𝒳_{n} follows that f ∈ 𝒳_{n+1} and moreover u ∈ 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 ∈ 𝒳_{n+1} ∧ u ∈ f(n + 1)) .

By the definition of 𝒳_{n+1}, u ∈ Γ(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 𝒳_{m} follows that f_{1} ∈ 𝒳_{m}. So, for all v ∈ f_{1}(m) we have HF(𝔸) ⊧ ∃f (f ∈ 𝒳_{m} ∧ v ∈ f(m)) . By induction it means that f_{1}(m) = f(m) ⊆ Γ^{m}.

The operator Γ is monotone, so we have

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

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

u ∈ Γ^{ω} ↔ ∃n∃f (f ∈ 𝒳_{n} ∧ u ∈ f(n))  (3)

is Σ-definable.

To check that Γ^{ω} is a fixed point i.e. Γ(Γ^{ω}) ⊆ Γ^{ω} let us consider u ∈ Γ(Γ^{ω}). From (3) it follows that Γ^{ω} is Σ-definable. From Proposition 2.5 it follows that there exists v ∈ S(HF(𝔸)) such that v ⊆ Γ^{ω} and u ∈ Γ(v). It is easy to check that v ⊆ Γ^{m} for some m ∈ ω. From this we have that u ∈ Γ(Γ^{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 𝔸 without the equality test.

Theorem 2.8 Let Γ : P(HF(𝔸)^{n}) → P(HF(𝔸)^{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(𝔸))) → P(S(HF(𝔸))) such that

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

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

Ψ(u, Q) = (∀r ∈ u) (Φ(r, P))_{∃vQ(v)∧t∈v}^{P (t)} .

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

F (D) = {u|(HF(𝔸), D) ⊧ Ψ(u, Q)}.

Let us show that

r ∈ Γ^{n} ↔ ∃u(u ∈ F^{n} ∧ r ∈ u)  (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(𝔸) & , Γ^{n}) ⊧ Φ(r, P) ↔ \\ (HF(𝔸) & , F^{n}) ⊧ ∃u (r ∈ u ∧ (∀r′ ∈ u) (Φ(r′, P))_{∃vQ(v)∧t∈v}^{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(𝔸), Γ^{n}, F^{n}) and prove that

(HF(𝔸),Γ^{n}, F^{n}) ⊧ Φ(r, P) ↔
(HF(𝔸),Γ^{n}, F^{n}) ⊧ ∃u (r ∈ u ∧ (∀r′ ∈ u) (Φ(r′, P))_{∃vQ(v)∧t∈v}^{P (t)}) .

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

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

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

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

and therefore (by replacement lemma) we have

(HF(𝔸), Γ^{n}, F^{n}) ⊧ (Φ(r, P))_{∃vQ(v)∧t∈v}^{P (t)} .

Now it is easy to check that

(HF(𝔸), Γ^{n}, F^{n}) ⊧ ∃u (r ∈ u ∧ (∀r′ ∈ u) (Φ(r′, P))_{∃vQ(v)∧t∈v}^{P (t)})

taking u = {r}.

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

(HF(𝔸), Γ^{n}, F^{n}) ⊧ ∃u (r ∈ u ∧ (∀r′ ∈ u) (Φ(r′, P))_{∃vQ(v)∧t∈v}^{P (t)}) .

From this we have that

(HF(𝔸), Γ^{n}, F^{n}) ⊧ (Φ(r, P))_{∃vQ(v)∧t∈v}^{P (t)}

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

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

Now from Theorem ?? 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.

□

3 Expressive Power of Σ-definability over the Reals

In this section we consider the standard model of the real numbers

⟨IR, 0, 1, +, ·, <⟩ = ⟨IR, σ_{0}⟩ ,

denoted also by IR, where + and · are regarded as the usual arithmetic operations on the real numbers. We use the language of strictly ordered rings, so we assume that the predicate < occurs positively in all formulas.

We use the same letters as for variables to denote elements from the corresponding structures.

A formula in the form p_{1}(x̄) < p_{2}(x̄), where p_{1} and p_{2} are polynomials with coefficients in IN, is called an atomic strict semi-algebraic (^{<}algebraic ) formula.

The set of atomic formulas is the union of the set of atomic ^{<}algebraic formulas and the formulas of the type N ∈ M, where M ranges over sets.

The closure of the atomic ^{<}algebraic formulas under finite conjunctions and disjunctions forms the set of ^{<}algebraic formulas.

The notion of Δ_{0}-formula is the same as in Section 1. We assume that predicates from the language σ_{0} can occur only positively in our formulas.

With every atomic ^{<}algebraic formula p_{1}(x_{1}, …, x_{n}) < p_{2}(x_{1}, …, x_{n}) we associate the following formula, called a lifted atomic ^{<}algebraic formula:

p_{1}(X_{1}, …, X_{n}) < p_{2}(X_{1}, …, X_{n}) ⇌
(∀x_{1} ∈ X_{1}) … (∀x_{n} ∈ X_{n}) p_{1}(x_{1}, …, x_{n}) < p_{2}(x_{1}, …, x_{n}).

The terms p_{1}(X̄) and p_{2}(X̄) are called lifted polynomials. In a similar way, we can also associate with each ^{<}algebraic formula a lifted ^{<}algebraic formula, i.e., the lifted ^{<}algebraic formulas are the closure of lifted atomic ^{<}algebraic formulas under finite conjunctions and disjunctions.

The notion of Σ-formula is the same as in Section 1.

In the following lemmas we obtain some properties of ^{<}algebraic and lifted <algebraic formulas that will be used later.

Lemma 3.1 If B ⊂ IR^{n} is definable by an ^{<}algebraic formula then it is open.

Lemma 3.2 Let Φ(x̄) be an ^{<}algebraic formula and Φ_{lifted}(X̄) be the corresponding lifted ^{<}algebraic formula. If R_{i} = {r_{i}} for i = 1 … n, then

HF(IR) ⊧ Φ(r̄) ↔ Φ_{lifted}(R̄).

Lemma 3.3 Let Φ(x̄) be an ^{<}algebraic formula and Φ_{lifted}(X̄) be the corresponding lifted ^{<}algebraic formula. Then for all x̄ ∈ IR^{n} we have

HF(IR) ⊧ Φ(x_{1}, …, x_{n}) ↔ ∃X_{1} … ∃X_{n}Φ_{lifted}(X_{1}, …, X_{n}) ∧ ⋀_{i≤n} (x_{i} ∈ X_{i}) .

Lemma 3.4 Let Φ_{lifted}(X̄) be a lifted ^{<}algebraic formula and Y_{1} ⊆ Z_{1}, …, Y_{n} ⊆ Z_{n}. If HF(IR) ⊧ Φ_{lifted}(Z_{1}, …, Z_{n}), then HF(IR) ⊧ Φ_{lifted}(Y_{1}, …, Y_{n}).

Lemma 3.5 Let Φ_{lifted}(Ȳ) be a lifted ^{<}algebraic formula. If for some X_{1}, …, X_{n} we have HF(IR) ⊧ Φ_{lifted}(X_{1}, …, X_{n}), then for all m > 0 there exist Y_{1}, …, Y_{n} of cardinality m such that for all i, j ≤ n Y_{i} = Y_{j} ↔ X_{i} = X_{j} and HF(IR) ⊧ Φ_{lifted}(Y_{1}, …, Y_{n}).

Lemma 3.6 Let Φ be an existentially quantified ^{<}algebraic formula. Then there exists an ^{<}algebraic formula Ψ such that HF(IR) ⊧ Φ(x̄) ↔ Ψ(x̄). Moreover Ψ can be constructed effectively from Φ.

Let us note that proofs of all lemmas are straightforward except Lemma 3.6 which follows from the finiteness theorem [5, 9].

3.1 Gandy’s Theorem and Inductive Definitions over the Reals

The following is an immediate corollary of Theorem 2.7.

Theorem 3.7 (Gandy’s Theorem for HF(IR)) Let Γ : P(HF(IR)^{n}) → P(HF(IR)^{n}) be an effective operator. Then the least fixed-point of Γ is Σ-definable and the least ordinal such that Γ(Γ^{γ}) = Γ^{γ} is less or equal to ω.

Proof. The claim follows from Theorem 2. □

Definition 3.8 A relation ℬ ⊂ IR^{n} is called Σ-inductive if it is the least-fixed point of an effective operator.

Corollary 3.9 Every Σ-inductive relation is Σ-definable.

3.2 Universal Σ-predicate for ^{<}algebraic Formulas

In order to obtain a result on the existence of a universal Σ-predicate for the^{<}algebraic formulas, we first construct a universal Σ-predicate for the lifted ^{<}algebraic formulas. For this purpose we prove Σ-definability of the truth of lifted ^{<}algebraic formulas.

In this section we fix a standard effective Gödel numbering of the terms and formulas of the language σ by finite ordinals which are elements of HF(∅). Let ⌈Φ⌉, ⌈p⌉ denote the codes of a formula Φ and a term p respectively. It is worth noting that the type of an expression is effectively recognisable by its code. We also can obtain effectively from the codes of expressions the codes of their subexpressions and vice versa. Since equality is Δ_{0}-definable in HF(∅), we can use the well-known characterisation which states that all effective procedures over ordinals are Σ-definable. Thus, for example, the following predicates

Code_{elem}(n, i, j) ⇌ n = ⌈X_{i} < X_{j}⌉,
Code_{sum1}(n, i, j, k) ⇌ n = ⌈p + q < f⌉ ∧ i = ⌈p⌉ ∧ j = ⌈q⌉ ∧ k = ⌈f⌉,
Code_{∧}(n, i, j)  ⇌ n = ⌈Φ ∧ Ψ⌉ ∧ j = ⌈Φ⌉ ∧ j = ⌈Ψ⌉

are Σ-definable. Hence, in Σ-formulas we can use such predicates.

With every element A ∈ HF(IR) we associate an interpretation γ_{A} of variables X_{1}, X_{2}, … such that

γ_{A}(X) = \{ \begin{matrix}N & if ⟨⌈X⌉, N⟩ ∈ A and \\ & for any ⟨⌈X⌉, M⟩ ∈ A, we have M = N \\ ∅ & otherwise. \end{matrix}

Let V be a set of variables. An interpretation γ_{A} is called correct for V if for all X ∈ V we have γ_{A}(X) ≠ ∅. Let Int denote the set of elements A ∈ HF(IR) with the following property: if ⟨i, X⟩ and ⟨i, Y ⟩ belong to A, then we have X = Y. It is easy to see that this set is Δ_{0}-definable by the following formula:

Int(A) ⇌  (∀U ∈ A) (∀W ∈ A) (∀V_{1} ∈ U) (∀V_{2} ∈ U) (∀i ∈ V_{1}) (∀X ∈ V_{2})
(∀V_{3} ∈ W) (∀Y ∈ V_{3}) ((U = ⟨i, X⟩ ∧ W = ⟨i, Y ⟩) → X = Y) .

Theorem 3.10 There exists a binary Σ-definable predicate T r such that for any n ∈ ω and A ∈ HF(IR) we have that (n, A) ∈ T r if and only if n is the Gödel number of a lifted ^{<}algebraic formula Φ, γ_{A} is a correct interpretation for free variables of Φ and HF(IR) ⊧ Φ[γ_{A}].

Proof. The predicate T r is the least fixed point of the operator defined by the following formula:

Φ(n, U, P) ⇌ Φ_{proper}(n) ∨ Φ_{elem}(n, U) ∨ Φ_{sum}(n, U, P) ∨
Φ_{mult}(n, U, P) ∨ Φ_{∧}(n, U, P) ∨ Φ_{∨}(n, U, P),

where n, U are free variables and P is a new predicate symbol. The formula Φ(n, U, P) represents the inductive definition of the truth of the lifted^{<}algebraic formulas, where the immediate subformulas have the following meaning. The formulas Φ_{proper}(n) and Φ_{elem}(n, U) define the basis of the inductive definition. In other words, the formula Φ_{proper}(n) represents the truth of the proper formulas, i.e., 0 < 1 and 1 < 0; the formula Φ_{elem}(n, U) represents the truth of the elementary formulas, i.e., the formulas of the type, X_{i} < 0, 0 < X_{i}, 1 < X_{i} and X_{i} < 1. The formulas Φ_{sum}(n, U, P) and Φ_{mult}(n, U, P) represent the inductive steps for sum and multiplication. Finally, the formulas Φ_{∧}(n, U, P) and Φ_{∨}(n, U, P) represent the inductive steps for conjunctions and disjunctions. Let us show how to construct these formulas. The Δ_{0}-formula Φ_{proper}(n) is obvious. The Σ-formula Φ_{elem}(n, U) can be given as follows.

Φ_{elem}(n, U) ⇌ ∃i∃j∃L∃M ( ( n = ⌈X < Y ⌉ ∧ i = ⌈X⌉ ∧ j = ⌈Y ⌉ ∧
U = {⟨i, L⟩ , ⟨j, M⟩} ∧ L < M ) ∨

(n = ⌈X < 0⌉ ∧ i = ⌈X⌉ ∧ U = {⟨i, L⟩} ∧ L < 0) ∨ (n = ⌈0 < X⌉ ∧ i = ⌈X⌉ ∧ U = {⟨i, L⟩} ∧ 0 < L) ∨ (n = ⌈X < 1⌉ ∧ i = ⌈X⌉ ∧ U = {⟨i, L⟩} ∧ L < 1) ∨ (n = ⌈1 < X⌉ ∧ i = ⌈X⌉ ∧ U = {⟨i, L⟩} ∧ 1 < L) ) .

Now we construct a Σ-formula Φ_{sum1}(n, U, P) which represents the case when n is the code of a formula of the type: p + q < f, where p, q and f are lifted polynomials. Let nextvar(⌈Ψ⌉, l) denote the Σ-definable predicate which means that if m is the maximal index of variables which occur in Φ, then l = m + 1. The formula Φ_{sum} can be given as follows.

Φ_{sum1}(n, U, P) ⇌ ∃i∃j∃k∃l∃m∃s∃V ∃W ∃Y ∃L∃M∃N ( n = ⌈p + q < f⌉ ∧
i = ⌈p⌉ ∧ j = ⌈q⌉ ∧ k = ⌈f⌉ ∧
nextvar(n, l) ∧ m = l + 1 ∧ s = m + 1 ∧
P (⌈p < X_{l}⌉, V) ∧ P (⌈q < X_{m}⌉, W) ∧ P (⌈X_{s} < f⌉, Y) ∧
⟨i, L⟩ ∈ V ∧ ⟨j, M⟩ ∈ W ∧ ⟨k, N⟩ ∈ Y ∧ L + M < N ∧
U = (V ∪ W ∪ Y) ∧ Int(U) ) .

In a similar way, we can produce a Σ-formula Φ_{sum2}(n, U, P) which represents the case when n is the code of a formula of the type: p < q +f, where p, q and f are lifted polynomials. Put Φ_{sum}(n, U, P) ⇌ Φ_{sum1}(n, U, P)∧Φ_{sum2}(n, U, P). In the same way, we can produce the Σ-formula Φ_{mul}(n, U, P) which represents the inductive steps for multiplication.

The Σ-formula Φ_{∧} can be constructed as follows:

Φ_{∧}(n, U, P) ⇌ ∃i∃j n = ⌈φ ∧ ψ⌉ ∧ i = ⌈φ⌉ ∧ j = ⌈ψ⌉ ∧ P (i, U) ∧ P (j, U).

In a similar way, we can produce the Σ-formula Φ_{∨}(n, U, P) which represents the inductive steps for disjunctions.

From Gandy’s theorem (c.f. Section 2.2) it follows that the least fixed point T r of the effective operator defined by Φ is Σ-definable.

□

Theorem 3.11 For every n ∈ ω there exists a Σ-formula Univ_{n}^{∗}(m, X_{1}, …, X_{n}) such that for any lifted ^{<}algebraic formula Φ(X_{1}, …, X_{n})

HF(IR) ⊧ Φ(R_{1}, …, R_{n}) ↔ Univ_{n}^{∗}(⌈Φ⌉, R_{1}, …, R_{n}).

Proof. It is easy to see that the following formula defines a universal Σ-predicate for the lifted ^{<}algebraic formulas of arity n

Univ_{n}^{∗}(m, X_{1}, … X_{n}) ⇌ ∃U (U = {⟨1, X_{1}⟩ , …, ⟨n, X_{n}⟩} ∧ T r(m, U)) .
□

Theorem 3.12 For every n ∈ ω there exists a Σ-formula Univ_{n}(m, x_{1}, …, x_{n}) such that for any ^{<}algebraic formula Φ(x_{1}, …, x_{n})

HF(IR) ⊧ Φ(r_{1}, …, r_{n}) ↔ Univ_{n}(⌈Φ⌉, r_{1}, …, r_{n}).

Proof. From the properties of the standard Gödel numbering it follows that the code of an ^{<}algebraic formula can be effectively constructed from the code of the corresponding lifted formula and vice versa. Let f : ω → ω be a recursive function which maps the code of an ^{<}algebraic formula to the code of the corresponding lifted formula. Then the following formula defines a universal Σ-predicate for the <algebraic formulas of arity n.

Univ_{n}(m, x̄) ⇌ ∃X_{1} … ∃X_{n}∃k f(m) = k ∧ Univ_{n}^{∗}(k, X̄) ∧ ⋀_{i≤n} (x_{i} ∈ X_{i}) .

□

4 Expressive Power of Σ-definability over the Reals

4.1 Constructive Infinitary Language L_{ω_{1}ω}

In order to study the expressive power of Σ-formulas, we will consider a suitable fragment L_{ω_{1}ω}^{al} of the constructive infinitary language L_{ω_{1}ω} (cf. [13] ) described below. Informally, the language L_{ω_{1}ω}^{al} is obtained by extending the ^{<}algebraic formulas to allow formulas with effective infinite disjunctions but only finitely many variables; that is, formulas of the form ⋁_{i∈I} Φ_{i}, where {Φ_{i}|i ∈ I} is an effectively indexed family of ^{<}algebraic formulas, possibly infinite. The meaning of these formulas is as follows: HF(IR) ⊧ ⋁_{i∈I} Φ_{i} if and only if for at least one i ∈ I we have HF(IR) ⊧ Φ_{i}.

Formally, we propose the inductive definition of formulas as follows. Let Var be a fixed finite set of variables. The set L_{Var} of formulas over Var includes the set of ^{<}algebraic formulas all of the variables of which belong to Var. In addition, if {Φ_{i}|i ∈ I} is an indexed family of formulas of L_{Var} and I is recursively enumerable, then ⋁_{i∈I} Φ_{i} is a formula of L_{Var}. The language L_{ω_{1}ω}^{al} is the union of all L_{Var} for all finite sets Var of variables which range over IR.

Let us discuss the computational meaning of the formula Φ(x̄) = ⋁_{i∈L} Φ_{i}(x̄). Each formula Φ_{i}(x̄) represents a simple approximation of the relation definable by Φ(x̄) and there exists a Turing machine that computes these approximations (i.e., enumerates Φ_{i}(x̄)). A universal Turing machine and a universal Σ-predicate for ^{<}algebraic formulas can then be used to enumerate and check validity of each approximation Φ_{i}.

4.2 Engeler’s Lemma for Σ-definability

In this section we prove Engeler’s lemma for Σ-definability which states that if a relation M ⊂ IR^{n} is Σ-definable, then it is definable by a formula of L_{ω_{1}ω}^{al} which can be constructed effectively from the corresponding Σ-formula.

In order to work effectively with elements of the structures HF(IR) and HF(IR^{∗}), we represent every element in a regular way. For this, we enrich the language σ to σ′ by the additional functions: singleton {U} and binary union U_{1} ∪ U_{2}. Note that these functions will be eliminated in the resulting formulas of Engeler’s Lemma. Below a term in the language {{, }, ∪} is called a structural term. With every α ∈ HF(n) we associate a structured term defined as follows:

t_{α}(x_{1}, …, x_{n}) = \{ \begin{matrix}x_{i} & if α = i \\ \{t_{α_{1}}(x̄)\} ∪ ⋯ ∪ \{t_{α_{k}}(x̄)\} & if α = \{α_{1}, …, α_{k}\}. \end{matrix}

Lemma 4.1 1. For every element M ∈ HF(IR) there exist a structural term t_{α}(x_{1}, …, x_{k}) and a substitution τ : {x_{1}, …, x_{k}} → IR such that M is represented by t_{α}(x̄)τ.

2. For every element U ∈ HF(IR^{∗}) there exist a structural term t_{β}(N_{1}, …, N_{l}) and a substitution ν : {N_{1}, …, N_{l}} → IR^{∗} such that U is represented by t_{β}(N̄)ν.

If τ(N_{i}) = r_{i} for i ≤ k and ν(N_{j}) = R_{j} for j ≤ l, then we write t(r_{1}, …, r_{k}) and t(R_{1}, …, R_{l}) instead of t_{α}(N̄)τ and t_{β}(N̄)ν respectively.

Lemma 4.2 Let t_{β}(X̄) and t_{γ}(X̄) be structural terms and R̄ ∈ HF(IR^{∗})^{n}. If t_{β}(R̄) represents U_{1}, t_{γ}(R̄) represents U_{2} and HF(IR) ⊧ U_{1} ∈ U_{2}, then we have HF(IR) ⊧ t_{β}(b̄) ∈ t_{γ}(b̄) for every b̄ ∈ HF(IR)^{n} such that for all i, j ≤ n b_{i} = b_{j} ↔ R_{i} = R_{j}.

With every Σ-formula Φ(x̄) we associate a lifted Σ-formula Φ_{lifted}(X̄) obtained from Φ by replacing every variable ranging over HF(IR) by a variable ranging over HF(IR^{∗}); every variable ranging over IR by a variable ranging over IR^{∗}. For example, ∃U (∀Y ∈ U) p_{1}(Y, X̄) < p_{2}(Y, X̄) is the lifted Σ-formula corresponding to ∃M (∀y ∈ M) p_{1}(y, x̄) < p_{2}(y, x̄).

Proposition 4.3 Let Φ_{lifted}(X̄) be the lifted Σ-formula corresponding to a Σ-formula Φ(x̄). Then we have

HF(IR) ⊧ Φ(x_{1} …, x_{n}) ↔ ∃X_{1} … ∃X_{n} Φ_{lifted}(X̄) ∧ ⋀_{i≤n} (x_{i} ∈ X_{j}) .

Proof. Let Φ(x̄) be a Σ-formula. By the Σ-reflection principle (c.f. Section 2.2.), the formula Φ(x̄) can be represented in the form:

Φ(x̄) ⇌ ∃c Φ′(c, x̄) ∧ ⋀_{i≤n} (x^{i} ∈ c) ⇌ ∃c Φ′′(c, x̄),  (6)

where Φ′ and Φ′′ are Δ_{0}-formulas. The corresponding lifted formula Φ_{lifted}(X̄) is obtained from Φ by replacing every variable ranging over HF(IR) by a variable ranging over HF(IR^{∗}); every variable ranging over IR by a variable ranging over IR^{∗}, i.e.,

Φ^{lifted}(X̄) ⇌ ∃ U Φ{′ \atop lifted}(U, X̄) ∧ ⋀_{i≤n} (X^{i} ∈ U) ⇌ ∃ U Φ{′′ \atop lifted}(U, X̄).  (7)

→) Suppose (6) is valid in HF(IR) and d, r̄ satisfy the formula Φ′′(c, x̄). In order to construct some V and R̄ which satisfy the corresponding lifted Σ-formula, we use the operation up defined by induction:

up(a) = \{ \begin{matrix}\{a\} & if a ∈ IR \\ \{up(a_{1}), … up(a_{l})\} & if a = \{a_{1}, …, a_{l}\}. \end{matrix}

We put V = up(d), R_{1} = up(r_{1}),…, R_{n} = up(r_{n}). By Lemma 3.2 and Lemma 4.2, V and R_{1}, …, R_{n} satisfy the formula Φ′′_{lifted}(U, X̄). ←) Suppose (7) is valid in HF(IR) and V, R_{1}, …, R_{n} satisfy the given formula Φ′′_{lifted}(U, X̄). By Lemma 4.1, the set V can be represented by t_{β}(R_{1}, …, R_{m}), where {R_{1}, …, R_{n}} ⊆ {R_{1}, …, R_{m}}. From Lemma 4.2 it follows that if V = t_{β}(R_{1}, …, R_{m}) satisfies the following requirement:

there exist r_{1} ∈ R_{1}, … r_{m} ∈ R_{m} such that

r_{i} = r_{j} ↔ R_{i} = R_{j} for all i, j ≤ m, (8)

then t_{β}(r̄) and r_{1}, …, r_{n} satisfy Φ′′(c, x̄). Let us note that V may not satisfy (8), for example, if V = {{r_{1}, r_{2}}, {r_{1}}, {r_{2}}}, where r_{1} ≠ r_{2} ≠ r_{3}. The problem here is that the number of elements in the sets is too small to pick different representatives. In this case we construct R′_{1}, … R′_{n} and V′ from R_{1}, …, R_{n} and V which satisfy the formula Φ′′_{lifted}(U, X̄) and the requirement (8). It can be done using Lemma 3.5. Indeed, there exist R′_{1} …, R′_{m} such that

1. for every i ≤ m we have |R′_{i}| ≥ m;

2. for every i, j ≤ m R′_{i} = R′_{j} if and only if R_{i} = R_{j};

3. for every ^{<}algebraic subformula ϕ_{alg}(Ȳ , X̄) of the formula Φ′′ and every substitution τ : {Ȳ , X̄} → {R_{1}, …, R_{m}} we have

HF(IR) ⊧ ϕ_{alg}(Ȳ , X̄)τ ↔ HF(IR) ⊧ ϕ_{alg}(Ȳ , X̄)τ′,

where τ′ : {Ȳ , X̄} → {R′_{1}, …, R′_{m}} is a substitution such that τ′(Y_{k}) = R′_{j} ↔ τ(Y_{k}) = R_{j} and τ′(X_{l}) = R′_{i} ↔ τ(X_{l}) = R_{i} for all i, j, k, l ≤ m.

By construction, t_{β}(R′_{1}, …, R′_{m}) and R′_{1}, …, R′_{n} satisfy Φ′′_{lifted}(U, X̄) and (8).

Now every R′_{i} contains enough elements to choose r_{i} from R′_{i} under the condition r_{i} = r_{j} ↔ R_{i} = R_{j}. It is easy to see that t_{β}(r̄) and r_{1}, …, r_{n} satisfy Φ′′(c, x̄).

□

In the following proposition the lifted ^{<}algebraic atomic formulas and the Δ_{0}- formulas of the type X = Y ⇌ (∀x ∈ X) x ∈ Y ∧ (∀y ∈ Y) y ∈ X and ¬X = Y ⇌ (∃x ∈ X) x ∉ Y ∨ (∃y ∈ Y) y ∉ X are considered as basic formulas.

Proposition 4.4 Let Φ(X_{1}, …, X_{n}) be a lifted Σ-formula. There exists a constructive infinite formula Ψ ⇌ ⋁_{i∈ω} Ψ_{i} such that:

• HF(IR) ⊧ Φ(X̄) ↔ Ψ(X̄).

• Every Ψ_{i}(X̄) is a formula of the form ∃Y_{m_{1}} … ∃Y_{m_{i}}Ψ′_{i}(Ȳ , X̄), where Ψ′ is a finite conjunction of basic formulas whose quantifiers range over IR^{∗}.

Proof. Let Φ(X) ⇌ ∃UΦ′(U, X̄), where Φ′ is a Δ_{0}-formula. In order to obtain the required formula, we first construct an equivalent infinite formula in the language σ′ (e.g. σ′ = σ ∪ {{, }, ∪}) without unbounded quantifiers. Then we prove by induction the existence of an equivalent infinite formula without bounded quantifiers. After that we eliminate {, },∪,∅, ∈ from the obtained formula. By Lemma 3.2, every U ∈ HF(IR^{∗}) can be represented by t_{β}(Y_{1}, … Y_{n}) for some Y_{1} ∈ IR^{∗}, … Y_{n} ∈ IR^{∗}. Put

Φ^{∗}(X) ⇌ ⋁_{n∈ω} ⋁_{β∈HF(n)} ∃Y_{1} … ∃Y_{n} Φ′(t_{β}(Y_{1}, …, Y_{n}), X̄)
⇌ ⋁_{n∈ω} ⋁_{β∈HF(n)} ∃Y_{1} … ∃Y_{n} Φ′_{β}(Ȳ , X̄),

where every Φ′_{β} is a Δ_{0}-formula with quantifiers bounded by subterms of t_{β}. Since for every U there exists a term t_{β} which codes the structure of U, the formula Φ^{∗} is equivalent to the given one.

Without loss of generality every formula Φ′_{β} can be represented as follows.

Φ′_{β}(Ȳ , X̄) ⇌ (Q U_{1} ∈ t_{γ_{1}}(Ȳ)) … (Q U_{m} ∈ t_{γ_{m}}(Ȳ)) ϕ_{β}(Ū, Ȳ , X̄)
⇌ (Q U ∈ t_{γ_{1}}(Ȳ)) ϕ′_{β}(Ū, Ȳ , X̄),

where Q is the quantifier ∃ or ∀ and t_{γ_{i}} is a subterm of t_{β} for all i ≤ k. Using induction on the length of the quantifier prefix and the depth of the term which bounds the first quantifier in the quantifier prefix, we show how to obtain an equivalent quantifier free formula. We proceed by induction on the pairs ⟨m, n⟩ with the lexicographic order, where m is the length of the quantifier prefix of Φ′_{β} and n is the depth of t_{γ_{1}}. Let ⊤ denote a logical truth which can be represented by the formula 0 < 1 and ⊥ denote a logical false which can be represented by the formula 1 < 0.

The cases ⟨0, 0⟩, ⟨0, n⟩ are obvious. In the case ⟨m, 0⟩ the formula Φ′_{β} can be represented in the form Φ′_{β} ⇌ (Q U_{1} ∈ ∅) ϕ′_{β} or Φ′_{β} ⇌ (Q U_{1} ∈ X) ϕ′_{β}. If Q is the existential quantifier, then put Ψ_{β} ⇌ ⊥. If Q is the universal quantifier, then put Ψ_{β} ⇌ ⊤.

Consider the inductive step ⟨m, n⟩ → ⟨m, n + 1⟩. The first possibility is that Φ′_{β} ⇌ (∃U_{1} ∈ t_{γ_{1}}(Ȳ)) ϕ′_{β}(U_{1}, Ȳ , X̄) and t_{γ_{1}}(Ȳ) = t′_{γ_{1}}(Ȳ)∪t′′_{γ_{1}}(Ȳ). Let us consider the formula (∃U_{1} ∈ t′_{γ_{1}}(Ȳ)) ϕ′_{β}(U_{1}, Ȳ , X̄) ∨ (∃U_{1} ∈ t′′_{γ_{1}}(Ȳ)) ϕ′_{β}(U_{1}, Ȳ , X̄) which is equivalent to Φ′_{β}. The complexity of t′_{γ_{1}} and t′′_{γ_{1}} is less than n + 1. By inductive hypothesis, there exists a formula Ψ_{β} without quantifiers which is equivalent to Φ′_{β}. The second possibility with a bounded universal quantifier can be considered in a similar way.

Consider the inductive step ⟨m, n⟩ → ⟨m + 1, k⟩. We have Φ′_{β} ⇌ (∃U_{1} ∈ {t(Ȳ)}) ϕ′_{β}(U_{1}, Ȳ , X̄). Let us consider ϕ′_{β}(t(Ȳ), Ȳ , X̄) which is equivalent to Φ′_{β}. The complexity of the quantifier prefix is less then m + 1. By inductive hypothesis, there exists a formula Ψ_{β} without quantifiers which is equivalent to Φ′_{β}. The case, when Φ′_{β} ⇌ (∀U_{1} ∈ {t(Ȳ)}) ϕ′_{β}(U_{1}, Ȳ , X̄), is similar.

Now we eliminate {, },∪, ∅, ∈ from every formula Ψ_{β}. It is easy to see that for any terms t_{γ}(Ȳ , X̄) and t_{κ}(Ȳ , X̄) of the language σ′ it is possible to write effectively χ_{∈}(Ȳ , X̄) and χ_{=}(Ȳ , X̄) such that χ_{∈}(Ȳ , X̄) and χ_{=}(Ȳ , X̄) are finite disjunctions of finite conjunctions of basic formulas and the formula t_{γ} ∈ t_{κ} is equivalent to χ_{∈}(Ȳ , X̄) and the formula t_{γ} = t_{κ} is equivalent to χ_{=}(Ȳ , X̄). For example, it is easy to see that the formula {Y_{1}} ∪ {Y_{2}} ∈ {{{Y_{3}} ∪ {Y_{4}}}} ∪ {{Y_{5}}} is equivalent to (Y_{1} = Y_{3} ∧ Y_{2} = Y_{4}) ∨ (Y_{1} = Y_{4} ∧ Y_{2} = Y_{3}).

Using these formulas we transform every formula Ψ_{β} into Ψ′_{β} without occurrences of {, },∪, ∅, ∈.

Put

Ψ(X) ⇌ ⋁_{n∈ω} ⋁_{β∈HF(n)} ∃Y_{1} … ∃Y_{n} Ψ′_{β}(Ȳ , X).

By construction, Ψ has the required form.

□

Now we are ready to prove Engeler’s Lemma for Σ-definability over the reals.

Theorem 4.5 (Engeler’s Lemma for Σ-definability) If a relation B ⊂ IR^{n} is Σ-definable, then it is definable by a formula of L_{ω_{1}ω}^{al}. Moreover this formula can be constructed effectively from the corresponding Σ-formula.

Proof. Suppose M is defined by a Σ-formula Φ(x̄). By Proposition 4.3 and Proposition 4.4, there exists an effective sequence {Ψ_{i}}_{i∈ω} such that

HF(IR) ⊧ Φ(x̄) ↔ ⋁_{i∈ω} (∃X_{1} … ∃X_{n} Ψ_{i}(X̄) ∧ ⋀_{j≤n} x_{j} ∈ X_{j}) ,

where every Ψ_{i}(X̄) is a formula of the form ∃Y_{m_{1}} … ∃Y_{m_{i}}Ψ′_{i}(Ȳ , X̄), and Ψ′ is a finite conjunction of lifted ^{<}algebraic formulas and formulas of the type X_{j} = Y_{i}, Y_{i} = Y_{j}, ¬X_{j} = Y_{i} and ¬Y_{i} = Y_{j}.

Now we show that for every i ∈ ω there exists an existential quantified ^{<}algebraic formula φ_{i} in the language σ_{0} = {0, 1, +, ·, <} such that

HF(IR) ⊧ φ_{i}(x̄) ↔ HF(IR) ⊧ (∃X_{1} … ∃X_{n}Ψ_{i}(X̄) ∧ ⋀_{j≤n} x_{j} ∈ X_{j}) .  (9)

For this purpose, in every Ψ_{i} we first eliminate subformulas of the type X_{j} = Y_{k} and Y_{j} = Y_{k} in the following way. For all j and k, such that there exists a subformula X_{j} = Y_{k}, we replace all occurrences of Y_{k} by X_{j}, the subformula X_{j} = Y_{k} by ⊤ and eliminate the quantifier over Y_{i}. For all i and k such that, there exists Y_{j} = Y_{k} for some j and k > j, we replace all occurrences of Y_{k} by Y_{j}, the subformula Y_{j} = Y_{k} by ⊤ and eliminate the quantifier over Y_{k}. It is easy to see that the resulting formula Ψ′_{i}(X̄) is equivalent to Ψ_{i}(X̄). Now if X_{j} = X_{k} occurs in Ψ′_{i}(…, X_{j}, …, X_{k}, …) then we replace Ψ′_{i} by Ψ′_{i}(…, X_{j}, …, X_{j}, …) ∧ Ψ′_{i}(…, X_{k}, …, X_{k}, …) and remove all X_{j} = X_{k} from this formula. Let us argue that the obtained formula Ψ′′_{i} is equivalent to Ψ′_{i} in the following sense

HF(IR) ⊧ ∀x_{1} … ∀x_{n} [(∃X_{1} … ∃X_{n}Ψ′_{i}(X̄) ∧ ⋀_{j≤n} x_{j} ∈ X_{j}) ↔

(∃X_{1} … ∃X_{n}Ψ′′_{i}(X̄) ∧ ⋀_{j≤n} x_{j} ∈ X_{j})] .

Implication from left to right is obvious. In order to prove implication from right to left, we need to show that if for x_{1}, …, x_{n} there exist X_{1}, …, X_{n} such that Ψ′′_{i}(X̄) ∧ ⋀_{j≤n} x_{j} ∈ X_{j}, then there exist X′_{1}, …, X′_{n} such that X′_{j} = X′_{k} and Ψ′_{i}(X̄′)∧⋀_{j≤n} x_{j} ∈ X′_{j}. For this we can take X′_{j} = X′_{k} = X_{j} ∪ X_{k}. In the same way we can eliminate all subformulas of the form X_{j} = X_{k} obtaining a formula Ψ′′′. We then construct formulas φ_{i} from Ψ′′′_{i} by replacing X by x, Y_{i} by y_{i} and subformulas of the type ¬x = y by x < y ∨ x > y. From the definition of a lifted ^{<}algebraic formula and Proposition 4.3 it follows that the formula φ_{i} satisfies (9). In order to complete the proof, using Lemma 3.6, we construct an effective sequence {φ′_{i}}_{i∈ω} of ^{<}algebraic formulas such that

HF(IR) ⊧ Φ(x) ↔ ⋁_{i∈ω} φ′_{i}(x).

□

4.3 Characterisation Theorem for Σ-definability

Let us prove the converse statement of Engeler’s Lemma for Σ-definability.

Theorem 4.6 If a relation B ⊂ IR^{n} is definable by a formula of L_{ω_{1}ω}^{al}, then it is Σdefinable. Moreover Σ-formula can be constructed effectively from the corresponding formula of L_{ω_{1}ω}^{al}.

Proof. Let M ⊂ IR^{n} be definable by ⋁_{⌈Ψ⌉∈I} Ψ(x̄), where J is recursively enumerable. By Theorem 3.12, there exists a universal Σ-predicate Univ_{n}(m, x̄) for <algebraic formulas with variables from {x_{1}, …, x_{n}}.

Put

Φ(x̄) ⇌ ∃i (i ∈ I) ∧ Univ^{n}(i, x̄).

It can be shown that Φ is a required Σ-formula.

□

Theorem 4.7 (Characterisation of Σ-definability) A relation B ⊂ IR^{n} is Σdefinable if and only if it is definable by a formula of L_{ω_{1}ω}^{al}.

These results reveal algorithmic aspects of Σ-definability. Indeed, suppose Φ(x̄) is a Σ-formula which defines a relation over the reals and we have HF(IR) ⊧ Φ(x̄) ↔ ⋁_{⌈Ψ⌉∈I} Ψ(x̄). Then each ^{<}algebraic formula Ψ(x̄), such that ⌈Ψ⌉ ∈ I, represents a simple approximation of the relation definable by Φ(x̄) and there exists a Turing machine that computes these approximations (i.e., enumerates Ψ(x̄)). A universal Turing machine and a universal Σ-predicate for ^{<}algebraic formulas can then be used to enumerate and check validity of each approximation Ψ.

We also obtain the following topological characterisation of Σ-definability over the reals.

Theorem 4.8 1. A set ℬ ⊂ IR^{n} is Σ-definable if and only if it is an effective union of open semi-algebraic sets.

2. A relation ℬ ⊂ IR^{n} is Σ-definable if and only if there exists an effective sequence {𝒞_{i}}_{i∈ω} of open semi-algebraic sets such that

(a) It monotonically increases: 𝒞_{i} ⊆ C_{i+1}, for i ∈ ω;

(b) ℬ = ⋃_{i∈ω} 𝒞_{i}.

Corollary 4.9 Every Σ-definable subset of IR^{n} is open.

Let Σ_{IR} denote the set of all Σ-definable subsets of IR^{n}, where n ∈ ω.

Corollary 4.10 1. The set Σ_{IR} is closed under finite intersections and effective infinite unions.

2. The set Σ_{IR} is closed under Σ-inductive definitions.

3. The set Σ_{IR} is closed under projections.

References

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

[2] A. Blass and Y. Gurevich. Background, reserve and gandy machines. In Proc. CSL’2000, volume 1862 of Lecture Notes in Computer Science, pages 1–17, 2000.

[3] A. Blass, Y. Gurevich, and S. Shelah. Choiceless polynomial time. APAL, pages 141–187, 1999.

[4] L. Blum, F. Cucker, M. Shub, and S. Smale. Complexity and Real Computation. Springer Verlag, Berlin, 1996.

[5] J. Bochnak, M. Coste, and M.-F. Roy. Real Algebraic Geometry. Springer Verlag, Berlin, 1999.

[6] V. Brattka and P. Hertling. Topological properties of real number representations. TCS, 284(2):1–17, 2002.

[7] E. Dahlhaus and J. A. Makowsky. Query languages for hierarchic databases. Information and Computation, pages 1–32, 1992.

[8] A. Davar and Y. Gurevich. Fixed-point logics. BSL, pages 65–88, 2002.

[9] C. N. Delzell. A finiteness theorem for open semi-algebraic sets, with application to hilbert’s 17th problem. In D. W. Dobois and T. Recio, editors, Ordered Fields and Real Algebraic Geometry, volume 8 of Contemp. Math, pages 79–97. AMS, 1982.

[10] H. Ebbinghaus and J. Flum. Finite Model Theory. Springer Verlag, Berlin, 1999.

[11] A. Edalat and M. Escardo. Integration in real pcf. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 382–393, 1996.

[12] A. Edalat and A. Lieutie. Domain theory and differential calculus (function of one variable. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 277–298, 2002.

[13] E. Engeler. Formal Languages: Automata and Structures. Markham Publishing Co, 1968.

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

[15] H. Freedman and K. Ko. Computational complexity of real functions. TCS, pages 323–352, 1992.

[16] H. Friedman. Algorithmic procedures, generalized turing algorithms, and elementary recursion theor. In C. M. E. Yates R. O. Gandy, editor, Logic colloquium 1969, pages 361–390. C.M.E, Hollang, Amsterdam, 1971.

[17] R. Gandy. Inductive definitions. In J. E. Fenstad and P. D. Hinman, editors, Generalized Recursion Theory, pages 265–300. North-Holland, Amsterdam, 1974.

[18] A. Grzegorczyk. On the definitions of computable real continuous function. Fundamenta Mathematik, pages 61–71, 1957.

[19] D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. The MIT press, Cambridge, MA, 2002.

[20] P. G. Hinman. Recursion on abstract structure. In E. R. Griffor, editor, Handbook of Computability Theory, pages 317–359. Elsevie, Amsterdam-Tokyo, 1999.

[21] N. Immerman. Descriptive Complexity. Springer Verlag, New-York, 1999.

[22] Ulrich Kohlenbach. Proof theory and computational analysis. Electronic Notes in Theoretical Computer Scienc, 1998.

[23] M Korovina. Computational aspects of σ-definability over the real numbers without the equality test. www.brics.dk/˜ korovina/definability.ps.

[24] M Korovina. Fixed points on the abstract structures without the equality test. Technical report, BRICS, 2002.

[25] M Korovina. Fixed points on the reals numbers without the equality test. Electronic Notes in TCS, 66(1), 2002.

[26] M. Korovina and O. Kudinov. Characteristic properties of majorantcomputability over the reals. In roc. of CSL’98, volume 1584 of Lecture Notes in Computer Science, pages 188–204, 1999.

[27] M. Korovina and O. Kudinov. Some properties of majorant-computability. In M. Arslanov and S.Lempp, editors, Recursion Theory and Complexity”, Proceedings of the Kazan-97 Workshop, July 14-19, pages 97–115. de Gruyter Series in Logic and its Applications, Berlin - New York, 1999.

[28] D. Locombe. Recursion theoretical structure for relational systems. In R. O. Gandy and C. M. E. Yates, editors, Proc. of Logic Colloquium’69, pages 3–17. ”North-Holland”, Amsterdam-London, 1971.

[29] K. Meer. Counting problems over the reals. TCS, 242(1-2):41–58, 2000.

[30] Y. N. Moschovakis. Abstract first order computability. i, ii. Transactions of the American Mathematical Society, 138:427–46, 1969.

[31] Y. N. Moschovakis. Elementary Induction on Abstract Structur, volume 77 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam-London; American Elsevier Publishing Co, 1974.

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

[33] V. Sazonov. Using agents for concurrent querying of web-like databases via hyper-set-theoretic approach. In Proc. of PSI’01, volume 2244 of Lecture Notes in Computer Science, pages 378–394, 2001.

[34] G. Takeuti and A. Kino. On predicates with constructive infinitary long expressions. J. Math. Soc. Japan, pages 176–190, 1963.

[35] J. V. Tucker and J. I. Zucker. Computable functions and semicomputable sets on many-sorted algebras. In T. S. E. Maibaum S. Abramsky, D. M. Gabbay, editor, Handbook of Logic in Computer Science, pages 397–525. Oxford University Press, Oxford, 2000.

[36] M. Vardi. The complexity of relational query languages. In In Proc. of the 14th ACM Symposium on the Theory of Computing, pages 37–146, 1982.

[37] Klaus Weihrauch. Computable Analysis. Springer Verlag, Berlin, 2000.

Recent BRICS Report Series Publications

RS-03-23 Margarita Korovina. Recent Advances in Σ-definability over Continuous Data Types. June 2003. 24 pp.

RS-03-22 Ivan B. Damgård and Mads J. Jurik. Scalable Key-Escrow. May 2003. 15 pp.

RS-03-21 Ulrich Kohlenbach. Some Logical Metatheorems with Applications in Functional Analysis. May 2003. 55 pp. Slighly revised and extended version to appear in Transactions of the American Mathematical Society.

RS-03-20 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. May 2003. 16 pp. Final version in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003. This report supersedes the earlier BRICS report RS-03-11.

RS-03-19 Christian Kirkegaard, Anders Møller, and Michael I. Schwartzbach. Static Analysis of XML Transformations in Java. May 2003. 29 pp.

RS-03-18 Bartek Klin and Pawe� Sobociński. Syntactic Formats for Free: An Abstract Approach to Process Equivalence. April 2003. 41 pp.

RS-03-17 Luca Aceto, Jens Alsted Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. The Complexity of Checking Consistency of Pedigree Information and Related Problems. March 2003. 31 pp. This paper supersedes BRICS Report RS-02-42.

RS-03-16 Ivan B. Damgård and Mads J. Jurik. A Length-Flexible Threshold Cryptosystem with Applications. March 2003. 31 pp.

RS-03-15 Anna Ingólfsdóttir. A Semantic Theory for Value–Passing Processes Based on the Late Approach. March 2003. 48 pp.

RS-03-14 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. March 2003. 36 pp.

RS-03-13 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Evaluators and Abstract Machines. March 2003. 28 pp.