On the Power of Model Theory in Specifying Abstract Data Types and in Capturing Their Recursiveness

1983 ◽  
Vol 6 (2) ◽  
pp. 127-170
Author(s):  
Alberto Bertoni ◽  
Giancarlo Mauri ◽  
Pierangelo Miglioli

In this paper a comparative analysis of some algebraic and model-theoretic tools to specify abstract data types is presented: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze various notions such as “initiality”, “finality”, “monoinitiality”, “epifinality”, “weak monoinitiality” and “weak epifinality”, both from the point of view of “abstractness” and of “cardinality”, in a general model theoretical frame. For the second aspect, it is shown that only “initiality”, “monoinitiality”, “epifinality” and “weak epifinality” allow us to select countable models (for theories with a countable language), a necessary condition to get recursive data types, while this is not the case for “finality” and “weak monoinitiality”. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the “abstractness” requirement. We also show that none of the above quoted categorial notions captures recursiveness. Finally, we consider our own definition of “abstract data type”, based on typically model-theoretic notions, and illustrate the sense according to which it captures recursiveness.

2000 ◽  
Vol 10 (2) ◽  
pp. 261-276 ◽  
Author(s):  
JONATHAN P. SELDIN

The representation of the inductively defined abstract data type for lists was left incomplete in Seldin (1997, Section 9). Here that representation is completed, and it is proved that all extra axioms needed are consistent. Among the innovations of this paper is a definition of cdr, whose definition was left for future work in Seldin (1997, Section 9). The results are then extended to other abstract data types – those of Berardi (1993). The method used to define cdr for lists is extended to obtain the definition of an inverse for each argument of each constructor of an abstract data type. These inverses are used to prove the injective property for the constructors. Also, Dedekind's method of defining the natural numbers is used to define a predicate associated with each abstract data type, and the use of this predicate makes it unnecessary to postulate the induction principle. The only axioms left to be proved are those asserting the disjointness of the co-domains of different constructors, and it is shown that those axioms can be proved consistent.


Author(s):  
Xavier Franch ◽  
Jordi Marco

We present in this paper a proposal for developing efficient programs in the abstract data type (ADT) programming framework, keeping the modular structure of programs and without violating the information hiding principle. The proposal focuses in the concept of “shortcut” as an efficient way of accessing to data, alternative to the access by means of the primitive operations of the ADT. We develop our approach in a particular ADT, a store of items. We define shortcuts in a formal manner, using algebraic specifications interpreted with initial semantics, and so the result has a well-defined meaning and fits in the ADT framework. Efficiency is assured with an adequate representation of the type, which provides O(1) access to items in the store without penalising the primitive operations of the ADT.


Author(s):  
J. Loeckx ◽  
H.-D. Ehrich

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as VDM [Woodman and Heal, 1993; Andrews and Ince, 1991], Raise [Raise Development Group, 1995], Z [Spivey, 1989] and B [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as Ada [Barstow, 1983] and ML [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. Formalization leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich et al., 1989; Sannella and Tarlecki, 2001].


2008 ◽  
Vol 01 (03) ◽  
pp. 337-346 ◽  
Author(s):  
Klaus Denecke ◽  
Somsak Lekkoksung

Many-sorted algebras are used in Computer Science for abstract data type specifications. It is widely believed that many-sorted algebras are the appropriate mathematical tools to explain what abstract data types are ([1]). In this paper we want to extend the concept of a hypersubstitution from the one-sorted to the many-sorted case. Hypersubstitutions are used for one-sorted algebras to define hyperidentities and M-solid varieties ([2]). We will prove that extensions of hypersubstitutions for many-sorted algebras are endomorphisms of the many-sorted clone of a given type. As in the one-sorted case we define a binary operation for hypersubstitutions and prove that with respect to this operation all many-sorted hypersubstitutions form a monoid.


1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.


1987 ◽  
Vol 22 (4) ◽  
pp. 103-110 ◽  
Author(s):  
J D Eckart

2007 ◽  
Vol 17 (3) ◽  
pp. 183-203 ◽  
Author(s):  
Borislav Nikolik ◽  
Dick Hamlet

Sign in / Sign up

Export Citation Format

Share Document