Notions of semicomputability in topological algebras over the reals

Abstract

Several results from classical computability theory (computability over discrete structures such as the natural numbers and strings over finite alphabets, due to Turing, Church, Kleene and others) have been shown to hold for generalisations of computability theory over total abstract algebras, using a computation model of a high level imperative ( While ) language.

We present a number of results relating to computation on topological partial algebras using an abstract model of computation, While , based on high level imperative languages. We investigate the validity of several results from the classical theory in the context of topological algebras on the reals: closure of semicomputable sets under finite union, the equivalence of semicomputable and projectively (semi)computable sets, and Post’s Theorem.

This research has significance in the field of scientific computation, which is underpinned by computability on the real numbers. By the Continuity Principle, computability of functions implies their continuity. Since equality, order, and other total boolean-valued functions on the reals are clearly discontinuous, we resolve this incompatibility by redefining such functions to be partial, leading us to consider topological partial algebras.

Keywords

Generalised computability computability on topological algebra computability on the reals

1. Introduction

1.1. Generalising computability theory

In classical computability theory, many formalisms have been presented and been proven to be equivalent, including the formalism of Turing machines, λ-calculus, and the μ-recursive functions, presented by Alan Turing [35], Alonzo Church [7] and Stephen C. Kleene [20] during the 1930’s. These all capture the informal notion of computation by a finite, deterministic algorithm on $N$ or on $Σ^{*}$ (the set of strings from a finite alphabet Σ).

We investigate generalisations of the classical computability theory to other abstract structures, especially the domain of real numbers $R$ . An important reason for this is that scientific computation is done largely on the reals.

An important difference between $R$ and $N$ is that real numbers can in general only be constructed or described as infinite objects; for instance, as infinite sequences of rational numbers. Thus when working with $R$ , at least with concrete computation models (described below), we must work with the idea of finite approximations. Further, the topology of the reals gives us the concept of “nearness”, and hence closeness of approximations. Hence the topology of the reals is a crucial concept in computation over the reals.

A model of computation is a mathematical model of some general method (algorithm) for computing functions, or deciding membership of a set. We distinguish two main kinds of such models: abstract and concrete [32,37].

In abstract models of computation, the data are taken as primitive, so that the programs and algorithms do not depend on representations. Examples of abstract models are high level imperative programming languages, flow charts and register machines over any algebra [2,9,31].

In concrete models, data are given by representations, and so the programs and algorithms depend crucially on the choice of representation, e.g. the representation of reals by (indices of) effective Cauchy sequences of rationals [28,36].

An important part of our work in this paper is to consider whether certain well-known results from classical computability theory still hold in the generalised theory, e.g. the closure of semicomputable sets under union. In addition, we investigate the properties of semicomputable subsets of the real plane, e.g. the equivalence or inequivalence with respect to some notion of semicomputability for variations of a high-level imperative language for topological algebras over the reals.

1.2. Related work

There is a rich history of work in generalised computability theory, with many models having been proposed. Good overviews of several of them are provided in [31,36].

We will focus in this paper on models based on the simple imperative language While , which have been investigated thoroughly by the second author [31,34]. In [12,13], an extension of the While model (with non-determinism and approximability) was shown to be equivalent to several other models of computation over the reals, including Grzegorczyk–Lacombe (GL) computability [16,17,22–24,26] and tracking computability [28,29,32,33], under some reasonable assumptions.

1.3. Overview

In Section 2 we review many-sorted algebras, relations and projections, topological partial algebras (in particular the algebra $R$ on $R$ with the ring structure of the reals), and the abstract models While , ${While}^{OR}$ and ${While}^{NE}$ over $R$ , as well as “starred” versions of those languages (i.e. with arrays).

In Section 3 we give definitions and lemmas for the $While (R)$ language, in preparation for a Structure Theorem for $While (R)$ in Section 4. Using that Structure Theorem, we prove that the class of $While (R)$ semicomputable sets is not closed under union.

In Section 5 we present results regarding the (in)equivalence of models of computation on $R$ based on the While language.

In Section 6 we summarise our conclusions, and give some ideas for future work.

In Appendix A we consider an adaptation of our (in)equivalence results to the 1-dimensional case over $R$ .

In Appendix B we outline a proof of the equivalence of $While (R)$ with its starred version.

In Appendix C we check that another result from the classical theory, Post’s Theorem, also holds in the case of $R$ .

1.4. Previous work

This paper developed out of the first author’s Master’s thesis. It serves as an extension of the work contained in [37].

Specifically, the structure theorems presented there for 1-dimensional computation were previously extended to 2-dimensional computation in [13], with an incomplete structure theorem for While ; we now present a complete version.

Additionally, in [37] it was shown that the model ${While}^{NE}$ is computationally equivalent to its projective version; we extend this result by showing the (in)equivalence of various models and their projective versions.

2. Signatures; algebras; the While language

We will study the computation of functions and relations by high level imperative programming languages based on the ‘while’ construct, applied to a many-sorted signature Σ. We give semantics for this language relative to a topological partial Σ-algebra, and define the notions of computability, semicomputability and projective semicomputability for this language. Much of the material is taken from [31,34].

We begin by reviewing basic concepts of many-sorted signatures and algebras. Next we define the syntax and semantics of the abstract computation model While . Then we present several extensions to this language.

2.1. Basic algebraic definitions

A many-sorted signature Σ is a pair $⟨ Sort (Σ), Func (Σ) ⟩$ , where $Sort (Σ)$ is a finite set of basic types or sorts $s_{1}, \dots$ , and $Func (Σ)$ is a finite set of basic function symbols, $F : s_{1} \times \dots \times s_{m} \to s$ ( $m ⩾ 0$ ) (the case $m = 0$ gives a constant symbol; we then write $F : \to s$ ).

A product type of Σ has the form $s_{1} \times \dots \times s_{m}$ , where $m > 0$ and $s_{1}, \dots, s_{m}$ are Σ-sorts. We write $u, v, \dots$ for product types. A function type has the form $u \to s$ , where u is a product type, or simply $\to s$ (for constant functions).

For a signature Σ, a Σ-algebra A has, for each Σ-sort s, a non-empty set $A_{s}$ , called the carrier of sort s, and for each function symbol $F : s_{1} \times \dots \times s_{m} \to s$ , a function $F^{A} : A_{s_{1}} \times \dots \times A_{s_{m}} ⇀ A_{s}$ .1

¹
We use ⇀ in place of → to signify that a function is partial.

We write $Σ (A)$ for the signature of an algebra A.

An algebra A is said to be total if $F^{A}$ is total for all $F \in Func (Σ)$ ; otherwise, it is partial.

Example 2.1.

The signature and (total) algebra of the booleans are as follows: The (total) algebra of the naturals is as follows: where the carrier sets $B$ and $N$ , the functions and constants $t^{B}$ , $f^{B}$ , ${and}^{B}$ , ${or}^{B}$ , ${not}^{B}$ , $0^{N}$ , $S^{N}$ , ${eq}^{N}$ and ${less}^{N}$ have their usual meanings.

We will use the infix notations ∨ and ∧ in place of ‘or’ and ‘and’ and also write ‘¬’ in place of not, and drop the superscripts ‘ $B$ ’ and ‘ $N$ ’ where unambiguous. Definition 2.2 (Standard signatures and algebras).

A signature is called standard if it includes the sorts and functions of $Σ (B)$ .

Correspondingly, an algebra is called standard if it is an expansion of $B$ (i.e. it contains the carrier $B$ with the standard boolean operators) and additionally, any equality operators, for sorts on which they are defined, are (partial) identities on these sorts.

Definition 2.3 ( $N$ -standard signatures and algebras).

A signature is called $N$ -standard if, in addition to being standard, it includes the sorts and functions of $Σ (N)$ .

Correspondingly, an algebra is called $N$ -standard if, in addition to being standard, it is an expansion of $N$ (i.e. it contains the carrier $N$ with the standard arithmetic operators).

Remark 2.4.
All signatures and algebras in this paper will be assumed to be $N$ -standard (and hence also standard). So Σ refers to any $N$ -standard signature and A to any $N$ -standard algebra.

2.2. Relations and projections

Notation 2.5.
For a Σ-product type $u = s_{1} \times \dots \times s_{m}$ , we write $\begin{matrix} A_{u} =_{df} A_{s_{1}} \times \dots \times A_{s_{m}} \end{matrix}$

A relation R on A of type u (written $R : u$ ) is a subset of $A_{u}$ .

The complement of a relation $R : u$ is the relation $\begin{matrix} R^{c} = A_{u} ∖ R = {a \in A_{u} ∣ a \notin R} \end{matrix}$ Definition 2.6 (Projection).

Let R be a relation of type $u = s_{1} \times \dots \times s_{m}$ where $m > 0$ . Let $\vec{i} = i_{1}, \dots, i_{r}$ be a list of numbers such that $1 ⩽ i_{1} < \dots < i_{r} ⩽ m$ , and let $\vec{j} = j_{1}, \dots, j_{m - r}$ be the list ${1, \dots, m} ∖ \vec{i}$ . Then the projection of R off $\vec{i}$ is the relation $S : s_{j_{1}} \times \dots \times s_{j_{m - r}}$ where $\forall x_{j_{1}} : s_{j_{1}}, \dots, x_{j_{m - r}} : s_{j_{m - r}}$ , $\begin{matrix} S (x_{j_{1}}, \dots, x_{j_{m - r}}) ⟺ \exists x_{i_{1}} : s_{i_{1}}, \dots, x_{i_{r}} : s_{i_{r}}, R (x_{1}, \dots, x_{m}) . \end{matrix}$

