Our earlier work on abstract data types is extended by the answers to a number of questions on the power and limitations of algebraic specification techniques and by an algebraic treatment of parameterized data types like sets-of-( ) and stacks-of-().The "hidden function" problem (the need to include operations in specifications which are wanted hidden from the user) is investigated; the relative power of conditional specifications and equational specifications is investigated; and it is shown that parameterized specifications must contain "side conditions" (e.g., that finite-sets-of-d requires an equality predicate on d).

We study the solutions to a (vector) equation somewhat analogous to the traditional equations of linear algebra. Whereas, in introductory linear algebra the domain of discourse is the field of real numbers (or an arbitrary field) our domain of discourse is the algebraic theory of (multi-rooted, leaf-labeled) trees (or, more generally, any iterative theory). As in linear algebra, we obtain a necessary and sufficient condition for our equations to have unique solutions and we can describe “parametrically” the totality of solutions. However, whereas in linear algebra, there is no way of giving $1 \div 0$ meaning in such a way that all the “old laws” hold, we can give meaning to the “iteration operation” (the analogue of division into 1) in such a way that all the “old laws” still hold. Indeed, we can describe “parametrically” all such ways of extending the (partially defined) scalar iteration operation to all trees (more generally, morphisms).

This paper is a sequel to a previous paper (S. L. Bloom, C. C. Elgot and J. B. Wright, Solutions of the iteration equation and extensions of the scalar iteration operations, SIAM J. Comput., 9 (1980), pp. 25–45. In that paper it was proved that for each morphism $ \bot :1 \to 0$ in an iterative theory J there is exactly one extension of the scalar iteration operation in J to all scalar morphisms such that $I_1^\dag = \bot $ and all scalar iterative identities remain valid. In this paper the scalar iteration operation in the pointed iterative theory $(J, \bot )$ is extended to vector morphisms while preserving all the old identities. The main result shows that the vector iterate $g^\dag $ in $(J, \bot )$ satisfies the equation $g^\dag = (g_ \bot )^\dag $, where $g_ \bot $ is a nonsingular morphism simply related to g (so that $(g_ \bot )^\dag $ is the unique solution of the iteration equation for $g_ \bot $). In the case that $J = \Gamma {\text{Tr}}$, the iterative theory of $\Gamma $-trees, it is shown that the vector iterate $g^\dag $ in $(J, \bot )$ is a metric limit of “modified powers” of g.

This paper extends our earlier work on abstract data types by providing an algebraic treatment of parametrized data types (e.g., sets-of-(), stacks-of-(), etc.), as well as answering a number of questions on the power and limitations of algebraic specification techniques. In brief: we investigate the “hidden function” problem (the need to include operations in specifications which we want to be hidden from the user); we prove that conditional specifications are inherently more powerful than equational specifications; we show that parameterized specifications must contain “side conditions” (e.g., that finite-sets-of-d requires an equality predicate on d), and we compare the power of the algebraic approach taken here with the more categorical approach of Lehman and Smyth.

Many apparently divergent approaches to specifying formal semantics of programming languages are applications of initial algebra semantics. In this paper an overview of initial algebra semantics is provided. The major technical feature is an initial continuous algebra which permits unified algebraic treatment of iterative and recursive semantic features in the same framework as more basic operations.

In a wide variety of situations, computer science has found it convenient to define complex object as (fixed-point) solutions of certain equations. This has been done in both algebraic and order-theoretic settings, and has often been contrasted with other approaches. This paper shows how to formulate such solutions in a setting which encompasses both algebraic and order-theoretic aspects, so that the advantages of both worlds are available. Moreover, we try to show how this is consistent with other approaches to defining complex objects, through a number of applications, including: languages defined by context-free grammars; flow charts and their interpretations; and monadic recursive program schemes. The main mathematical results concern free rational theories and quotients of rational theories. However, the main goal has been to open up what we believe to be a beautiful and powerful new approach to the syntax and semantics of complex recursive specifications.

Abstract Let N, O and S denote the set of nonnegative integers, the graph of the constant 0 function and the graph of the successor function respectively. For sets P, Q, R ⊆ N 2 operations of transposition, composition, and bracketing are defined as follows: P ∪ = {〈 x, y 〉 ∣ 〈 y, x 〉 ∈ P }, PQ = {〈 x, z 〉 ∣ ∃ y 〈 x, y 〉 ∈ P & 〈 y, z 〉 ∈ Q }, and [ P, Q, R ] = ⋃ n ∈ M ( P n Q R n ). Theorem. The class of recursively enumerable subsets of N 2 is the smallest class of sets with O and S as members and closed under transposition, composition, and bracketing . This result is derived from a characterization by Julia Robinson of the class of general recursive functions of one variable in terms of function composition and “definition by general recursion.” A key step in the proof is to show that if a function F is defined by general recursion from functions A, M, P and R then F = [ P ∪ , A ∪ M, R] . The above definitions of the transposition, composition, and bracketing operations on subsets of N 2 can be generalized to subsets of X 2 for an arbitrary set X. In this abstract setting it is possible to show that the bracket operation can be defined in terms of K, L, transposition, composition, intersection, and reflexive transitive closure where K: X → X and L: X → X are functions for decoding pairs.

article Free AccessRealization of Events by Logical Nets Authors: Irving M. Copi University of Michigan, Ann Arbor, Mich. University of Michigan, Ann Arbor, Mich.View Profile , Calvin C. Elgot University of Michigan, Ann Arbor, Mich. University of Michigan, Ann Arbor, Mich.View Profile , Jesse B. Wright University of Michigan, Ann Arbor, Mich. University of Michigan, Ann Arbor, Mich.View Profile Authors Info & Claims Journal of the ACMVolume 5Issue 2April 1958 pp 181–196https://doi.org/10.1145/320924.320931Published:01 April 1958Publication History 75citation572DownloadsMetricsTotal Citations75Total Downloads572Last 12 Months39Last 6 weeks9 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF