\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 3$x$ 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
[1995$a,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).
\tag$ii$
\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
\tag$iii$
\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
\tag$iv$
\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