Generalizing Computability Theory to Abstract Algebras

Abstract

We present a survey of our work over the last four decades on generalizations of computability theory to many-sorted algebras. The following topics are discussed, among others: (1) abstract v concrete models of computation for such algebras; (2) computability and continuity, and the use of many-sorted topological partial algebras, containing the reals; (3) comparisons between various equivalent and distinct models of computability; (4) generalized Church-Turing theses.

AMS Classifications: 03D75, 03D78

1 Introduction

Since 1936, most of the development of computability theory has focused on sets and functions of strings and natural numbers—though computability theory immediately found applications, first in logic and algebra and then pretty much everywhere. Indeed, recall that when Turing created his model of computation on strings [38], he applied it to solve a problem involving real numbers. The applications were via codings or representations of other data.

Why would we want to generalize classical computability theory from strings and natural numbers to arbitrary abstract algebras? How should we do it?

Computability theory is a general theory about what and how we compute. At its heart is the notion of an algorithm that processes data. Today, algorithms and data abound in all parts of our professional, social and personal lives. Data are composed of numbers, texts, video and audio. We know that, being digital, this vast range of data is coded or represented by bitstrings (or strings over a finite alphabet). However, the algorithms that make data useful are created specifically for a high-level, independent model of the data close to the use and users of the data. Therefore, computability theory cannot be content with bitstrings and natural numbers.

Now, the algorithms are designed to schedule sequences of basic operations and tests on the data in order to accomplish a task. They are naturally high-level and their level of abstraction is defined by the nature of the basic operations and tests. In fact, a fundamental observation is this:

What an algorithm knows of the data it processes is precisely determined

by what operations and tests on the data it can employ.

This is true of strings and natural numbers, of course. This observation leads to the fundamental idea of an abstract data type in computer science. Mathematically, an implementation of a data type is modelled by an algebraic structure with operations and relations, and an abstract data type is modelled by a class of algebraic structures. The signature of an algebra is a syntactic interface to the operations and tests. The abstract data type can be specified by giving a signature and a set of axioms that the operators and relations must satisfy. The algebraic theory of abstract data types is a theory about all data, now and in the future.

What about the models of computation? Thanks to computer science, there is an abundance of computation models, practical and theoretical. Even within the theory of computation, the diversity is daunting: so many motivations, intuitions and technical developments.¹ In this chapter we will give an introduction to one abstract model of computation for an arbitrary abstract algebra. Our account will be rather technical and very quick, but it will contain what we think are the key ideas that can launch a whole mathematical theory and sustain its application. The model is a simple form of imperative programming, being an idealised programming language for manipulating data in a store using the constructs of assignments, sequencing, conditionals and iteration. By concentrating on this model the reader will be able to explore and benchmark other models, however complicated or obscure their origins.

To make some sense of the jungle of models of computation, we discuss, in Sect. 2, two basic types of model, abstract and concrete. The distinction is invaluable when we meet other models, and applications to specific data types, later in Sect. 8. The first part of this chapter introduces data types modelled by algebras (Sect. 3) and the imperative programming model (Sect. 4), and covers universality (Sect. 5), and semicomputability (Sect. 6). Here we consider only the case where algebras have total operations and tests. Next (Sect. 7) we look closely at data types with continuous operations, such as the real numbers. At this point the theory deepens. New questions arise and there are a number of changes to the imperative model, not least the use of algebras that have partial operations and tests and the need for nondeterministic constructs. Finally (Sect. 8) we take a quick look other models and propose some generalizations of the Church-Turing thesis to abstract many-sorted algebras.

2 On Generalizing Computability Theory

By a computability theory we mean a theory of functions and sets that are definable using a model of computation. By a model of computation we mean a theoretical model of some general method of calculating the value of a function or of deciding, or enumerating, the elements of a set. We allow the functions and sets to be constructed from any kind of data. Thus, classical computability theory on the set $\mathbb{N}$ of natural numbers is made up of many computability theories (based upon Turing machines, recursive definitions, register machines, etc.).

We divide computability theories into two types:

In an abstract computability theory the computations are independent of all the representations of the data. Computations are uniform over all representations and are necessarily isomorphism invariant. Typical of abstract models of computation are models based on abstract ideas of program, equation, recursion scheme, or logical formula.

In a concrete computability theory the computations are dependent on some data representation. Computations are not uniform, and different representations can yield different results. Computations are not automatically isomorphism invariant. Typical of concrete models of computation are those based on concrete ideas of coding, numbering, or data representations using numbers or functions.

Now in computer science, it is obvious that a computation is fundamentally dependent on its data. By a data type we mean

(1) data,

together with

(2) some primitive operations and tests on these data.

Often we also have in mind the ways these data are

(3) axiomatically specified, and

(4) represented or implemented.

To choose a computation model, we must think carefully about what forms of data the user may need, how we might model the data in designing a system—where some high level but formal understanding is important—and how we might implement the data in some favoured programming language.

We propose the working principle:

Any computability theory should be focused equally on the data types and

the algorithms.

Now this idea may be difficult to appreciate if one works in one of the classical computability theories of the natural numbers, for data representations rarely seem to be an important topic there. Although the translation between Turing machines and register machines involves data transformations, these can be done on an ad hoc basis.

However, representations are always important. Indeed, representations are a subject in themselves. This is true even in the simple cases of discrete data forming countable sets and structures. From the beginning there has been a great interest in comparisons between different kinds of numberings, for example in Mal’cev’s theory of computability on sets and structures [18]. The study of different notions of reduction and equivalence of numberings, and the space of numberings, has had a profound influence on the theory and has led to quite remarkable results, such as Goncharov’s Theorem and its descendants² [5, 24]. These notions also include the idea of invariance under computable isomorphisms, prominent in computable algebra, starting in [10]. In the general theory of computing with enumerated structures, there was always the possibility of computing relative to a reasonable numbering that was standard in some sense. For example, earlier work on the word problem for groups, such as [19], and on computable rings and fields, such as [22], was not concerned with the choice of numberings.

We see the importance of representations even more clearly when computing with continuous data forming uncountable sets. For example, in computing with real numbers, it has long been known that if one represents the reals by infinite decimal expansions then one cannot even compute addition (consider, e.g., 0. 333⋯ + 0. 666…). But if one chooses the Cauchy sequence representations then a great deal is computable [3].

In general, what is the relationship between abstract and concrete computability models with a common set of data D?

Let $\mathbf{\mathit{AbstComp}}_{\mathbf{\mathit{A(D)}}}$ be the set of functions on the data set D that are computable in an abstract model of computation associated with a structure A containing D.

Let ConcComp_R(D) be the set of functions on D that are computable in a concrete model of computation with representation R.

• Soundness: An abstract model of computation AbstComp_A(D) is sound for a concrete model of computation ConcComp_R(D) if

  $$\displaystyle{\boldsymbol{AbstComp}_{A}(D)\ \subseteq \ \boldsymbol{ConcComp}_{R}(D).}$$

• Adequacy: An abstract model of computation AbstComp_A(D) is adequate for a concrete model of computation ConcComp_R(D) if

  $$\displaystyle{\boldsymbol{ConcComp}_{R}(D)\ \subseteq \ \boldsymbol{AbstComp}_{A}(D).}$$

• Completeness: An abstract model of computation AbstComp_A(D) is complete for a concrete model of computation ConcComp_RD if it is both sound and adequate, i.e.,

  $$\displaystyle{\boldsymbol{AbstComp}_{A}(D)\ =\ \boldsymbol{ConcComp}_{R}(D).}$$

As an example for the l.h.s. here, let us take the data set $D = \mathbb{R}$, the set of reals, the structure $A = \mathcal{R}_{\mathsf{p}}^{N}$, the partial algebra $\mathcal{R}_{\mathsf{p}}$ of reals defined below in Sect. 7, with the naturals adjoined, and $\boldsymbol{AbstComp}_{A}(D) = \boldsymbol{While}^{\boldsymbol{{\ast}}}(\mathcal{R}_{\mathsf{p}}^{N})$, the set of functions on $\mathbb{R}$ definable by the While programming language with arrays over $\mathcal{R}_{\mathsf{p}}^{N}$ defined in Sect. 5. For the r.h.s., take a standard enumeration $\mbox{ $\alpha $}: \mathbb{N} \rightarrow \mbox{ $\mathbb{Q}$}$ of the rationals, which generates a representation $\overline{\alpha }$ of the computable reals (as described in Sect. 7.1.1 below), and let $\boldsymbol{ConcComp}_{\overline{\alpha }}(\mathbb{R})$ be the corresponding “$\overline{\alpha }$-tracking” model. Then our abstract model is sound, but not adequate, for this concrete model:

$$\displaystyle{ \boldsymbol{While}^{\boldsymbol{{\ast}}}(\mathcal{R}_{\mathsf{ p}})\ \subsetneq \ \boldsymbol{ConcComp}_{\overline{\alpha }}(\mathbb{R}). }$$

On the other hand, if we take for our abstract model over $\mathcal{R}_{\mathsf{p}}$ the non-deterministic $\boldsymbol{WhileCC}^{\boldsymbol{{\ast}}}$ (While + “countable choice” + arrays) language, and further replace “computability” by “approximable computability” [33, 34], then we obtain completeness (see Sect. 7.3 below):