2.3. Topological partial algebras

Recall the definition of continuity of partial functions:

Definition 2.7 (Continuity).

Given two topological spaces X and Y, a partial function $f : X ⇀ Y$ is continuous iff the preimage under f of any open subset of Y is open in X, or equivalently

$dom (f)$ is open, and

for every open $V \subseteq Y$ , $f^{- 1} [V] =_{df} {x \in X ∣ x \in dom (f) and f (x) \in V}$ is open (in X).

Definition 2.8 (Topological partial algebra).

A topological partial algebra is a partial Σ-algebra with topologies on the carriers such that each of the basic Σ-functions is continuous. The carriers $B$ and $N$ have the discrete topology.

Discussion 2.9 (Continuity of computable functions).

The significance of the continuity of the basic functions of a topological algebra A is that it implies continuity of all While computable function on A [30,31].

This is in accordance with the Continuity Principle, which can be expressed as $\begin{matrix} computability ⟹ continuity \end{matrix}$ This principle is a classical design decision for models of computation over the reals; see for example [26,30,36].

One motivation for this design decision is Hadamard’s principle [18], which, as re-formulated by Courant and Hilbert [8,19], states that for a scientific problem to be well posed, the solution must (apart from existing and being unique) depend continuously on the data.

2.4. The algebra $R$ of reals

In the following sections, we work mostly with the following topological algebra:2

²
In [14] ‘ $R$ ’ was used for the algebra of reals which also included the multiplicative inverse operation on the reals. ‘ $R_{0}$ ’ referred to the algebra without the multiplicative inverse.

where the functions and constants $0^{R}$ , $1^{R}$ , ${plus}^{R}$ and ${times}^{R}$ have their usual definitions, the function ${eq}^{R}$ and ${less}^{R}$ are defined as in Remark 2.11 below and the “conditional” boolean operators $cand$ and $cor$ can defined using ${if-then-else}^{B}$ as in Discussion 2.12.

We will often write −, + and ∗ in place of ‘ ${neg}^{R}$ ’, ‘ ${plus}^{R}$ ’ and ‘ ${times}^{R}$ ’, = and < in place of ‘ ${eq}^{R}$ ’ and ‘ ${less}^{R}$ ’ (and ‘ ${eq}^{N}$ ’ and ‘ ${less}^{N}$ ’), $\overset{c}{\land}$ and $\overset{c}{\lor}$ in place of cand and cor, and drop the superscripts ‘ $R$ ’, ‘ $B$ ’ and ‘ $N$ ’ where unambiguous.

The signature $Σ (R)$ can be inferred from the above, with real as the sort of $R$ . Notation 2.10.

We write ↑ to denote “undefinedness”. We use the symbol ‘≃’ to denote “Kleene equality”, where the two sides are either both defined and equal, or both undefined [21, Section 63].

Remark 2.11 (Equality on the reals).

