HYPERSUBSTITUTIONS OF MANY-SORTED ALGEBRAS

2008 ◽  
Vol 01 (03) ◽  
pp. 337-346 ◽  
Author(s):  
Klaus Denecke ◽  
Somsak Lekkoksung
Keyword(s):  
Computer Science ◽  
Binary Operation ◽  
Data Type ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
The Many ◽  
The One

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.

On lists and other abstract data types in the calculus of constructions

2000 ◽  
Vol 10 (2) ◽  
pp. 261-276 ◽  
Author(s):  
JONATHAN P. SELDIN
Keyword(s):  
Data Type ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Natural Numbers ◽  
Data Types ◽  
Induction Principle ◽  
Calculus Of Constructions ◽  
Abstract Data ◽  
Definition Of ◽  
Future Work

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.

scholarly journals Adding Alternative Access Paths to Abstract Data Types

2002 ◽  
pp. 256-267 ◽  
Author(s):  
Xavier Franch ◽  
Jordi Marco
Keyword(s):  
Information Hiding ◽  
Data Type ◽  
Modular Structure ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Programming Framework ◽  
Algebraic Specifications ◽  
Abstract Data ◽  
Adequate Representation

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.

scholarly journals Tree-Shaped Formats of Address Programming Language

2021 ◽  
Vol 4 ◽  
pp. 78-87
Author(s):  
Yury Yuschenko
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Theoretical Research ◽  
Direct Access ◽  
Complex Data ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
The One ◽  
High Level

In the Address Programming Language (1955), the concept of indirect addressing of higher ranks (Pointers) was introduced, which allows the arbitrary connection of the computer’s RAM cells. This connection is based on standard sequences of the cell addresses in RAM and addressing sequences, which is determined by the programmer with indirect addressing. Two types of sequences allow programmers to determine an arbitrary connection of RAM cells with the arbitrary content: data, addresses, subroutines, program labels, etc. Therefore, the formed connections of cells can relate to each other. The result of connecting cells with the arbitrary content and any structure is called tree-shaped formats. Tree-shaped formats allow programmers to combine data into complex data structures that are like abstract data types. For tree-shaped formats, the concept of “review scheme” is defined, which is like the concept of “bypassing” trees. Programmers can define multiple overview diagrams for the one tree-shaped format. Programmers can create tree-shaped formats over the connected cells to define the desired overview schemes for these connected cells. The work gives a modern interpretation of the concept of tree-shaped formats in Address Programming. Tree-shaped formats are based on “stroke-operation” (pointer dereference), which was hardware implemented in the command system of computer “Kyiv”. Group operations of modernization of computer “Kyiv” addresses accelerate the processing of tree-shaped formats and are designed as organized cycles, like those in high-level imperative programming languages. The commands of computer “Kyiv”, due to operations with indirect addressing, have more capabilities than the first high-level programming language – Plankalkül. Machine commands of the computer “Kyiv” allow direct access to the i-th element of the “list” by its serial number in the same way as such access is obtained to the i-th element of the array by its index. Given examples of singly linked lists show the features of tree-shaped formats and their differences from abstract data types. The article opens a new branch of theoretical research, the purpose of which is to analyze the expe- diency of partial inclusion of Address Programming in modern programming languages.

THE C++ EMBEDDABLE RULE SYSTEM

1993 ◽  
Vol 02 (01) ◽  
pp. 33-46 ◽  
Author(s):  
DANIEL P. MIRANKER ◽  
FREDERIC H. BURKE ◽  
JERI J. STEELE ◽  
JOHN KOLTS ◽  
DAVID R. HAUG
Keyword(s):  
Data Type ◽  
Third Party ◽  
Abstract Data Type ◽  
Data Types ◽  
Forward Chaining ◽  
Abstract Data ◽  
Data Objects ◽  
Rule System

Most the execution environments, having been derived from LISP, inference on internally defined data-types and come packaged with stand-alone development environments. Data derived from outside these systems must be reformatted before it can be evaluated. This mismatch leads to a duplicate representation of data, which, in turn, introduces both performance and semantic problems. This paper describes a C++ Embeddable Rule System (CERS) which avoids this mismatch. CERS is a compiled, forward-chaining rule system that inferences directly on arbitrary C++ objects. CERS can be viewed as an extension of C++, where the methods associated with a ruleset class can be defined either procedurally or declaratively. CERS is unique in that rules may match against and manipulate arbitrary, user-defined C++ objects. There is no requirement that the developer anticipated using CERS when defining the class. Thus CERS rules can inference over data objects instantiated in persistent object stores and third-party. C++ abstract data-type libraries.

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
Keyword(s):  
Model Theory ◽  
Point Of View ◽  
Necessary Condition ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Definition Of ◽  
Recursive Data ◽  
Better Than

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.

Algebraic specification of abstract data types

2001 ◽  
Author(s):  
J. Loeckx ◽  
H.-D. Ehrich
Keyword(s):  
Programming Languages ◽  
Data Structures ◽  
Complex Structure ◽  
Abstract Data Type ◽  
Specification Languages ◽  
Abstract Data Types ◽  
Data Types ◽  
Control Structures ◽  
Abstract Data ◽  
Number Of Publications

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].

scholarly journals A Constructive Approach to Compiler Correctness

1980 ◽  
Vol 9 (118) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Target Language ◽  
Constructive Approach ◽  
Abstract Data Types ◽  
Machine Code ◽  
Data Types ◽  
Denotational Semantic ◽  
Abstract Data ◽  
The One ◽  
Semantic Definition

<br /> It is suggested that denotational semantic definitions of programming languages should be based on a small number of abstract data types, each embodying a fundamental concept of computation. Once these fundamental abstract data types have been implemented in a particular target language (e.g. stack-machine code), it is a simple matter to construct a correct compiler for any source language from its denotational semantic definition. The approach is illustrated by constructing a compiler similar to the one which was proved correct by Thatcher, Wagner <em>Et</em> Wright ( 1979). Some familiarity with many-sorted algebras is presumed.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

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.

Sign in / Sign up

Export Citation Format

Share Document