$$\displaystyle{ \boldsymbol{WhileCC}^{\boldsymbol{{\ast}}}\!-\boldsymbol{approx}(\mathcal{R}_{\mathsf{ p}})\ =\ \boldsymbol{ConcComp}_{\overline{\alpha }}(\mathbb{R}). }$$

(1)

3 While Computation on Standard Many-Sorted Total Algebras

We will study a number of high level imperative programming languages based on the “ while” construct, applied to a many-sorted signature $\varSigma$. We give semantics for these languages relative to a total Σ-algebra A, and define the notions of computability, semicomputability and projective semicomputability for these languages on A. Much of the material is taken from [31].

We begin by reviewing basic concepts: many-sorted signatures and algebras. Next we define the syntax and semantics of the While programming language. Then we extend this language with special programming constructs to form two new languages: While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$.

3.1 Basic Concepts: Signatures and Partial Algebras

A many-sorted signature Σ is a pair $\langle \boldsymbol{Sort}(\varSigma ),\boldsymbol{Func}\,(\varSigma )\rangle$ where

• (a) Sort(Σ) is a finite set of basic types called sorts s, s′,….

• (b) Func (Σ) is a finite set of basic function symbols

  $$\displaystyle{F: \mbox{ $s_{1} \times \cdots \times s_{m}$} \rightarrow s\ \ \ \ \ \ \ \ \ \ (m \geq 0).}$$

The case m = 0 gives a constant symbol; we then write $F: \ \rightarrow s$.

A product type has the form s₁ ×⋯ × s_m (m ≥ 0), where s₁, …, s_m are sorts. We write u, v, … for product types. A function type has the form u → s, where u is a product type.

A Σ-algebra A has, for each $\mbox{ $\varSigma $}$-sort s, a non-empty set A_s, the carrier of sort s, and for each Σ-function symbol $F: \mbox{ $s_{1} \times \cdots \times s_{m}$} \rightarrow s$, a (basic) function

$$\displaystyle{\mbox{ $F^{A}$}: \mbox{ $A^{u}$} \rightarrow A_{s}}$$

where $u = \mbox{ $s_{1} \times \cdots \times s_{m}$}$, and $\mbox{ $A^{u}$}\ =\ A_{s_{1}} \times \cdots \times A_{s_{m}}$.

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

A Σ-algebra is called total if all the basic functions are total; it is called partial in the absence of such an assumption. Sections 3–6 will be devoted to total algebras. In Sect. 7 we will turn to a more general theory, with partial algebras.

Example 3.1.1 (Booleans)

The signature $\mbox{ $\varSigma (\mathcal{B})$}$ of the booleans is

The algebra B of booleans contains the carrier of sort bool, and the standard interpretations of the constant and function symbols of $\varSigma (\mathcal{B})$.

Note that for a structure A to be useful for computational purposes, it should be susceptible to testing, which means it should contain the carrier $\mathbb{B}$ of booleans and the standard boolean operations; in other words, it should contain the algebra B as a retract. Such an algebra A is called standard. All the examples of algebras discussed below will be standard.

Example 3.1.2 (Naturals)

The signature $\mbox{ $\varSigma $}(\mbox{ $\mathcal{N}$})$ of the naturals is

The algebra $\mbox{ $\mathcal{N}$}$ of naturals consists of the carrier $\mbox{ $\mathbb{N}$} =\ \{ 0,1,2,\ldots \}$ of sort nat, the carrier $\mbox{ $\mathbb{B}$}$ of sort bool, and the standard constants and functions $0_{\mathsf{N}}: \ \rightarrow \mbox{ $\mathbb{N}$}$, $\mathsf{suc}_{\mathsf{N}}:\ \mbox{ $\mathbb{N}$} \rightarrow \mbox{ $\mathbb{N}$}$, and $\mbox{ $\mathsf{eq}_{\mathsf{N}}$},\mbox{ $\mathsf{less}_{\mathsf{N}}$}: \mbox{ $\mathbb{N}$}^{2} \rightarrow \mbox{ $\mathbb{B}$}$ (as well as the standard boolean operations).

We will use the infix notations “ = ” and “ < ” for “eq_N” and “less_N”, and also use “$\mbox{ $\vee $}$” and “$\mbox{ $\wedge $}$” for the boolean operations “or” and “and”.

Example 3.1.3 (Total Algebra of Reals)

The signature $\mbox{ $\varSigma $}(\mbox{ $\mathcal{R}$}_{\mathsf{t}})$ of the total algebra of reals is:

(We will study a partial algebra of reals in Sect. 7.) The algebra $\mbox{ $\mathcal{R}$}_{\mathsf{t}}$ of reals has the carrier $\mbox{ $\mathbb{R}$}$ of sort real, as well as the imported carrier $\mbox{ $\mathbb{B}$}$ of sort bool with the boolean operations, the real constants and operations ($0,1,+,\times,-$), and the (total) boolean-valued functions $\mathsf{eq}_{\mathsf{R}}: \mathbb{R}^{2} \rightarrow \mathbb{B}$. and $\mathsf{less}_{\mathsf{R}}:\mathbb{R}^{2} \rightarrow \mathbb{B}$. Again, we will use the infix notations “ = ” and “ < ” for these.

Definition 3.1.4 (Minimal Carriers; Minimal Algebra)

Let A be a Σ-algebra, and s a Σ-sort.

• (a) A is minimal at s (or the carrier A_s is minimal in A) if A_s is generated by the closed Σ-terms of sort s.

• (b) A is minimal if it is minimal at every Σ-sort.

To take two examples:

• Every N-standard algebra (see Sect. 3.3) is minimal at sorts bool and nat.

• The algebra $\mbox{ $\mathcal{R}$}_{\mathsf{t}}$ of reals (Example 3.1.3) is not minimal at sort real.

3.2 Syntax and Semantics of Σ-Terms

For a signature Σ, the set Tm(Σ) of Σ-terms is defined from Σ-variables x^s, … of sort s (for all Σ-sorts s) by

$$\displaystyle{t^{s}::= \mathtt{x}^{s}\vert F(t_{ 1}^{s_{1} },\ldots,t_{m}^{s_{m} })}$$

where F is a Σ-function symbol of type $\mbox{ $s_{1} \times \cdots \times s_{m}$} \rightarrow \ s$.

We write t: s to indicate that t is a Σ-term of sort s, and more generally, t: u to indicate that t is a tuple of terms of product type u. We also write b, … for boolean Σ-terms, i.e. Σ-terms of sort bool.

We turn to the semantics of terms.

A state over an algebra A is a family $\langle \mbox{ $\sigma _{s}$}\mid s \in \boldsymbol{Sort}(\varSigma )\rangle$ of functions $\mbox{ $\sigma $}_{s}: \boldsymbol{V ar}_{s} \rightarrow \mbox{ $A_{s}$}$ (where Var_s is the set of variables of sort s). Let State(A) be the set of states on A. We will write $\mbox{ $\sigma $}(\mathtt{x})$ for $\mbox{ $\sigma $}_{s}(\mathtt{x})$ where x: s. Also, for a tuple $\mathtt{x} \equiv (\mbox{ $\mathtt{x}_{1},\ldots,\mathtt{x}_{m}$})$, we write σ[x] for $(\mbox{ $\sigma $}(\mathtt{x}_{1}),\ldots,\mbox{ $\sigma $}(\mathtt{x}_{m}))$.

Let σ be a state over A, and for some Σ-product type u, let $\mathtt{x} \equiv (\mbox{ $\mathtt{x}_{1},\ldots,\mathtt{x}_{n}$}): u$ and $a = (\mbox{ $a_{1},\ldots,a_{n}$}) \in \mbox{ $A^{u}$}$ (for n ≥ 1). We define the variant$\mbox{ $\sigma $}\{\mathtt{x}/a\}$ to be the state over A formed from σ by replacing its value at x_i by a_i for i = 1, …, n.

For a term t: s, we will define the function

$$\displaystyle{\mbox{ $[\![t]\!]$}^{A}:\ \boldsymbol{State}(A) \rightarrow \mbox{ $A_{ s}$}}$$

where [​[t]​]^Aσ is the value of t in A at state σ.

The definition of $\mbox{ $[\![t]\!]^{A}$}\mbox{ $\sigma $}$ is by structural induction on Σ-terms t:

$$\displaystyle{ \begin{array}{rl} \mbox{ $[\![\mathtt{x}]\!]^{A}$}\mbox{ $\sigma $}\ & =\ \mbox{ $\sigma $}(\mathtt{x}) \\ \mbox{ $[\![F(t_{1},\ldots,t_{m})]\!]^{A}$}\mbox{ $\sigma $}\ & =\ F^{A}(\mbox{ $[\![t_{1}]\!]^{A}$}\mbox{ $\sigma $},\ldots,\mbox{ $[\![t_{m}]\!]^{A}$}\mbox{ $\sigma $})\end{array} }$$

(2)

3.3 Adding Counters: N-Standard Signatures and Algebras

A signature Σ is N-standard if (1) it is standard (see Sect. 3.1), and (2) it contains the standard signature of naturals (Example 3.1.2), i.e., $\mbox{ $\varSigma $}(\mbox{ $\mathcal{N}$})\ \subseteq \mbox{ $\varSigma $}$.

Given an N-standard signature Σ, a Σ-algebra A is N-standard if it is an expansion of $\mbox{ $\mathcal{N}$}$, i.e., it contains the carrier $\mbox{ $\mathbb{N}$}$ with the standard arithmetic operations.

N-standardness is clearly very useful in computation, with the presence of counters, and the facility for enumerations and numerical coding.

Any standard signature Σ can be “N-standardised” to a signature Σ^N by adjoining the sort nat and the operations 0, suc, eq_N and less_N. Correspondingly, any standard Σ-algebra A can be N-standardised to an algebra A^N by adjoining the carrier $\mbox{ $\mathbb{N}$}$ together with the corresponding arithmetic and boolean functions on $\mbox{ $\mathbb{N}$}$.

3.4 Adding Arrays: Algebras A^∗ of Signature Σ^∗

Given a standard signature Σ, and standard Σ-algebra A, we expand Σ and A in two stages: (1) N-standardise these to form Σ^N and A^N, as in Sect. 3.3; and (2) define, for each sort s of Σ, the carrier A_s^∗ to be the set of finite sequences or arrays a^∗ over A_s, of “starred sort” s^∗.

The resulting algebras A^∗ have signature Σ^∗, which extends Σ^N by including, for each sort s of Σ, the new starred sorts s^∗, and certain new function symbols to read and update arrays. Details are given in [30, 31].

We conclude this section with a very useful syntactic conservativity theorem, which says that every Σ^∗-term with sort in Σ is effectively semantically equivalent to a Σ-term. This theorem will be used later for proving universality for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computations by a While^N procedure (Theorem 3^∗) and deriving a strong form of Engeler’s Lemma (Theorem 8).

Theorem 1 ($\boldsymbol{\varSigma }^{{\ast}}/\varSigma$ Conservativity for Terms)

For every Σ-sort s, every Σ ^∗ -term t of sort s without any variables of starred sort is effectively semantically equivalent ³ to a Σ-term.

4 The While Programming Language

Note that we will use “$\equiv$” to denote syntactic identity between two expressions.

We define Stmt(Σ) to be the class of While(Σ)-statements S, … generated by:

$$\displaystyle{S::= \mathsf{skip}\ \vert \ \mathtt{x}:= t\ \vert \ S_{1}\;S_{2}\ \vert \ \mathsf{if}\ b\ \mathsf{then}\ S_{1}\ \mathsf{else}\ S_{2}\ \mathsf{fi}\ \vert \ \mathsf{while}\ b\ \mathsf{do}\ S_{0}\ \mathsf{od}}$$

where the variable x and term t have the same Σ-sort.

Proc(Σ) is the class of While(Σ)-procedures P, …, of the form:

$$\displaystyle{ P\ \equiv \ \mathsf{proc}\ \mathsf{in}\ \mathtt{a}\ \mathsf{out}\ \mathtt{b}\ \mathsf{aux}\ \mathtt{c}\ \mathsf{begin}\ S\ \mathsf{end} }$$

(3)

where S is the body, and and a, b and c are tuples of (distinct) input, output and auxiliary variables respectively.

If a: u and b: v, then P is said to have type $u \rightarrow v$, written $\mbox{ $P: u \rightarrow v$}$.

We turn to the semantics of statements and procedures.

The meaning [​[S]​]^A of a statement S is a partial state transformer⁴ on an algebra A:

$$\displaystyle{\mbox{ $[\![S]\!]^{A}$}:\ \boldsymbol{State}(A) \rightharpoonup \boldsymbol{State}(A).}$$

Its definition is standard [30, 31] and lengthy, and so we omit it. Briefly, it is based on defining the computation sequence of states from S starting in a state σ, or rather the n-th component of this sequence, by a primary induction on n, and a secondary induction on the size of S.

Next, given a procedure (3) of type u → v, its meaning is a partial function $P^{A}: A^{u} \rightharpoonup A^{v}$ defined as follows. For a ∈ A^u, let $\mbox{ $\sigma $}$ be any state on A such that $\mbox{ $\sigma $}[\mathtt{a}] = a$, and $\sigma [\mathtt{b}]$ and $\mbox{ $\sigma $}[\mathtt{c}]$ are given preassigned default values. Then

$$\displaystyle{P^{A}(a)\ \simeq \ \left \{\begin{array}{@{}l@{\quad }l@{}} \mbox{ $\sigma $}'[b]\quad &\mbox{ if $[\![S]\!]^{A}\sigma \downarrow \sigma '$ (say)} \\ \uparrow \quad &\mbox{ if $[\![S]\!]^{A}\sigma \uparrow $}. \end{array} \right.}$$

Here “$\simeq$” means that the two sides either both converge to the same value, or both diverge (“Kleene equality” [15, Sect. 63]).

We are also using the notation $\mbox{ $[\![S]\!]^{A}$}\mbox{ $\sigma $}\! \downarrow$ to mean that evaluation of [​[S]​]^A at σ halts or converges; $\mbox{ $[\![S]\!]^{A}$}\mbox{ $\sigma $}\! \downarrow \mbox{ $\sigma $}'$ that it converges to $\mbox{ $\sigma $}'$, and $\mbox{ $[\![S]\!]^{A}$}\mbox{ $\sigma $} \uparrow$ that it diverges.

It is worth noting that the semantics of While(Σ) procedures is invariant under Σ-isomorphism.

Modifications in these semantic definitions (equations (2) in Sect. 3.2, and (3) in Sect. 4) required for partial algebras will be indicated in Sect. 7 (Remark 7.3.1).

4.1 While, While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ Computability

A (partial) function f on A is Whilecomputable if $f = \mbox{ $P^{A}$}$ for some While procedure P.

Consider now the While programming language over Σ^N and Σ^∗.

A While^N(Σ) procedure is a While(Σ^N) procedure in which the input and output variables have sorts in Σ. However the auxiliary variables may have sort nat.

Similarly, a $\boldsymbol{While}^{\boldsymbol{{\ast}}}(\mbox{ $\varSigma $})$ procedure is a While(Σ^∗) procedure in which the input and output variables have sorts in Σ. However the auxiliary variables may have starred sorts.

A function f on A is While^N (or $\boldsymbol{While}^{\boldsymbol{{\ast}}}$) computable if $f = \mbox{ $P^{A}$}$ for some While^N (or $\boldsymbol{While}^{\boldsymbol{{\ast}}}$) procedure P.

We write While(A), While^N(A) and $\mbox{ $\boldsymbol{While}^{\boldsymbol{{\ast}}}(A)$}$ for the classes of functions While, While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A.

Remarks 4.1.1

• (a) Clearly, if A is N-standard, then While^N computability coincides with While computability on A.

• (b) Because of the effective enumeration of the set $\mbox{ $\mathbb{N}$}\mbox{ $^{{\ast}}$}$, While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability coincide with While computability on $\mbox{ $\mathcal{N}$}$, which is in turn equivalent to classical partial recursiveness over $\mbox{ $\mathbb{N}$}$.

• (c) $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability will be the basis for a generalized Church-Turing Thesis, as we will see later (Sect. 8.2). On the other hand, While^N computability is useful for representing the syntax of While programming within the formalism, by means of coding (Sect. 5).

5 Representations of Semantic Functions; Universality

We examine whether the While programming language is a so-called universal model of computation. This means answering questions of the following form. Let A be a standard Σ-algebra.

Is there a universal While procedure $\boldsymbol{U}_{\mathsf{proc}} \in \boldsymbol{Proc}(\mbox{ $\varSigma $})$ that can compute

all the While computable functions on A?

To this end we need the techniques of numerical codings (Gödel numberings) and symbolic computations on terms. More accurately, for this to be possible, we need the sort nat, and so we will consider the possibility of representing the syntax of a standard Σ-algebra A (not in A itself, but) in its N-standardisation A^N, or (failing that) in the array algebra A^∗. We will see that

For any given Σ-algebra A, there is a universal While procedure over A

if, and only if, there is a While program for term evaluation over A.

Consequently, since term evaluation is always $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A, we have

For any Σ-algebra A there is a universal While^∗ program and universal

While ^∗ procedure over A.

Thus, for any algebra A our While^∗ model of computation is universal.

Hence, if the Σ-algebra A has a While program to compute term evaluation, then

$$\displaystyle{\mbox{ $\boldsymbol{While}^{\boldsymbol{{\ast}}}(A)$}\ =\ \mbox{ $\boldsymbol{While}^{N}(A)$}.}$$

5.1 Numbering of Syntax

We assume given families of effective numerical codings of the syntactic classes E with which we deal, i.e., 1–1 maps $\boldsymbol{code}: E \rightarrow \mbox{ $\mathbb{N}$}$, with $\mbox{ $\ulcorner e\urcorner $} = \boldsymbol{code}(e)$ denoting the code of the expression e ∈ E. Further, we assume standard effective numberings of sets such as $\mbox{ $\mathbb{N}$}\mbox{ $^{{\ast}}$}$, $\mbox{ $\mathbb{Q}$}^{2}$, etc. Hence we assume that we can primitive recursively simulate all operations involved in processing the syntax of the programming language.

By “effective(ly)”, we will mean effective in the codes of the syntactic or mathematical objects referred to.

We will use the notation

$$\displaystyle{\mbox{ $\ulcorner \boldsymbol{Tm}\urcorner $}\ =\ \{ \mbox{ $\ulcorner t\urcorner $}\mid t \in \boldsymbol{Tm}\},}$$

etc., for sets of codes of syntactic expressions.

5.2 Representation of States