$R$ is a partial algebra, with the basic boolean-valued partial functions ${eq}^{R}$ and ${less}^{R}$ , which for $x, y \in R$ are defined as: $\begin{matrix} {eq}^{R} (x, y) ≃ \{\begin{matrix} ↑ & if x = y \\ f & o/w \end{matrix} \end{matrix}$ and $\begin{matrix} {less}^{R} (x, y) ≃ \{\begin{matrix} t & if x < y \\ f & if x > y \\ ↑ & o/w . \end{matrix} \end{matrix}$

Note that by contrast, the basic functions ${eq}^{N}$ and ${less}^{N}$ on $N$ are total.

Discussion 2.12 (Conditional boolean operators).

For $b_{1}, b_{2} \in B$ , the semantics of the “conditional” operators $\overset{c}{\land}$ and $\overset{c}{\lor}$ of $R$ can be defined by: $\begin{matrix} b_{1} \overset{c}{\land} b_{2} ≃ if b_{1} then b_{2} else f \end{matrix}$ and $\begin{matrix} b_{1} \overset{c}{\lor} b_{2} ≃ if b_{1} then t else b_{2} \end{matrix}$ i.e., the operators $\overset{c}{\land}$ and $\overset{c}{\lor}$ are “evaluated from the left”.

By contrast, the semantics of operators ∧ and ∨ are taken to be “strict”, i.e. $b_{1} \land b_{2}$ is undefined whenever either $b_{1}$ or $b_{2}$ is (and similarly for ∨).

While it is not strictly necessary to include the conditional operators, they seem a natural inclusion when dealing with partial functions.

Note that we will discuss the semantics of the infinite conditional disjunction in Discussion 3.3.

Discussion 2.13 (Motivation for use of partial functions).

We present two approaches motivating the above partial functions. The first is a discussion of the continuity of comparison operators on $R$ . The second is a Gedankenexperiment involving concrete models of computation.

The total versions of the comparison operators ${eq}^{R}$ and ${less}^{R}$ on $R$ are not continuous. (By contrast any boolean-valued operator on $N$ is trivially continuous, because $N$ has the discrete topology). Continuity of these operators is important because of the Continuity Principle and our definition of topological partial algebras (Definition 2.8 and Discussion 2.9), which requires all basic operators to be continuous.

Consider now the task of determining whether, in some concrete model, two representations denote the same real number or not. As an example, let us use, as representations of these real numbers, effective Cauchy sequences of rationals $(r_{0}, r_{1}, r_{2}, \dots)$ . We assume for our convenience3

³
When using effective Cauchy sequences as a representation, we assume given a computable modulus of convergence; given this, we can (by effectively taking subsequences) easily restrict our attention to sequences which are fast.

that the sequences are “fast”, i.e.,

\begin{matrix} \forall n, \forall m ⩾ n, | r_{n} - r_{m} | < 2^{- n} . \end{matrix}

Now suppose given two reals x and y with such representations

(r_{0}, r_{1}, r_{2}, \dots)

and

(s_{0}, s_{1}, s_{2}, \dots)

respectively. Suppose also that for

n = 0, 1, 2, 3, \dots

the inputs

r_{n}

and

s_{n}

are observed (from some device) at n time units. Then the first real is less than the second iff for some n,

r_{n} + 2 \cdot 2^{- n} < s_{n}

, and this can be determined in a finite amount of time. Correspondingly, the two reals are equal iff for all n,

| r_{n} - s_{n} | < 2 \cdot 2^{- n}

, but this cannot be determined in a finite amount of time. So from this example it is natural for comparison operators on reals x and y to diverge in cases when

x = y

Remark 2.14.

Throughout this paper we focus on functions on $R^{2}$ . The well-established methods of proof for $R$ do not generally “lift” to $R^{2}$ (see e.g. Appendix A), but the methods we will use for $R^{2}$ easily “lift” to $R^{n}$ for $n > 2$ .

2.5. The algebra

R^{*}

The algebra $R^{*}$ is formed from $R$ by adding the carriers $R^{*}$ , $N^{*}$ and $B^{*}$ (of sorts ${real}^{*}$ , ${nat}^{*}$ and ${bool}^{*}$ respectively) consisting of all finite sequences or arrays of reals, naturals and booleans (respectively), together with certain standard constants and operations for the empty array, updating of arrays, etc.

The significance of arrays for computation is that they provide finite but unbounded memory. Note that despite the convenience of the starred sorts, $R^{*}$ is computationally equivalent to $R$ (a proof of this fact is outlined in Appendix B). As such, we omit the precise definition of $R^{*}$ , which can be found in [31,34].

2.6. Syntax of terms and the While programming language

As has been mentioned, we will study the abstract models of high level imperative programming languages based on the ‘while’ construct. We begin with the syntax.

Note that ‘≡’ denotes syntactic identity between two expressions.

Σ -variables : For each Σ-sort s, there are variables $x^{s}, y^{s}, \dots$ of sort s. ${Var}_{s} (Σ)$ is the set of variables of sort s, and $Var (Σ)$ is the set of all Σ-variables.

Σ -terms : $Tm (Σ)$ is the set of Σ-terms: $t, \dots$ and ${Tm}_{s} (Σ)$ is the set of Σ-terms of sort s: $t^{s}, \dots$ . We define this using a modified BNF: $\begin{matrix} t^{s} : : = x^{s} ∣ F (t_{1}^{s_{1}}, \dots, t_{m}^{s_{m}}) \end{matrix}$ where F is a Σ-function symbol of type $s_{1} \times \dots \times s_{m} \to s$ ( $m ⩾ 0$ ).

Statements : $Stmt (Σ)$ is the set of Σ-statements $S, \dots$ generated by: $\begin{matrix} S : : = skip ∣ x : = t ∣ S_{1}; S_{2} ∣ if b then S_{1} else S_{2} fi ∣ while b do S_{0} od \end{matrix}$ where $x : = t$ denotes simultaneous assignment, i.e., for some $m > 0$ , $x \equiv (x_{1}, \dots, x_{m})$ and $t \equiv (t_{1}, \dots, t_{m})$ are variable and term tuples of the same product type, with the condition that $x_{i} ≢ x_{j}$ for $i \neq j$ ; and b is a Σ-boolean.4

⁴
That is, a Σ-term of sort bool.

Procedures : $Proc (Σ)$ is the set of Σ-procedures $P, \dots$ of the form: $\begin{matrix} P \equiv proc D begin S end \end{matrix}$ where the statement S is the body and D is a variable declaration of the form $\begin{matrix} D \equiv in a : u out b : v aux c : w \end{matrix}$ where $a$ , $b$ and $c$ are tuples of input, output and auxiliary variables respectively. We stipulate further:

$a$ , $b$ and $c$ each consist of distinct variables, and they are pairwise disjoint,

every variable occurring in the body S must be declared in D (among $a$ , $b$ or $c$ ).

a : u

and

b : v

, then P has type

u \to v

, written

P : u \to v

2.7. Semantics of terms and the While language

We now give the semantics of terms, statements and procedures. To begin, we need to define the notions of state and variant a of state.

A state over A is a family $⟨ σ_{s} ∣ s \in Sort (Σ) ⟩$ of functions $σ_{s} : {Var}_{s} (Σ) \to A_{s}$ . $State (A)$ is the set of states over A, with elements $σ, \dots$ .

We write $σ (x)$ for $σ_{s} (x)$ when $x \in {Var}_{s} (Σ)$ . We also write, for tuples $x \equiv (x_{1}, \dots, x_{m}) : u$ , $σ [x]$ in place of $(σ (x_{1}), \dots, σ (x_{m}))$ .

Let σ be a state over A, and for some Σ-product type u, let $x \equiv (x_{1}, \dots, x_{n}) : u$ and $a = (a_{1}, \dots, a_{n}) \in A_{u}$ (for $n ⩾ 1$ ). We define the variant $σ {x / a}$ to be the state over A formed from σ by replacing its value at $x_{i}$ by $a_{i}$ for $i = 1, \dots, n$ . That is, for all variables $y$ : $\begin{matrix} σ {x / a} (y) = \{\begin{matrix} σ (y) & if y ≢ x_{i} for i = 1, \dots, n \\ a_{i} & if y \equiv x_{i} \end{matrix} \end{matrix}$

We can now define the semantics of terms, statements and procedures:

Σ -terms : The meaning of a Σ-term t is given by the function $\begin{matrix} {⟦ t ⟧}^{A} : State (A) ⇀ A_{s} \end{matrix}$ where ${⟦ t ⟧}^{A} σ$ is the value of t in A at state σ.

The definition of ${⟦ t ⟧}^{A} σ$ is by structural induction on Σ-terms t:

${⟦ x ⟧}^{A} σ = σ (x)$

$⟦ F {(t_{1}, \dots, t_{m}) ⟧}^{A} σ ≃ {\begin{matrix} {F {(⟦ t_{1} ⟧}^{A} σ, \dots, ⟦ t_{m} ⟧}^{A} σ) & {if ⟦ t_{i} ⟧}^{A} σ ↓ for all i = 1, \dots, m \\ ↑ & o/w \end{matrix}$

Statements : The meaning of a While statement S w.r.t. A, written ${⟦ S ⟧}^{A}$ , is a partial state transformation on the algebra A: $\begin{matrix} {⟦ S ⟧}^{A} : State (A) ⇀ State (A) . \end{matrix}$ Its definition is standard [30,31] and lengthy, and so we omit it. Briefly, it is based on defining the computation sequence of S starting in a state σ, or rather the nth component of this sequence, by a primary induction on n, and a secondary induction on the size of S.

Procedures : The meaning of a While procedure $\begin{matrix} P \equiv proc in a : u out b : v aux c : w begin S end, \end{matrix}$ of type $u \to v$ , written ${⟦ P ⟧}^{A} : A_{u} ⇀ A_{v}$ , is defined as follows.5

⁵
We overload the symbols ↑, ↓ and ≃, discussed in Notation 2.10 where they deal with the definedness of terms, for use with statements and procedures. Here instead of definedness they refer to the convergence or divergence of computations.

For

a \in A_{u}

, let σ be any state on A such that

σ [a] = a

. Then6

⁶

The definition can be shown to be independent of the exact choice of σ (by the Functionality Lemma [31, Lemma 3.4]).

\begin{matrix} {⟦ P ⟧}^{A} (a) ≃ \{\begin{matrix} σ^{'} [b] & {if ⟦ S ⟧}^{A} σ ↓ σ^{'} \\ ↑ & {if ⟦ S ⟧}^{A} σ ↑ . \end{matrix} \end{matrix}

2.8. While computability and semicomputability

A function $f : A_{u} ⇀ A_{v}$ is said to be computable (on A) by a While procedure $P : u \to v$ if $f = P^{A}$ .

$While (A)$ is the class of functions While computable on A.

The halting set of a procedure $P : u \to v$ on A is the set $\begin{matrix} {Halt}^{A} (P) =_{df} {a \in A_{u} ∣ P^{A} (a) ↓} . \end{matrix}$

A set $R \subseteq A_{u}$ is While semicomputable on A if it is the halting set on A of some While procedure.

2.9. Extending While to ${While}^{OR}$ and ${While}^{NE}$

In preparation for the theorems in Sections 4 and 5, we give the semantics of strong disjunction and strong existential quantification to introduce the ${While}^{OR}$ and ${While}^{NE}$ extensions to the While language.

The motivation for these extensions is that with our model of While computation on $R$ , the partial operations leave us unable to implement interleaving or merging. The problem is that in the interleaving of two processes, one process may converge and the other diverge locally (because of the partial operations). The resulting process will then diverge, whereas we might want it to converge. Thus, as we will see in Section 4, the union of two semicomputable sets is not necessarily semicomputable. Concrete models, which work with representations of the reals instead of taking them as primitive, do not have this deficiency, as local divergence is not an issue. The extensions ${While}^{OR}$ and ${While}^{NE}$ compensate for this deficiency in While .

The ${While}^{OR}$ language is created from While by introducing the strong disjunction operator ‘ $\nabla$ ’, where $b_{1} \nabla b_{2}$ converges to $t$ if either $b_{1}$ or $b_{2}$ do so, even if the other diverges.

The ${While}^{NE}$ language is created from While by introducing a strong existential quantification construct over the naturals in the context of an assignment: $\begin{matrix} x^{B} : = \exists n P (t, n) \end{matrix}$ where $n : nat$ and P is a boolean-valued procedure. Its semantics are defined by $\begin{matrix} ⟦ \exists n P {(t, n) ⟧}^{A} σ ≃ \{\begin{matrix} t & if P {(⟦ t ⟧}^{A} σ, m) ↓ t for some m \\ ↑ & o/w . \end{matrix} \end{matrix}$

To simplify the exposition, we include the strong disjunction operator ‘ $\nabla$ ’ in the ${While}^{NE}$ language.

If instead of strong existential quantification, we constructed ${While}^{NE}$ using existential quantification “evaluated from the left”, this would (as can easily be shown) give a conservative extension of While , in that any function implemented in it could be implemented in While (assuming here we do not include the strong disjunction operator).7

⁷
cf. the two definitions of infinite disjunction given in Discussion 3.3.

By means of these constructs, interleaving of processes may be simulated. The ${While}^{OR}$ language allows for the interleaving of an arbitrary but finite number of processes, and the ${While}^{NE}$ language for infinitely many processes.

3. Semantic disjointedness; Engeler’s Lemma

We now present some important background relating to boolean terms. We begin by introducing notation used throughout this section and Section 4:

Notation 3.1.

We will often write $x$ to mean a u-tuple of variables; i.e. $x \equiv (x_{1}, \dots, x_{m}) : u$ .

For a tuple of variables $x \equiv (x_{1}, \dots, x_{m})$ , $m ⩾ 1$ , let $Bool (R) (x)$ be the set of $Σ (R)$ -booleans containing variables in $x$ only.

Similarly define $Bool (R^{OR}) (x)$ , where $R^{OR}$ is the extension of the algebra $R$ including strong disjunction ( $\nabla$ ).

3.1. Engeler’s Lemma

This is of vital importance in proving our Structure Theorem for $While (R)$ semicomputable sets.

First we need the concepts of semantic disjointedness of a sequence of booleans.

Definition 3.2 (Semantic Disjointedness).

A sequence $(b_{0}, b_{1}, b_{2}, \dots)$ of boolean terms is semantically disjoint over A if for any state σ over A and any n, $\begin{matrix} {{⟦ b_{n} ⟧}^{A} σ ↓ t ⟹ \forall i \neq n, ⟦ b_{i} ⟧}^{A} σ ↓ f . \end{matrix}$

Discussion 3.3 (Semantics of infinite disjunction).

Let $(b_{k})$ be a sequence of Σ-booleans. There are (at least) two different reasonable semantic definitions for the infinite disjunction $\begin{matrix} ⋁_{k = 0}^{\infty} b_{k} \end{matrix}$ for 3-valued logics (“reasonable” in the sense of having computational significance):

Infinite conditional disjunction (“evaluation from the left”), written $⋁_{k = 0}^{\begin{array}{c} \infty \\ c \end{array}} b_{k}$ , with two possible results, $t$ and ↑: $\begin{matrix} {⟦ ⋁_{k = 0}^{\begin{array}{c} \infty \\ c \end{array}} b_{k} ⟧}^{A} σ ≃ \{\begin{matrix} t & {{if \exists k, ⟦ b_{k} ⟧}^{A} σ ↓ t and \forall i < k, ⟦ b_{i} ⟧}^{A} σ ↓ f \\ ↑ & otherwise . \end{matrix} \end{matrix}$ This definition is easily seen to be While computable (in the sequence of codes $⌜ b_{k} ⌝$ ).

Infinite strong disjunction (“strong Kleene evaluation”), written $\nabla_{k = 0}^{\infty} b_{k}$ , again with two possible results, $t$ and ↑: $\begin{matrix} {⟦ \nabla_{k = 0}^{\infty} b_{k} ⟧}^{A} σ ≃ \{\begin{matrix} t & {if \exists k, ⟦ b_{k} ⟧}^{A} σ ↓ t \\ ↑ & otherwise . \end{matrix} \end{matrix}$ This definition is not (in general) While computable. If it were, While would be at least as powerful as ${While}^{NE}$ , which we will show is not the case (Theorems 4, 5).

Remark 3.4.
Note that if an effective sequence of booleans $(b_{k})$ is semantically disjoint over A, then for any σ, $\begin{matrix} {⟦ \nabla_{k = 0}^{\infty} b_{k} ⟧}^{A} σ ≃ {⟦ ⋁_{k = 0}^{\begin{array}{c} \infty \\ c \end{array}} b_{k} ⟧}^{A} σ \end{matrix}$ i.e. ${⟦ \nabla_{k = 0}^{\infty} b_{k} ⟧}^{A} σ$ can be “evaluated from the left”.

We will only consider infinite disjunction in the context of semantically disjoint sequences of booleans, and so for our purposes the choice of semantic definition is irrelevant.
Lemma 3.5 (Engeler’s Lemma for While ).

Given a partial Σ-algebra A and a Σ-product type $u = s_{1} \times \dots \times s_{m}$ , if a relation $R \subseteq A_{u}$ is While semicomputable over A then R can be expressed as the infinite disjunction of a semantically disjoint effective sequence of Σ-booleans over A; i.e., for all $x : A_{u}$ $\begin{matrix} x \in R ⟺ ⋁_{k = 0}^{\infty} ⟦ b_{k} ⟧ σ {x / x} \end{matrix}$ for some semantically disjoint effective sequence of booleans $(b_{0}, b_{1}, \dots)$ , where σ is any state and each $b_{k}$ has no free variables other than those in $x : u$ .

Remark 3.6.
Engeler’s Lemma can be proved by an analysis of the computation trees for While programs [31]. It was originally stated in [11] without the semantic disjointedness property; this property was subsequently noted in [37, Section 4].

3.2. Canonical form for $Bool (R) (x)$

In the proof of our Structure Theorem in Section 4 for $While (R)$ semicomputable sets, we require a canonical form for booleans containing real variables only.

Lemma 3.7 (Canonical form for $Bool (R) (x)$ ).

For a tuple $x$ of real variables, any term in $Bool (R) (x)$ is effectively semantically equivalent to a boolean combination of equations and inequalities of the form: $\begin{matrix} p (x) = 0 and q (x) > 0 \end{matrix}$ where p and q are polynomials in $x$ of $degree > 0$ . 8

⁸
Note that this “canonical form” is not unique.

The proof is by structural induction on the booleans.

Note that the canonical form of booleans coincides with the notion of semi-algebraic set, to which we now turn.

3.3. Basic and semi-algebraic sets

We introduce the concepts of basic and semi-algebraic sets, which are fundamental to our results. We consider these sets on $R^{2}$ , though they can clearly be generalised to $R^{n}$ for any $n ⩾ 1$ .

Definition 3.8 (Basic set).

A basic set is a subset of $R^{2}$ that can be expressed in the form $\begin{matrix} {x \in R^{2} ∣ p_{1} (x) > 0 \land \dots \land p_{k} (x) > 0} (k > 0) \end{matrix}$ where $p_{1}, \dots, p_{k}$ are polynomials.

Remark 3.9.
In this paper, polynomials are always taken as having rational [or, equivalently, integer] coefficients.

Note that all basic sets are open.9
⁹
We use “basic sets” to mean “basic open semialgebraic sets”.

Definition 3.10 (Semi-algebraic set).

A semi-algebraic set is a subset of $R^{2}$ that can be expressed in the form $\begin{matrix} ⋃_{i = 1}^{n} {x \in R^{2} ∣ p_{i, 1} (x) > 0 \land \dots \land p_{i, k_{i}} (x) > 0 \land q_{i, 1} (x) = 0 \land \dots \land q_{i, l_{i}} (x) = 0} (k_{i}, l_{i} > 0) \end{matrix}$ where each $p_{i, j}$ and $q_{i, j}$ is a polynomial.

Remark 3.11.
The class of basic sets is closed under binary intersection.
Remark 3.12.
Given a polynomial $p (x)$ on $R^{2}$ , there are disjoint basic sets $B^{+}$ , $B^{-}$ and a semi-algebraic set D, such that
$p > 0$ on $B^{+}$

$p < 0$ on $B^{-}$

$p = 0$ on D
and $B^{+} \cup B^{-} \cup D = R^{2}$

3.4. Positive and negative sets

Definition 3.13 (Positive, negative and divergent sets of booleans).

Let $x \equiv (x_{1}, x_{2})$ . For any $b \in Bool (R) (x)$ , let: $\begin{array}{l} PS (b) =_{df} {x \in R^{2} ∣ b [x] = t} \\ NS (b) =_{df} {x \in R^{2} ∣ b [x] = f} \\ DS (b) =_{df} {x \in R^{2} ∣ b [x] ↑} . \end{array}$

These will be used in the proof of the Partition Lemma in the next section.

4. $While (R)$ semicomputable sets: Structure Theorem and failure of closure under union

We present a Partition Lemma for booleans in $Bool (R) (x)$ , where $x \equiv (x_{1}, x_{2})$ , which we then use to give a Structure Theorem for $While (R)$ semicomputability over $R^{2}$ . By means of this we will give an example of two $While (R)$ semicomputable sets whose union is not $While (R)$ semicomputable.

Convention 4.1.
For the remainder of this section, let $x \equiv (x_{1}, x_{2})$ .
4.1. Partition Lemma for booleans in $Bool (R) (x)$

Lemma 4.2 (Partition Lemma for booleans in $Bool (R) (x)$ ).

Consider any boolean $b \in Bool (R) (x)$ . The positive and negative sets 10

¹⁰
cf. Definition 3.13. For our purpose, the form of the divergent set of $b$ , $DS (b)$ , is unimportant.

for

b

R^{2}

can be expressed as:

\begin{array}{l} PS (b) = ⋃_{i = 1}^{k} B_{i}^{+} \\ NS (b) = ⋃_{j = 1}^{l} B_{j}^{-} . \end{array}

where

B_{i}^{+}

B_{j}^{-}

are basic sets, and

Before giving the proof, we consider some examples of positive and negative sets in $R^{2}$ .

Examples 4.3 (Positive and negative sets in

R^{2}

These examples are of interest because our counterexample to the closure of semicomputable sets under union will build on them.

Consider the polynomials $p_{1} \equiv - x_{1}^{2} - x_{2}^{2} + 1$ and $p_{2} \equiv - {(x_{1} - 1)}^{2} - x_{2}^{2} + 1$ , and the booleans $b_{1} \equiv p_{1} (x_{1}, x_{2}) > 0$ and $b_{2} \equiv p_{2} (x_{1}, x_{2}) > 0$ . Define: $\begin{array}{l} B_{1} = PS (b_{1}) = {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) > 0} \\ B_{2} = PS (b_{2}) = {(x_{1}, x_{2}) \in R^{2} ∣ p_{2} (x_{1}, x_{2}) > 0} \end{array}$

Figure 1.

$B_{1} = PS (b_{1})$ and $B_{2} = PS (b_{2})$ .

$B_{1}$ and $B_{2}$ are basic sets, and can be easily seen to be $While (R)$ semicomputable. They are pictured in Fig. 1.

The sets $PS (b_{1} \overset{c}{\lor} b_{2})$ and $PS (b_{1} \lor b_{2})$ , pictured in Fig. 2, are also easily seen to be $While (R)$ semicomputable. These sets can be represented as the union of two and three disjoint basic sets respectively:11

¹¹

The proof of the Partition Lemma serves as an algorithm for constructing such representations.

\begin{array}{l} \begin{matrix} PS (b_{1} \overset{c}{\lor} b_{2}) & = {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) > 0} \\ \cup {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) > 0, p_{2} (x_{1}, x_{2}) < 0} \end{matrix} \\ \begin{matrix} PS (b_{1} \lor b_{2}) & = {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) > 0, p_{2} (x_{1}, x_{2}) > 0} \\ \cup {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) > 0, p_{2} (x_{1}, x_{2}) < 0} \\ \cup {(x_{1}, x_{2}) \in R^{2} ∣ p_{1} (x_{1}, x_{2}) < 0, p_{2} (x_{1}, x_{2}) > 0} \end{matrix} \end{array}

Figure 2.

$PS (b_{1} \overset{c}{\lor} b_{2})$ and $PS (b_{1} \lor b_{2})$ .

Proof of the Partition Lemma.

This is by structural induction on $R$ -booleans with variables in $x \equiv (x_{1}, x_{2})$ , which we assume are in canonical form.

Base case: $b \equiv p (x) = 0$ or $p (x) > 0$ . Immediate from Remark 3.12. In each case there is a single basic set for each positive and negative set.

Induction step: In what follows, suppose: $\begin{array}{l} PS (b_{1}) = ⋃_{i = 1}^{k_{1}} B_{1 i}^{+} \\ NS (b_{1}) = ⋃_{i = 1}^{l_{1}} B_{1 i}^{-} \\ PS (b_{2}) = ⋃_{j = 1}^{k_{2}} B_{2 j}^{+} \\ NS (b_{2}) = ⋃_{j = 1}^{l_{2}} B_{2 j}^{-} \end{array}$

Now we consider the various cases based on the major operator of b:

$b \equiv \neg b_{1}$ . Just exchange the positive and negative sets of $b_{1}$ ; since all three properties hold for both, they still hold after switching.

$b \equiv b_{1} \lor b_{2}$ . Then let $\begin{array}{l} {PS}_{1} = ⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{+} \cap B_{2 j}^{+}) \\ {PS}_{2} = ⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{+} \cap B_{2 j}^{-}) \\ {PS}_{3} = ⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{-} \cap B_{2 j}^{+}) \end{array}$

Then: $\begin{array}{l} PS (b) = {PS}_{1} \cup {PS}_{2} \cup {PS}_{3} \\ NS (b) = ⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{-} \cap B_{2 j}^{-}) \end{array}$

