×

zbMATH — the first resource for mathematics

Implementation of data types by algebraic methods. (English) Zbl 0537.68026
This paper presents a precise definition of implementation of data types, which are taken to be many-sorted algebras of a given signature (sorts and operations). No particular presentation (e.g. equational) of the data types is assumed but each element of the type is required to be reachable from the given operations. For each operation \(w_ B\) of the \(\Omega\)- algebra B to be implemented, this notion of implementation calls for the construction of an operation \(f_ w\) on the implementing algebra A and the explicit definition of an \(\Omega\)-homomorphism T from F(A) (the \(\Omega\)-subalgebra of A generated by the simulators \(f_ w)\) onto B. The surjectivity of T insures that every element of B can be represented by elements of A. This representation can be multiple as T is not required to be an isomorphism and this implies, in the case of equational presentation of the algebras A and B, that F(A) need not satisfy the axioms defining B. Unlike other approaches, the operations of the two algebras A and B are kept separate and only the operations of A are allowed in the generalized Gödel-Herbrand-Kleene schemes used to define the simulators. Sufficient conditions are given for such a scheme to define a (possibly partial) function using substitution and replacements rules. The notions are illustrated with two examples of implementations of stacks and symbol-tables, dealing with the cases of polynomial and recursively-defined simulators, respectively. Similarities with the approach by H. Ehrig, H.-J. Kreowski and P. Padawitz are analyzed and comparisons with other approaches are mentioned.