We will be interested in the representation of various semantic functions on syntactic classes such as Tm(Σ), Stmt(Σ) and Proc(Σ) by functions on A or A^∗, and in the computability of these representing functions. These semantic functions have states as arguments, so we must first define a representation of states.

Let x be a u-tuple of program variables. A state σ on A is represented (relative to x) by a tuple of elements a ∈ A^u if $\sigma [{\rm x}] = {\mathbf{a}}$.

The state representing function

$$\displaystyle{\boldsymbol{Rep}_{\mathtt{x}}^{A}:\ \boldsymbol{State}(A)\ \rightarrow \ \mbox{ $A^{u}$}}$$

is defined by

$$\displaystyle{\boldsymbol{Rep}_{\mathtt{x}}^{A}(\mbox{ $\sigma $})\ =\ \mbox{ $\sigma [\mathtt{x}]$}.}$$

5.3 Representation of Term Evaluation; Term Evaluation Property

Let x be a u-tuple of variables. Let $\boldsymbol{Tm}_{\,\mathtt{x}} = \boldsymbol{Tm}_{\,\mathtt{x}}(\mbox{ $\varSigma $})$ be the class of all Σ-terms with variables among x only, and for all sorts s of Σ, let $\boldsymbol{Tm}_{\,\mathtt{x},s} = \boldsymbol{Tm}_{\,\mathtt{x},s}(\mbox{ $\varSigma $})$ be the class of such terms of sort s.

The term evaluation function on A relative tox

$${\mathbf{TE}}_{\mathtt{x},s}^{A}:\ \boldsymbol{Tm}_{\,\mathtt{x},s} \times \boldsymbol{State}(A)\ \rightarrow \ A_{s},$$

defined by

$${\mathbf{TE}}_{\mathtt{x},s}^{A}(t,\sigma )\ =\ [\![t]\!]^{A}\sigma ,$$

is represented by the function

$${\mathbf{te}}\,_{\mathtt{x},s}^{A}:\ \ulcorner \boldsymbol{Tm}_{\,\mathtt{x},s}\urcorner \times A^{u}\ \rightarrow \ A_{s}$$

defined by

$${\mathbf{te}}\,_{\mathtt{x},s}^{A}(\ulcorner t\urcorner ,\,a)\ =\ [\![t]\!]^{A} \sigma ,$$

where σ is any state on A such that $\mbox{ $\sigma $}[\mathtt{x}] = a$, in the sense that the diagram in Fig. 1 commutes.

Fig. 1

Term evaluation representing function

We will be interested in the computability of this term evaluation representing function.

Definition 5.3.1 (Term Evaluation)

The algebra A has the term evaluation property (TEP) if for all x and s, the term evaluation representing function te _x, s^A is While computable on A^N.

Many well-known varieties (i.e., equationally axiomatisable classes of algebras) have (uniform versions of) the TEP. Examples are: semigroups, groups, and associative rings with or without unity. This follows from the effective normalisability of the terms of these varieties. In the case of rings, this means an effective transformation of arbitrary terms to polynomials.

Thus, for example, the algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ of reals has the TEP.

Theorem 2

The term evaluation representing function on A ^∗ is While computable on A ^∗.

Corollary 5.3.2

The term evaluation representing function on A is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A ^N.

Recall the Definition 3.1.4 of minimal carriers.

Corollary 5.3.3

• (a) If A is minimal at s, then there is a $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable enumeration (or listing) of the carrier A _s , i.e., a surjective total mapping

  $$\displaystyle{\boldsymbol{enum}_{s}^{A}:\ \mbox{ $\mathbb{N}$}\ \rightarrow \ \mbox{ $A_{ s}$},}$$

  which is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A ^N.

• (b) If in addition A has the TEP, then  enum _s ^A  is also  While  computable on A ^N.

Theorem 3 (Universality Characterization Theorem for While Computations)

The following are equivalent:

• (i) A has the TEP;

• (ii) For all Σ-product types u,v, there is a While (Σ ^N ) procedure

  $$\displaystyle{\mbox{ $\mathsf{Univ}_{u\rightarrow v}$}:\ \mathsf{nat} \times u\ \rightarrow \ v}$$

  which is universal for Proc _u→v on A, in the sense that for all  $P \in \boldsymbol{Proc}_{\mbox{ $u \rightarrow v$}}$  and  a ∈ A ^u ,

  $$\displaystyle{\mbox{ $\mathsf{Univ}_{u\rightarrow v}^{A}$}(\mbox{ $\ulcorner P\urcorner $},\,a)\ \simeq \ \mbox{ $P^{A}$}(a).}$$

Using the Σ^∗/Σ conservativity theorem (Theorem 1), we can strengthen the above theorem, so as to construct a universal While(Σ^N) procedure for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computation,

Theorem 3^∗ (Universality Characterization Theorem for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ Computations)

The following are equivalent.

• (i) A has the TEP.

• (ii) For all Σ-product types u,v, there is a While (Σ ^N ) procedure

  $$\displaystyle{\mbox{ $\mathsf{Univ}_{u\rightarrow v}$}:\ \mathsf{nat} \times u\ \rightarrow \ v}$$

  which is universal for Proc _u→v ^∗ on A, in the sense that for all  $P \in \boldsymbol{Proc}_{\mbox{ $u \rightarrow v$}}^{{\ast}}$  and  a ∈ A ^u ,

  $$\displaystyle{\mbox{ $\mathsf{Univ}_{u\rightarrow v}^{A}$}(\mbox{ $\ulcorner P\urcorner $},\,a)\ \simeq \ \mbox{ $P^{A}$}(a).}$$

We conclude that there are universal While^N procedures for While^∗ computation on ℛ_t.

6 Concepts of Semicomputability

We want to generalize the notion of recursive enumerability to many-sorted algebras. There turn out to be many non-equivalent ways to do this.

The primary idea is that a set is While semicomputable if, and only if, it is the domain or halting set of a While procedure; and similarly for While^N and While^∗ semicomputability.

This concept satisfies the standard closure properties (under finite union and intersection) and also Post’s Theorem:

A set is computable if, and only if, it and its complement are semicomputable.

The second idea of importance is that of a projection of a computable or semicomputable set. set. In classical computability theory on $\mbox{ $\mathbb{N}$}$, the class of semicomputable sets is closed under projections, but this is not true in the general case of algebras, as we will see. Projective semicomputability is strictly more powerful (and less algorithmic) than semicomputability.

We will also characterize the semicomputable sets as the sets definable by some effective countable disjunction of boolean valued terms. This result, first observed by E. Engeler, has a number of interesting applications.

Definition 6.0.4

• (a) R is Whilecomputable on A if its characteristic function is.

• (b) R is While semicomputable on A if it is the halting set on A of some While procedure P, i.e., $R\ =\ \{ a \in \mbox{ $A^{u}$}\ \vert \ \mbox{ $P^{A}$}(a) \downarrow \}$.

Examples 6.0.5

We will have need for the notation $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}}$}$ to indicate the algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ without the “ < ” operation.

• (a) On the naturals $\mbox{ $\mathcal{N}$}$ the While semicomputable sets are precisely the recursively enumerable sets, and the While computable sets are precisely the recursive sets.

• (b) On $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}}$}$ the set of naturals (as a subset of $\mbox{ $\mathbb{R}$}$) is While semicomputable, being the halting set of the following procedure:

  $$\displaystyle\begin{array}{rcl} \mathsf{is}\_\mathsf{nat}\ & \equiv \ \ &\mathsf{proc}\ \mathsf{in}\ \mathtt{x}: \mathsf{real} {}\\ & & \quad \mathsf{begin}\ \mathsf{while}\ \mathsf{not}\ \mathtt{x} = 0 {}\\ & & \qquad \quad \ \ \mathsf{do}\ \mathtt{x}:= \mathtt{x}- 1\ \mathsf{od} {}\\ & & \quad \mathsf{end} {}\\ \end{array}$$

• (c) Similarly, the set of integers is While semicomputable on $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}}$}$.

• (d) However, the sets of naturals and integers are Whilecomputable on $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$, as can be easily seen.

• (e) The set of rationals is While semicomputable on $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}}$}$. (Exercise. Hint: Prove this first for $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}N}$}$.)

6.1 Merging Two Procedures; Closure Theorems

The classical “merge” theorems generalize:

Theorem 4

The union and intersection of two While semicomputable relations of the same type are again While semicomputable.

In the case of union, if we assume that (1) A is N-standard, and (2) A has the TEP, then the construction of the “merge” of the two characteristic procedures, i.e., interleaving their steps to form the new procedure, simply follows the classical proof for computation on $\mbox{ $\mathbb{N}$}$. Failing this, the construction of the merge procedure (by structural induction on the pair of statements) is quite challenging. (The tricky case is where both are “while” statements.)

If R is a relation on A of type u, we write the complement of R as $\mbox{ $R^{\mathsf{c}}$} = \mbox{ $A^{u}$}\setminus R$.

Theorem 5 (Post’s Theorem for While Semicomputability)

For any relation R on A

$$\displaystyle{\mbox{ $R$ is}\ \boldsymbol{While}\ \mbox{ computable}\ \ \ \mbox{ $\Longleftrightarrow$}\ \ \ \mbox{ $R$ and $R^{\mathsf{c}}$ are}\boldsymbol{While}\ \mbox{ semicomputable}.}$$

Note that the proofs of the above two theorems depend strongly on the totality of A. (See Remark 7.3.2.)

Another useful closure result, applicable to N-standard structures, is:

Theorem 6 (Closure of While Semicomputability Under $\mbox{ $\mathbb{N}$}$-Projections)

Suppose A is N-standard. If $R \subseteq A^{u\times \mathsf{nat}}$ is While semicomputable on A, then so is its $\mbox{ $\mathbb{N}$}$ -projection $\{\mbox{ $x \in A^{u}$}\mid \exists n \in \mbox{ $\mathbb{N}$}\,R(x,n)\}$.

To outline the proof: From a procedure P which halts on R, we can effectively construct another procedure which halts on the required projection. Briefly, for input x, we search by “dovetailing” for a number n such that P halts on (x, n).

We can generalize this theorem to the case of an A_s-projection for any minimal carrier A_s (recall Definition 3.1.4), provided A has the TEP.

Corollary 6.1.1 (Closure of While Semicomputability Under Projections off Minimal Carriers)

Suppose A is N-standard and has the TEP. Let A _s be a minimal carrier of A. If $R \subseteq A^{u\times s}$ is While semicomputable on A, then so is its projection off A _s.

Note that Corollary 6.1.1 is a many-sorted version of (part of) Theorem 2.4 of [9], cited in [23]. The minimality condition (a version of Friedman’s Condition III) means that search in A_s is computable (or, more strictly, semicomputable) provided A has the TEP. Thus in minimal algebras, many of the results of classical recursion theory carry over, e.g.,

• the domains of semicomputable sets are closed under projection (as above)

• a semicomputable relation has a computable selection function

• a function with semicomputable graph is computable [9, Theorem 2.4].

If, in addition, there is computable equality at the appropriate sorts, other results of classical recursion theory carry over, e.g.,

• the range of a computable function is semicomputable [9, Theorem 2.6].

6.2 Projective While semicomputability and Computability

A set $R \subseteq A^{u}$ is projectivelyWhilesemicomputable (or computable) on A iff R is a projection of a While semicomputable (or computable) set on A, i.e., for some product types u and v,

$$\displaystyle{\forall x \in A^{u}\ \big[x \in R\ \ \Longleftrightarrow\ \ \exists y \in A^{v}: (x,y) \in R'\big].}$$

where R′ is a semicomputable (or computable) subset of A^u×v.

We note that although the emphasis in this subsection is on projective semicomputability, the concept of projective computability will be used in our formulation of a generalized Church-Turing thesis for specifiability (in Sect. 8).

In this connection we note further that

• (1) The concepts of projective $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability and projective $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability coincide, by the projective equivalence theorem (Theorem 10 below).

• (2) Projective $\boldsymbol{While}^{(\boldsymbol{{\ast}})}$ semicomputability is, in general, a broader concept than $\boldsymbol{While}^{(\boldsymbol{{\ast}})}$ semicomputability (Sect. 6.7).

We do, however, have closure of semicomputability in the case of $\mbox{ $\mathbb{N}$}$-projections, i.e., existential quantification over $\mbox{ $\mathbb{N}$}$, as we saw in Theorem 6. Further, we have from Corollary 6.1.1:

Theorem 7

Suppose A is N-standard and minimal and has the TEP. Then on A

$$\displaystyle{\mbox{ projective}\ \boldsymbol{While}\ \,\mbox{ semicomputability}\ \ =\ \boldsymbol{While}\ \,\mbox{ semicomputability.}}$$

6.3 $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ Semicomputability

A relation R on A is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$semicomputable if it is the halting set of some While(Σ^∗) procedure on A^∗.

Again, we have Post’s Theorem for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability and semicomputability, and again, we have closure of $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability under $\mbox{ $\mathbb{N}$}$-projections, and projections off minimal carriers.

Note that we do not have to assume the TEP for the latter (cf. Corollary 6.1.1), since the term evaluation representing function is always $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable.

Example 6.3.1

The subalgebra relation⁵:

$$\displaystyle{\boldsymbol{subalg}^{A}(x,y)\ \ \mbox{ $\Longleftrightarrow$}\ \ \mbox{ $x$ is in the subalgebra of $A$ generated by $y$}}$$

is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable on A. This follows from $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability of term evaluation on A^N (Corollary 5.3.2).

6.4 Projective $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ Semicomputability

A relation R on A is said to be projectively$\boldsymbol{While}^{\boldsymbol{{\ast}}}$computable (or semicomputable) on A if R is a projection of a While(Σ^∗) computable (or semicomputable) relation on A^∗.

Theorem 7 can be re-stated for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability:

Theorem 7^∗

Suppose A is a minimal. Then on A

$$\displaystyle{\mbox{ projective}\boldsymbol{While}^{\boldsymbol{{\ast}}}\mbox{ semicomputability}\ \ =\ \boldsymbol{While}^{\boldsymbol{{\ast}}}\mbox{ semicomputability.}}$$

Note again that the TEP does not have to be assumed here (cf. Theorem 7). Also we are using the fact that if A is minimal then so is A^∗.

Example 6.4.1

In $\mbox{ $\mathcal{N}$}$, the various concepts we have listed: While, While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability, as well as projective While, While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability, all reduce to recursive enumerability over $\mbox{ $\mathbb{N}$}$.

In general, however, projective $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability is strictly broader than projective While^N semicomputability. In other words, projecting along starred sorts is stronger than projecting along simple sorts or nat. (Intuitively, this corresponds to existentially quantifying over a finite, but unbounded, sequence of elements.) An example to show this will be given below.

We do, however, have the following equivalence:

$$\displaystyle{\mathit{projective}\ \boldsymbol{While}^{\boldsymbol{{\ast}}}\mathit{semicomputability\ =\ projective}\boldsymbol{While}^{\boldsymbol{{\ast}}}\mathit{computability.}}$$

This is the projective equivalence theorem for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ (Theorem 10).

6.5 Computation Trees; Engeler’s Lemma

For any While statement S over Σ, we can define a (possibly infinite) computation tree for S. The construction is by structural induction on S. Details are given in [31].

Using this and the Σ/Σ^∗ conservativity theorem (Theorem 1), we can prove the following. Let R be a relation on A.

Theorem 8 (Engeler’s Lemma for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ Semicomputability)

R is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable over A iff R can be expressed as an effective countable disjunction of booleans over Σ.

If, moreover, A has the TEP, then we can say more:

Theorem 9 (Semicomputability Equivalence Theorem)

Suppose A has the TEP. Then the following assertions are equivalent:

• (i) R is While ^N semicomputable on A;

• (ii) R is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable on A.

• (iii) R can be expressed as an effective countable disjunction of booleans over Σ.

The step (i) ⇒ (ii) is trivial, and (ii) ⇒ (iii) is just Engeler’s Lemma for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$. The new step (iii) ⇒ (i) follows from an analysis of the coding of an effective infinite disjunction.

Corollary 6.5.1

Suppose A has the TEP. Then the following are equivalent:

• (i) R is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A;

• (ii) R is While ^N computable on A.

This follows from the above theorem, and Post’s Theorem for While^N and $\boldsymbol{While}^{\boldsymbol{{\ast}}}$.

6.6 Projective Equivalence Theorem for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$

The following theorem uses Engeler’s Lemma, and the $\mbox{ $While^{\boldsymbol{{\ast}}}$}$ computability of term evaluation.

Theorem 10 (Projective Equivalence Theorem)

The following are equivalent:

• (i) R is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable on A;

• (ii) R is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A.

We can strengthen the theorem with a third equivalent clause, if we add an assumption about computability of equality in A.

First we must define certain syntactic classes of formulae over Σ.

Let $\mbox{ $\mathit{\mathbf{Lang}}^{{\ast}}$} = \mbox{ $\mathit{\mathbf{Lang}}(\varSigma ^{{\ast}})$}$ be the first order language with equality over Σ^∗. We are interested in special classes of formulae of Lang^∗.

Formulae of Lang^∗ are formed from the atomic formulae by means of the propositional connectives and universal and existential quantification over variables of any Σ^∗-sort.

Definition 6.6.1 (Classes of Formulae of Lang(Σ^∗))

• (a) An atomic formula is an equality between a pair of terms of the same Σ^∗-sort.

• (b) A bounded quantifier has the form ‘$\forall k < t$’ or “$\exists k < t$”, where t: nat.

• (c) An elementary formula is one with only bounded quantifiers.

• (d) A $\mbox{ $\Sigma _{1}^{{\ast}}$}$formula is formed by prefixing an elementary formula with existential quantifiers only.

• (e) An extended$\mbox{ $\Sigma _{1}^{{\ast}}$}$formula is formed by prefixing an elementary formula with a string of existential quantifiers and bounded universal quantifiers (in any order).

We can show that an extended $\mbox{ $\Sigma _{1}^{{\ast}}$}$ formula is equivalent to a $\mbox{ $\Sigma _{1}^{{\ast}}$}$ formula over Σ. Hence we will use the term “$\mbox{ $\Sigma _{1}^{{\ast}}$}$” to denote (possibly) extended $\mbox{ $\Sigma _{1}^{{\ast}}$}$ formulae.

We can now re-state the projective equivalence theorem in the presence of equality.

Theorem 10⁼ (Projective Equivalence Theorem for Σ^∗ with Equality)

Suppose Σ has an equality operator at all sorts. Then the following are equivalent:

• (i) R is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable on A;

• (ii) R is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A;

• (iii) R is $\mbox{ $\Sigma _{1}^{{\ast}}$}$ definable.

6.7 Semicomputability and Projective Semicomputability on $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$

We apply some of the above ideas and results to the algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$. Details can be found in [31, Sects. 6.2, 6.3]⁶

We begin again with a restatement of the semicomputability equivalence theorem (Theorem 9), for the particular case of $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$.

Theorem 11 (Semicomputability for $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$)

Suppose  $R \subseteq \mbox{ $\mathbb{R}^{n}$}$ (n = 1,2,…). Then the following are equivalent:

• (i) R is While ^N semicomputable on $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ ,

• (ii) R is $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable on $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ ,

• (iii) R can be expressed as an effective countable disjunction

  $$\displaystyle{x \in R\ \mbox{ $\Longleftrightarrow$}\ \bigvee _{i}b_{i}(x)}$$

  where each b _i (x) is a finite conjunction of equations and inequalities of the form

  $$\displaystyle{p(x) = 0\qquad \mbox{ and}\qquad q(x) > 0,}$$

  where p,q are polynomials in  $x \equiv (\mbox{ $x_{1},\ldots,x_{n}$}) \in \mbox{ $\mathbb{R}$}^{n}$ , with coefficients in $\mbox{ $\mathbb{Z}$}$.

We also have:

Theorem 12

In $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ , the following three concepts coincide for subsets of $\mbox{ $\mathbb{R}^{n}$}$ :

• (i) While ^N semicomputability,

• (ii) $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputability,

• (iii) projective While ^N semicomputability.

The proof of equivalence between (iii) and the other two concepts follows from the fact that semialgebraic sets are closed under projection, which in turn follows from Tarski’s quantifier-elimination theorem for real closed fields [16, Chap. 4].

Interestingly, in the algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}^{\mathsf{o}}$}$ (i.e., $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ without the order relation “ < ”), where Tarski’s theorem fails, one can find an example of a relation (namely, “ < ” itself!) which is projectively While semicomputable, but not While (or $\boldsymbol{While}^{\boldsymbol{{\ast}}}$) semicomputable.