The sets ${PS}_{1}$ , ${PS}_{2}$ and ${PS}_{3}$ are disjoint, because for any i and j, $B_{1 i}^{+} \cap B_{1 j}^{-} = \emptyset$ and $B_{2 i}^{+} \cap B_{2 j}^{-} = \emptyset$ . Further, the sets $B_{1 i}^{a} \cap B_{2 j}^{b}$ ( $a, b \in {+, -}$ ) are all mutually disjoint, because $B_{n i_{1}}^{+} \cap B_{n i_{2}}^{+} = \emptyset$ for $i_{1} \neq i_{2}$ and $n \in {1, 2}$ , and $B_{n j_{1}}^{-} \cap B_{n j_{2}}^{-} = \emptyset$ for $j_{1} \neq j_{2}$ and $n \in {1, 2}$ . So $PS (b)$ and $NS (b)$ are finite unions of disjoint basic sets (by Remark 3.11).

$b \equiv b_{1} \land b_{2}$ . Then $\begin{array}{l} PS (b) = ⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{+} \cap B_{2 j}^{+}) \\ NS (b) = (⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{-} \cap B_{2 j}^{-})) \cup (⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{+} \cap B_{2 j}^{-})) \cup (⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{-} \cap B_{2 j}^{+})) \end{array}$

