Implementation of data types by algebraic methods (Q792753)

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.