On the other hand (returning to $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$) the three equivalent concepts of semicomputability given in Theorem 12 differ from a fourth:

• (iv) projective$\boldsymbol{While}^{\boldsymbol{{\ast}}}$semicomputability,

as we now show.

Example 6.7.1 (A set which is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable, but not projectively While^N semicomputable)

In order to prepare for this example, we must first enrich the structure $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$. Let E = { e₀, e₁, e₂, …} be a sequence of reals such that

$$\displaystyle{\mbox{ for all $i$, \,$e_{i}$ is transcendental over $\mathbb{Q}(e_{0},\ldots,e_{i-1})$}.}$$

We define $\mbox{ $\mathcal{R}_{\mathsf{t}}^{E}$}$ to be the algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ augmented by the set E as a separate sort E, with the embedding $j: E \rightarrow \mbox{ $\mathbb{R}$}$ in the signature, thus:

We write $\mbox{ $\overline{E}$} \subset \mbox{ $\mathbb{R}$}$ for the real algebraic closure of $\mbox{ $\mathbb{Q}$}(E)$.

It is easy to see that $\mbox{ $\overline{E}$}$ is projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable in $\mbox{ $\mathcal{R}_{\mathsf{t}}^{E}$}$. (In fact, $\mbox{ $\overline{E}$}$ is the projection on $\mbox{ $\mathbb{R}$}$ of a While semicomputable relation on $\mbox{ $\mathbb{R}$} \times E^{{\ast}}$.) We must show that, on the other hand, $\mbox{ $\overline{E}$}$ is not projectively While^N semicomputable in $\mbox{ $\mathcal{R}_{\mathsf{t}}^{E}$}$.

Briefly, we proceed by showing that if $F \subseteq \mbox{ $\overline{E}$}$ is any projectively While^N semicomputable set in ℛ_t^E, then, using Engeler’s Lemma and Tarski’s theorem, we can show that F cannot equal $\mbox{ $\overline{E}$}$.

The proof further shows that $\mbox{ $\overline{E}$}$ (although a projection on $\mbox{ $\mathbb{R}$}$ of a While semicomputable relation on $\mbox{ $\mathbb{R}$} \times E^{{\ast}}$) is not a projection of a While^N semicomputable relation in $\mbox{ $\mathcal{R}_{\mathsf{t}}^{E}$}$. In fact, it can be shown (still using Engeler’s Lemma) that $\mbox{ $\overline{E}$}$ is not even a projection of a $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ semicomputable relation on $\mbox{ $\mathbb{R}$}^{n} \times E^{m}$ (for any n, m > 0). Thus to define $\mbox{ $\overline{E}$}$, we must project off the starred sortE^∗, or (in other words) existentially quantify over a finite, but unbounded sequence of elements of E.

7 Computation on Topological Partial Algebras

When one considers the relation between abstract and concrete models, a number of intriguing problems appear. We will explain them by considering a series of examples based on the data type of real numbers. Then we formulate our strategy for solving these problems. The picture for topological algebras in general will be clear from our examples with the reals.

7.1 Abstract Versus Concrete Data Types of Reals; Continuity; Partiality

7.1.1 Abstract and Concrete Data Types of Reals

To compute on $\mbox{ $\mathbb{R}$}$ with an abstract model of computation, we have only to select an algebra A in which $\mbox{ $\mathbb{R}$}$ is a carrier set. Abstract computability on $\mbox{ $\mathbb{R}$}$ is then computability on A, and we may apply the general theory of computable functions on many-sorted algebras outlined in the previous sections.

By contrast, to compute on $\mbox{ $\mathbb{R}$}$ with a concrete model of computation (say the tracking model), we first take a standard enumeration of the rationals $\mbox{ $\alpha $}: \mbox{ $\mathbb{N}$} \rightarrow \mbox{ $\mathbb{Q}$}$, which in turn yields a representation $\mbox{ $\overline{\alpha }$}: C \rightarrow \mbox{ $\mathbb{R}_{\mathsf{c}}$}$ that maps the set $C \subset \mbox{ $\mathbb{N}$}$ of codes of effective fast Cauchy sequences of rationals onto the computable reals $\mbox{ $\mathbb{R}_{\mathsf{c}}$} \subset \mbox{ $\mathbb{R}$}$. With this natural number representation, computable functions on $\mbox{ $\mathbb{R}$}$ are investigated by means of their (classically computable) $\mbox{ $\overline{\alpha }$}$-tracking functions on $\mbox{ $\mathbb{N}$}$ [33, 34].

7.1.2 Continuity

 Computations with real numbers involve infinite data. Computations are finite processes that approximate in some way infinite processes. The topology of $\mbox{ $\mathbb{R}$}$ defines a process of approximation for infinite data; the functions on the data that are continuous in the topology are exactly the functions that can be approximated to any desired degree of precision. This suggests a continuity principle:

$$\displaystyle{ \mathit{computability}\ \ \,\Longrightarrow\ \ \mathit{continuity}. }$$

(4)

For abstract models, we assume the algebra A that contains $\mbox{ $\mathbb{R}$}$ is a topological algebra, i.e., one in which the basic operations are continuous in its topologies. This implies, in turn, that all computable functions will be continuous. As it turns out, the class of functions that can be exactly abstractly computed is, in general, quite limited—“approximate” computations are also necessary [30].

In the concrete models, on the other hand, continuity of computable functions is a consequence of the the Kreisel-Lacombe-Tseitin Theorem [17, 26, 27].

Thus, in both abstract and concrete approaches, an analysis of basic concepts leads to the continuity principle.

7.1.3 Partiality

 In computing with an abstract model on A we assume A has some boolean-valued functions to test data. For example, in computing on $\mbox{ $\mathbb{R}$}$ we need the functions

$$\displaystyle{ \mbox{ $\mathsf{eq}_{\mathsf{R}}$}: \mbox{ $\mathbb{R}$}^{2}\ \rightarrow \ \mbox{ $\mathbb{B}$}\qquad \mbox{ and}\qquad \mbox{ $\mathsf{less}_{\mathsf{ R}}$}: \mbox{ $\mathbb{R}$}^{2}\ \rightarrow \ \mbox{ $\mathbb{B}$}. }$$

(5)

This presents a problem, since total continuous boolean-valued functions on the reals, being continuous functions from a connected space $\mbox{ $\mathbb{R}^{n}$}$ to a discrete space $\mbox{ $\mathbb{B}$}$, must be constant. Furthermore, in consequence, we can show that the “ while” and “ while”-array computable functions on connected total topological algebras are precisely the functions explicitly definable by terms over the algebra [30]. This demands the use of partiality for such functions.

To study the full range of real number computations, we must therefore redefine these tests as partial boolean-valued functions. This has interesting effects on the theory of computable functions in the areas of nondeterminism and many-valuedness, as we will see.

We turn to some examples to illustrate these features.

7.2 Examples of Nondeterminism and Many-Valuedness

We look at two examples of computing functions on $\mbox{ $\mathbb{R}$}$.

Example 7.2.1 (Nonzero Selection Function)

Define the function

$$\displaystyle{\boldsymbol{piv}: \mbox{ $\mathbb{R}^{n}$}\ \rightharpoonup \ \mbox{ $\{\,1,\ldots,n\,\}$}}$$

by

$$\displaystyle{ \boldsymbol{piv}(\mbox{ $x_{1},\ldots,x_{n}$})\ =\ \left \{\begin{array}{@{}l@{\quad }l@{}} \mbox{ some}\ i:\ x_{i}\neq 0\quad &\mbox{ if such an $i$ exists} \\ \uparrow \quad &\mbox{ otherwise}. \end{array} \right. }$$

(6)

Computation of this nondeterministic (“pivot”) function is a crucial step in the Gaussian elimination algorithm for inverting matrices.

Note that (depending on the precise semantics for the phrase “some i” in (6)) piv is nondeterministic or (alternatively) many-valued on $\mathit{\mathbf{dom}}(\mathbf{\mathit{\,piv}}) = \mbox{ $\mathbb{R}^{n}$}\setminus \mbox{ $\{0\}$}$. Further:

• (a) There is no single-valued function which satisfies definition (2) in Sect. 3.2 and is continuous on $\mbox{ $\mathbb{R}^{n}$}$ (as can be easily seen).

• (b) However there is a computable (and hence continuous!) single-valued function

  $$\displaystyle{\boldsymbol{piv}: \mbox{ $\mathbf{CS}^{n}$}\ \rightharpoonup \ \mbox{ $\{\,1,\ldots,n\,\}$}}$$

  (where CS is the space of fast Cauchy sequences of rationals) with a simple algorithm. Note however that piv is not extensional on CSⁿ, in the sense that it cannot be factored through $\mbox{ $\mathbb{R}^{n}$}$:

  

  where κ is the map from Cauchy sequences to their limits.

  In effect, we can regain continuity (for a single-valued function), by foregoing extensionality.

• (c)  Alternatively, we can maintain continuity and extensionality by giving up single-valuedness. For the many-valued function

  $$\displaystyle{\boldsymbol{piv}_{\mathsf{m}}: \mbox{ $\mathbb{R}^{n}$}\ \rightarrow \ \wp (\mbox{ $\{1,\ldots,n\}$})}$$

  defined, for k = 1, …, n, by

  $$\displaystyle{k\, \in \,\boldsymbol{piv}_{\mathsf{m}}(\mbox{ $x_{1},\ldots,x_{n}$})\ \mbox{ $\,\Longleftrightarrow$}\ x_{k}\neq 0}$$

  is extensional and continuous, where a function $f: A\ \rightarrow \ \mbox{ $\mathcal{P}$}(B)$ is defined to be continuous iff for all open $Y \subseteq B$, f⁻¹[Y ] ($= _{df}\ \mbox{ $\{\,x \in A\vert f(x) \cap Y \neq \emptyset \,\}$}$) is open in A.

Note that the complete Gaussian algorithm for inverting matrices is continuous and deterministic (hence single-valued) and extensional, even though it contains piv as an essential component!

Example 7.2.2 (Finding the Root of a Function—Adapted from [39])

Consider the function f_a (Fig. 2),⁷ with real parameter a, defined by

$$\displaystyle{f_{a}(x)\ =\ \left \{\begin{array}{@{}l@{\quad }l@{}} x + a + 2\quad &\mbox{ if $x \leq -1$} \\ a - x \quad &\mbox{ if $ - 1 \leq x \leq 1$} \\ x + a - 2\quad &\mbox{ if $1 \leq x$.}\\ \quad \end{array} \right.}$$

Fig. 2

Function f_a in Example 7.2.2

Fig. 3

Non-repeated roots of f_a

This function has either 1 or 3 roots, depending on the size of a. For a < −1, f_a has a single (large positive) root; for a > 1, f_a has a single (large negative) root; and for − 1 < a < 1, f_a has three roots, two of which become equal when a = ±1.

Let g be the (many-valued) function, such that g(a) gives all the non-repeated roots of f_a (Fig. 3). Again we have the situation of the previous examples:

• (a) We cannot choose a (single) root of f_a continuously as a function of a.

• (b) However, one can easily choose and compute a root of f_a continuously as a function of a Cauchy sequence representation of a, i.e., non-extensionally in a.

• (c) Finally, g(a), as a many-valued function of a, is continuous. (Note that in order to have continuity, we must exclude the repeated roots of f_a, at a = ±1.)

Other examples of a similar nature abound, and can be handled similarly; for example, the problem of finding, for a given real number x, an integer n > x.

7.3 Partial Algebra of Reals; Completeness for the Abstract Model

At the level of concrete models of computation, there is no real problem with the issues raised by these examples, since concrete models work only by computations on representations of the reals (say by Cauchy sequences).

The real problem arises with the construction of abstract models of computation on the reals which should model the phenomena illustrated by these examples, and also correspond, in some sense, to the concrete models.

An immediate problem in this regard is that the total boolean-valued functions eq_R and less_R are not continuous, and hence also (by the continuity principle, Sect. 7.1.2) not (concretely) computable.

We therefore define an N-standard partial algebra$\mbox{ $\mathcal{R}_{\mathsf{p}}$}$ on the reals, formed from the total algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ (Example 3.1.3) by replacing the total boolean-valued functions eq_R and less_R (Sect. 7.1.3, (5)) by the partial functions

These partial functions (unlike the total versions), are continuous, and hence $\mbox{ $\mathcal{R}_{\mathsf{p}}$}$ (unlike $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$) is a topological partial algebra. Moreover, these partial functions are concretely computable (by e.g. the tracking model, cf. Sect. 7.1.1).

Then we have the question:

Can such continuous many-valued functions be computed on the abstract

data type A containing $\mbox{ $\mathbb{R}$}$ using new abstract models of computation?

If so, are the concrete and abstract models equivalent?

The solution presented in [33] was to take $A = \mbox{ $\mathcal{R}_{\mathsf{p}}^{N}$}$, the N-standard extension of ℛ_p, and then extend the $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ programming language over A [31] with a nondeterministic “countable choice” programming construct, so that in the rules of program term formation,

$$\displaystyle{\mathsf{choose}\ \mathtt{z}: b}$$

is a new term of type nat, where z is a variable of type nat and b a term of type bool. In addition (calling the resulting language $\boldsymbol{WhileCC}^{\boldsymbol{{\ast}}}$ for $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computability with countable choice), $\boldsymbol{WhileCC}^{\boldsymbol{{\ast}}}$computability is replaced by $\boldsymbol{WhileCC}^{\boldsymbol{{\ast}}}$approximability [33, 34]. We then obtain a completeness theorem for abstract/concrete computation, i.e. the equivalence (1) shown at the end of Sect. 2. Actually (1) was proved in [33] for N-standard metric algebras satisfying some general conditions.

The above considerations lead us to propose the topological partial algebra $\mbox{ $\mathcal{R}_{\mathsf{p}}$}$ as a better basis for abstract models of computation on $\mbox{ $\mathbb{R}$}$ than the (total) algebra $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$—better in the sense of being more faithful to the intuition of computing on the reals.⁸

Remark 7.3.1 (Semantics of Partial Algebras)

We briefly indicate the semantics for terms and statements over partial algebras, or rather indicate how the semantics for total algebras given in Sects. 3.2 and 4 can be adapted to partial algebras.

First, the semantics of terms is as given by the Eq. (2) in Sect. 3.2 (with the second “ = ” replaced by “$\simeq$”), using strict evaluation for partial functions (i.e., divergence of any subterm entailing divergence of the term).⁹

Secondly, the semantics of statements is as given in Sect. 4; i.e., the value $\mbox{ $[\![S]\!]^{A}$}\mbox{ $\sigma $}$ of a statement S at a state σ is the last state in a computation sequence (i.e. a sequence of states) generated by S at σ, provided that the sequence is (well defined and) finite. Otherwise (with an infinite computation sequence) the value diverges. The case of partial algebras is similar, except that there are now two cases where the value of [​[S]​]^Aσ diverges: (1) (as before, global divergence) where the computation sequence is infinite, and (2) (a new case, local divergence) where the computation sequence is finite, but the last item diverges (instead of converging to a state) because of a divergent term on the right of an assignment statement or a divergent boolean test.

Remark 7.3.2 (Comparison of Formal Results for $\mbox{ $\mathcal{R}_{\mathsf{p}}$}$ and $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$)

It would be interesting to see to what extent the results concerning abstract computing on the reals with $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ detailed in Sects. 3–6 (for example, the merging and closure theorems (Sect. 6.1) and comparisons of various notions of semicomputability and projective semicomputability in $\mbox{ $\mathcal{R}_{\mathsf{t}}$}$ (Sect. 6.7) hold, or fail to hold, in $\mbox{ $\mathcal{R}_{\mathsf{p}}$}$.¹⁰

It should be noted, in this regard, that the merging procedure used in our proofs of the closure theorems (Theorems 3–5) depend heavily on the totality of the algebra A.

8 Comparing Models and Generalizing the Church-Turing Thesis

To conclude, we will mention several other abstract approaches to computability on abstract algebras, comment on their comparison, and discuss how to generalize the Church-Turing thesis. These other methods have a variety of technical intuitions and objectives, though they share the abstract setting of an algebraic structure. So let us suppose their common purpose to be the characterization of those functions that are computable in an abstract setting.

8.1 Abstract Models of Computation

The computable functions on an abstract algebra can also be characterized by approaches based upon

• (1) machine models;

• (2) high-level programming constructs;

• (3) recursion schemes;

• (4) axiomatic methods;

• (5) equational calculi;

• (6) fixed-point methods for inductive definitions;

• (7) set-theoretic methods;

• (8) logical languages.

We consider only a couple of these; a fuller survey can be found in [31].

Recursion schemes. Kleene’s recursion schemes suggest that we create the class $\mbox{ $\boldsymbol{\mu }\boldsymbol{PR}(A)$}$ of functions $\boldsymbol{\mu }\boldsymbol{PR}$ computable on a standard algebra A, namely those functions definable from the basic operations of A by the application of composition, simultaneous primitive recursion and least number search. We can also extend this to the class $\mbox{ $\boldsymbol{\mu }\boldsymbol{PR}^{{\ast}}(A)$}$ of functions on A definable by the $\boldsymbol{\mu }$PR operations on A^∗ (analogous to the definition of the class $\mbox{ $While^{\boldsymbol{{\ast}}}(A)$}$ from While(A^∗) in Sect 4.1).

Alternatively, we can define the class $\mbox{ $\boldsymbol{\mu }\boldsymbol{CR}(A)$}$ of functions on A in which simultaneous primitive recursion is replaced by simultaneous course-of-values recursive schemes. (Simultaneous recursions are needed because the structures are many-sorted.) Then we have:

Theorem 13 (Recursive Equivalence Theorem)

For any N-standard Σ-algebra A,

$$\displaystyle{\mbox{ $\boldsymbol{\mu }\boldsymbol{CR}(A)$}\ =\ \mbox{ $\boldsymbol{\mu }\boldsymbol{PR}^{{\ast}}(A)$}\ \ =\ \mbox{ $\boldsymbol{While}^{\boldsymbol{{\ast}}}(A)$}.}$$

The question of unbounded memory—A^∗ versus A—re-appears here in the difference between primitive and course-of-values recursion. This model of computation was created [29] with the needs of equational and logical definability in mind.

Axiomatic Methods. In an axiomatic method one defines the concept of a computation theory as a set $\boldsymbol{\varTheta }(A)$ of partial functions on an algebra A having some of the essential properties of the set of partial recursive functions on $\mbox{ $\mathbb{N}$}$. To take an example, $\boldsymbol{\varTheta }(A)$ can be required to contain the basic algebraic operators and tests of A; be closed under operations such as composition; and, in particular, possess an enumeration for which appropriate universality and s-m-n properties are true. Thus in Sect. 5 we saw that $\mbox{ $While^{\boldsymbol{{\ast}}}(A)$}$ is a computation theory in this sense.

The definition of a computation theory used here is due to Fenstad [7, 8] who takes up ideas from Moschovakis [21]. Computation theory definitions typically require a code set (such as $\mbox{ $\mathbb{N}$}$) to be part of the underlying structure A for the indexing of functions.

The following fact is easily derived from [20] (where register machines are used); see also Fenstad [8, Chap. 0].

Theorem 14 (Minimal Computation Theory)

The set $\mbox{ $\boldsymbol{While}^{\boldsymbol{{\ast}}}(A)$}$ of $\mbox{ $While^{\boldsymbol{{\ast}}}$}$ computable functions on an N-standard algebra A is the smallest set of partial functions on A to satisfy the axioms of a computation theory; in consequence, $\mbox{ $\boldsymbol{While}^{\boldsymbol{{\ast}}}(A)$}$ is a subset of every computation theory  $\boldsymbol{\varTheta }(A)$ on A.

8.2 Generalizing the Church-Turing Thesis

The $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable functions are a mathematically interesting and useful generalization of the partial recursive functions on $\mbox{ $\mathbb{N}$}$ to abstract many-sorted algebras A and classes $\mbox{ $\mathbb{K}$}$ of such algebras. Do they also give rise to an interesting and useful generalization to A and $\mbox{ $\mathbb{K}$}$ of the Church-Turing thesis, concerning effective computability on $\mbox{ $\mathbb{N}$}$? They do; though this answer is difficult to explain fully and briefly. In this section we will only sketch some reasons. The issues are discussed in more detail in [29, 31], as well as in the chapter by Feferman in this volume [6].

First, consider the following naive attempt at a generalization of the Church-Turing thesis.

Thesis 1 (A Naive Generalized Church-Turing Thesis)

The functions “effectively computable” on a many-sorted algebra A are precisely the functions $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A.

Consider now: what can be meant by “effective computability” on an abstract algebra?

The idea of effective computability is inspired by a variety of distinct philosophical and mathematical ideas about the nature of finite computation with finite elements. There are many ways to analyse and formalize the notion of effective calculability, by thinking about concepts such as algorithm; deterministic procedure; mechanical procedure; computer program; programming language; formal system; machine; device; and, of course, the functions definable by these entities.

The idea of effective computability is invaluable because of the close relationships that exist between its constituent concepts. However, only a few of these constituent concepts make sense in an abstract setting. Therefore the general concept of “effective computability” does not belong in a generalization of the Church-Turing thesis. We propose to use the term “effective computation” only to talk about finite computation on finite data.

In seeking a generalization of the Church-Turing thesis, we are trying to make explicit certain primary informal concepts that are formalized by the technical definitions, and hence to clarify the nature and use of the computable functions.

We will start by trying to clarify the nature and use of abstract structures. There are three points of view from which to consider the step from concrete to abstract structures, and hence three points of view from which to consider $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable functions.

• (1) There is abstract algebra, which is a theory of calculation based upon the “behaviour” of elements in calculations without reference to their “nature”. This abstraction is achieved through the concept of isomorphism between concrete structures; an abstract algebra A can be viewed as “a concrete algebra considered unique only up to isomorphism”.

• (2) There is the viewpoint of formal logic, concerned with the scope and limits of axiomatizations and formal reasonings. Here structures are used to discuss formal systems and axiomatic theories in terms of consistency, soundness, completeness, and so on.

• (3) There is data type theory, an offshoot of programming language theory, which is about data types that the user may care to define and that arise independently of programming languages. Here structures are employed to discuss the semantics of data types, and isomorphisms are employed to make the semantics independent of implementations. In addition, axiomatic theories are employed to discuss their specifications and implementation.

Data type theory is built upon and developed from the first two subjects: it is our main point of view.

Computation in each of the three cases is thought of slightly differently. In algebra, it is natural to think informally of algorithms built from the basic operations that compute functions and sets in algebras, or over classes of algebras uniformly. In formal logic, it is natural to think of formulae that define functions and sets, and their manipulation by algorithms. In data type theory, we use programming languages to define computations. We return to a consideration of each of these approaches, which, because of its special concerns and technical emphasis, leads to a distinctive theory of computability on abstract structures:

Going first to (1): suppose the $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable functions are considered with the needs of doing algebra in mind. Then the context of studying algorithms and decision problems for algebraic structures (groups, rings, fields, etc.) leads to a formalization of a generalized Church-Turing thesis tailored to the language and use of algebraists:

Thesis 2 (Generalized Church-Turing Thesis for Algebraic Computability)

The functions computable by finite deterministic algebraic algorithms on a many-sorted algebra A are precisely the functions $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable on A.

An account of computability on abstract structures from this algebraic point of view is given in [28].

We agree with Feferman [6] who argues that this should be termed a Church-Turing thesis for algorithms on abstract structures, rather than computations. He prefers, in this context, to reserve the term “computation” for calculations on concrete structures composed of finite symbolic configurations.¹¹

Now (jumping to viewpoint (3)) suppose that the $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable functions are considered with the needs of computation in mind. This context of studying data types, programming and specification constructs, etc., leads to a formulation tailored to the language and use of computer scientists:

Thesis 3 (Generalized Church-Turing Thesis for Programming Languages)

Consider a deterministic programming language over an abstract data type dt . The functions that can be programmed in the language on an algebra A which represents an implementation of dt , are the same as the functions $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ programmable on A.

This thesis has been discussed in [29].

Finally, returning to approach (2): we note that “logical” and non-deterministic languages are suitable for specifying problems. These can be considered as languages for specification rather than computation. Here projectively computable relations (Sect. 6.2) and the use of selection functions for these, play a central role.

We define a specification language to be adequate for an abstract data type dt if all computations on any algebra A implementing dt can be specified in A. We then formulate a generalized Church-Turing thesis for specifiability on abstract data types:

Thesis 4 (Generalized Church-Turing Thesis for Specifiability)

Consider an adequate specification language S over an abstract data type dt . The relations on a many-sorted algebra A implementing dt that can be specified by S are precisely the projectively $\boldsymbol{While}^{\boldsymbol{{\ast}}}$ computable relations on A.

8.3 Concluding Remarks

We have sketched the elements of our work over four decades on generalizing computability theory to abstract structures. A thorough exposition is to be found in our survey paper [31]. In [32] we have had the opportunity to recall the diverse origins of, and influences on, our research programme.

Since [31], our research has emphasized computation on many-sorted topological partial algebras (the focus of Sect. 7 here) and its diverse applications:

• computable analysis, especially on the reals [11, 30, 34],

• classical analog systems [14, 35–37],

• analog networks of discrete and continuous processors [25, 35],

• generalized stream processing in discrete and continuous time [36, 37].

These applications bring us close to an investigation of the physical foundation of computability. In this regard, considerations of continuity are central (cf. the discussion in Sect. 7.1.2). This is related to the issue of stability of analog systems, and more broadly, to Hadamard’s principle [12] which, as (re-)formulated by Courant and Hilbert [4, 13], states that for a scientific problem to be well posed, the solution must exist, be unique and depend continuously on the data. To this we might add: it must also be computable.