Similar to case (ii).

$b \equiv b_{1} \overset{c}{\lor} b_{2}$ . Then $\begin{array}{l} PS (b) = ⋃_{i = 1}^{k_{1}} B_{1 i}^{+} \cup (⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{-} \cap B_{2 j}^{+})) \\ NS (b) = ⋃_{i = 1}^{l_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{-} \cap B_{2 j}^{-}) \end{array}$

Again, similar to case (ii).

$b \equiv b_{1} \overset{c}{\land} b_{2}$ . Then $\begin{array}{l} PS (b) = ⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{k_{2}} (B_{1 i}^{+} \cap B_{2 j}^{+}) \\ NS (b) = ⋃_{i = 1}^{k_{1}} B_{1 i}^{-} \cup (⋃_{i = 1}^{k_{1}} ⋃_{j = 1}^{l_{2}} (B_{1 i}^{+} \cap B_{2 j}^{-})) \end{array}$

Again, similar to ((ii)). □

Remark 4.4.

The Partition Lemma for booleans in $Bool (R) (x)$ does not hold for booleans in $Bool (R^{OR}) (x)$ because, given any two booleans $b_{1}, b_{2} \in Bool (R^{OR}) (x)$ , the positive set of $b_{1} \nabla b_{2}$ cannot necessarily be reduced to a disjoint union of basic sets, as we will see in Section 4.3.

4.2. Structure Theorem for

While (R)

semicomputability

Theorem 1 (Structure Theorem for $While (R)$ ).

For subsets of $R^{2}$ , $\begin{matrix} While (R) s/comp ⟺ union of disjoint eff. seq. of basic sets . \end{matrix}$

Proof.
For the ‘ $⟹$ ’ direction: If $R \subseteq R^{2}$ is $While (R)$ semicomputable, then by Engeler’s Lemma (Lemma 3.5), for all $x \in R^{2}$ , $\begin{matrix} x \in R ⟺ ⋁_{k = 0}^{\infty} b_{k} [x] \end{matrix}$ for some semantically disjoint effective sequence $(b_{k})$ of Σ-booleans in $Bool (R) (x)$ .12
¹²
Recall Remark 3.4.

By the Partition Lemma, each $b_{k}$ defines a finite union of disjoint basic sets. Also since $(b_{k})$ is semantically disjoint, the positive sets for different $b_{k}$ ’s are disjoint.

Hence $(b_{k})$ is a disjoint effective sequence of basic sets as desired.