MSC:
68P05 Data structures
68N01 General topics in the theory of software
08A99 Algebraic structures
03C05 Equational classes, universal algebra in model theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Guttag, J.V.; Horning, J.J., The algebraic specification of abstract data types, Acta inform., 10, 27-52, (1978) · Zbl 0369.68010
[2] Guttag, J.V.; Horowitz, E.; Musser, D., Abstract data types and software validation, Comm. ACM, 21, 1048-1064, (1978) · Zbl 0387.68012
[3] Zilles, S., An introduction to data algebras, (), 248-272
[4] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Initial algebra semantics and continuous algebras, J. assoc. comput. Mach., 24, 68-95, (1977) · Zbl 0359.68018
[5] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., Abstract data types as initial algebras and the correctness of data representation, (), 80-149
[6] Blum, E.K.; Lynch, N., Relative complexity of algebras, Math. systems theory, 14, 193-214, (1981) · Zbl 0473.68031
[7] Blum, E.K.; Estes, D.R., A generalization of the homomorphism concept, Algebra universalis, 7, 143-161, (1977) · Zbl 0386.08003
[8] Blum, E.K., Machines, algebras and axioms, (), 1-29
[9] Majster, M., Limits on the algebraic specification of abstract data types, SIGPLAN notices,, Vol. 12, 37-42, (1977)
[10] Bergstra, J.A.; Tucker, J., On the adequacy of finite equational methods for data types specification, SIGPLAN notices, Vol. 14, 13-18, (1979)
[11] Enrich, H.D., Extensions and implementations of abstract data type specifications, (), 155-163
[12] Enrich, H.D., On the theory of specification, implementation and parametrization of abstract data types, J. assoc. comput. Mach., 29, 1, 206-227, (1982) · Zbl 0478.68020
[13] Ehrig, H.; Kreowski, H.-J.; Padawitz, P., Stepwise specification and implementation of abstract data types, (), 205-226
[14] Ehrig, H.; Mahr, B., Complexity of algebraic implementations for abstract data types, J. comput. system sci., 23, (1981) · Zbl 0474.68021
[15] Blum, E.K., Towards a theory of semantics and compilers for programming languages, J. comput. system sci., 3, 248-275, (1969) · Zbl 0174.28903
[16] Gratzer, G., Universal algebra, (1968), Von Nostrand Princeton, N.J · Zbl 0182.34201
[17] Cohn, P.M., Universal algebra, (1965), Harper & Row New York · Zbl 0141.01002
[18] Parisi-Presicce, F., On the faithful regular extensions of iterative algebras, () · Zbl 0884.68084
[19] Courcelle, B.; Nivat, M., The algebraic semantics of recursive program schemes, (), 16-30 · Zbl 0384.68016
[20] Ganzinger, H., Parameterized specifications: parameter passing and optimizing implementation, Tech. U. Munich-18110, (August 1981)
[21] Ehrig, H.; Kreowski, H.-J.; Padawitz, P., Algebraic implementation of abstract data types: concept, syntax, semantics, and correctness, (), 142-156 · Zbl 0412.68018
[22] Theoret. Comput. Sci., in press.
[23] Ehrig, H.; Kreowski, H.-J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Parameter passing in algebraic spcification languages, (), 157-168
[24] Hupbach, U.L., Abstract implementation of abstract data types, (), 291-304 · Zbl 0499.68011
[25] Elgot, C.C., Monadic computation and iterative algebraic theories, (), 175-230 · Zbl 0327.02040
[26] Tiuryn, J.; Tiuryn, J., Fixed-points and algebras with infinitely long expressions. II. regular algebras, Fund. inform., Fund. inform., 2, 317-335, (1979) · Zbl 0436.68015
[27] Tiuryn, J., Unique fixed points vs least fixed points, Theoret. comput. sci., 12, 3, 229-254, (1980) · Zbl 0439.68026
[28] Gallier, J.H., Recursion-closed algebraic theories, J. comput. system sci., 23, 69-105, (1981) · Zbl 0472.68006
[29] Garland, S.G.; Luckham, D.C., Program schemes, recursion schemes and formal languages, J. comput. system sci., 7, 119-160, (1973) · Zbl 0277.68010
[30] Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Programming languages as mathematical objects, () · Zbl 0394.68008
[31] Courcelle, B.; Guessarian, I., On some classes of interpretations, J. comput. system sci., 17, 388-413, (1978) · Zbl 0392.68009
[32] Scott, D.; Strachey, C., Towards a mathematical semantics for computer languages, () · Zbl 0268.68004
[33] Kfoury, D., Comparing algebraic structures up to algorithmic equivalence, (), 253-263 · Zbl 0281.68007
[34] Englefriet, J.; Schmidt, E.; Englefriet, J.; Schmidt, E., IO and IO. I. II, J. comput. system sci., J. comput. system sci., 16, (1978)
[35] Mailbaum, T.S.E., A generalized approach to formal languages, J. comput. system sci., 8, 409-439, (1974) · Zbl 0361.68113
[36] Bloom, S.L.; Elgot, C.C., The existence and construction of free iterative theories, J. comput. system sci., 12, 305-318, (1976) · Zbl 0333.68017
[37] Ginalt, S., Regular trees and the free iterative theory, J. comput. system sci., 18, 228-242, (1979)
[38] Guessarian, I., Algebraic semantics, () · Zbl 0602.68017
[39] Manna, Z.; Ness, S.; Vullemin, J., Inductive methods for proving properties of programs, Comm. ACM, 16, 8, (1973)
[40] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., An introduction to categories, algebraic theories and algebras, IBM, RC 5369, (1975)
[41] Kleene, S.C.; Kleene, S.C., Introduction to metamathematics, (), 347 ff · Zbl 0047.00703
[42] Rogers, H., Theory of recursive functions and effective computability, (), 194
[43] Thatcher, J.W., Characterizing derivation trees of context-free grammars through a generalization of finite automata theory, J. comput. system sci., 1, 317-322, (1967) · Zbl 0155.01802
[44] Levy, M.R.; Mailbaum, T.S.E., Continuous data types, SIAM J. comput., 11, 2, 201-216, (1982) · Zbl 0479.68016
[45] Sannella, D.; Wirsing, M., Implementation of parametrized specifications, ()
[46] {\scM. Broy, B. Moller, P. Pepper, and M. Wirsing}, A model-independent approach to implementation of abstract data types, in “Proceedings, Symp. on Algorithmic Logic and the Programming Language LOGLAN, Poznam, Poland”, Lecture Notes in Computer Science, to appear.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.