\input h \nbb \cbb{Computation by While' Programs on Topological Partial Algebras} \bigskipn \cb{J.V. Tucker} \smskip \ce{\it Department of Computer Science,} \ce{\it University College of Swansea, Swansea SA2 8PP, Wales} \medskip \cb{J.I. Zucker \footnote{ Research partially supported by a grant from the Natural Sciences and Engineering Research Council of Canada (NSERC)}} %and by the Telecommunications Research Institute of Ontario (TRIO).}} \smskip \ce{\it Department of Computer Science and Systems,} \ce{\it McMaster University, Hamilton, Ontario L8S 4K1, Canada} \bigskip \bigskip \bigskip \cb{\bf Abstract} \medskipn {\narrower\narrower The language of \whiles\ \,programs is a fundamental model for imperative programming on any data type. It leads to a generalisation of the theory of computable functions on the natural numbers to the theory of computable functions on any many-sorted algebra. The language is used to express many algorithms in scientific computing where \whiles\ \,programs are applied to continuous data. In the theory of data, continuous data types are modelled by topological many-sorted algebras. We study both exact and approximate computations by \whiles\ \,programs, and \whiles\ \,programs with arrays, over topological many-sorted algebras with partial operations. First, we establish that partial operations are necessary in order to compute a wide range of continuous functions. We prove basic continuity properties of our abstract computability: {\it Any partial function computable over a partial topological algebra by a \whiles-array program is continuous. Any set semicomputable, or computable, over a partial topological algebra by a \whiles-array program is open, or clopen, respectively.\/} Secondly, we contrast exact and approximate computations. The class of functions that can be computed exactly can be quite limited. We show that on connected total algebras, the \whiles\ \,and \whiles-array computable functions are precisely those that are explicitly definable by terms. We show that for certain general classes of topological algebras, the total functions that can be approximated by \whiles\ \,programs are precisely those that can be effectively approximated by terms. This property we call {\it generalised Weierstrass approximation\/}. An application of this result is that a function on the set \,\RR\ \,of reals is computable in the sense of computable analysis if, and only if, it is \whiles\ \,program approximable on a simple algebra based on \,\RR. } \newpage \Shead0{Introduction} The theory of computable functions and sets on many-sorted algebras is a mathematical theory for the analysis of finite deterministic computation on any kind of data. It is a beautiful and useful generalisation of the theory of computable functions and sets on the natural numbers \NN. The theory is abstract in the sense that it does not depend on concrete representations of the algebras of data. The origins of the generalisation lie in the formalisation of flowcharts in the 1950s. Subsequently, the subject has been developed by many contributions having one of essentially three motivations, namely: \itemitem{($i$)} to better understand computability theory (\eg, the early work of Moschovakis \cite{moscho69:I,moscho69:II,moscho71} and Friedman \cite{friedman71:turing}; \itemitem{($ii$)} to make applications in programming language theory (\eg, the early work in \cite{mccarthy63,thiele,engeler67} on logical foundations of programming); \,and \itemitem{($iii$)} to make applications in mathematics (\eg, the early work by Engeler \cite{engeler68:geom,engeler71:approx} on real number computations and ruler and compass constructions). At various times the subject has been surveyed in \cite{chandra-manna72,fitting,shep85:friedman,tz:book} and, most recently, in \cite{tz:hb} which contains historical information and a comprehensive introduction to the subject. In the generalisation, the basic concepts and results of classical computability theory on \NN\ are refined and clarified, and new applications become possible. Different models of computation and formal systems are used to define functions and sets on algebras. The equivalence of these methods demonstrates the stability of the generalised computability notions, and a {\it Generalised Church-Turing Thesis\/} is proposed for the computation and specification of functions and sets on algebras, as explicated in \cite{tz:book,tz:hb}. On choosing an algebra of real numbers, infinite bit streams, or a Hilbert space, these theories may be used to establish results on the computability of functions and sets on continuous data types made from infinite data. Recently, applications to computation on the real numbers have been popularised by the work on register machine models of S\. Smale and co-workers \cite{bss,bcss}. In that theory, functions on infinite data are computed exactly and defined by methods based on total algebras. In this paper we will further develop abstract computability theory to include both {\it exact\/} and {\it approximate computations\/} on any set of infinite data; we will also compare the two notions formally. We assume that computations are performed on sets of data possessing a topology. The topology defines a process of approximation for 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. Specifically, we study both exact and approximate computations by \whiles\ \,{\it programs\/}, and \whiles\ \,{\it programs with arrays\/}, over {\it topological many-sorted algebras with partial operations}. The language of \whiles\ \,programs is a fundamental model for imperative programming and is used to express many algorithms in scientific computing. Among the examples of algebras that we will use to illustrate our theory are algebras of real numbers, and algebras of infinite streams. The generalisation of computability from total to partial algebras is necessary for computing in topological algebras. In Section 1 we show that total algebras are problematic because of the requirement of continuity for computable functions. For example, in computing on the reals, it is reasonable algebraically to allow total Boolean functions (such as $=$ or $<$) as tests in programs. However, they are not continuous and their usefulness in programs turns out to be severely limited. To study the full range of real number computations we must redefine these tests as partial Boolean functions. We will explain the importance of continuity by general principles for comparing abstract and concrete models of computation for topological algebras. The first goal is to establish the continuity properties of our abstract computability models. We proceed in two steps: \itemitem{($i$)} we define an operational semantics for \whiles\ \,and \whiles-array programs over partial algebras (Sections 2 and 4), \,and \itemitem{($ii$)} we prove the operational semantics is continuous on appropriate spaces of computation states, whose topologies are derived from the topologies on the partial algebra (Sections 3 and 6). \ni We use an algebraic method for defining the operational semantics of a language which allows us to prove the continuity results by simply composing certain continuous functions. We deduce the following basic theorems (Section 6, Theorem and Corollaries 1 and 2) for our imperative model: {\displaytext Any partial function computable over a partial topological algebra by a \whiles-array program is continuous. } {\displaytext Any set semicomputable, or computable, over a partial topological algebra by a \whiles-array program is open, or clopen, respectively. } \ni We examine computable functions, and computable and semicomputable sets, in a number of topological algebras, including {\it compact algebras\/} where the computable sets are precisely the clopen sets. The second goal is to compare exact and approximate \whiles\ \,computations. It is easy to see that approximate computation generalises exact computation. The class of functions that can be computed exactly can be quite limited. To begin with, we show (Section 8) that {\displaytext on connected total algebras, the \whiles\ \,and \whiles-array computable total functions are precisely those that are explicitly definable by terms or polynomials. } \ni \newpage Then (Section 9) we show that, for a general class of connected topological algebras, {\displaytext the total functions that can be approximated by \whiles\ \,programs are precisely those that can be effectively approximated by terms or polynomials. } \ni This property we call {\it generalised Weierstrass approximation\/}, after Weierstrass's theorem on approximating continuous functions on the reals by means of polynomials. In computable analysis on the real numbers, there are several equivalent methods for defining the computable functions. All are based on making computable representations of the reals. (See Section 1 for a survey.) The computable functions can be also be characterised by means of effective Weierstrass approximations \cite{pourel-caldwell75}. Thus, in Section 10, we derive from our general theorem that a total function on the set \,\RR\ \,of reals is computable if, and only if, it is \whiles\ \,program approximable on a simple algebra based on \,\RR. This result was observed in \cite{shep76} for register machines. This type of application linking abstract and concrete models of computation may be generalised from the reals to other topological algebras. Important new results by Brattka \cite{brattka96,brattka97} show how this may be done for relations using a generalisation of recursion schemes (abstract computability) and the type two enumerability of \cite{weih87} (concrete computability). Brattka's work suggests a number of promising directions for research. This work is part of a research programme that aims at the precise formulation, analysis and classification of many interesting notions of computability, specifiability, and verifiability that may be found in different areas of computer science and mathematics (Tucker and Zucker [1988, 1991, 1992$a,b,c$, 1993, 1994, 1998]). \cite{tz:book,tz:ijfocs,tz:jlp,tz:sanantonio,tz:prague,tz:leeds,tz:markt,tz:hb}. Specifically, it has developed from our studies of real and complex number computation \cite{tz:sanantonio} and stream algebras \cite{tz:prague,tz:markt}. We wish to thank two anonymous referees for their valuable suggestions. \Shead{1}{Continuity and models of computation} We show how, in developing an abstract computability theory for topological algebras, the mathematical goal of making attractive and useful connections with continuity and other topological properties requires us to use partial algebras (\S1.1). Furthermore, we survey a number of different approaches to defining computability on topological algebras and explain why continuity is necessary if we are to compare abstract computability theories on topological algebras with concrete computability theories (\S1.2). \newpage \shead{1.1}{Motivation for partial algebras} Consider the many-sorted total algebra on the reals $$\boxed{ \matrix \format\l&\quad\l\\ \algebras &\RRR \\ \carrierss &\RR, \BB\\ \functionss&0,1:\ \ \to\RR,\\ &+,\times:\RR^2\to\RR,\\ &-:\RR\to\RR,\\ &\ifR:\BB\times\RR^2\to\RR,\\ &\eqR:\RR^2\to\BB,\\ &\trues, \falses:\ \ \to\bools,\\ &\ands, \ors:\bools^2\to\bools,\\ &\nots: \bools\to\bools\\ \ends& \endmatrix }$$ with the carriers \RR\ and \BB\ (= the booleans), which includes the standard boolean operations. Let \RRRL\ be the algebra which extends \RRR\ with \,\lsR\ \,(or $<$'): $$\boxed{ \matrix \format\l&\quad\l\\ \algebras &\RRRL \\ \imports &\RRR \\ \functionss&\lsR:\RR^2\to\BB\\ \ends& \endmatrix }$$ For an algebra $A$, let \WhileA\ be the class of functions computable on $A$ by \whiles\ programs. (Exact definitions of all these concepts are given or referenced below.) Now not all the functions in \,\While(\RRR) \,and \,\While(\RRRL) \,are continuous. This is obvious, because both algebras contain certain basic operations, namely \,\eqR\ and \lsR \,($=$' and $<$'), \,that are not continuous (with respect to the usual topology on \RR). We pose the following problem: {\displaytext If $A$ is an algebra built on \RR\ such that all its basic operations are continuous, then is every function in \,\WhileA\ \,continuous? } \ni Let us consider this question more generally. Given a signature \Sig, a {\it topological (total) \Sig-algebra} is a pair \,\ATTT, \,where $A$ is a \Sig-algebra which is total in the sense that the basic operations are total, and \,\TTT\ \,is a family \,\ang{\TTT_s \mid \sinSortSig}, \, where for each \sinSortSig, \,\TTTs\ \,is a topology on \As, such that for each basic function symbol \,$F:\utos$ \,of \Sig, the function \,$\FA:\Au\to\As$ \,is continuous. (An exact definition of \Sig-algebra is given later.) We will often speak of a topological algebra $A$", without stating the topology explicitly. We are interested in topological algebras which are {\it standard} in the sense that they contain the sort \,$\BB= \{\ttt,\fff\}$ \, of booleans (with the discrete topology), together with the standard boolean operations, including the {\it equality} operation at various sorts, the {\it equality sorts}, which include, typically, the sort \nats\ of natural numbers. Note that in a topological algebra, the carriers of all {\it equality sorts} must be discrete, in order for the equality operation on them to be continuous. In particular, the carrier \NN, if present, must be discrete. To provide motivation, we state the following theorem here. (It will be formulated and proved later in a more general context.) \Thm \sl Let $A$ be a standard total topological algebra. If \,$f\in\WhileA$ \,then $f$ is continuous on $A$. \endpr At first sight this gives a satisfactory answer to the above question about continuity of \whiles\ computable functions. However, a standard topological total algebra based on \RR\ has the following problem. There can be no non-constant basic operations of the form \ $F:\RRq\to\BB$ \ such as $<$' or even $=$'. This is because if \ $f:\RRq\to\BB$ \ is continuous, then \,$f^{-1}[\ttt]$ \,and \,$f^{-1}[\fff]$ \,are disjoint open sets whose union is \RRq. So one must be \RRq, and the other $\emptyset$, by the connectness of \RR. (We investigate connectedness in topological algebras in \S6.8.) Hence the problem with the above theorem is the paucity of useful applications. In fact, the only continuous equality test is on a {\it discrete space}. However, equality and order on \RR\ do have some properties close to continuity. For example, given two points $x$ and $y$ with $xy$}\\ \ua \tif{$x=y$}, \endcases %\tag"so that" $$%and$$ \eqp(x,y) \ = \ \cases \ua \tif{$x=y$}\\ \fff \tif{$x\ne y$}. \endcases \tag"and" $$\TOR These partial functions are continuous, in the sense that the inverse images of \{\ttt\} and \{\fff\} are always open subsets of \RR^2. Another example of continuity associated with non-totality of a function can be given with {\it real division}:$$ x\,\divs_\realss \,y \ = \ \cases x/y \tif{$y\ne0$}\\ \ua \tif{$y=0$} \endcases $$We will exploit these observations %about \,<' \,and \,=' to the full by studying {\it topological partial algebras}. We will also prove a more general version of the above theorem for such partial algebras. \shead{ 1.2} {Abstract and concrete models} The study of \whiles\ \,computation is relevant to the solution of an important general problem: {\displaytext To develop a comprehensive theory of computing in topological algebras. } There are many ways of defining computable functions on topological algebras, and some have the beginnings of significant mathematical theories. To better organise our discussion of the present situation we introduce the informal concepts of {\it abstract\/} and {\it concrete\/} computability models and their theories. The \whiles\ \,language is one of many that qualify as an abstract computability model. \Defn{1.2.1 \ (Abstract models of computation)} A model of computation is {\it abstract\/} if, when applied to any algebra, the resulting programs for computable functions and sets on that algebra are invariant under isomorphisms, and hence do not depend on a representation for the algebra. \endpr In contrast, we have: \Defn{1.2.2 \ (Concrete models of computation)} A model of computation is {\it concrete\/} if, when applied to any algebra, the resulting programs for computable functions and sets on that algebra are not invariant under isomorphisms, and hence do depend on a representation for the algebra. \endpr The difference is particularly striking in the case of real number computation. As we have seen in \S1.1, to compute on the set \,\RR\ \,of real numbers with the \whiles\ \,language, we have only to choose an algebra A in which \,\RR\ \,is a carrier set. There are infinitely many choices of operations with which to make an algebra. There are thus infinitely many choices of classes of computable functions, all defined uniquely up to isomorphism. Thanks to the general theory of computable functions on many-sorted algebras (see below and \cite{tz:book}) all the classes of computable functions on \,\RR\ \,have decent mathematical theories, resembling the theory of the computable functions on the natural numbers \,\NN. However, unlike the case of \,\NN, \,it is easy to list different algebras of reals with different classes of \whiles\ \,computable functions. The theory of computability on an algebra A is a theory of computability relative to A: a function is \whiles\ computable over A if it can be programmed by a \whiles\ \,program on A. All of these remarks should apply to any abstract model of computation. In contrast, to compute on \RR\ with a concrete model of computation, we choose an algebra A in which \,\RR\ \,is a carrier set and, in particular, we choose an appropriate concrete representation of the algebra. The real numbers can be built from the rational numbers, and hence the natural numbers, in a variety of equivalent ways (such as Cauchy sequences, decimal expansions, etc.). The key ideas are those of {\it computable real numbers\/}, and that computable functions on the reals can be computably approximated on computable real numbers. (We use these concepts in Section 10.) It is natural to investigate the computability of functions on \,\RR, \,starting from the theory of computable functions on \,\NN. The study of the computability of \RR\ began in \cite{turing36}, but only later was taken up in a systematic way \cite{rice54,lacombe55,grzeg55,grzeg57}. However, the comparison of different concrete models of computation for \RR\ is much more complicated than concrete models of computation for \NN. For example, although the different representations of the field of reals are specified axiomatically, uniquely up to isomorphism, as a complete Archimedian ordered field, computationally they are far from being equivalent. For instance, representing real numbers by infinite decimals leads to the problem that the trivial function 3x is not computable, whereas the elementary functions on the reals {\it are\/} computable if Cauchy sequences are used \cite{weih87}. The problems of representation are even worse when investigating computational complexity \cite{ko91}. Clearly, in the case of concrete computability there is a general supplementary problem: {\displaytext To understand and classify the structure of concrete representations of \linebreak infinite data. } There have been a number of approaches to the analysis and classification of representations for the reals and other topological structures. The ideas about computable functions on the reals were generalised to {\it countable metric spaces\/} and their completions in \ns[.Moscho 1964.], using certain numberings. Some of the special theorems on continuity of \ns[.Ceitin 1959.], obtained earlier with a constructive point of view, were re-proved in a classical setting. An axiomatic approach to computability on Banach spaces was developed in \ns[.PourEl Richards.]. This gives general theorems about the independence of computations from representations, and provides a series of remarkable results characterising computable operators in terms of continuity. Computability theory on \,\NN\ \,includes a theory of computation for functionals on the set \Bb\ of all functions \,\NN\to\NN. The set \Bb\ is commonly called {\it Baire space\/}, and the theory of computation on \Bb\ is called {\it type 2 computability theory\/}. Klaus Weihrauch and his collaborators, in a long series of papers, have created a fine generalisation of the theory of numberings of countable sets (after A.I. Mal'cev and Yu. Ershov) to a theory of type 2 numberings of uncountable sets. In type 2 enumeration theory, numberings have the following form. Let X be a topological space. A {\it type 2 enumeration\/} of X is a surjective partial continuous (quotient) map$$ \al: \ \Bb \ \to \ X. $$Computability on X is then analysed using type 2 computability on \Bb, and the different possible representations form a topic of investigation. See, for example, \ns[.Kreitz Weihrauch.] \ and, especially, the monograph [.Weihrauch 1987.]. A more abstract method for the systematic study of effective approximations of uncountable topological algebras was developed by V. Stoltenberg-Hansen and J.V. Tucker. It is based on representing topological algebras using algebras built from algebraic domains, and applying the theory of {\it effective algebraic domains\/}. It was first developed for topological algebras and used on completions of local rings in Stoltenberg-Hansen \& Tucker [1985, 1988]. The method effectively approximates a large class of examples: ultrametric algebras (see Stoltenberg-Hansen \& Tucker [1991, 1993, 1995], also \ns[.stolt 1994.], Chapter 8); locally compact Hausdorff algebras (Stoltenberg-Hansen \& Tucker [1995]); and complete metric algebras (\ns[.Blanck 1997.]). An introduction can be found in Stoltenberg-Hansen \& Tucker [1995], where domain representations for the real numbers were studied. %[.stolt jvt 1985.] %[.stolt jvt 1988.] %[.stolt jvt 1991.] %[.stolt jvt 1993.] %[.stolt jvt 1995.] An early attempt at using partially ordered sets to handle representations of metric spaces was made in \ns[.Weihrauch Schreiber.]. Similar ideas have been used in Edalat [1995a,b], applying continuous domains to analytical questions, such as integration and measure. In \ns[.edalat sunder.] \ continuous domains are used to model the real numbers. %[.edalat 1995a.] %[.edalat 1995b.] In fact, all of these concrete computability theories have been compared and, for certain basic topological algebras, shown to be essentially equivalent (Stoltenberg-Hansen \& Tucker [1998]). %[.stolt jvt 1998 tcs.] \shead{1.3}{Relation between abstract and concrete models} What is the relationship between the abstract and concrete computability theories? It is possible to answer this question in a very general way. The various concrete computability theories discussed above have the following common form. Let A be a topological algebra. To compute in A, a {\it concrete representation}$$ \al: \ R \ \to \ A \tag1 $$of A must be made where: \itemitem{(i)} R is a topological algebra, made from computable data types, on which we can compute; \,and \itemitem{(ii)} \al\ is a surjective continuous homomorphism that allows us to compute on A by computing on R. \ni In particular, there is a set \,\Comp_\al(A) \,of functions on A computable in terms of the representation (1). In general terms, when comparing abstract and concrete models of computation, we may expect the following situation. Let \,\AbsCompA\ \,be a set of functions on A that is computable in an abstract model of computation (e.g., the \whiles\ \, language). Let \,\ConcRepA\ \,be a class of concrete representations of the form \,\al: R \to A \,(\eg, a type 2 enumeration, or domain representation). Let \,\al\in\ConcRepA \,and let \,\CompalA\ \,be the set of functions on A computable with the representation \al. A specific representation of a topological algebra has a specific structure that can be used in defining computations. Thus, computing with a concrete representation R of an algebra A enables more functions to be computed than with an abstract model of computation based solely on the operations. In fact, for a class of representations of a concrete model of computation, we expect the following to hold: \smskipn {\bi General Abstraction Principle:}$$ \tsize \AbsCompA \ \ \sseq \ \ \bigcap_{\al\in\ConcRepA}\CompalA. $$For models of computation that characterise the set of functions computable in the classical sense (according to the Church-Turing Thesis), we postulate, more specifically: \smskipn {\bi Abstraction Principle:}$$ \tsize \WhilexA \ \ \sseq \ \ \bigcap_{\al\in\ConcRepA}\CompalA. $$where \WhilexA\ \,is the class of functions computable on A by \whiles-array programs. The study of concrete models of computation leads to the following postulate: \smskipn \ce{\sl computability \ \ \llongto \ \ continuity.} \smskipn Historically, this idea has graduated from being a working principle in 1950s recursion theory to a fundamental principle through \itemitem{(a)} the equivalence of known concrete models of computation on the real numbers; \itemitem{(b)} conceptual analyses of models of physical computing devices; \ and \itemitem{(c)} mathematical generalisations of recursion theory, most notably domain theory. \smskipn Let \,\ContA\ \,be the set of all partial continuous functions on A. Then we propose: \smskipn {\bi Continuity Principle:}$$ \tsize \WhilexA \ \ \sseq \ \bigcap_{\al\in\ConcRepA}\CompalA \ \ \sseq \ \ \ContA. $$Thus, the continuity of the abstract computable functions, sought after in \S1.1, is essential. There is much to explore in the border between abstract and concrete computability. For example, in addition to our results for while computations, there are the important results of Brattka [1996, 1997] %[.brattka 1996.] [.brattka 1997.] which show that by strengthening a fundamental abstract computability model (relations defined by {\it primitive recursion\/}, {\it minimalisation\/} and a {\it limit operation\/}) it is possible to characterise a fundamental concrete computability model (relations in type 2 enumerability). The implications of Brattka's results for other abstract models, such as the \whiles\ \,language, are under investigation. \Shead{2}{Signatures and partial algebras} \sshead{2.1}{Basic definitions} A {\it signature} \Sig\ (for a many-sorted partial algebra) is a pair consisting of (i) a finite set \SortSig\ of {\it sorts}, and (ii) a finite set \FuncSig\ of {\it (primitive) function symbols}, each symbol F having a {\it type} \ \tuptimes{s}{1}{m}\to s, where s_1 ,\ldots, s_m, s \in \SortSig; in that case we write \ F:\ \tuptimes{s}{1}{m}\to s. \ (The case m = 0 corresponds to {\it constant symbols}.) A \Sig-{\it product type}, has the form \ u = \tuptimes{s}{1}{m} \ (m\ge0), where \,\tup{s}{1}{m} \,are \Sig-sorts. We use the notation \ u,v,w,\dots \ for \Sig-product types. A \Sig-{\it algebra} A has, for each sort s of \Sig, a non-empty {\it carrier set} \,\As\ \,of sort s, and for each \Sig-function symbol \ F:\utos, \ a (not necessarily total) function \ \FA : \Au \to \As \ (where,for the \Sig-product type \ u = \tuptimes{s}{1}{m}, \ we write \ \Au \ \eqdf \ A_{s_1} \times\dots\times A_{s_m}). %We will sometimes use the same notation for a function symbol F %and its interpretation \FA. The algebra A is {\it total} if \,\FA\ is total for each \Sig-function symbol F. Without such a totality assumption, A is called {\it partial}. In this paper we deal mainly with partial algebras. {\it The default assumption is that function" and algebra" refer to partial function and partial algebra.} We will, nevertheless, for the sake of emphasis, often speak explicitly of partial algebras". \Examples The following examples of algebras are all total. (Examples of partial algebras will be given in Section 3.) \smskipn(a) The algebra of naturals \ \NNNo = (\NN;\,0,\,\sucs), \ has a signature containing the sort \nats\ and the function symbols \ 0:\ \ \to\nats \,and \,\sucs:\nats\to\nats. We can display it thus:$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\NNNo \\ \carrierss &\NN\\ \functionss&0:\ \ \to\NN,\\ &\sucs:\NN\to\NN\\ \ends& \endmatrix } $$(b) The ring of reals \ \RRRo = (\RR;\,0,\,1,\,+,\,-,\,\times) \ has a carrier \RR\ of sort \reals, and can be displayed as follows:$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\RRRo \\ \carrierss &\RR\\ \functionss&0,1:\ \ \to\RR,\\ &+,\times:\RR^2\to\RR,\\ &-:\RR\to\RR\\ \ends& \endmatrix } $$(c) The algebra of {\it booleans}$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\BBB\\ \carrierss &\BB\\ \functionss&\ttt, \fff:\ \ \to\BB,\\ &\con, \dis:\BB^2\to\BB\\ &\neg: \BB\to\BB\\ \ends& \endmatrix } $$with the carrier \ \BB = \{\ttt,\,\fff\} \ of sort \,\bools. %where the corresponding signature %\,\Sig(\BBB) %\,contains the sort \,\bools\ %\,and the constant and function symbols %\,\trues, \,\falses, %\,\ands, \,\ors, \,\nots, %\,with their standard interpretations %\,\trues^\BBB = \ttt \,etc. Throughout this work we make the following assumption about the signatures \Sig. \pr{Instantiation Assumption} {\sl For every sort s of \Sig, there is a closed term of that sort, called the default term \,\delbs\ \,of that sort.} \endpr This guarantees the presence of {\it default values} \,\delbsA\ \, in a \Sig-algebra A at all sorts s, and {\it default tuples} \,\delbuA\ \,at all product types u. \shead{2.2}{Adding booleans: \ Standard signatures and algebras} A signature \Sig\ is {\it standard} if \itemitem{(i)} \Sig(\BBB) \ \sseq \Sig, \ and \itemitem{(ii)} The function symbols of \Sig\ include a {\it discriminator}$$ \ifs_s :\bools\times s^2 \to s $$for all sorts s of \Sig\ other than \bools, and an {\it equality operator}$$ \eqs_s: s^2 \to \bools $$for certain sorts s, called {\it equality sorts}. (We assume there is a computable equality" on these sorts.) Given a standard signature \Sig, a \Sig-algebra A is a {\it standard} if \itemitem{(i)} it is an expansion of \BBB, \ and \itemitem{(ii)} the discriminators and equality operators have their standard interpretation in A; \ie, \,for \,b\in\BB \,and \,x,y \in \As,$$ \ifs_s(b,x,y) \ = \ \cases x \tif{$b = \ttt$}\\ y \tif{$b = \fff$}, \endcases $$and \,\eqs_s \,is interpreted as {\it identity} on each equality sort s. \smskipn Note that any many-sorted signature \Sig\ can be {\it standardised} to a signature \,\SigB\ \,by adjoining the sort \,\bools\ \,together with the standard boolean operations; and, correspondingly, any algebra A can be standardised to an algebra \AB\ \,by adjoining the algebra \BBB\ and the discriminator and equality operators. \Examplesn{ \ {\rm (all total)}} (a) The simplest standard algebra is the algebra \BBB\ of the booleans. \smskipn (b) The standard algebra of naturals \NNN\ %\NNN = (\NN,\,\BB;\,0,\,\sucs,\,\ifN, \,\eqN,\,\lsN,\,\dots) is formed by standardising the algebra \NNNo\ given in \S2.1, with \nats\ as an equality sort, and, further, adjoining the order relation \lsN\ on \NN:$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\NNN \\ \imports &\NNNo, \,\BBB\\ \functionss &\ifN:\BB\times\NN^2\to\NN,\\ &\eqN,\,\lsN:\NN^2\to\BB\\ \ends& \endmatrix } $$(c) The standard algebra \RRR\ of reals (mentioned already in \S1.1) is formed similarly by standardising the ring \RRRo\ given in \S2.1, with \reals\ as an equality sort. \smskipn (d) The expansion \RRRL\ of \RRR\ (also mentioned in \S1.1) is formed by adjoining the order relation on the reals \ \lsR: \RR^2 \to \BB. \endpr Throughout this paper, we will assume the following. \pr{Standardness Assumption}\sl The signature \Sig\ and the \Sig-algebra A are standard. \endpr \shead{2.3}{Adding counters: \ N-standard signatures and algebras} A standard signature \Sig\ is called {\it N-standard} if it includes (as well as \bools) the {\it numerical sort} \nats, and also function symbols for the {\it standard operations} of {\it zero}, {\it successor} and {\it order} on the naturals:$$ \align 0: \ \ &\to\nats\\ \Ss:\nats&\to\nats\\ \lsN:\nats^2&\to\bools \endalign $$as well as the {\it discriminator} \,\ifN\ \,and the {\it equality operator} \,\eqN\ \,on \nats. The corresponding \Sig-algebra A is {\it N-standard} if the carrier A_\natss is the set of natural numbers \ \NN = \{0,1,2,\dots\}, and the standard operations (listed above) have their {\it standard interpretations} on \NN. \endpr Note that any standard signature \Sig\ can be N-{\it standardised} to a signature \SigN\ by adjoining the sort \nats\ and the operations 0, \Ss, \eqN, \lsN\ and \ifN. Correspondingly, any standard \Sig-algebra A can be N-{\it standardised} to an algebra \AN\ by adjoining the carrier \NN\ together with the corresponding standard functions. %certain standard operations to A, thus: %$$ %\boxed{ %\matrix \format\l&\quad\l\\ %\algebras &\AN \\ %\imports &A \\ %\carrierss &\NN\\ %\functionss %&0: \ \ \to\NN\\ %&\Ss:\NN\to\NN\\ %&\ifN:\BB\times\NN^2\to\NN\\ %&\eqN,\lsN:\NN^2\to\BB\\ %\ends& %\endmatrix %} %$$\newpage \Examplesn{ \ {\rm (again, all total)}} (a) The simplest N-standard algebra is the algebra \NNN\ given in \S2.2. \smskipn (b) We can N-standardise the standard real algebras \,\RRR\ \,and \,\RRRL, \,to form the algebras \,\RRRN\ \,and \,\RRRLN. \endpr \shead{2.4}{Adding arrays: \ Algebras \Ax\ of signature \Sigx} Given a standard signature \Sig, and standard \Sig-algebra A, we extend \Sig\ and expand A in two stages: \ni(1^\circ) N-standardise these to form \SigN\ and \AN, as in \S2.3. \ni(2^\circ) Define, for each sort s of \Sig, the carrier \Asx\ to be the set of {\it finite sequences\/} or {\it arrays\/} \ax\ over \As, of starred sort" \sx. The resulting algebras \Ax\ have signature \Sigx, which extends \SigN\ by including, for each sort s of \Sig, the new starred sorts \sx, and also the following new function symbols: \ni(i) the operator \ \Lgths_s: \,s^*\to \nats, \ where \,\Lgths(\ax) \,is the length of the array \ax; \smskipn (ii) the application operator \ \Aps_s: \,\sx\times\nats \to s, \ where$$ \Aps_s^A (\ax, k ) \ = \ \cases \ax [ k ] \tif{$k<\Lgths(\ax)$}\\ \delbs \ow \endcases $$where \,\delbs\ \,is the default value at sort s (\S2.1); \smskipn (iii) the null array \ \Nulls_s: \sx \ of zero length; \smskipn (iv) the operator \ \Updates_s: \,\sx\times\nats\times s \to s^*, \ where \ \Updates_s^A (\ax,n ,x ) \ is the array \ \bx\in\Asx \ such that for all k \in \NN,$$ \bx [k] = \cases \ax [k] \tif{$k < \Lgths(\ax), k \neq n$} \\ x \tif{$k < \Lgths(\ax), k = n$} \\ \delbs \ow. \endcases (v) the operator \ \Newlengths_s: \ \sx\times\nats \to s^*, \ where \ \Newlengths_s^A (\ax, m ) \ is the array \bx\ of length m such that for all k0\quad\{\tx{if \xtt=0, test diverges!}\}\\ &\qquad\qquad\dos\ \ \xtt:=\xtt-1\\ &\qquad\qquad\ods\\ &\ends. \endalign \smskipn($b$) The truncation function \ $\truncs: \RR^+\to\ZZ$, \ where $$\truncs(x) \ = \ \cases \floor{x} \tif{x is not an integer}\\ \ua \ow. \endcases$$ The procedure for this is similar: \align &\procs \ \ins\ \ \ \xtt:\posreals\\ &\qquad\outs\ \ \ctt:\ints\\ &\begins\\ &\qquad\ctt :=0;\\ &\qquad \whiles\ \ \xtt>1\quad\{\tx{if \xtt=1, test diverges}\}\\ &\qquad\qquad\dos\ \ \xtt:=\xtt-1;\\ &\qquad\qquad\quad\ \ \ctt:=\ctt+1\\ &\qquad\qquad\ods\\ &\ends. \endalign ($c$) More generally, we note that many practical algorithms for calculating with reals, such as finding roots of polynomials, or matrix inversion, are typically based on iterative procedures which can be written in pseudo-code based on the \whiles\ \,language. Assume from now on that $A$ is a standard topological \Sig-algebra. \shead{3.4}{Expansions of topological algebra} Corresponding to the possible algebraic expansions of $A$ detailed in \S2, there are induced topological expansions. \smskipn($a$) The topological partial algebra \AN, of signature \SigN, is constructed from $A$ by giving the new carrier \NN\ the discrete topology. \smskipn($b$) The topological partial algebra \Ax, of signature \Sigx, is constructed from \AN\ as follows. Viewing the elements of each new carrier \Asx\ as (essentially) {\it infinite sequences} of elements of \As, which take the default value \delbs\ for all indices greater than $\Lgths(\ax)$, we give \Asx\ the subspace topology of the set \,$(\As)^\NN$ \, of all infinite sequences from \As, with the {\it product topology} over \As. Equivalently, viewing the elements of \Asx\ as (essentially) arrays of elements of \As\ of finite length, we can give \Asx\ the {\it disjoint union} topology of the sets \,$(\As)^n$ \,of arrays of length $n$, for all $n\ge0$, where each set $(\As)^n$ is given the {\it product topology} of its components \As. It is easy to check that \Ax\ is indeed a topological algebra, \ie, all the new functions of \Ax\ are continuous. \smskipn($c$) The topological partial algebra \Abar, of signature \Sigbar, is constructed by giving each new carrier \Asbar\ the {\it product topology} over \As. Note that, if \As\ is {\it compact} for any sort $s$, then so is \Asbar, by Tychonoff's Theorem. \endpr \Def $A$ is {\it Hausdorff} if each carrier of $A$ is Hausdorff, \ie, any distinct pair of points can be separated by disjoint neighbourhoods. \Prop If $A$ is Hausdorff , then so are the expansions \,\AN, \,\Ax\ \,and \,\Abar. \endpr \newpage \shead{3.5}{Metric algebra} A particular type of topological algebra is a {\it metric (partial) algebra}. This is a pair \,\Ad\ \,where $d$ is a family of metrics \,\ang{d_s \mid \sinSortSig}, \, where for each \sinSortSig, \,$d_s$ \,is a metric on \As, such that for each basic function symbol \,$F:\utos$ \,of \Sig, the function \,$\FA:\Au\to\As$ \,is continuous (where continuity of a partial function can again be defined as in \S3.1($a$)). This induces or defines a {\it topological algebra} in the standard way. Note that if $A$ is {\it standard}, then the carrier \BB, as well as the carriers of all equality sorts, will have the {\it discrete metric}, defined by $$d(x,y) \ = \ \cases 0 \tif{x=y}\\ 1 \tif{x\ne y}, \endcases$$ which induces the discrete topology. We will often speak of a metric algebra $A$", without stating the metric explicitly. \Example The real algebra \RRRp\ and interval algebras \IIIp\ (\S3.2) can be viewed (or recast) as metric algebras in an obvious way. \endpr Note that if $A$ is a metric algebra, then for each product sort \,$u=\tuptimes{s}{1}{m}$, \,we can define a metric \,$d_u$ on \Au, \,which induces the product topology on \Au, by $$d_u((x_1,\dots,x_m),(y_1,\dots,y_m)) \ = \ \max_{i=1}^m\bigl(d_{s_i}(x_i,y_i)\bigr)$$ or more generally, by the $\ell_p$ metric $$d_u((x_1,\dots,x_m),(y_1,\dots,y_m)) \ = \ \bigl(\sum_{i=1}^m(d_{s_i}(x_i,y_i))^p\bigr)^{1/p} \tag{(1\le p \le\infty)}$$ Metric algebras will be used in our study of approximable computability (Section 9). \Shead{4}{\Whilebig\ \,computation on standard partial algebras} We study the computation of functions and relations on algebras by means of imperative programming models. We start by defining a simple programming language $\While \ = \ \WhileSig$, \,whose programs are constructed from: {\it concurrent assignments}, {\it sequential composition}, the {\it conditional} and the \qwhiles\ construct, and may be interpreted on any standard many-sorted partial \Sig-algebra. \shead{4.1}{Syntax of \WhileSig} For each \Sig-sort $s$, there are ({\it program}) {\it variables} \ $\att^s,\btt^s,\dots,\xtt^s,\ytt^s\dots$ of sort $s$. We define four syntactic classes: {\it variables}, {\it terms}, {\it statements} and {\it procedures}. \smskipn($a$) $\Var = \VarSig$ \,is the class of \Sig-variables, \ and \,$\Vars$ \,is the class of variables of sort $s$. For \,$u = \tuptimes{s}{1}{m}$, \,we write \,$\xtt:u$ \,to mean that \xtt\ is a $u$-tuple of {\it distinct variables}, \ie, a tuple of distinct variables of sorts \ \tup{s}{1}{m} \ respectively. \smskipn($b$) $\Term \,= \TermSig$ \ is the class of \Sig-terms \ $t,\dots$, \ and for each \Sig-sort $s$, \,\Terms\ \,is the class of terms of sort $s$. %These are %generated from the variables of the \Sig-sorts %by application of the \Sig-function symbols. These are generated by the rules $$t \ ::= \ \xtt^s \mid F(\tup{t}{1}{n})$$ where \,$s,\tup{s}{1}{n}$ \,are \Sig-sorts, \ $F: \tup{s}{1}{n}\to s$ \ is a \Sig-function symbol and \ $t_i\in \Term_{s_i}$ \,for \,$i=1,\dots,n$ \ ($n\ge0$). We write \,$t:s$ \,to indicate that \ $t \in \Terms$, and for \,$u = \tuptimes{s}{1}{m}$, \,we write \,$t:u$ \,to indicate that $t$ is a $u$-{\it tuple} of terms, \ie, a tuple of terms of sorts \ \tup{s}{1}{m}. We also use the notation \,$b,\dots$ \,for boolean terms, \ie, terms of sort \,\bools. \smskipn($c$) $\Stmt = \StmtSig$ \ is the class of statements \ $S,\dots$. The {\it atomic statements} are \skips' and the {\it concurrent assignment} \ $\xtt:= t$ \ where for some product type $u$, \ $\xtt:u$ \ and \ $t:u$. Statements are then generated by the rules $$S \ ::= \ \skips \br \xtt:= t \br \ S_1;S_2 \br \ifs\ b \ \thens\ S_1 \ \elses\ S_2 \ \fis \br \whiles\ b \ \dos\ S \ \ods$$ %Here $P(t)$ is a procedure call", where %$P$ is a procedure of type \utov\ (let us say; see below), %and $t$ is a tuple of terms of type $u$, %the {\it arguments} or {\it actual parameters} of this call. \smskipn($d$) $\Proc = \ProcSig$ \ is the class of procedures \ $P,Q,\dots$. \ These have the form $$P \ \ident \ \procs \ \ins \ \att\ \outs \ \btt\ \auxs \ \ctt\ \begins \ S\ \ends$$ %$$%P \ \ident \ \procs\ D\ \begins \ S\ \ends %$$ %where %$D$ is the {\it variable declaration} and $S$ is the {\it body}. %Here $D$ has the form %$$%D \ \ident \ \ins \ \att\ \outs \ \btt\ \auxs \ \ctt %$$ where \att, \btt\ and \ctt\ are lists of {\it input variables}, {\it output variables} and {\it auxiliary} (or {\it local) variables} respectively, and $S$ is the {\it body}. Further, we stipulate: \bull \att, \btt\ and \ctt\ \,each consist of distinct variables, and they are pairwise disjoint, \bull all variables occurring in $S$ must be among \,\att, \btt\ or \ctt, \bull the {\it input variables} \att\ must not occur on the lhs of assignments in $S$, \bull {\it initialisation condition}: \ $S$ has the form \ $\Sinit;S'$, \ where \Sinit\ is a {\it concurrent assignment} which {\it initialises} all the {\it output} and {\it auxiliary variables}, \ie, assigns to each of them the default term (\S2.1) of the same sort. If \,$\att:u$ \,and \,$\btt:v$, then $P$ is said to have {\it type} \utov, \ written \ $P: \utov$. Its {\it input type} is $u$. We use $\ident$' to denote syntactic identity between two expressions. \shead{4.2}{Semantics of \WhileSig} For each standard \Sig-algebra $A$, a {\it state} on $A$ is a family \ \ang{\sigs\mid \sinSortSig} \ of functions $$\sigs : \Vars \to \As. \tag1$$ Let \StateA\ be the set of states on $A$, with elements \ $\sig,\dots$. Note that \StateA\ is the product of the state spaces \,\StatesA\ \,for all \sinSortSig, \,where each \,\StatesA\ \,is the set of all functions as in (1). \endpr Let \sig\ be a state over $A$, \ $\xtt \ident (\tup{\xtt}{1}{n}):u$ \ and \ $a = (\tup{a}{1}{n}) \in \Au$ \ (for $n\ge1$). The {\it variant} \,$\sig\{\xtt / a\}$ \,of \sig\ is the state over $A$ formed from \sig\ by replacing its value at $\xtt_i$ by $a_i$ for $i=1,\dots,n$. We now give the semantics of each of the three syntactic classes: \Term, \Stmt\ and \Proc, relative to any standard \Sig-algebra $A$. For an expression $E$ in each of these classes, we will define a {\it semantic function} \,$\bb{E}^A$. These three semantic functions are defined below, in subsections ($a$), ($b,c$) and ($d$) respectively. \pr{$(a)$ Semantics of terms} For \ $t\in \Terms$, we define the (partial) function $$\tA :\ \StateA \pto \As$$ where \tA(\sig) is the value of $t$ in $A$ at state \sig. The definition is by structural induction on $t$: \align \bb{\xtt}^A\sig \ &=\ \sig(\xtt) \\ \bb{F(\tup{t}{1}{m})}^A\sig \ &\simeq\ \FA(\bb{t_1}^A\sig,\dots,\bb{t_m}^A\sig) \endalign Here the second clause is interpreted as: $$\bb{F(\tup{t}{1}{m})}^A\sig \ \simeq\ \cases z \tif{\bb{t_i}^A\sig\da y_i (say) \,for i=1,\dots,m}\\ &\tx{and \FA(\tup{y}{1}{m})\da z}\\ \ua \ow \endcases$$ {\it except} for the case that $F(\dots)$ is the discriminator \,$\ifs(b,t_1,t_2)$, \,in which case we have a non-strict" computation of {\it either} \,$\bb{t_1}^A\sig$ \,{\it or} \,$\bb{t_2}^A\sig$, depending on the value of \,$\bb{b}^A\sig$: $$\bb{\ifs(b,t_1,t_2)}^A\sig \ \simeq\ \cases \bb{t_1}\sig \tif{\bb{b}^A\sig \da \ttt} \\ \bb{t_2}\sig \tif{\bb{b}^A\sig \da \fff} \\ \ua \tif{\bb{b}^A\sig \ua.} \endcases$$ For any {\it closed term} \,$t:s$, \,we write \,$t_A$ \,for the valuation of $t$ in \As, which is independent of the state, \ie, $$t_A \ \eqdf \ \tA\sig \qquad \tx{for any state \,\sig}.$$ \pr{$(b)$ Algebraic operational semantics} We will describe a general method for defining the meaning of a statement $S$, in a wide class of imperative programming languages, as a partial {\it state transformation}, \ie, a (partial) function $$\SA :\ \StateA \pto \StateA.$$ We define this via a (partial) {\it computation step} function $$\CompA: \Stmt\times\StateA \times\NN\pto \StateAcupx$$ where $*$' is a new symbol or object. The idea is that \,$\CompA (S,\sig,n)$ \,is the $n$th step, or the state at the $n$th time cycle, in the computation of $S$ on $A$, starting in state \sig. The symbol $*$' indicates that the computation is over. Thus if for any $n$, \linebreak $\CompA(S,\sig,n)=*$, \,then for all $m\ge n$ $\CompA(S,\sig,m) = *$. Similarly, if for some $n$, \,$\CompA(S,\sig,n)\ua$ (\ie, is undefined), \,then for all $m\ge n$ \ $\CompA(S,\sig,m) \ua$. If we put \,$\sig_n = \CompA(S,\sig,n)$, \,then the sequence of states $$\sig = \sig_0,\ \sig_1,\ \sig_2,\ \dots, \ \sig_n, \ \dots$$ \ is called the {\it computation sequence generated by} $S$ at \sig, written \,\CompSeqA{S,\sig}. There are three possibilities: \itemitem{($1^\circ$)} the sequence terminates in a final state \,$\sig_l$, where \,$\CompA(S,\,\sig, \,l+1) = *$. \itemitem{($2^\circ$)} it is infinite, \itemitem{($3^\circ$)} it is undefined from some point on. \ni In case ($1^\circ$) the computation has an output, given by the final state; in case ($2^\circ$) the computation is non-terminating, and has no output; and in case ($3^\circ$) the computation is also non-terminating, and has no output, because a state at one of the time cycles is undefined, as a result of a divergent computation of a term in an assignment, or of a boolean term in a test. We will use an {\it algebraic operational semantics}, in which \,\CompA\ \,is defined equationally. This approach was first used in [.tz book.], and developed and applied in [.stephenson thesis.]. This general method will then be applied to the present programming language \WhileSig. Assume, {\it first}, that (for the language under consideration) there is a class $\AtSt \subset \Stmt$ \,of {\it atomic statements} for which we have a (partial) meaning function $$\angg{S}^A :\ \StateA \pto \StateA,$$ for $S \in \AtSt$, \ and {\it secondly}, that we have two functions \align \First&:\ \Stmt \to \AtSt\\ \RestA&:\ \Stmt \times \StateA \pto \Stmt , \endalign where, for a statement $S$ and state \sig, \,$\First (S)$ \ is an atomic statement which gives the {\it first} step in the execution of $S$ (in any state), and \ $\RestA (S,\sig)$ \ is a statement which gives the {\it rest} of the execution in state \sig. In each language we can define these three functions (\angg{\cdot}, \First\ and \RestA). First we define the one-step computation of $S$ at \sig" $$\CompIA : \ \Stmt\times\StateA \pto \StateA$$ by $$\CompIA (S,\sig) \ \simeq \ \angg{\First(S)}^A\sig.$$ The definition of \,$\CompA (S,\sig,n)$ \,follows by recursion on $n$: \aligned \CompA (S,\sig,0) \ &= \ \sig\\ \CompA (S,\sig,n+1) \ &\simeq \ \cases * \tif{n>0 and}\\ &\quad\tx{S is atomic}\\ \CompA (\RestA(S,\sig),\CompIA(S,\sig),n) \ow. \ \endcases \endaligned \tag1 %Note that for $n =1$, this yields %$$%\CompA (S,\sig,1) \ \simeq \ \CompIA (S,\sig). %$$ From this semantics we derive the {\it i/o semantics} as follows. First we define the {\it length of a computation} of a statement $S$, starting in state \sig, as the function $$\CompLengthA : \Stmt \times \StateA \pto \NN$$ where $$\CompLengthA (S,\sig) \ \simeq \ \left\{ \matrix \format\l&\l\\ \tx{least} \ n \ \tx{s.t.}\ &\CompA (S,\sig,n+1) \ = \ *\\ \tif{such an n exists}\\ \ua \ow. \endmatrix \right.$$ Note that \,$\CompLengthA(S,\sig)\da$ \,in case ($1^\circ$) above only. Then $$\SA(\sig) \ \simeq\ \ \CompA ( S,\,\sig,\,\CompLengthA(S,\sig)).$$ \pr{$(c)$ Semantics of statements} We now apply the above theory to the language \WhileSig. Here there are two atomic statements: \ \skips\ and concurrent assignment. We define \,$\angg{S}^A$ \,for these: \align \angg{\skips}^A\sig \ &= \ \sig\\ \angg{\xtt:=t}^A\sig \ &\simeq \ \cases \sig\{\xtt/\tA\sig\} \tif \tA\sig\da\\ \ua \ow \endcases \endalign (Note that the case \,$\tA\sig\ua$ \,leads to case ($3^\circ$) above.) Next we define \,$\First (S)$ \,and \,$\RestA (S,\sig)$, \,by structural induction on $S$. \smskipn {\it Case 1.} \ $S$ is atomic. \align \First (S) \ &= \ S \\ \RestA (S,\sig) \ &= \ \skips. \endalign {\it Case 2.} \ $S \ \ident \ S_1;S_2$ \ (the interesting case!). \align \First (S) \ &= \ \First (S_1 ) \\ \RestA (S,\sig) \ &\simeq \ \cases S_2 \ift{S_1 is either atomic or of the form}\\ &\qquad\whiles\ b \ \dos \ S_0 \ \ods, \ \ \tx{where} \ \bb{b}^A\sig\da\fff\\ \ua \tif{S_1 is of the form}\\ &\qquad\whiles\ b \ \dos \ S_0 \ \ods, \ \ \tx{where} \ \bb{b}^A\sig\ua\\ \RestA (S_1,\sig) ;S_2 \ow. \endcases \endalign {\it Case 3.} \ $S \ \ident \ \ifs \ b \ \thens \ S_1 \ \elses \ S_2 \ \fis$. \align \First (S) \ &= \ \skips\\ \RestA (S,\sig) \ &= \ \cases S_1 \ift{\bb{b}^A\sig \da \ttt}\\ S_2 \ift{\bb{b}^A\sig \da \fff}\\ \ua \ift{\bb{b}^A\sig \ua} \endcases \endalign {\it Case 4.} \ $S \ \ident \ \whiles\ b \ \dos \ S_0 \ \ods$. \align \First (S) \ &= \ \skips\\ \RestA(S,\sig) \ &\simeq \ \cases S_0;S \tif{\bb{b}^A\sig \da \ttt}\\ \skips \tif{\bb{b}^A\sig \da \fff}\\ \ua \tif{\bb{b}^A\sig\ua}. \endcases \endalign This completes the definition of \First\ and \RestA. %Note (in cases 3 and 4) that the boolean test %in an \ifs' or \qwhiles\ statement $S$ %is assumed to %take up one time cycle; %this is modelled by %taking \,$\First(S) \ident \skips$. The following shows that the i/o semantics, derived from our algebraic operational semantics, satisfies the usual desirable properties. \Lemma ($i$) For $S$ atomic, \ $\SA \simeq \angg{S}^A$, \ \ie, \align \bb{\skips}^A\sig \ &= \ \sig \\ \bb{\xtt:=t}^A\sig \ &\simeq \ \sig\{\xtt/\tAsig\}. \endalign $$\TOL \bb{S_1;S_2}^A\sig \ \simeq \ \bb{S_2}^A(\bb{S_1}^A\sig). \tagii \TOR$$ $$\TOL \bb{\ifs\ b\ \thens\ S_1\ \elses\ S_2\ \fis}^A\sig \ \simeq\ \cases \bb{S_1}^A\sig \tif{\bb{b}^A\sig \simeq \ttt}\\ \bb{S_2}^A\sig \tif{\bb{b}^A\sig \simeq \fff}\\ \ua \tif{\bb{b}^A\sig\ua}. \endcases \tagiii \TOR$$ $$\TOL \bb{\whiles\ b\ \dos\ S\ \ods}^A\sig\ \simeq \ \cases \bb{S; \whiles\ b\ \dos\ S\ \ods}^A\sig \tif{\bb{b}^A\sig \simeq \ttt}\\ \sig \tif{\bb{b}^A\sig \da \fff}\\ \ua \tif{\bb{b}^A\sig\ua}. \endcases \tagiv \TOR$$ \endpr \pr{$(d)$ Semantics of procedures} Finally, if $$P \ \ident \ \procs\ \ins \ \att\ \outs \ \btt\ \auxs \ \ctt \ \begins \ S\ \ends$$ is a procedure of type \utov, then its meaning is a function $$\bb{P}^A : \ \Au \pto \Av$$ defined as follows. For \ainAu, let \sig\ be any state on $A$ such that \ $\sig[\att] = a$. (We are using the notation \ $\sig[\att] \,\eqdf (\sig(\att_1),\dots,\sig(\att_m))$ \ for tuples \ $\att\,\ident\,(\tup{\att}1m)$.) \ Then $$\bb{P}^A(a) \ \simeq \ \cases \sig'[\btt] \tif{\SA\sig\da \sig'} \ \tx{(say)}\\ \ua \tif{\SA\sig\ua.} \endcases$$ This can be shown to be well-defined, \ie, independent of the choice of \sig. We will often write \ \PA\ \ for \ $\bb{P}^A$. Finally, a function $f$ on $A$ is defined to be {\it computable on $A$ by a \While\ procedure} $P$ if \ $f = \PA$. It is \While\ {\it computable on} $A$ if it is computable on $A$ by some \While\ procedure. \WhileA\ is the class of functions \While\ \,computable on $A$. \shead{4.3}{\WhileN\ \,and \Whilex\ \,computability} Consider now the \While\ programming languages over \SigN\ and \Sigx. A \WhileNSig\ {\it procedure} is a \WhileSigN\ procedure in which the {\it input} and {\it output} variables have sorts in \Sig. (However the auxiliary variables may have sort \nats.) A function on $A$ is \WhileN\ {\it computable on} $A$ if it is computable by some \WhileN\ procedure on $A$. A \WhilexSig\ procedure is a \WhileSigx\ procedure in which the {\it input} and {\it output} variables have sorts in \Sig. (However the auxiliary variables may have starred sorts or sort \nats.) A function on $A$ is \Whilex\ {\it computable on} $A$ if it is computable by some \Whilex\ procedure on $A$. The importance of \Whilex\ \,computability lies in the fact that it forms the basis for a generalised Church-Turing Thesis for computability on abstract many-sorted algebras (\ns[.tz hb.]). \shead{4.4}{Representation of term evaluation; \ the term evaluation property} Let \ $\xtt=(\tup{\xtt}{1}{n}):u$. Let \,\Termx(\Sig) \,be the class of all \Sig-terms with variables among \xtt\ only, and let \,\Termxs(\Sig) \,be the class of such terms of sort $s$. The {\it term evaluation representing function on $A$ relative to \xtt} is the function $$\texsA: \ \cnr{\Termxs(\Sig)} \times \Au \ \to \ \As$$ (where \,\cnr{S} \,denotes the set of G\"odel numbers of the set $S$) defined by $$\texsA ( \cnr{t}, \ a_1,\dots,a_n ) \ = \ \tAsig,$$ %for all \,$t\in\Termxs(Sig)$, where \cnr{t} is the G\"odel number of $t$, and \sig\ is any state on $A$ such that \,$\sig(\xtt_i) = a_i$ \ $(i=1,\dots,n)$. The algebra $A$ is said to have the {\it term evaluation property \,(TEP)} \,if for all \xtt\ and $s$, the term evaluation representing function \,\texsA\ \,is \While\ computable on \AN. Many well-known varieties (\ie, 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 {\it effective normalisability\/} of the terms of these varieties. In the case of rings, this means an effective transformation of arbitrary terms to polynomials. Consequently, the unordered and ordered algebras of real and complex numbers (\RRR, \RRRL, \CCC\ and \CCCL, defined in \S1.4.3), which we will study in Section 5, have the TEP. (See \ns[.cas <, \S5>.].) The TEP will be important in applications of Engeler's Lemma (Section 5). \Shead{5}{While' semicomputability on standard partial algebras} We want to generalise the notion of {\it 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 \WhileN\ and \Whilex\ semicomputability. There are many useful applications of these concepts, and they satisfy certain {\it closure properties\/} (\ie, closure under finite unions and intersections), and also {\it Post's Theorem\/}: {\displaytext A set is computable if, and only if, it and its complement are semicomputable. } The second idea of importance is that of a {\it projection} of a semicomputable set. In computability theory on the set \NN\ of natural numbers, the class of semicomputable sets is closed under taking projections, but this is not true in the general case of algebras, even with \Whilex\ computability. (A reason is the restricted form of computable local search available in our models of computation.) Projective semicomputability is strictly more powerful (and less algorithmic) than semicomputability. In \ns[.tz hb.] \ we study these two notions in some detail. \shead{5.1}{\While\ \,semicomputability} The {\it halting set} of a procedure \ $P:\utov$ \ on $A$ is the relation $$\HaltAP \ \eqdf\ \{ a\in \Au \br \PA(a)\da\}.$$ A relation $R$ on $A$ is \While\,\ {\it semicomputable} on $A$ if it is the halting set on $A$ of some \While\,\ procedure. \Examples ($a$) On the naturals \NNN\ the \While\ semicomputable sets are precisely the recursively enumerable sets, and the \While\ computable sets are precisely the recursive sets. \smskipn ($b$) On the standard algebra \RRR\ of reals (\S1.1), the set of {\it naturals} (as a subset of \RR) is \While\ semicomputable on \RRR, being the halting set of the following procedure: \align \tx{\sf is}\_\nats \ \ident\ \ &\procs \ \ins \ \xtt: \reals\\ &\quad \begins\ \whiles\ \nots\ \xtt = 0\\ &\qquad\quad\ \ \dos\ \xtt := \xtt-1 \ \ods\\ &\quad\ends \endalign ($c$) Similarly, the set of {\it integers} is \While\ semicomputable on \RRR. \smskipn ($d$) However, the sets of naturals and integers are \While\ {\it computable} on \RRRL. \smskipn ($e$) The set of {\it rationals} is \While\ semicomputable on \RRR. \smskipn Note that Examples ($b$)--($e$) depend on the fact that equality and order on the reals is decidable --- in fact, primitive --- in the algebras \RRR\ and \RRRL\ (\S1.1). The situation is, of course, quite different with the topological partial algebra \RRRp\ (\S3.2) or total algebra \RRRtN\ (\S8.2). \shead{5.2}{\WhileN\ \,and \Whilex\ \,semicomputability} A relation $R$ on $A$ is \WhileN\ (or \Whilex) {\it semicomputable} on $A$ if it is the halting set of some \WhileN\ (or \Whilex\ respectively) procedure on \AN\ (or \Ax\ respectively). Post's Theorem applies also to \WhileN\ and \Whilex\ semicomputability. We also have projective versions of these notions: A relation $R$ on $A$ is {\it projectively} \WhileN\ \,(or \Whilex) {\it semicomputable} on $A$ iff $R$ is a {\it projection} of a \WhileSigN\ \, (or \WhileSigx\ respectively) semicomputable relation on \AN\ (or \Ax\ respectively). The importance of \Whilex\ \,semicomputability lies in the fact that it forms the basis for a {\it generalised Church-Turing Thesis for specifiability of relations on abstract many-sorted algebras} (\ns[.tz hb.]). \shead{5.3}{Computation tree; \ Engeler's Lemma} We can define, for any \While\ procedure $P$ over \Sig, a {\it computation tree} for $P$, which is like an unfolded flow chart'' of $P$. Using this computation tree, we can prove an important structure theorem for \While\ semicomputabilty due to E. Engeler ([.engeler markham.]). For each leaf \lam\ of the computation tree \TTT, there is a {\it boolean} $\bbb_\lam$, which expresses the conjunction of results of all the successive tests, that (the current values of) the variables in $P$ must satisfy in order for the computation to follow'' the finite path from the root to \lam. Next, using an effective enumeration of the leaves of \TTT, \ we can express the {\it halting formula for $S$} as an {\it effective (countably) infinite disjunction of booleans}, which expresses the conditions under which execution of $P$ eventually {\it halts}, if started in the initial state (represented by) the input variables of $P$. Hence we obtain \pr{Engeler's Lemma} {\sl Let $R$ be a \While\,\ semicomputable relation on a standard \Sig-algebra $A$. Then $R$ can be expressed as an effective countable disjunction of booleans over \Sig.} \endpr Next, using the above results applied to \Whilex\ procedures, together with the \Sigx/\Sig\ conservativity lemma for terms (Section 2), we can prove a stronger version of Engeler's Lemma. \pr{Engeler's Lemma for \Whilex\ semicomputability} {\sl Let $R$ be a \Whilex\,\ semicomputable relation on a standard \Sig-algebra $A$. Then $R$ can be expressed as an effective countable disjunction of booleans over \Sig. \endpr From this we can derive: \Thmn{ \ (Semicomputability equivalence theorem)} Suppose that $A$ is a standard \Sig-algebra with the TEP, and that $R$ is a relation on $A$. Then the following assertions are equivalent: \smskipn ($i$) \ $R$ is \WhileN\ semicomputable on $A$, \smskipn ($ii$) \ $R$ is \Whilex\ semicomputable on $A$, \smskipn ($iii$) \ $R$ can be expressed as an effective countable disjunction of booleans over \Sig. \endpr Details of the proofs of Engeler's Lemma and of the semicomputabilty equivalence theorem can be found in \ns[.tz hb.]. \Shead{6}{Continuity of computable functions} In this section we will prove that computational processes associated with \Whilex\ programs over topological partial algebras are continuous. More precisely, we will prove the following \pr{Continuity Theorem} Let $A$ be a standard topological partial algebra. \itemitem{($a$)} If \,$f\in\WhileA$ \,then $f$ is continuous on $A$. \itemitem{($b$)} If \,$f\in\WhileNA$ \,then $f$ is continuous on $A$. \itemitem{($c$)} If \,$f\in\WhilexA$ \,then $f$ is continuous on $A$. \endpr \smskipn Before we prove this theorem, we give two corollaries. \newpage \Corn{1 \ (Openness Theorem)} If $R$ is \smskipn ($a$) \Whilex\ semicomputable on $A$, \ or \smskipn ($b$) projectively \Whilex\ semicomputable on $A$, \smskipn then $R$ is open in $A$. \endpr \Pf \ ($a$) \,Suppose $R$ is the halting set of a \Whilex\ computable function \,$f:\Au\to\As$. By the Continuity Theorem (Section 6), $f$ is continuous. Hence \,$R = f^{-1}[\As]$ \ is open. \smskipn ($b$) \,Suppose \,$R:u$ \, is projectively \Whilex\ semicomputable. Then $$R \ = \ \{x\in \Au \mid \ex y \in \Av R^0(x,y)\}$$ for some \While\ semicomputable relation $R^0$ in \Ax\ of type \,$u\times v$, \,where $u$ and $v$ are product types over \Sig\ and \Sigx\ respectively. By part ($a$) applied to \Ax, \,$R^0$ is open in the product space \,$A^{u\times v}$. Hence $R$, which is the projection of $R^0$ on \Au, is open. \endpf In the above proof, we used the fact that a projection of an open set is open. \Corn{2 \ (Clopenness Theorem)} A \Whilex\ computable relation on $A$ is clopen ($=$ closed and open) in $A$. \endpr \Pf By Post's Theorem and Corollary 1. \endpf We turn to the proof of the Continuity Theorem, which occupies the rest of this section. Clearly, part ($a$) follows trivially from parts ($b$) and ($c$). Note that conversely, parts ($b$) and ($c$) follow easily from ($a$). For example, if \,$f\in\WhilexA$ \,then \,$f\in\While(\Ax)$, \,therefore $f$ is continuous on \Ax, and hence on $A$. We will prove part ($a$) by demonstrating the continuity of the operational semantics developed in \S4.2. We will see the advantage of the algebraic approach to operational semantics used there, since these functions are built up from simpler functions using composition, thus preserving continuity. We proceed with a series of lemmas. Let \,$X,Y,\dots$ \,be topological spaces. Remember, functions are (in general) partial. \Lemmasn{ \ (Basic lemmas on continuity)} \smskipn (1) A composition of continuous functions is continuous. \smskipn(2) Let \ $f:X\,\pto \,\tuptimes{Y}{1}{n}$ \ have component functions \ $f_i:X\,\pto \,Y_i$ \ for $i=1,\dots,n$, \ \ie, \ $f(x) \simeq (f_1(x),\dots,f_n(x))$ \ for all $x\in X$. Then $f$ \,is continuous iff all the $f_i$ are continuous for $i=1,\dots,n$. \smskipn(3) If $D$ is a discrete space, then a function \ $f:X\times D \,\pto \,Y$ \ is continuous iff \ $f(\,\cdot\,,d):X\,\pto \,Y$ \ is continuous for all \,$d\in D$. \endpr \Corn3 The discriminator \ $f:\BB \times X^2 \to X$, \ defined by \ $f(\ttt,x,y) = x$ \ and \ $f(\fff,x,y) = y$, \ is continuous. \endpr \Corn4 Let \ $f:X\pto Y$ \ be defined by $$f(x) \simeq \cases g_1(x) \tif{h(x)\da \ttt}\\ g_2(x) \tif{h(x)\da \fff}\\ \ua \tif{h(x)\ua,} \endcases$$ where \ $g_1,g_2:X\pto Y$ \ and \ $h:X\pto \BB$ \ are continuous. Then $f$ is continuous. \endpr \Pf From Corollary 3 and Lemma 1. \endpf \Lemman4 Let \ $g:X\times\NN\to Y$ \ be continuous, and let \,$y_0\in Y$ \,be such that \,$\{y_0\}$ \,is clopen in $Y$. Let \ $f:X\to \NN$ \ be defined by $$f(x) \ \simeq \ \mu k [g(x,k) \da y_0],$$ \ie, \TOL $$f(x) \da k \ \ \llongtofrom \ \ \all i0. Also, in a topological \Sig-algebra A, if \,u=\tuptimes{s}{1}{m}\in \ProdTypeSig, \,and A_{s_i} is compact for i=1,\dots,m, \,then so is \Au\ (with the product topology). Now we have seen (by Corollaries 1 and 2 in \S3.4) that for sets:$$ \gather \tx{semicomputable} \ \ \llongto\ \ \tx{open}\\ \tx{computable} \ \ \llongto\ \ \tx{clopen}. \endgather $$We can reverse the direction of the implication in the second of these assertions, under the assumption of {\it compactness}. \newpage \Thm Let A be a topological partial algebra, and let \,u = \tuptimes{s}{1}{m} \in \linebreak \ProdTypeSig, \,where for \,i=1,\dots,n: \itemitem{(a)} \,A_{s_i} is compact, \,and \itemitem{(b)} \,A_{s_i} has an open subbase of \While\ semicomputable sets. \smskipn Then for any relation \,R\sseq\Au, the following are equivalent: \smskipn (i) R is \While\ computable, \smskipn (ii) R is \Whilex\ computable, \smskipn (iii) R is clopen in \Au. \endpr \Pf (i)\llongto(ii) is trivial. \smskipn (ii)\llongto(iii) follows from Corollary 1 in \S3.4. \smskipn (iii)\llongto(i): Note first that from assumptions (a) and (b), the product space \Au\ is compact, and has an open subbase of \While\ semicomputable sets. Suppose now that R is clopen in \Au. Since R is {\it open}, we can write$$ R \ = \ \bigcup_{i\in I}B_i $$where the B_i are basic open sets. Each B_i is a finite intersection of subbasic open sets, and hence semicomputable, by (b) and closure of \While\ semicomputability under finite intersections. Since R is {\it closed}, R is compact by (a), and hence R is the union of {\it finitely many} of the B_i's, and so R is semicomputable, by closure of \While\ semicomputability under finite unions. Repeating the above argument for the complement of R in \Au, we infer by Post's Theorem (Section 5) that R is computable. \endpf Note that (by closure of \While\ semicomputability under finite intersections) assumption (b) in the above Theorem is equivalent to: \itemitem{(b)} {\sl \,A_{s_i} has an open {\rm base} of \While\ semicomputable sets.} \Example Let \,A = \BBBbar, \,the {\it stream algebra\/} \,(\S2.5) \,over the algebra \,\BBB\ \,of booleans. The carrier \,\BBbar\ \,consists of all binary streams$$ \be : \ \NN \ \to \ \BB. $$It has the product topology over \,\BB, \,and is therefore compact (\S3.4(c)). It has an open subbase, consisting of sets of the form$$ \{\be\in\BBbar \mid \be(k) = \ttt\} \qquad\tx{and}\qquad \{\be\in\BBbar \mid \be(k) = \fff\}, \tag1 $$for all k\in\NN, \,which are easily seen to be \While\ computable over \BBbar. By the above theorem, the \While\ \,or \Whilex\ \,computable subsets of \,\BB\ \,are exactly the clopen subsets of \,\BB, \,which are precisely all {\it finite unions of finite intersections\/} of sets of the form (1). \endpr \newpage \Shead8{Connected algebras} We investigate the relationship between computability and explicit definability for functions in a connected domain of an algebra. \shead{8.1}{Basic concepts} A topological space X is said to be {\it connected} if the only clopen subsets of X are X and \emptyset. The following are two important properties of connected spaces. (Proofs may be found in most standard topology texts.) \Props (1) X is connected iff the only continuous total functions from X to any discrete space is constant. \smskipn(2) A finite product of connected spaces is connected. Hence in a topological \Sig-algebra A, if \,u=\tuptimes{s}{1}{m}\in \ProdTypeSig, \,and A_{s_i} is connected for i=1,\dots,m, \,then so is \Au. \endpr \Examples (1) The space \,\RR\ \,of the reals, with its usual topology, is connected. Therefore, so is the product space \,\RRq\ \,for any q. Hence (by \S3.4, Corollary 2) for any topological partial algebra over \,\RR, \,such as the algebra \,\RRRp\ \,(\S3.2(b)), \,the only \While\ \,or \Whilex\ \,computable subsets of \,\RRq\ \,are \,\RRq\ \,itself and \,\emptyset. \smskipn(2) Similarly, by the connectedness of the unit interval I (and hence of \Iq), the only \While\ or \Whilex\ computable subsets of \Iq\ in any interval algebra \,\IIIp\ \,over I (\S3.2(c)) are \Iq\ and \emptyset, {\it regardless of the choice of (continuous partial) functions \,\tup{F}1k \,as basic operations of this algebra!} \endpr We will only develop the theory in this section for {\it total functions} on {\it total algebras}. The essential idea is that if f is a computable total function on a connected domain in A, then f is continuous, and so, by Proposition 1, its definition cannot depend non-trivially on any boolean tests involving variables of sort s if \As\ is connected. (We will make this precise below, in the proof of Lemma 3.) In this section we make the following assumption. \pr{Totality Assumption}\sl A is a total topological algebra. \endpr \shead{8.2}{Examples of total topological algebras on the reals} Two important total topological algebras based on the reals which will also be important for our purposes are: \smskipn (a) The algebra \RRRtN\ (t" for total topological"), defined by$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\RRRtN \\ \imports &\RRRo, \,\NNN,\,\BBB\\ \functionss&\ifR:\BB\times\RR^2\to\RR,\\ &\divN:\RR\times\NN\to\RR,\\ \ends& \endmatrix } $$Here \RRRo\ is the ring of reals (\S2.1, Example (b)), \NNN\ is the standard algebra of naturals (\S2.2, Example (b)), \divN\ is division of reals by naturals (where division by zero is defined as zero), and \RR\ has its usual topology. Note that \RRRtN\ does not contain the (total) boolean-valued functions \eqR\ or \lsR, since they are not continuous (\cf\ the partial functions \eqp\ and \lsp\ of \RRRp). It is therefore not an expansion of the standard algebra \RRR\ of reals (\S2.2, Example (c)) which contains \eqR. (Compare the N-standardisation \RRRN\ of \RRR\ (\S2.3, Example (b)) which does contain \eqR). \smskipn (b) ({\it The interval algebra of reals.}) Here the unit interval \,I = [0,1] \,is included as a separate carrier of sort \intvls', again with the usual topology. This is useful for studying real continuous functions with compact domain. (We could also choose \,I = [-1,1], \,etc.) The total topological algebra \IIItN\ is defined by$$ \boxed{ \matrix \format\l&\quad\l\\ \algebras &\IIItN \\ \imports &\RRRtN\\ \carrierss & I\\ \functionss &\iI:I\to\RR\\ \ends& \endmatrix } $$Here \iI\ is the embedding of I into \RR. \endpr The reason that \NN, and the function \divN, are included in these total algebras (unlike the partial algebras \RRRp\ and \IIIp\ of \S3.2) is because of their applicability in the theory of approximable computability in Section 9. \sheads{8.3}{Explicit definability and \While\ computability} \Defsn{ \ (Explicit definability)} Let f be a function on A. \smskipn(a) f is \Sig-{\it explicitly definable on A} if f is definable on A by a \Sig-term. \smskipn(b) f is \Sigx-{\it explicitly definable on A} if f is definable on A by a \Sigx-term. \endpr By the \Sigx/\Sig\ Conservativity Theorem for terms (\S2.5), the two concepts defined above are equivalent: \Lemman1 \ \Sig-explicit definability on A \ \ \llongtofrom\ \ \Sigx-explicit definability on A. \endpr Because of Lemma 1, we shall usually speak of explicit definability" over an algebra to mean either \Sig- or \Sigx-explicit definability. \endpr \Lemman2 \ Explicit definability on A \ \ \llongto\ \ \While\ computability on A. \endpr This is the easy" direction for the theorem below. (For this direction, A need not be connected or even topological.) In preparation for the converse direction, we need the following \Lemman3 Suppose \Au\ is connected. Let \,P:\utov \,be a (\While\ or \Whilex) procedure which defines a total function on A, \ie, \,\HaltAP = \Au. Then the computation tree \,\TP\ \, for P is essentially finite, or (more accurately) semantically equivalent to a finite, unbranching tree. \endpr \Pf Put$$ P \ \ident \ \procs\ \ins \ \att\ \outs \ \btt\ \auxs \ \ctt \ \begins \ S\ \ends $$where \,\att:u, \btt:v and \ctt:w, \,and \,S \ \ident\ \Sinit;S', \,where \,\Sinit\ \,is an initialisation of the variables \,\btt,\ctt\ to their default values. Let \,\TTT \ = \ \TP. First, we show that all branches in \TTT\ can be eliminated. Consider a branch at a test node in \TTT:$$ \beginpicture \arrow <0.1in> [0.2,0.5] from 0 0 to 0 -0.2 \put {$t$} [lb] at 0.1 -0.2 \putrule from 0 -0.2 to 0 -0.3 \setlinear\plot 0 -0.3 0.2 -0.5 0 -0.7 -0.2 -0.5 0 -0.3 / \put {$b$} at 0 -0.5 \arrow <0.1in> [0.2,0.5] from 0.1 -0.6 to 0.3 -0.8 \put {N} [lb] at 0.35 -0.75 \setlinear\plot 0.3 -0.8 0.4 -0.9 / \arrow <0.1in> [0.2,0.5] from -0.1 -0.6 to -0.3 -0.8 \put {Y} [rb] at -0.35 -0.75 \setlinear\plot -0.3 -0.8 -0.4 -0.9 / \endpicture $$\smskipn Note that each edge of \TTT\ is labeled with a {\it syntactic state}, \ie, a tuple of terms t which gives the current state" of the variables \,\abct, \,assuming execution of S starts in the initial state" (represented by) those variables. This boolean test then defines a function$$ f_{b,t}:\Au \ \to \ \BB $$where \,(putting \,\xtt \ident \abct, \,and writing \,b\xttt' \,for the syntactic substitution of the tuple t for \xtt\ in b)$$ f_{b,t}(a) \ = \ b\xttt[a,\delbAv,\delbAw] $$\ie, \,f_{b,t}(a) \,is the evaluation of \,b\xttt \,when a is assigned to \att\ \,and the default tuples \,\delbAv, \delbAw\ \,are assigned to \,\btt,\ctt\ \,respectively. The function f_{b,t} is clearly (\While\ or \Whilex) computable, by Lemma 2, and hence continuous, by the Theorem in Section 6. It is also total, by the Totality Assumption. By Proposition 1 of \S8.1, it must therefore be {\it constant} on \Au. If it is constantly \ttt, we can replace this test node by its left branch (\ie, delete the node and the right branch), and if it is constantly \fff, we can similarly replace the node by its right branch only. By repeating this process, we can replace \TTT\ by a semantically equivalent tree \TTTp\ without any boolean tests, and (hence) without any branching. The tree \TTTp\ consists of a single path, which must be finite, since \PA\ is total by assumption. \endpf Examples of the application of this lemma are the total topological algebras \RRRtN\ and \IIItN, and procedures of type \,\reals^q\to\reals \,and \,\intvls^q\to\reals \,respectively. In general, this transformation of \,\TP\ \,to a finite unbranching tree given by the proof of Lemma 3 is {\it not effective in} P, since it depends on the evaluation of (constant) boolean tests. If we want it to be effective in P (as we will in the next section, dealing with approximable computability), we will need a further condition on A, such as the {\it boolean computability property} (defined in Section 9). \Lemman4 If a computation tree for a (\While\ or \Whilex) procedure P is finite and unbranching, then \PA\ is (\Sig)-explicitly definable on A. \endpr \Pf This is straightforward, by induction on the length of the tree. \endpf Note that more generally, Lemma 4 holds if the tree for P is finite but (possibly) branching. (Use the discriminator in constructing the defining term.) \endpr Combining Lemmas 2, 3 and 4, we have conditions for an equivalence between explicit definability and \While\ computability: \Thm Let A be a total topological algebra, and suppose \Au\ is connected. Let \,f:\Au\to\Av \,be a total function. Then the following are equivalent: \smskipn(i) f is \While\ computable on A; \smskipn(ii) f is \Whilex\ computable on A; \smskipn(iii) f is explicitly definable on A. \endpr \Examples This theorem holds for the total topological algebras \RRRtN\ and \IIItN, and total functions \ f:\RRq \to \RR \ and \ f:\Iq \to I \ respectively. \endpr \Shead{9}{Approximable computability} It is often the case that functions are computed approximately, by a sequence of polynomial approximations". In this way we extend the class of computable functions to that of {\it approximably computable} functions. This theory will build on the work of Section 8. First we review some basic notions on convergence of sequences of functions. \Defn{1 \ (Effective uniform convergence)} Given a set X, a metric space Y, a total function \,f:X\to Y, \, and a sequence of total functions \,g_n:X\to Y \,(n=0,1,2,\dots), %\,and a sequence of real numbers \,M_n \,(n=0,1,2,\dots) %\,which is monotonically decreasing to zero, we say that g_n {\it converges effectively uniformly to f on X} (or {\it approximates f effectively uniformly on} X) %with modulus of convergence} (M_n) iff there is a total recursive function \,e:\NN\to\NN \,such that for all n,k and all x \in X,$$ k\ge e(n) \ \ \llongto \ \ d_Y(g_k(x),f(x)) < 2^{-n}. $$\endpr Note that for an equivalent definition, \,2^{-n}' \,on the rhs of the above inequality could be replaced by \,1/M(n)', \,where \,M:\NN\to\NN \,is any total recursive function which is increasing and unbounded. The theory here will be developed for {\it total functions} on {\it total metric algebras}. In this section therefore, we make the following \pr{Totality Assumption}\sl A is a total metric algebra \endpr \Examplesn{\ (Total metric algebras on the reals)} The two total topological algebras based on the reals given in \S8.2 can be viewed as metric algebras in an obvious way. The second of these, the interval algebra \IIItN, will be particularly useful here. \endpr So suppose A is a total metric \Sig-algebra. Let \,u,v \,be \Sig-product types \, and \,s a \Sig-sort. \Defn{2 \ (Effective uniform \While\ approximability)} A total function \,f:\Au\to \Av \,is {\it effectively uniformly} \While\ (or \Whilex) {\it approximable on A} if there is a \While\ (or \Whilex\ respectively) procedure$$ P:\nats\times u \ \to \ v $$on \AN\ such that \PAN\ is total on \AN\ and, putting \,g_n(x) \eqdf \PAN(n,x), \ the sequence g_n approximates f effectively uniformly on \Au. \endpr Note that if A is N-standard, we can replace \AN' by A' in the above definition. \Lemman1 If \Au\ is compact, and \,f:\Au\to\As \,is effectively uniformly \Whilex\ approximable on A, then f is continuous. \endpr \Pf By the Theorem in \S3.4, the approximating functions for f are continuous. The lemma follows by a standard result for uniform convergence on compact spaces. \endpf \Lemman2 (a) A function from \RRq\ to \RR\ \,is explicitly definable over \RRRtN\ iff it is definable by a {\it polynomial} in q variables over \RR\ with rational coefficients. \smskipn(b) A function from \Iq\ to \RR\ \,is explicitly definable over \,\IIItN\ \,iff it is definable by a polynomial in q variables over I with rational coefficients. \endpr \Pf In both cases, definability by a polynomial clearly implies explicit definability. For the reverse direction: in a term which explicitly defines the function, all \ifR' subterms involving boolean tests can be eliminated by the connectedness of \RRq, using a similar argument as in the proof of Lemma 3 in \S8.3. The result is a polynomial definition. \endpf This lemma explains the following terminology, since Weierstrass-type theorems deal typically with approximations of real functions by polynomial functions (uniformly on compact domains). \endpr \Defn{3 \ (Effective Weierstrass approximability)} (a) A total function \,f:\Au\to\As \,is {\it effectively \Sig-Weierstrass approximable over A} \,if, for some \,\xtt:u, \,there is a total computable function$$ h:\ \NN \ \to \ \cnr{\Termxs(\Sig)} $$such that, putting \,g_n(x) \eqdf \texsA(h(n),x), \ the sequence g_n approximates f effectively uniformly on \Au. (Recall the syntactic class \Termxs\ and the term evaluation representing function \,\texsA\ \,from \S4.4.) \smskipn (b) {\it Effective \Sigx-Weierstrass approximability} is defined similarly, by replacing \Sig' by \Sigx' and \texsA' by \texsAx'. \endpr %(The syntactic class \Termxs\ and the term evaluation representing function %\texsA\ were both defined in \S4.4.) \Lemman3 A function on A is effectively \Sig-Weierstrass approximable iff it is effectively \Sigx-Weierstrass approximable. \endpr \Pf From a computable function$$ h^*:\ \NN \ \to \ \cnr{\Termxs(\Sigx)} $$we can construct a computable function$$ h:\ \NN \ \to \ \cnr{\Termxs(\Sig)} $$where for each n, h(n) and h^*(n) are G\"odel numbers for semantically equivalent terms, using the fact that the transformation of \Sigx-terms to \Sig-terms in the Conservativity Theorem (2.5) is effective. \endpf We shall therefore usually speak of effective Weierstrass approximability" over an algebra to mean effective Weierstrass approximability in either sense. We now investigate the connection between effective uniform \While\ approximability and effective Weierstrass approximability. We are looking for a uniform version of the Theorem in \S8.3 (\ie, uniform over \NN-sequences of functions). To attain this uniformity, we need an extra condition in each direction: for effective Weierstrass \tto effective uniform \While" (\ie, a uniform version of Lemma 2 in \S8.3) we need the TEP (\S4.4), and for `effective uniform \While\ \tto effective Weierstrass" (\ie, a uniform version of Lemma 3 in \S8.3) we need a new condition, the {\it boolean computability property}, which we now define. \Defn{4 \ (BCP)} An \Sig-algebra A has the {\it boolean computability property \,(BCP)} if for any closed \Sig-boolean term b, its valuation \,b_A (= \ \ttt or \fff, \,\cf\ 4.2(a)) can be effectively computed, or (equivalently) there is a recursive function$$ f:\cnr{\Term_{\emptyset,\boolss}(\Sig)} \ \to \ \BB $$with \ f(\cnr{b}) \ = \ b_A \ (where \,\Term_{\emptyset,\boolss}(\Sig) \,is the set of closed boolean \Sig-terms). \endpr To avoid confusion: \ the BCP is {\it not} a special case of the TEP, for closed terms of sort \bools. It requires the function f in the above definition to be recursive, \ie, computable over \NN\ (and \BB) in the sense of {\it classical recursion theory}. The TEP entails only that f be computable over A --- a weaker assumption (in general). \Examples Both \RRRtN\ and \IIItN\ have the TEP and the BCP. \endpr We will see how these two conditions (TEP and BCP) are applied in opposite directions to obtain a uniform version of the Theorem in \S8.3. In the following lemma, A is any total algebra, not necessarily metric or even topological (\cf\ Lemma 2 in \S8.3). \Lemman4 Suppose A has the TEP. Given variables \xtt:u, \,let$$ h:\ \NN \ \to \ \cnr{\Termxs(\Sig)} $$be a total computable function. Then there is a \While(\SigN) procedure \,P:\nats\times u \to s \,such that for all \xinAu\ and \ninNN,$$ \PAN(n,x) \ = \ \texsA(h(n),x). $$\endpr \Pf Simple exercise. \endpf For the converse direction: \Lemman5 Suppose \Au\ is connected and A has the BCP. Let \,P:\nats\times \utov \,be a (\While\ or \Whilex) procedure over \AN\ which defines a total function on \AN. Then there is a computable function \ h:\ \NN \to \cnr{\Termxs(\Sig)} \ such that for all \xinAu\ and \ninNN,$$ \texsA(h(n),x) \ = \ \PAN(n,x). $$\endpr \Pf Suppose$$ P \ \ident \ \procs\ \ins \ \ntt,\att\ \outs \ \btt\ \auxs \ \ctt \ \begins \ S\ \ends $$where \,\ntt:\nats. Consider the \WhileNSig\ procedures \,P_n:\utov \,(n=0,1,2,\dots) \,defined by$$ P_n \ \ident \ \procs\ \ins \ \att\ \outs \ \btt\ \auxs \ \ntt,\ctt \ \begins \ \ntt:=\bar n; S\ \ends $$where \bar n is the numeral for n. It is clear that for all \ninNN\ and \xinAu,$$ P_n^A(x) \ = \ \PAN(n,x). $$By Lemmas 3 and 4 of \S8.3, P_n^A is definable by a \Sig-term t_n. Moreover, the sequence (t_n) is {\it computable in} n, by use of the BCP to effectivise the transformation of the tree \TTT\ to \TTTp\ in the construction given by the proof of Lemma 3 of \S8.3. (Note that the evaluation of a {\it constant boolean test} can be effected by the computation of any {\it closed instance} of the boolean term, which exists by the Instantiation Assumption.) Hence the function h defined by$$ h(n) \ = \ \cnr{t_n} $$is computable. \endpf We now have a uniform version of the Theorem in \S8.3: \newpage \Thm Suppose \Au\ is connected and A has the TEP and BCP. Let \,f:\Au\to\As \,be a total function. Then the following are equivalent: \smskipn(i) f is effectively uniformly \While\ approximable on A; \smskipn(ii) f is effectively uniformly \Whilex\ approximable on A; \smskipn(iii) f is effectively Weierstass approximable on A. \endpr \Pf From Lemmas 4 and 5. \endpf The equivalence of (i) and (iii) was noted for the special case A = \IIItN, \Au = \Iq and \As = \RR \,in [.shepherd 1976.], in the course of proving the equivalence of these with another notion of computability on the reals. (See the historical remark in Section 10.) \endpr \Shead{10}{Application: \ Equivalences with GL-computability} We are especially interested in computability on the reals, and, in particular, a notion of computability of functions from \Iq\ to \RR, developed in Grzegorczyk [1955,1957] and [.lacombe 1955.]. %[.grzegor 1955.] %[.grzegor 1957.] We repeat the version given in [.pourel richards.], giving also, for completeness, the definitions of computable sequences of rationals and computable reals. Finally (in the Theorem below) we state the equivalence of this notion with the others listed in the Theorem in Section 9. \Defs (1) A sequence (r_k) of rationals is {\it computable} if there exist recursive functions \ a,b,s: \NN\to \NN \ such that for all k, b(k)\ne0 \,and$$ r_k \ = \ (-1)^{s(k)}{a(k)\over b(k)}. $$A {\it double sequence} of rationals is {\it computable} if it is mapped onto a computable sequence of rationals by one of the standard recursive pairing functions from \,\NN^2 \,onto \,\NN. \smskipn (2) A sequence (x_k) of reals is {\it computable} if there is a computable double sequence of rationals \,(r_{nk}) \,such that$$ | r_{nk} - x_n | \le 2^{-k} \qquad \tx{for all $k$ and $n$}. $$(3) A total function \ f:\Iq\to\RR \ is {\it GL} (or {\it Grzegorczyk/Lacombe}) {\it computable} if: \itemitem{(i)} f is {\it sequentially computable}, \ie, f maps every computable sequence of points in \Iq\ into a computable sequence of points in \RR; \itemitem{(ii)} f is {\it effectively uniformly continuous}, \ie, there is a recursive function \ \del:\NN\to\NN \ such that for all \,x,y\in\Iq \,and all \ninNN:$$ |x-y| < 2^{-\del(n)} \implies |f(x) - f(y)| < 2^{-n}.  \endpr \newpage \Thm Let \,$f:\Iq\to\RR$ \,be a total function. Then the following are equivalent: \smskipn($i$) $f$ is effectively uniformly \While\ approximable on \IIItN; \smskipn($ii$) $f$ is effectively uniformly \Whilex\ approximable on \IIItN; \smskipn($iii$) $f$ is effectively Weierstrass approximable on \IIItN; \smskipn($iv$) $f$ is GL-computable. \endpr \Pf As we have noted, \Iq\ is connected and \IIItN\ has the TEP and BCP. Hence the equivalence of the first three assertions is a special case of the Theorem in Section 9. The equivalence of ($iii$) and ($iv$) is proved in detail in [.pourel richards.]. \endpf \pr{Historical Remark} The equivalence \,$(iii)\ttofrom(iv)$ \,was proved in [.pourel caldwell.]. An exposition of this proof is given in [.pourel richards.]. Shepherdson [1976] gave a proof of \,$(i)\ttofrom(iv)$ \,by (essentially) noting the equivalence \,$(i)\ttofrom(iii)$ \,and re-proving \,$(iii)\ttofrom(iv)$. The new features in the present treatment are: \ ($a$) the equivalence \,$(i)\ttofrom(iii)$ \,in a more general context, \,and \,($b$) the equivalence of ($ii$) with the rest (both from the Theorem in Section 9). \endpr