For the ‘ $⟸$ ’ direction: Given an effective encoding of basic sets (we write $⌜ B ⌝$ for the code of B), there is a $While (R)$ computable function $\begin{matrix} in : nat \times {real}^{2} ⇀ bool \end{matrix}$ such that for any basic set B, $\begin{matrix} in (⌜ B ⌝, x_{1}, x_{2}) = \{\begin{matrix} t & if (x_{1}, x_{2}) \in B \\ f & if (x_{1}, x_{2}) \notin \overline{B} \\ ↑ & o/w, i.e. (x_{1}, x_{2}) is on the boundary of B . \end{matrix} \end{matrix}$ where $\overline{B}$ is the closure of B.

This is clear from the definition of basic sets.

Then the disjoint effective sequence $(B_{i})$ of basic sets gives us a total recursive function $f : N \to N$ such that $f (n)$ is the code of the nth basic set. Hence the countable union of $(B_{i})$ is the halting set of the $While (R)$ procedure □
Remark 4.5.
An incomplete version of our structure theorem for $While (R)$ semicomputability was given in [13, Section 4.6]; for subsets of $R^{2}$ : $\begin{array}{l} While (R) s/comp ⟹ union of disjoint eff. seq. of finite unions of basic sets \\ While (R) s/comp ⟸ union of disjoint eff. seq. of basic sets \end{array}$

Figure 3.
$B_{1} \cup B_{2} = PS (b_{1} \nabla b_{2})$ .
4.3. Failure of closure of $While (R)$ semicomputable sets under union

For total standard algebras, we have the following proposition [31, Section 5.2], [34, Section 6.1]:

Proposition 4.6 (Closure of While semicomputable sets under union for total standard algebras).

For any total standard algebra A, the class of $While (A)$ semicomputable sets is closed under finite unions.

We now use the Structure Theorem for $While (R)$ (Theorem 1) to give a counterexample to the closure of semicomputable sets under finite union in our partial algebra on the reals.

This follows simply from:

Example 4.7 (A union of two basic sets which is not basic).

Consider the overlapping basic sets (cf. Examples 4.3): $\begin{array}{l} B_{1} = {(x_{1}, x_{2}) ∣ - x_{1}^{2} - x_{2}^{2} + 1 > 0}, \\ B_{2} = {(x_{1}, x_{2}) ∣ - {(x_{1} - 1)}^{2} - x_{2}^{2} + 1 > 0} . \end{array}$ Their union is clearly semi-algebraic, but not basic.

This follows from a more general result [1]: if the boundaries of two semi-algebraic subsets of $R^{2}$ intersect transversally at some point, then their union is never basic.13

¹³
We thank Professor Bröcker (Münster) for pointing this out (personal communication).

Theorem 2 (Failure of closure of

While (R)

semicomputable sets under union).

The class of $While (R)$ semicomputable sets on $R^{2}$ is not closed under finite unions.

Proof.
Recall the sets $B_{1}$ and $B_{2}$ from Example 4.7. Consider $B_{1} \cup B_{2} = PS (b_{1} \nabla b_{2})$ , pictured in Fig. 3. It is a union of two semicomputable sets (pictured in Fig. 1). If it is semicomputable, then by the Structure Theorem for $While (R)$ it is a union of a disjoint effective sequence of basic sets. However, since it is open and connected, it must in fact be equal to a single basic set. This contradicts the conclusion of Example 4.7. □

Note that with respect to ${While}^{OR} (R)$ and ${While}^{NE} (R)$ , the set $PS (b_{1} \nabla b_{2})$ is trivially semicomputable (cf. Remark 4.4).
5. Classes of subsets of $R$ semicomputable sets by models based on the While language

In this section we consider the equivalence or inequivalence of the classes of $While (R)$ , ${While}^{OR} (R)$ and ${While}^{NE} (R)$ semicomputable sets, as well as the projectively semicomputable sets for these languages.

5.1. A set which is projectively $While (R)$ semicomputable but not $While (R)$ semicomputable

We will show, by means of an example, that the concept of projective $While (R)$ semicomputability is strictly broader than $While (R)$ semicomputability on $R^{2}$ .

Figure 4.

Domain of $f_{0} (x_{1}, x_{2}, y)$ .

Example 5.1.

Consider the three-dimensional function $f_{0} : R^{3} \to B$ , where: $\begin{matrix} f_{0} (x_{1}, x_{2}, y) ≃ \{\begin{matrix} t & if y > 1 \land x_{1}^{2} + x_{2}^{2} < 1 \\ t & if y < - 1 \land {(x_{1} - 1)}^{2} + x_{2}^{2} < 1 \\ ↑ & o/w \end{matrix} \end{matrix}$ the domain of which is pictured in Fig. 4.

The domain of $f_{0}$ is easily seen to be $While (R)$ semicomputable, and so its projection off the third argument: $\begin{matrix} {(x_{1}, x_{2}) ∣ \exists y \in R, (y > 1 \land x_{1}^{2} + x_{2}^{2} < 1) \nabla (y < - 1 \land {(x_{1} - 1)}^{2} + x_{2}^{2} < 1)} \end{matrix}$ is projectively $While (R)$ semicomputable.

We have met this set previously in Fig. 3, and we have seen that it is not $While (R)$ semicomputable (in the proof of Theorem 2), as it is not a union of disjoint basic sets.

From this example, we have:

Theorem 3.

For subsets of $R^{2}$ ,

5.2. Inequivalence of

While (R)

{While}^{OR} (R)

and

{While}^{NE} (R)

semicomputability

In [13, Section 4.6], structure theorems for ${While}^{OR} (R)$ and ${While}^{NE} (R)$ semicomputability over $R^{2}$ were given. Along with the structure theorem for $While (R)$ given in Section 4.2, this gives us the following:

Semicomputability Structure Theorems for $R^{2}$ .
For subsets of $R^{2}$ , $\begin{array}{l} While (R) s/comp ⟺ union of disj . eff. seq. of basic sets \\ {While}^{OR} (R) s/comp ⟺ union of disj . eff. seq. of finite unions of basic sets \\ {While}^{NE} (R) s/comp ⟺ union of eff. seq. of basic sets. \end{array}$

The above three structure theorems will be used (in Theorems 4 and 5 below) to show the inequivalence between $While (R)$ , ${While}^{OR} (R)$ and ${While}^{NE} (R)$ semicomputability on $R^{2}$ . This will be done by providing two examples: a subset of $R^{2}$ which is ${While}^{OR} (R)$ but not $While (R)$ semicomputable, and one which is ${While}^{NE} (R)$ but not ${While}^{OR} (R)$ semicomputable.

For the first example, we return to our working example, $B_{1} \cup B_{2}$ , pictured in Fig. 3. As discussed, this set is not $While (R)$ semicomputable. However, from its definition and from the ${While}^{OR} (R)$ structure theorem, it is clearly ${While}^{OR} (R)$ semicomputable. So we have:
Theorem 4.
For subsets of $R^{2}$ ,

For the second example, consider a sequence of polynomials $\begin{matrix} p_{i} \equiv {(x_{1} - 2 i)}^{2} + x_{2}^{2} < 1 \end{matrix}$ and booleans $\begin{matrix} b_{i} \equiv p_{i} (x_{1}, x_{2}) > 0 \end{matrix}$ $(i = 0, 1, 2, \dots)$ . Let $\begin{matrix} B_{i} = PS (b_{i}) = {(x_{1}, x_{2}) \in R^{2} ∣ p_{i} (x_{1}, x_{2}) > 0} . \end{matrix}$ and let $\begin{matrix} (5.1) & B = ⋃_{i} B_{i} = {(x_{1}, x_{2}) ∣ p_{i} (x_{1}, x_{2}) > 0 for some i = 0, 1, 2, \dots} . \end{matrix}$

B is partially pictured in Fig. 5, for $- 1 ⩽ x_{1} ⩽ 4$ .

Figure 5.
$g (x_{1}, x_{2})$ .

$(B_{i})$ is an effective sequence of basic sets, and so their union B is ${While}^{NE} (R)$ semicomputable, by the ${While}^{NE} (R)$ structure theorem.

Now consider whether B is ${While}^{OR} (R)$ semicomputable. By the ${While}^{OR} (R)$ structure theorem, that would mean B is a union of a disjoint sequence of finite unions of basic sets. On the other hand, because B is connected, it must be a (single) finite union of basic sets, and (hence) a single semi-algebraic set. But that cannot be the case, for in (5.1), by substituting 0.9 for $x_{2}$ , we get the 1-dimensional “slice” of B: $\begin{matrix} {x \in R ∣ p_{i} (x, 0.9) > 0 for some i = 0, 1, 2, \dots} . \end{matrix}$

If B were semi-algebraic, then this set would also be semi-algebraic. However, this set is a union of infinitely many disjoint intervals (the intervals on which the horizontal line at $x_{2} = 0.9$ intersects the “tops” of the discs), and therefore cannot be semi-algebraic, since a semi-algebraic subset of $R$ can have at most finitely many components.

So B is not semi-algebraic, and therefore not ${While}^{OR} (R)$ semicomputable. Hence we have:
Theorem 5.
For subsets of $R^{2}$ ,
5.3. Equivalence of projective $While (R)$ and ${While}^{NE} (R)$ semicomputability

The following was proved in [37, Section 5.6].

Lemma 5.2.
For subsets of $R^{2}$ , $\begin{matrix} proj- {While}^{NE} (R) s/comp ⟺ {While}^{NE} (R) s/comp . \end{matrix}$

Essentially, this involves replacing a projection onto a real plane, i.e. existential quantification over $R$ , by existential quantification over a countable dense subset $Q \subset R$ , by continuity considerations, and (hence, by coding rationals as naturals) by existential quantification over $N$ .

We want to show further: Lemma 5.3.
For subsets of $R^{2}$ , $\begin{matrix} proj- While (R) s/comp ⟺ {While}^{NE} (R) s/comp . \end{matrix}$
Proof.
The ‘ $⟹$ ’ direction is obvious.

For the ‘ $⟸$ ’ direction: Consider any ${While}^{NE} (R)$ semicomputable set in $R^{2}$ . This is the halting set of some ${While}^{NE}$ program P over $R^{2}$ .

We will construct a $While (R)$ program $P_{0}$ over $R^{3}$ such that the projection of the halting set of $P_{0}$ off $R$ is equal to the halting set of P.

We construct $P_{0}$ from P by replacing each statement of the form: $\begin{matrix} x^{B} : = \exists n Q (t, n) \end{matrix}$ by the two statements: $\begin{array}{l} x^{B} : = Q (t, item [floor (z), i]); \\ i : = i + 1 \end{array}$ where $z : real$ is the new argument for $P_{0}$ , $i : nat$ is a new auxiliary variable which is initialized to 0 at the start of the program, item is a function for fetching the ith item from a list of naturals encoded as a single natural, and $floor : R ⇀ N$ is defined as $\begin{matrix} floor (z) ≃ \{\begin{matrix} the greatest n \in N s.t. n < z & if z \in R ∖ N \\ ↑ & o/w, \end{matrix} \end{matrix}$ which is easily seens to be $While (R)$ semicomputable.

Then suppose that for some input values $x_{1}, x_{2} \in R^{2}$ , $P (x_{1}, x_{2})$ halts. Then since P halted in finitely many steps, there exists a finite list of natural numbers $i_{1}, \dots, i_{n}$ which are existentially quantified corresponding to the ‘ $x^{B} : = \exists n Q (t, n)$ ’ nodes in the halting branch of the computation tree for P.14
¹⁴
See [31,34] for information about computation trees.

This gives a list of naturals which may be encoded as a single natural i. Then if $i < z < i + 1$ , $P_{0} (x_{1}, x_{2}, z)$ halts.15
¹⁵
Note that the order of the naturals used in the existential quantification steps may have no relation to the order of the $x^{B} : = \exists n P (t, n)$ lines in the code, due to loops and branches.

So the set ${While}^{NE} (R)$ semicomputed by P is also a projection ${(x_{1}, x_{2}) ∣ \exists z \in R, P_{0} (x_{1}, x_{2}, z)}$ of the $While (R)$ semicomputable set $P_{0}$ . □

5.4. Classes of sets semicomputable by models based on the While language

We now compare the classes of subsets of $R^{2}$ semicomputable by the While , ${While}^{OR}$ and ${While}^{NE}$ languages, and their projective versions.

We begin by combining the results discussed in the previous subsection:

Theorem 6.
For subsets of $R^{2}$ , $\begin{array}{l} proj- While (R) s/comp & ⟺ proj- {While}^{OR} (R) s/comp \\ ⟺ proj- {While}^{NE} (R) s/comp \\ ⟺ {While}^{NE} (R) s/comp \end{array}$
Proof.
This follows from $\begin{array}{l} proj- While (R) s/comp & ⟹ proj- {While}^{OR} (R) s/comp \\ ⟹ proj- {While}^{NE} (R) s/comp \\ ⟹ {While}^{NE} (R) s/comp by Lemma 5.2 \\ ⟹ proj- While (R) s/comp by Lemma 5.3 . \end{array}$ □

We have thus established the existence of three distinct classes of subsets of $R^{2}$ , as shown in the following diagram:

We further have the equivalence of each model in the above diagram with its respective starred version (as shown in Appendix B).
6. Conclusion and future work

6.1. Conclusion

In this paper, we investigated the possible generalisation of two results from classical computability theory to the context of topological partial algebras on the reals: closure of semicomputable sets under finite union, and the equivalence of semicomputable sets to projectively (semi)computable sets. Both results were shown not to hold over $R^{2}$ (Theorems 2 and 3 respectively).

In the process we also developed a Structure Theorem for $While (R)$ semicomputability over $R^{2}$ (Theorem 1), and distinguished the classes of sets semicomputed by $While (R)$ , ${While}^{OR} (R)$ and ${While}^{NE} (R)$ programs and their projective versions (again over $R^{2}$ ) (Section 5.4).

In Appendix A, we give an adaptation of our (in)equivalence results to the 1-dimensional case over $R$ .

In Appendix B, we outline a proof of the equivalence of $While (R)$ with its starred version.

In Appendix C, we show that another result from classical computability theory, Post’s Theorem, holds in the case of While computation on $R$ .

6.2. Future work

We have compared various classes of subsets of $R^{2}$ with respect to semicomputability by abstract models based on the While language (Section 5.4). Similarly, we would like to investigate concrete models of computability (Section 1.1), and compare them amongst themselves and with abstract models with respect to computable functions and semicomputable sets. Equivalences have been shown between various concrete and abstract models of computability16

¹⁶

See Section 1.2.

over the reals [13 ,32 ,33]. However, important questions remain regarding equivalences between digital (abstract and conrete) and analog models, such as suitable extensions of Shannon’s GPAC [27]. Some interesting results have been obtained in this direction [4–6,15,25], but much remains to be done.

Footnotes

Acknowledgements

We are very grateful to Professor Ludwig Bröcker for his input on the properties of basic semi-algebraic sets. This research was supported by a grant from the Natural Sciences and Engineering Research Council of Canada.

Inequivalence results for 1 dimension

The Semicomputability Structure Theorems (Section 5.1) were formulated for the case $n = 2$ (computation on $R^{2}$ ). As pointed out in the introduction, these theorems, as well as the inequivalences (Theorems 4, 5) generalize readily to $R^{n}$ for all $n ⩾ 2$ .

For the case $n = 1$ , these Structure Theorems also hold. However there are two problems with their formulation:

To prove Theorem 7, we need some facts about algebraic intervals and algebraic numbers.

In other words, the set of polynomials over $Z$ forms a principle ideal domain.18

¹⁸

See e.g. [10].

We may now show, by another example, that Theorem 8.

For 1-dimensional computation over $R$ ,

Proof.

Consider $I = (0, π)$ .

Since I is a single interval, if it were ${While}^{OR} (R)$ semicomputable, it would have to be an algebraic interval, but it is not.

However, it is ${While}^{NE} (R)$ semicomputable, since it is the union of the (non-disjoint) effective sequence of intervals $(I_{n})$ where $I_{n} = (0, r_{n})$ and $(r_{n})$ is an increasing sequence of rational numbers converging to π. □

Remark A.3.

It is interesting to note that the counterexample used in the proof of Theorem 8 generalises easily to the case of $R^{2}$ by taking the product of the intervals $(I_{n})$ with the unit interval.

However, the counterexamples used earlier in the paper for $R^{2}$ do not reduce to $R$ .

The equivalence of While ( R ) and While ∗ ( R )

We wish to justify our claims that the $While (R)$ and ${While}^{*} (R)$ are equivalent in terms of computing power.

A similar result was shown in [31, Section 4] for a total algebra $R_{t}$ on the reals,19

¹⁹

$R_{t}$ is equivalent to $R$ except for the definitions of ${eq}^{R}$ and ${less}^{R}$ , which are taken to have their standard, total meaning. It was simply called $R$ in [31, Section 4].

by showing that:

We may use the same technique to show that $While (R) = {While}^{*} (R)$ (and similarly for ${While}^{OR}$ and ${While}^{NE}$ and their starred versions). Steps (2) and (3) can be easily inferred from the respective proofs for $R_{t}$ in [31, Section 4], as most of the proofs of those facts involve primitive recursive operations on the syntax of the While language, and so the partiality of $R$ is irrelevant. In these proofs, the only step that involves semantics is the use of term evaluation to traverse a “computation tree” for the universal $While (A)$ procedure for ${While}^{*} (A)$ programs. In that step, however, if a term which is evaluated diverges, the ${While}^{*} (A)$ program being simulated by the universal procedure would diverge as well, and so the universal procedure behaves as expected.

So we proceed with a proof of Step (1), i.e. that $R$ has the term evaluation property (cf. [31, Example 4.5]).

In this proof, we must work with encodings of the syntactic expressions used in the While language. We assume given a family of effective numerical codings for each of the classes of syntactic expressions over Σ. We write $⌜ E ⌝$ for the code of an expression E. We assume that we can go primitive recursively from codes of expressions to codes of their immediate subexpressions and vice versa; thus, for example, $⌜ t_{1} ⌝$ and $⌜ t_{2} ⌝$ are primitive recursive in $⌜ t_{1} + t_{2} ⌝$ , and conversely. In short, we can primitive recursively simulate all operations involved in processing the syntax of the programming language.

For the remainder of this Appendix, let A be any $N$ -standard (possibly partial) algebra, let u and v be product types of A, let $x$ be a u-tuple of variables, let ${Tm}_{x} (Σ)$ be the set of all Σ-terms with variables among $x$ only, and for all sorts s or Σ, let ${Tm}_{x, s} (Σ)$ be the class of such terms of sort s.

We define the term evaluation function on A relative to $x$ $\begin{matrix} {TE}_{x, s}^{A} : {Tm}_{x, s} (Σ) \times State (A) ⇀ A_{s} \end{matrix}$ by $\begin{matrix} {TE}_{x, s}^{A} {(t, σ) ≃ ⟦ t ⟧}^{A} σ . \end{matrix}$

This term evaluation function on A relative to $x$ is then represented by the function $\begin{matrix} {te}_{x, s}^{A} : ⌜ {Tm}_{x, s} (Σ) ⌝ \times A_{u} ⇀ A_{s} \end{matrix}$ defined by $\begin{matrix} {te}_{x, s}^{A} {(⌜ t ⌝, a) ≃ ⟦ t ⟧}^{A} σ, \end{matrix}$ where σ is any state on A such that $σ [x] = a$ .20

²⁰

This is well defined by the Functionality Lemma [31, Lemma 3.4].

The equivalence of $While (R)$ and ${While}^{*} (R)$ now follows from the preceding discussion.

Post’s Theorem for the partial algebra R

For total standard algebras, we have the following theorem [31, Section 5.2], [34, Section 6.1]:

For partial algebras, Post’s Theorem does not always hold [3]. However it holds trivially on $R$ , since semicomputable sets are open by the Structure Theorem for $While (R)$ , and the only clopen subsets of $R^{n}$ ( $n ⩾ 1$ ) are $R^{n}$ and ∅.

References

Andradas,

Bröcker and

Ruiz, Constructible Sets in Real Geometry, Springer, 1996. doi:10.1007/978-3-642-80024-5.

K.R.

Apt and

E.-R.

Olderog, Verification of Sequential and Concurrent Programs, Springer-Verlag, 1991. doi:10.1007/978-1-4757-4376-0.

Armstrong, Notions of semicomputability in topological algebras over the reals, MSc Thesis, Department of Computing & Software, McMaster University, 2015, Archived in DSpace at http://hdl.handle.net/11375/18334.

Bournez,

M.L.

Campagnolo,

D.S.

Graça and

Hainry, Polynomial differential equations compute all real computable functions, Journal of Complexity 23 (2007), 317–335. doi:10.1016/j.jco.2006.12.005.

Bournez,

Graça and

Pouly, On the functions generated by the general purpose analog computer, Information and Computation 257 (2017), 34–57. doi:10.1016/j.ic.2017.09.015.

Bournez,

Graça and

Pouly, Polynomial time corresponds to solutions of polynomial ordinary differential equations, Journal of the Association for Computing Machinery 64(6) (2017), 38:1–38:76. doi:10.1145/3127496.

Church, An unsolvable problem of elementary number theory, American Journal of Mathematics 58 (1936), 345–363. doi:10.2307/2371045.

Courant and

Hilbert, Methods of Mathematical Physics, Vol. II, Interscience, 1953, Translated and revised from the German edition [1937].

J.W.

de Bakker, Mathematical Theory of Program Correctness, Prentice Hall, 1980.

10.

D.S.

Dummit and

R.M.

Foote, Abstract Algebra, John Wiley and Sons, 1991.

11.

Engeler, Formal Languages: Automata and Structures, Markham, 1968.

12.

M.Q.

Fu, Models of computability of partial functions on the reals, MSc Thesis, Department of Computing & Software, McMaster University, 2007, Technical Report CAS-08-01-JZ, January 2008.

13.

M.Q.

Fu, Characterizations of semicomputable sets, and computable partial functions, on the real plane, PhD Thesis, Department of Computing & Software, McMaster University, 2014, Archived in DSpace at http://hdl.handle.net/11375/16066.

14.

M.Q.

Fu and

J.I.

Zucker, Models of computation for partial functions on the reals, Journal of Logical and Algebraic Methods in Programming (2015). doi:10.1016/j.jlamp.2014.11.001.

15.

D.S.

Graça and

J.F.

Costa, Analog computers and recursive functions over the reals, Journal of Complexity 19 (2003), 644–664. doi:10.1016/S0885-064X(03)00034-7.

16.

Grzegorczyk, Computable functions, Fundamenta Mathematicae 42 (1955), 168–202. doi:10.4064/fm-42-1-168-202.

17.

Grzegorczyk, On the defintions of computable real continuous functions, Fundamenta Mathematicae 44 (1957), 61–71.

18.

Hadamard, Lectures on Cauchy’s Problem in Linear Partial Differential Equations, Dover, 1952, Translated from the French edition [1922].

19.

Hadamard, La Théorie des Équations aux Dérivées Partielles, Éditions Scientifiques, 1964.

20.

S.C.

Kleene, General recursive functions of natural numbers, Mathematische Annalen 112 (1936), 727–742. doi:10.1007/BF01565439.

21.

S.C.

Kleene, Introduction to Metamathematics, North Holland, 1952.

22.

Lacombe, Extension de la notion de fonction récursive aux fonctions d’une ou plusieurs variables réelles, I, C.R. Acad. Sci. Paris 240 (1955), 2470–2480.

23.

Lacombe, Extension de la notion de fonction récursive aux fonctions d’une ou plusieurs variables réelles, II, C.R. Acad. Sci. Paris 241 (1955), 13–14.

24.

Lacombe, Extension de la notion de fonction récursive aux fonctions d’une ou plusieurs variables réelles, III, C.R. Acad. Sci. Paris 241 (1955), 151–153.

25.

Poças, Analog computability in differential equations, PhD Thesis, Department of Mathematics & Statistics, McMaster University, 2017, archived in DSpace at http://hdl.handle.net/11375/22593.

26.

M.B.

Pour-El and

J.I.

Richards, Computability in Analysis and Physics, Springer-Verlag, 1989. doi:10.1007/978-3-662-21717-7.

27.

Shannon, Mathematical theory of the differential analyser, Journal of Mathematics and Physics 20 (1941), 337–354. doi:10.1002/sapm1941201337.

28.

Stoltenberg-Hansen and

J.V.

Tucker, Concrete models of computation for topological algebras, Theoretical Computer Science 219 (1999), 347–378. doi:10.1016/S0304-3975(98)00296-5.

29.

Stoltenberg-Hansen and

J.V.

Tucker, Computable and continuous homomorphisms on metric partial algebras, Bulletin of Symbolic Logic 9 (2003), 299–334. doi:10.2178/bsl/1058448675.

30.

Tucker and

J.I.

Zucker, Computation by ‘while’ programs on topological partial algebras, Theoretical Computer Science 219 (1999), 379–420. doi:10.1016/S0304-3975(98)00297-7.

31.

Tucker and

J.I.

Zucker, Computable functions and semicomputable sets on many-sorted algebras, in: Handbook of Logic in Computer Science, Vol. 5,

Abramsky,

Gabbay and

Maibaum, eds, Oxford University Press, 2000, pp. 317–523.

32.

Tucker and

J.I.

Zucker, Abstract versus concrete computation on metric partial algebras, ACM Transactions on Computational Logic 5 (2004), 611–668. doi:10.1145/1024922.1024924.

33.

Tucker and

J.I.

Zucker, Computable total functions, algebraic specifications and dynamical systems, Journal of Logic and Algebraic Programming 62 (2005), 71–108. doi:10.1016/j.jlap.2003.10.001.

34.

Tucker and

J.I.

Zucker, Generalizing computability theory to abstract algebras, in: Turing’s Revolution. The Impact of His Ideas About Computability,

Sommaruga and

Strahm, eds, Birkhauser/Springer Basel, 2015, pp. 127–160. doi:10.1007/978-3-319-22156-4_5.

35.

A.M.

Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society 42 (1936), 230–265, With correction, ibid., 43, 544–546, 1937. Reprinted in The Undecidable, M. Davis, ed., Raven Press, 1965.

36.

Weihrauch, Computable Analysis: An Introduction, Springer, 2000. doi:10.1007/978-3-642-56999-9.

37.

Xie,

M.Q.

Fu and

Zucker, Characterizations of semicomputable sets of real numbers, Journal of Logic and Algebraic Programming 84 (2015), 124–154. doi:10.1016/j.jlap.2013.11.001.

Notions of semicomputability in topological algebras over the reals

Abstract

Keywords

1. Introduction

1.1. Generalising computability theory

1.2. Related work

1.3. Overview

1.4. Previous work

2. Signatures; algebras; the While language

2.1. Basic algebraic definitions

1 We use ⇀ in place of → to signify that a function is partial.

Definition 2.3 ( N -standard signatures and algebras).

Remark 2.4. All signatures and algebras in this paper will be assumed to be N -standard (and hence also standard). So Σ refers to any N -standard signature and A to any N -standard algebra. 2.2. Relations and projections

Notation 2.5. For a Σ-product type u = s 1 × ⋯ × s m , we write A u = df A s 1 × ⋯ × A s m A relation R on A of type u (written R : u ) is a subset of A u . The complement of a relation R : u is the relation R c = A u ∖ R = { a ∈ A u ∣ a ∉ R } Definition 2.6 (Projection).

2.3. Topological partial algebras

Definition 2.7 (Continuity).

Definition 2.8 (Topological partial algebra).

Discussion 2.9 (Continuity of computable functions).

2.4. The algebra R of reals

2 In [14] ‘ R ’ was used for the algebra of reals which also included the multiplicative inverse operation on the reals. ‘ R 0 ’ referred to the algebra without the multiplicative inverse.

Discussion 2.12 (Conditional boolean operators).

Discussion 2.13 (Motivation for use of partial functions).

3 When using effective Cauchy sequences as a representation, we assume given a computable modulus of convergence; given this, we can (by effectively taking subsequences) easily restrict our attention to sequences which are fast.

2.6. Syntax of terms and the While programming language

4 That is, a Σ-term of sort bool.

5 We overload the symbols ↑, ↓ and ≃, discussed in Notation 2.10 where they deal with the definedness of terms, for use with statements and procedures. Here instead of definedness they refer to the convergence or divergence of computations.

2.9. Extending While to While OR and While NE

7 cf. the two definitions of infinite disjunction given in Discussion 3.3.

Definition 3.2 (Semantic Disjointedness).

Discussion 3.3 (Semantics of infinite disjunction).

Remark 3.6. Engeler’s Lemma can be proved by an analysis of the computation trees for While programs [31]. It was originally stated in [11] without the semantic disjointedness property; this property was subsequently noted in [37, Section 4]. 3.2. Canonical form for Bool ( R ) ( x )

Lemma 3.7 (Canonical form for Bool ( R ) ( x ) ).

8 Note that this “canonical form” is not unique.

Definition 3.8 (Basic set).

Remark 3.9. In this paper, polynomials are always taken as having rational [or, equivalently, integer] coefficients. Note that all basic sets are open.9 9 We use “basic sets” to mean “basic open semialgebraic sets”. Definition 3.10 (Semi-algebraic set).

Definition 3.13 (Positive, negative and divergent sets of booleans).

4. While ( R ) semicomputable sets: Structure Theorem and failure of closure under union

Convention 4.1. For the remainder of this section, let x ≡ ( x 1 , x 2 ) . 4.1. Partition Lemma for booleans in Bool ( R ) ( x )

Lemma 4.2 (Partition Lemma for booleans in Bool ( R ) ( x ) ).

10 cf. Definition 3.13. For our purpose, the form of the divergent set of b , DS ( b ) , is unimportant.

Theorem 1 (Structure Theorem for While ( R ) ).

Proposition 4.6 (Closure of While semicomputable sets under union for total standard algebras).

Example 4.7 (A union of two basic sets which is not basic).

13 We thank Professor Bröcker (Münster) for pointing this out (personal communication).

5.1. A set which is projectively While ( R ) semicomputable but not While ( R ) semicomputable

6.1. Conclusion

6.2. Future work

Footnotes

Acknowledgements

Inequivalence results for 1 dimension

The equivalence of While ( R ) and While ∗ ( R )

Post’s Theorem for the partial algebra R

References

¹
We use ⇀ in place of → to signify that a function is partial.

Definition 2.3 ( $N$ -standard signatures and algebras).

Remark 2.4.
All signatures and algebras in this paper will be assumed to be $N$ -standard (and hence also standard). So Σ refers to any $N$ -standard signature and A to any $N$ -standard algebra.

2.2. Relations and projections

2.4. The algebra $R$ of reals

²
In [14] ‘ $R$ ’ was used for the algebra of reals which also included the multiplicative inverse operation on the reals. ‘ $R_{0}$ ’ referred to the algebra without the multiplicative inverse.

³
When using effective Cauchy sequences as a representation, we assume given a computable modulus of convergence; given this, we can (by effectively taking subsequences) easily restrict our attention to sequences which are fast.

⁴
That is, a Σ-term of sort bool.

⁵
We overload the symbols ↑, ↓ and ≃, discussed in Notation 2.10 where they deal with the definedness of terms, for use with statements and procedures. Here instead of definedness they refer to the convergence or divergence of computations.

2.9. Extending While to ${While}^{OR}$ and ${While}^{NE}$

⁷
cf. the two definitions of infinite disjunction given in Discussion 3.3.

Remark 3.6.
Engeler’s Lemma can be proved by an analysis of the computation trees for While programs [31]. It was originally stated in [11] without the semantic disjointedness property; this property was subsequently noted in [37, Section 4].

3.2. Canonical form for $Bool (R) (x)$

Lemma 3.7 (Canonical form for $Bool (R) (x)$ ).

⁸
Note that this “canonical form” is not unique.

Remark 3.9.
In this paper, polynomials are always taken as having rational [or, equivalently, integer] coefficients.

Note that all basic sets are open.9
⁹
We use “basic sets” to mean “basic open semialgebraic sets”.

Definition 3.10 (Semi-algebraic set).

4. $While (R)$ semicomputable sets: Structure Theorem and failure of closure under union

Convention 4.1.
For the remainder of this section, let $x \equiv (x_{1}, x_{2})$ .
4.1. Partition Lemma for booleans in $Bool (R) (x)$

Lemma 4.2 (Partition Lemma for booleans in $Bool (R) (x)$ ).

¹⁰
cf. Definition 3.13. For our purpose, the form of the divergent set of $b$ , $DS (b)$ , is unimportant.

Theorem 1 (Structure Theorem for $While (R)$ ).

¹³
We thank Professor Bröcker (Münster) for pointing this out (personal communication).

5.1. A set which is projectively $While (R)$ semicomputable but not $While (R)$ semicomputable