\input h \cbb{Infinitary Algebraic Specifications for Stream Algebras \fn""{ Presented at the Workshop on Computability and Complexity in Analysis, held in conjunction with MFCS'98, Brno, Czech Republic, August 1998.} \fn""{$^1$Research partially supported by a grant from the Natural Sciences and Engineering Research Council of Canada (NSERC).}} \mn \cb{J.V. Tucker} \ce{\it Computer Science Department, University of Wales, Swansea SA2 8PP, Wales} \ce{\tt J.V.Tucker\@swansea.ac.uk} \sn \ce{{\bf J.I. Zucker}$\,^1$} \ce{\it Dept of Computing and Software, McMaster University, Hamilton, Ont\. L8S 4L7, Canada} \ce{\tt zucker\@mcmaster.ca} \bn {\displayquote {\bf Abstract.} \ A {\smallit stream\/} is an infinite sequence of data from a set $A$. A wide variety of algorithms and architectures operate continuously in time, producing streams of data, for example: systolic arrays, data-flow machines, neural networks and cellular automata. Also many models of real number computation use streams. In this paper we study the construction of an algebra \Abar\ of streams over a many-sorted algebra $A$ of data. In particular, we show how an initial algebra specification for \Abar\ can be constructed from one for $A$. One problem is that \Abar\ is uncountable even when $A$ is finite. To handle this, we work with infinitary terms called {\smallit stream terms}, and infinitary formulae that generalise conditional equations, called \,\om-{\smallit conditional stream equations\/}. } \mn \Shead0{Introduction} A {\it stream} \al\ is an infinite sequence \ $\al(0), \al(1), \dots$ \ of data from a set $A$. A variety of algorithms and architectures operate continuously in time, producing streams of data, for example: systolic arrays, data-flow machines, neural networks and cellular automata. Also many models of real number computation use streams. In this paper we study the construction of an algebra \Abar\ of streams over a many-sorted algebra $A$ of data. In particular, we show how an initial algebra specification for \Abar\ can be constructed from one for $A$ in a uniform way. One problem is that \Abar\ is uncountable even when $A$ is finite! We will develop a new class of infinitary formulae, that generalise the conditional equations, called \,\om-{\it conditional stream equations}. These have the form $$ \conconlims{i=0}{\infty} Q_i \ \imp \ Q $$ where the $Q_i$ and $Q$ are equations that may involve {\it stream terms} of the form $$ \ang{\,t_0,t_1,t_2,\dots\,} $$ where the $t_i$ are data terms. We give a logic \,\CondEqom\ \,for these formulae, and show it is conservative with respect to the corresponding stream version of the infinitary logic \,\Lomiom. We show that certain \om-conditional stream equational theories have initial models that are complete for closed stream terms. Using these infinitary algebraic tools, we prove that the construction of \Abar\ from $A$ is defined by a set \,\StrAx\ \,of \om-conditional stream equations in the following sense: \ If $A$ is the initial algebra of the \om-conditional stream equational theory $E$ then \Abar\ is the initial algebra of the \om-conditional equational theory \,$E+\StrAx$. This work is part of a research programme in computability theory on abstract \linebreak many-sorted algebras \cite{tz:book,tz:ijfocs,tz:leeds,tz:hb}. Specifically, it is related to our studies of real and complex number computation \cite{tz:sanantonio} and computation on stream algebras \cite{tz:marktoberdorf}. \Shead{1}{Many-sorted signatures and algebras} \ssheadrun{1.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 which case we write \ $F: \tuptimes{s}{1}{m}\to s$. \ (The case $m = 0$ corresponds to {\it constant symbols}.) 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: \tuptimes{s}{1}{m}\to s$, \ a function \ $\FA : A_{s_1}\times\dots\times A_{s_m} \to \As$. An {\it abstract data type} of signature \Sig\ (\Sig-\adt) is defined to be a class \KK\ of \Sig-algebras {\it closed under isomorphism}. \shead{1.2}{Adding booleans and counters: \ Standard signatures and algebras} A signature \Sig\ is {\it standard} if it includes the sorts \,\bools\ \,and \,\nats, \,and also \itemitem{($i$)} the standard boolean constants and operations \,\trues, \,\falses, \,\ands, \,\ors\ \,and \,\nots, \,the {\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}, which include \,\nats, \itemitem{($ii$)} the standard operations on the naturals of {\it zero}, {\it successor} and {\it order}. Given a standard signature \Sig, a \Sig-algebra $A$ is a {\it standard} if the carriers of sort \,\bools\ \,and \,\nats\ are (respectively) \,$\BB = \{\ttt,\fff\}$ \,and \,$\NN = \{0,1,2,\dots\}$, \,and the standard operations on these sorts \,listed above have their standard interpretations. Note that any many-sorted signature \Sig, and \Sig-algebra $A$, can be {\it standardised} to a signature \SigBN, and a standard \SigBN-algebra \ABN, by adjoining the sorts \,\bools\ \,and \,\nats\ and the standard operations, with their standard interpretations. We also consider a notion stricter than standardness. A standard signature \Sig\ is {\it strictly standard} if the only operations of \Sig\ with range sort \nats\ or \bools\ are the {\it standard operations} listed above. A algebra is {\it strictly standard} if its signature is. Note that any standardised algebra is automatically strictly standard. (Note also that the terminology used here, for simplicity, differs from that in \cite{tz:hb}. What is here called ``standard" is there called ``N-standard".) \shead{1.3}{Adding streams: \ stream signatures and stream algebras} A standard signature \Sig\ is called a {\it stream signature} if for some designated subsets \,\PreStrSig, \,and \,\StrSig\ \,of \,\SortSig, the following holds: \itemitem{($i$)} There is a bijection \ $s\tofrom \sbar$ \ of \PreStrSig\ with \StrSig, \,where we also write \sbar\ as \ $\nats \to s$ \ for clarity; \itemitem{($ii$)} For all \,$\sbar\in\StrSig$, \,the only \Sig-operations with \sbar\ in its domain are $$ \evals_s : \ (\nats\to s)\times\nats\to s, $$ and the discriminator \,$\ifs_\sbar$ \,on sort \sbar\ (but not equality on \sbar). \nin The sets \PreStrSig\ and \StrSig\ are called (respectively) the sets of {\it pre-stream sorts} and {\it stream sorts} of \Sig. If \Sig\ is a stream signature, then a standard \Sig-algebra $A$ is called a \Sig-{\it stream algebra\/} if for each \,$s\in\PreStrSig$, \,the carrier \Abars\ is given by $$ \Abars \ = \ [\NN\to A_s], $$ \ie, the set of all {\it streams on} $A$, or functions from \NN\ to $A$, and \,$\evals_s$ \,is interpreted as as the function \ $\evalAs: \NNtoAs \times \NN \to \As$ \ which {\it evaluates} a stream at an index, \ie, $$ \evalAs(\al,n) = \al(n). $$ \Example A common way to construct a stream algebra is as follows. Start with any signature \Sig\ and \Sig-algebra $A$. First we standardise them (assuming they are not already standard), to form \SigBN\ and \ABN. Then choose a set \,$\Sbi \subseteq \SortSig$ \,of {\it pre-stream sorts}. We then extend \SigBN\ to a {\it stream signature \SigbarS\ relative to \Sbi}, as follows. With each \sinS, associate a new stream sort \sbar. Then $\Sort(\SigbarS) = \SortSig \cup \Sbar$, \ where \ $\Sbar \eqdf \{\sbar\mid\sinS\}$, \,and \,$\Func(\SigbarS)$ consists of \FuncSig, together with \,$\evals_s$ \,and \,$\ifs_\sbar$ \,for each \sinS. Now expand \ABN\ to a \SigbarS-stream algebra \,\AbarS\ \,by adding, for each \sinS, the carrier \,$\Abars \ = \ \NNtoAs$. The algebra \,\AbarS\ \,is the {\it (full) stream algebra over $A$ with respect to \Sbi}. Note that in order for the closed terms over a signature \Sig\ to form a \Sig-{\it term algebra\/}, we should make one more assuption on \Sig: \pr{Instantiation Assumption} {\sl Each sort of \Sig\ is instantiated, \ie, there is a closed term of each sort.} \endpr \nin This assumption is satisfied for all the familiar algebras used as abstract data types. We should note, however, that it is {\it not\/} satisfied by {\it stream signatures\/} at their stream sorts, since there are no ``constant" streams or, indeed, any streams, definable from the basic stream operations. Nevertheless, the assumption {\it is\/} satisfied by these stream signatures with respect to the {\it infinite term construction\/} described below (Section 5). \Shead2{Infinitary logic over stream signatures} \ssheadrun{2.1}{Infinitary terms} The problem we have is this: we want initial algebra specifications for theories based on stream signatures. Initial algebra semantics usually involve term models. However a full stream algebra \Abars\ based on a sort $s$ is uncountable, even if \As\ is finite! Hence, to construct a term model for a theory over a stream signature, we must work with {\it infinitary terms}, as follows. %Let \,$\Tm = \TmSig$ \,be the usual set of (finite) %\Sig-terms of sort $s$. We can define a set \,$\Tmoms = \TmomsSig$ \,of \om-(\Sig-)terms of sort $s$, for all \Sig-sorts $s$. We do not give a complete definition of \Tmoms, but note the clause: \bull for a {\it stream sort\/} \sbar, if \,$t_0,t_1,t_2,\dots$ \,is any infinite sequence of \om-terms of sort $s$, then \ \ang{t_0,t_1,t_2,\dots} \ is an \om-term of sort \sbar, \ie, a ``stream term". We will write \,$t:s$ \,to signify that $t$ is a term of sort $s$. \sheadrun{2.2}{Finitary and infinitary logics over \Sig} We define four formal systems over \Sig: based on either {\it finitary\/} or {\it infinitary\/} logic, and in either a {\it conditional equational\/} or a ``{\it full\/}" form. \sn \pr{(1) \ \CondEqSig: \ finitary conditional equational logic over \Sig} This can be conveniently formulated in the {\it sequent calculus}, as a subsystem of Takeuti's \LJe\ \cite{tak}. The \Sig-{\it atomic formulae} are {\it equations\/} between terms of the same sort, for all \Sig-sorts (whether equality sorts or not). A {\it conditional equation} is a formula of the form $$ P_1 \con \dots \con P_n \to P \tag"($*$)" $$ where $n \ge 0$ and $P_i$ and $P$ are equations. A {\it conditional equational theory} is a set of such formulae (or their universal closures). An {\it equational sequent} is a sequent of the form $$ P_1, \dots, P_n \seqt P $$ where $n \ge 0$ and $P_i$ and $P$ are equations. This sequent {\it corresponds to} the conditional equation ($*$). The {\it initial sequents\/} are the \Sig-equality axioms, and the {\it inferences\/} are: \nl\indent\qqquad\bu\ \ structural inferences, \nl\indent\qqquad\bu\ \ atomic cuts. This system can be augmented in two ways: \sn ($a$) Adding {\it axioms of a conditional equation theory}, or rather all substitution instances of these, as initial sequents; \sn ($b$) Adding {\it induction\/} for a class \CCC\ of formulae, in the form of the inference rule $$ \CCCInd: \ \ { \Gam \seqt P(0)\qquad P(a), \Pi \seqt P(\Ss a) \over \Gam,\Pi \seqt P(t) } $$ where the induction variable $a$ has sort \nats, and the induction formula $P(a)$ belongs to the class \CCC. (We are assuming here that \Sig\ is standard.) We write \,\IndSig\ \,for full \Sig-induction, \ie, where \CCC\ is the set of all first-order \Sig-formulae. Analogous augmentations can be made for the other systems considered below. \pr{(2) \ \CondEqomSig: \ \omb-conditional equational logic over \Sig} This modifies the above system in the following ways. The atomic formulae are now \om-(\Sig-)equations, \ie, equations between \om-terms of the same sort in \Sig. An \om-{\it conditional equation} is a formula of the form $$ \conconlims{i=0}{\infty}Q_i \ \seqt \ Q \tag"($**$)" $$ where $Q_i$ and $Q$ are \om-equations. An \om-{\it equational sequent} is an (infinite) sequent of the form $$ Q_0,Q_1, \dots, Q_n,\dots \ \seqt \ \ Q $$ where $Q_i$ and $Q$ are \om-equations. This sequent {\it corresponds to} the conditional equation ($**$). The {\it initial sequents\/} are the \om-\Sig-equality axioms, including the axiom $$ t_0 = t_0',\ t_1=t_1',\ t_2=t_2',\ \dots \ \ \seqt \ \ \ang{t_0,t_1,t_2,\dots} = \ang{t_0',t_1',t_2',\dots} $$ and the {\it inferences\/} are: \nl\indent\qqquad\bu \ \ structural inferences, \nl\indent\qqquad\bu \ \ atomic cuts, \nl\indent\qqquad\bu \ \ \om-cuts, \ie, cuts of the form $$ {\Gam\seqt Q_0 \qquad \Gam\seqt Q_1 \qquad \dots \qqquad Q_0,Q_1,\dots,\Del\seqt Q \over \Gam,\Del\seqt Q} $$ \sn \pr{(3) \ \FullSig: \ full finitary (first order) logic with equality over \Sig} This can be formulated in a system \ \LKeSig, \ which is an adaptation to the many-sorted signature \Sig\ of the system \LKe\ of \cite{tak}. The atomic formulae are equations, as in (1). \pr{(4) \ \FullomSig: \ full \omb-logic with equality over \Sig} This resembles the system \Lomiom\ of \cite{karp:book} (\ie, countable conjunctions and disjunctions, plus the usual quantifiers) adapted to the signature \Sig, with the additional feature that the atomic formulae are \om-equations. We omit details, except to point out that the rule of induction can be subsumed under the rule of universal quantification over \nats, which can be given in the form $$ \all L : \ {{R(t),\Gam \seqt \Del} \over {\all z R(z), \Gam \seqt \Del}} \qqquad \all_\om R: \ {{\dots \ \Gam \seqt \Del,F(\bar n) \ \dots \quad (\tx{all} \ n \in \NN)} \over {\Gam \seqt \Del,\all z R(z)}} $$ and similarly (dually) for existential quantification. One reason for the importance of (finite or infinite) conditional equational logic lies in the following \pr{Conservativity Lemmas} \nin (1) \ (\Full\ \,over \,\CondEq). \ Let $E$ be a conditional equational theory over \Sig, \,and let \,\GamP\ \,be a closed \om-equational sequent. If \,\GamP\ \,is provable from $E$ in \,\FullSig, \,then it is provable from $E$ in \,$\CondEqSig$. \nin (2) \ (\Fullom\ \,over \,\CondEqom). \ Let $F$ be an \om-conditional equational theory over \Sig, \,and let \,\GamQ\ \,be a closed equational sequent. If \,\GamQ\ \,is provable from $F$ in \,\FullomSig, \,then it is provable from $F$ in \,\CondEqomSig. \nin (3) \ (\CondEqom\ \,over \,\CondEq). \ Let $E$ be a (finite) conditional equational theory over \Sig, \,and let \,\GamP\ \,be a (finite) equational sequent. If \,\GamP\ \,is provable from $E$ in \,\CondEqomSig, \,then it is provable from $E$ in \,\CondEqSig. \endpr All three lemmas can be proved by cut elimination. %actually (for Lemmas 1 and~2) elimination of all non-atomic cuts, %and (for Lemma 3) elimination of redundant (atomic) cuts. \Remarks (1) \ Note that Conservativity lemmas 1 and 2 also follow from the Mal'cev-type completeness theorems in Sections 3, 4 and 5. \sn (2) \ As a result of Lemma 2, it is often unnecessary to distinguish between \,\FullomSig\ \,and \,\CondEqomSig, in which case we refer to either logic as `\om-(\Sig)-logic'. \Shead3{Initial algebras for conditional equations} In this section (only) we make no assumption about standardness of signatures. Let \Sig\ be a signature and \KK\ a \Sig-\adt. A \Sig-algebra $A$ is {\it pre-initial for} \KK\ if there is a unique \Sig-homomorphism from $A$ to every algebra in \KK. An {\it initial algebra of\/} \KK\ is a pre-initial algebra which belongs to \KK. Any two initial algebras of \KK\ are \Sig-isomorphic. Let \ISigK\ denote any initial algebra of \KK. Of special interest is the case that \ $ \KK = \ModSigT$, \ the class of models of a first-order theory $T$ over \Sig. We write \,$\ISigT \eqdf \ISigModSigT$, \ the {\it initial model} of $T$ (if it exists). Let \,\TmSig\ \,be the {\it closed term algebra\/} (in the finite language) over \Sig. Consider the {\it quotient algebra of\/} \TmSig\ w.r.t. $T$ $$ \TmSigT \ \eqdf \ \TmSig/\eqT $$ where $$ t_1 \,\eqT \,t_2 \ \ \ifff\ \ T \tstile t_1 = t_2 $$ where `$\tstile$' denotes provability in \CondEqSig\ (or, equivalently, in \,\FullSig, \,by Conservativity Lemma 1). \newpage \Prop ($a$) \TmSigT\ is pre-initial for \ModSigT. \smskipn ($b$) If \,$\TmSigT \ttstile T$ \,then \TmSigT\ is an initial model of $T$, \,\ie, $$ \TmSigT \ \isom \ \ISigT. $$ \endpr We say that $A$ has an {\it initial algebra specification} \,\SigT\ \,if \,$A \,\isom\, \ISigT$. \Thmn{1 \ (Mal'cev)} Let $E$ be a {\rm conditional equational} theory over \Sig. Then \ \TmSigE\ \ is an initial model of $E$. \ Further, for two closed \Sig-terms $t_1, t_2$ of the same sort, the following are equivalent: \itemitem{($i$)} $\TmSigE \ttstile t_1 = t_2$; \itemitem{($ii$)} $\ModSigE \ttstile t_1 = t_2$; \itemitem{($iii$)} $E \tstile t_1 = t_2$ \ in \,\CondEqSig; \itemitem{($iv$)} $E \tstile t_1 = t_2$ \ in \,\FullSig. \endpr \Remark Mal'cev's Theorem \cite{malcev}, in the form given above, can be viewed as expressing both \ ($a$) {\it completeness} of \,\CondEqSig, \,given by the implication \ $(ii)\impp(iii)$, \,and \ ($b$) {\it conservativity\/} of \,\FullSig\ \,over \,\CondEqSig, \,given by the implication \ $(iv)\impp(iii)$ (see Remark 1 at the end of Section 2). \endpr \Shead4{Initial standard algebras for conditional equations} We now repeat the theory of Section 3 for {\it standard} algebras. So assume that \Sig\ is standard, and that \KK\ consists of {\it standard} \Sig-algebras; in particular, \KK\ is the set of {\it standard} models of a \Sig-theory $T$, \,\ie, \ $\KK = \StdModSigT$, \ for some \Sig-theory $T$. Then although \,\TmSigT, \,is pre-initial for \KK, it might fail to be initial for \KK\ for two reasons: it might not satisfy $T$, and it might not even be standard! (We return to the latter point below.) An {\it initial standard model of\/} $T$ is an initial algebra of \ \StdModSigT. Any two initial standard models of $T$ are \Sig-isomorphic. We denote any such model by $$ \ISSigT \eqdf \Init(\Sig,\,\StdModSigT). $$ \Propn1 If \,\TmSigT\ \,is a standard \Sig-model of $T$, \,then \TmSigT\ is initial in \StdModSigT. \endpr The question arises: how can we construct (or characterise) {\it initial standard} models of $T$? Let $A$ be a standard \Sig-algebra. We say that $A$ has an {\it initial standard algebra specification} \SigT\ if \ $A \,\cong\, \ISSigT$. Now \TmSigT\ (even if it is a model of $T$) may fail to be {\it standard\/} for two reasons: namely, $T$ proves ``too little" or ``too much", roughly speaking. The first reason is connected with non-standard interpretations of the sorts \nats\ and \bools. Thus, there might be a \Sig-function symbol $f$, but no corresponding axioms in $T$ capable of ``reducing" a closed term of sort \nats\ containing $f$ to a numeral. Similarly not all closed boolean terms (\ie, terms of sort \bools) may be (provably in $T$) equal to \trues\ or \falses. (In the terminology of \cite{guttag-horning}, the specification \SigT\ is not ``sufficiently complete".) The second reason is that $T$ may be {\it inconsistent}, in the sense that it proves `$\trues = \falses$' (or, equivalently in a suitable weak background theory, `$0 = 1$'). This motivates the following. From now on we restrict attention to the case of conditional equational theories. So let $E$ be a conditional equational theory over \Sig. \Defs (1) $E$ {\it determines \nats} [resp\. \bools] if every closed term of sort \nats\ [resp\. \bools] is, provably from $E$, equal to a numeral [resp\. \trues\ or \falses]. \sn (2) $E$ is {\it trivial} if the equation `$\trues = \falses$' is provable from $E$ \endpr Note that ``provability from $E$" in the above definition can refer to either conditional equational logic or \,\FullSig, \,by Conservativity Lemma 1. Let \,\StdAxSig\ \,be the following set of axioms: $$ \gather \cons(\trues,\trues) = \trues, \qquad \cons(\trues,\falses) = \cons(\falses,\trues) = \cons(\falses,\falses) = \falses, \\ \negs(\trues) = \falses, \qquad \negs(\falses) = \trues, \\ \eqN(0,0) = \trues, \qquad \eqN (\Ss z,0) = \eqN(0,\Ss z) = \falses, \\ \eqN(\Ss z_1,\Ss z_2) = \eqN(z_1,z_2), \endgather $$ $$ \gather \lsN(0,\Ss z) = \trues, \qquad \lsN (0,0) = \lsN(\Ss z,0) = \falses, \\ \lsN(\Ss z_1,\Ss z_2) = \lsN(z_1,z_2), \\ \eqs_s(x,x) = \trues, \qquad \eqs_s(x_1,x_2) = \trues \ \to \ x_1 = x_2 \endgather $$ where the last two axioms hold at all {\it equality sorts} $s$. Note that \ $\StdAxSig + \IndSig$ \ holds in any standard \Sig-algebra. Also, the axioms in \StdAxSig\ are all equations, except for the last one, which is a conditional equation. \pr{Standardness Lemma}\sl Let $E$ be a \Sig-conditional equational theory containing \linebreak \StdAxSig. Then \ \TmSigE\ \ is standard iff $E$ determines \,\nats\ \,and \,\bools, \,and is non-trivial. \rm \Propn2 If \Sig\ is strictly standard then \StdAxSig\ determines \,\nats\ \,and \,\bools. \Cor Suppose \Sig\ is strictly standard, and $E$ is a non-trivial \Sig-conditional equational theory containing \StdAxSig. Then \TmSigE\ is standard. \endpr We now give the analogue of Mal'cev's Theorem (Theorem 1 in Section 3) for standard algebras. \newpage \Thmn2 Let $E$ be a conditional equational theory over \Sig. Suppose that the theory \ $E + \StdAxSig$ \ determines \nats\ and \bools\ and is non-trivial. Then \ $A =_{df} \Tm(\Sig,\,E + \StdAxSig)$ \ is an initial standard model of $E$. \ Further, for two closed \Sig-terms $t_1, t_2$ of the same sort, the following are equivalent: \itemitem{($i$)} $A \ttstile t_1 = t_2$; \itemitem{($ii$)} $\StdModSigE \ttstile t_1 = t_2$; \itemitem{($iii$)} $E + \StdAxSig \ \tstile \ t_1 = t_2$ \ in \,\CondEqSig; %\ in conditional equational logic over \Sig; \itemitem{($iv$)} $E+ \StdAxSig \ \tstile \ t_1 = t_2$ \ in \,\FullSig\ $+$ \IndSig. \endpr \Shead5{Initial standard algebras for \omb-conditional equations} We repeat again the theory of Sections 3 and 4 for standard algebras with \om-logic. Let \Sig\ be a stream signature (\cf\ Section 1). Let $T$ be a theory in the language \FullomSig, \,and let \,\TmomSig\ \,be the term algebra built from the closed \om-\Sig-terms \,(\S2.1). Consider the {\it quotient algebra of\/} \TmomSig\ w.r.t. $T$ $$ \TmomSigT \ \eqdf \ \TmomSig/\eqT $$ where $$ t_1 \,\eqT \,t_2 \ \ \ifff\ \ T \tstile t_1 = t_2 $$ and `$\tstile$' denotes provability in \om-logic (\cf\ Remark 2 at the end of Secction 2). Again (as with \TmSig\ in Section 4) \,\TmomSig\ \,may fail to be standard. Note that it {\it is} possible to characterise standard algebras in \,\FullomSig\, by the two formulae $$ \all z \disdislims{n=0}{\infty} (z = \nbar) \qqquad \tx{and} \qqquad \all b \,(b = \trues \,\dis \,b = \falses) $$ (where $z:\nats$ and $b:\bools$), but these are {\it not} \om-conditional equations! We want to concentrate on \om-conditional equational theories, and therefore proceed as in Section 4 with finitary logic. Let $F$ be an \om-\Sig-equational theory. We define the concepts: ``$F$ determines \,\nats\ \,and \,\bools", and ``$F$ is trivial", \,as in Section 4, but now with repect to \om-logic. Also, define \,\StdAxSig\ \,as in Section 4. We give the analogue of Mal'cev's Theorem (\cf\ Theorems 1 and 2) for stream signatures \Sig\ and \om-logic. \newpage \Thmn3 Let $F$ be an \,\om-{\rm conditional equational} theory over \Sig. Suppose that the theory \ $F + \StdAxSig$ \ determines \nats\ and \bools\ and is non-trivial. Then \ $A =_{df} \Tm(\Sig,\,F + \StdAxSig)$ \ is an initial standard model of $F$. \ Further, for two closed \Sig-terms $t_1, t_2$ of the same sort, the following are equivalent: \itemitem{($i$)} $A \ttstile t_1 = t_2$; \itemitem{($ii$)} $\StdModSigF \ttstile t_1 = t_2$; \itemitem{($iii$)} $F + \StdAxSig \tstile \ t_1 = t_2$ \ in \,\CondEqomSig; \itemitem{($iv$)} $F+ \StdAxSig \ \tstile \ t_1 = t_2$ \ in \,\FullomSig. \endpr \Shead6{Definability of the stream algebra operation} \ssheadrun{6.1}{Expanding operations} Assume from now on that \Sigp\ is a standard signature with $\Sig \subset \Sigp$. Also, $A$ is a standard \Sig-algebra and $A'$ is a standard \Sigp-algebra. Also, $T$ is a \Sig-theory (in either the finite or infinitary language over \Sig), and $T'$ is a \Sigp-theory. \Defs (1) Two \Sigp-algebras $A_1'$ and $A_2'$ are {\it \Sigp/\Sig-isomorphic}, written \newline $A_1' \cong_{\Sigp/\Sig} A_2'$, \ if there is a \Sigp-isomorphism from $A_1'$ to $A_2'$ whose restriction to \Sig\ is the identity on $A_1'\redSig$. \nin(2) An operation \ $\Phi : \StdSig \to \Std(\Sig')$ \ is {\it expanding (over \Sig)} \,iff for all standard \Sig-algebras $A$, \,$\Phi(A)$ \,is a \Sigp-expansion of $A$. \Example For any standard signature \Sig, fix \,$s \in\SortSig$ \,and let \Sigbar\ be the extension of \Sig\ formed by adjoining the {\it stream sort} \,\sbar\ \,(associated with $s$), and the operation \,$\evals_s$ \,(which we will write below without the subscript `$s$'). Let \,\Abar\ \,be the \Sigbar-algebra which expands $A$ by adding the carrier $$ \Abar_s \ \eqdf \ [\NN\to\As] $$ consisting of all streams over \As, together with the function \ $\evals_s^A: \Abar_s \times \NN \to \As$. Then the {\it stream algebra construction\/} $$ \AtoAbar $$ \,is an expanding operation. (Note that we are working with a single pre-stream sort $s$ for simplicity. We could just as easily take a {\it set\/} \Sbi\ of pre-stream sorts, as in the example in Section 1.) \endpr Assume from now on that \,$\Phi : \StdSig \to \Std(\Sig')$ \, is an expanding operation over \Sig. We will write \APhi\ for $\Phi(A)$, and \KKPhi\ for \ $\{ \APhi \mid A \in \KK \}$ \ (or rather, its closure w.r.t. \Sigp-isomorphism). \newpage \sheadrun{6.2}{Definability of operations by theories} \Defs (1) Suppose $A'$ is a \Sigp-expansion of $A$. We say that $T'$ {\it defines $A'$ over $A$} iff $A'$ is the unique (up to \Sigp/\Sig-isomorphism) standard \Sigp-expansion of $A$ satisfying $T'$; \ in other words: \ ($i$) $A' \ttstile T'$; \ and \ ($ii$) for all standard \Sigp-expansions $B'$ of $A$, \ if \,$B' \ttstile T'$ \, then \,$B' \cong_{\Sigp/\Sig} A'$. \sn (2) $T'$ {\it defines \Ph\ uniformly over} \Sig\ \,iff for all \,\AinStdSig, \,$T'$ defines \APhi\ over $A$. \Propn1 Suppose $T'$ defines \Ph\ uniformly over \Sig. Then \nin ($i$) \ \ \ $A \ttstile T \ \ \llongtofrom \ \ \APhi \ttstile T + T'$; \nin ($ii$) \ If \ $\KK = \StdMod(\Sig, T)$, \,then \ $\KKPhi = \StdMod(\Sig', \,T + T')$. \endpr \Defs (3) \Ph\ has the {\it homomorphism extension property (HEP) (w.r.t\. \Sig\ and \Sigp)} iff every homomorphism \ $h: A \to B$ \ between standard \Sig-algebras can be {\it extended uniquely} to a homomorphism \ $h^\Phi : \APhi \to B^\Phi$ \ between their images under \Ph. \nin (4) \Ph\ is {\it initiality preserving\/} ({\it w.r.t\. \Sig\ and \Sigp}) iff for all \,$\KK \subseteq \StdSig$ \,and \,$A \in \StdSig$: \sn \ce{$A$ is initial in \KK\ \ \ \ifff \ \ \APhi\ is initial in \KKPhi.} \endpr \Propn2 If \Ph\ has HEP, then \Ph\ is initiality preserving. \endpr \Remark The stream algebra construction \,$A \mapsto \Abar$ \,has HEP, and (hence) is initiality preserving. \endpr \Propn3 Suppose \Ph\ is initiality preserving. If the \Sigp-theory $T'$ defines \Ph\ uniformly over \Sig, then for any \Sig-theory $T$ and standard \Sig-algebra $A$, $$ A \,\isom \,\ISSigT \ \ \ \llongtofrom \ \ \APhi \,\isom \,\IS(\Sigp, \ T + T'). $$ \endpr \sheadrun{6.3}{Stream axioms} We are looking for a theory to define the stream operation \,\AtoAbar. Note that we could define this operation in \,\FullomSig\ \,by the scheme $$ \ex \al \conconlims{n=0}{\infty} \big(\evals(\al,\nbar)= t_n\big) $$ for all sequences \,$(t_0,t_1,\dots)$ \,of closed terms of sort $s$, \,together with the single axiom $$ \all \al,\all \be \big[\all z\big(\evals(\al,z) = \evals(\be,z)\big)\ \longimp \ \al = \be\big] $$ \nin (where \,$\al, \be:\sbar$ \,and \,$z:\nats$), and in this way, avoid infinite terms! However neither of these is an (\om-)conditional equation. So we proceed instead as follows. Let \,\StrAxSigs\ \,be the following ``stream axioms": \TOL $$ \evals(\ang{t_0,t_1,t_2,\dots},\ \nbar) \ = \ t_n \tag1 $$ for all sequences \,$(t_0,t_1,t_2,\dots)$ \,of \Sig-terms of sort $s$ and all $n$, \,and \goodbreak $$ \conconlims{n=0}{\infty}(t_n=t_n') \ \longimp \ \ang{t_0,t_1,\dots} \,= \,\ang{t_0',t_1',\dots} \tag2 $$ for all sequences \,$(t_0,t_1,\dots)$ \,and \,$(t_0',t_1',\dots)$ \,of \Sig-terms of sort $s$. Note that (2) is an \om-conditional equation, and so \,\StrAxSigs\ \,is an \om-conditional equational theory. We first present a kind of normal form lemma for stream terms. A closed \om-\Sig-term $t$ is called {\it simple} if neither $t$ nor any subterm of $t$ is of sort \sbar\ (and it is therefore a finitary \Sig-term). \Lemman{ \ (Normal forms for stream terms)} Suppose $E$ is an \om-conditional equational theory, and \,$E + \StdAxSig$ \,determines \,\nats\ \,and \,\bools. %(e.g. if \Sig\ is strictly standard; \,\cf\ Proposition 2 of Section 4). Then \itemitem{($i$)} if $t$ is a closed term not of sort \sbar, then $$ E+\StdAxSig + \StrAxSigs\ \tstile \ t = \that $$ for some {\rm simple\/} term \that. \itemitem{($ii$)} if $t$ is a closed term of sort \sbar, then $$ E+\StdAxSig + \StrAxSigs\ \tstile \ t = \ang{t_0, t_1,t_2,\dots} $$ for some {\rm simple} terms \,$t_0, t_1, t_2,\dots$ \,of sort $s$. \endpr \Thmn4 The theory \,\StrAxSigs\ \,defines the stream algebra construction \ \AtoAbar\ \ uniformly over \StdSig. \endpr \nin From Proposition 3 and the Remark that precedes it: \Corn1 For any standard \Sig-algebra $A$ and theory $T$ (in \FullomSig): $$ A \,\isom \,\ISSigT \ \ \ \llongtofrom \ \ \ \Abar \,\isom \,\IS(\Sigbar, \ T + \StrAxSigs). $$ \endpr \nin By considering the special case that $T$ is an \om-conditional equational theory, we obtain \Corn2 If a \Sig-algebra $A$ has an initial standard algebra specification by a set of \om-conditional equations, then so does the stream algebra \,\Abar. \endpr \nin In particular, taking for $A$ the term model of a conditional equational theory, we have from Theorem 3: \Corn3 Let $E$ be a conditional equational theory over \Sig. Suppose that the theory \ $E + \StdAxSig$ \ determines \nats\ and \bools\ and is non-trivial. Then \ $A =_{df} \Tm(\Sig,\ E + \StdAxSig)$ \ is an initial standard model of $E$, and furthermore the stream algebra \Abar\ constructed from $A$ is (\Sigp/\Sig-isomorphic to) the \om-term model: $$ \Abar \ \isom\ \Tmom(\Sigbar, \ \Ebar) $$ and is also the initial standard model of the \om-conditional equational theory \Ebar, where $$ \Ebar \ \eqdf \ E + \StdAxSig + \StrAxSigs. $$