In [18] a ML-program for computations in category theory, including an implementation of the semantics of specification-building operations for the language CLEAR [6] is presented. We propose a similar approach but use object oriented methods to achieve better abstractness, reusability and efficiency. We prove correctness and the worst case time bounds of the basic algorithm computing colimits on set diagrams. We show how the comma category representations of signatures, specifications and attributed graphs suggests colimit algorithms on the corresponding diagrams.
The paper introduces a notion of a context institution. The notion is explicitly illustrated by two standard examples. Morphism between context institutions are introduced, thus yielding a category of context institutions. Some expected constructions on context institutions are presented as functors from this category. The potential usefulness of these notions is illustrated by one such a construction, yielding a Hoare logic for an arbitrary small context institution satisfying mild extra assumptions.
In this paper we propose a semantic framework for dealing with class- sort polymorphism as presented in the last version of GLIDER. This kind of polymorphism is quite more powerful than the standard sort polymorphism that can be found in a number of functional languages (e.g. Standard ML, Miranda, etc.).In particular, polymorphic or generic types are considered to be parameterized by specifications (i.e. sorts, operations and even axioms) and not just by sorts. The semantic framework defined is based on the idea that the type structure underlying a certain specification should be a category. In particular, this category has, as objects, the given specifications including all the implicit instances of the generic types and the derived subclass relationships. Then, the semantics of a GLIDER specification is a category having the “same structure” as the underlying category of types.
Initial structures are appropriate for modelling constructor-based data types because they fit the intuition and admit inductive theorem proving. In practice, the latter requires a distinction between constructors and defined functions and an axiomatization that complies with the constructor discipline. This badly suits non- free or permutative types such as sets, bags and maps and is yet less reasonable when infinite structures like streams or processes come into play. Instead, non-free as well as infinite structures should be regarded as dynamic objects and identified through observable reactions (observers, inquiries, attributes) upon received messages (transitions, actions, methods) rather than by constructors they are built of. The intended model is based on an extensional, contextual, behavioural, observational or bisimilarity relation and given by the final object in a category of conservative structures. This enforces a hierarchical approach because the nature of attributes is to map higher-level to lower-level objects. Data types with both constructor and action sorts are split into swinging chains of specifications each of which extends its predecessor by either a constructor type or an action type. Constructor types are characterized by visible domains, inductively defined total functions, structural equality and safety conditions expressed as Horn clauses. Action types are given by hidden, but — via predecessors in the chain of specifications — observable domains, partial functions and coinductively defined behavioural equality and liveness conditions. The canonical model of a swinging specification is a chain of initial and final models. For proof-theoretical purposes action types are transformed into their Horn clause completions whereby the semantics of the whole specification reduces to a chain of initial models captured by uniform proof rules and induction principles.
Unification of theories is the long-standing goal of the natural sciences; and modern physics offers a spectacular paradigm of its achievement. The structure of modern mathematics has also been determined by its great unifying theories - topology, algebra and the like. The same ideals and goals are shared by researchers and students of theoretical computing science.
Existing models for I/O in side-effect free languages focus on functional languages, which are usually based on a largely deterministic reduction strategy, allowing for a strict sequentialization of I/O operations. In concurrent logic programming languages a model is used which allows for don't care non-determinism. We apply this model to equational languages, which are closely related to functional languages, but exhibit don't care non-determinism. The semantics are formulated as constrained narrowing, a relation that contains the rewrite relation, and is contained in the narrowing relation.We present constrained narrowing and some of its properties; a constructive method to transform conventional term rewriting systems (TRSs) to constrained narrowing systems (CNSs); and a discussion on requirements for an implementation.
We describe a method to improve the efficiency of normalization procedures for term rewriting systems. This improvement does not restrict the semantics of the term rewriting specification in any respect. In particular, the expressive power of term rewriting systems as a programming language for generic programs and as a theorem prover has been preserved. Our method is based on the following observation. Many rewrite specifications are instances of theories for which efficient data structures exist. In that case we can exploit the canonical representation of objects of such a data structure by translating terms to corresponding objects, and retranslating these objects to terms (in normal form). We will call an implementation of a data structure that allows for this kind of transformations for all (not necessarily ground) terms an evaluation domain. This is then extended to the case where only part of a rewrite specification can directly be transformed using an evaluation domain. We develop the semantical requirements for such evaluation domains and discuss how evaluation domains can support the normalization process. We propose language extensions necessary for term rewriting software to take advantage of evaluation domains. Many experiments with an implementation based on the ReDuX term rewriting laboratory emphasize the efficiency of our approach.
The proofs are restricted to natural deduction proofs and the programs to functional programs (terms of )~-calculus) written with recursion operators which guarantee termination. The analogy is more than mere resemblance: it can be shown to be an isomorphism by considering proof normalisation and program evaluation. A consequence of the analogy is to merge the notions of recursion and induction. The languages originally adopted by the TYPES community, namely MartinL5f type theory and Calculus of Constructions, provided rather Weak facilities for recursion and induction. They allowed special rules for each data type or secondorder definitions of data types. So the three groups concerned, at Chalmers University GSteborg, INRIA Rocquencourt/Lyon and Edinburgh University added a general feature to define
We investigate functorial relationships between the categories of theories in different institutions, namely adjunctions, as a means of translating between the different specification spaces that they provide. We show that there is a canonical way in which adjunctions between the categories of signatures can be lifted to the categories of theories. This lifting is associated with a duality between the concepts of institution map and institution morphism. Finally, we make an attempt at generalising these results to institution semi-morphisms that can be presented by an inference system.
The Larch Shared Language for the specification of abstract data types has evolved over a number of years from a simple algebraic language to one that is both more complicated and more useful. This talk reviews some of its major design decisions and then discusses some of the design issues and remaining open problems—most of which are consequences of the same decisions that contribute to LSL's good properties.
This paper presents an object-oriented functional programming language core, its ML-style static type inference and a corresponding type reconstruction algorithm. The language allows object definitions as in Eiffel, algebraic value definitions as in Haskell and most code reuses in Eiffel and Haskell. The type inference combines the usual structural subtyping relation and Haskell type classes. The type reconstruction algorithm computes static types for those programs, in which explicit type annotations are given at the positions of subtyping coercions.
We construct a category of circuits: the objects are alphabets and the morphisms are deterministic automata. The construction differs in several respects from the bicategories of circuits appearing previously in the Literature: it is parameterized by a monad which allows flexibility in the emergent notion of process.We focus on the circuits which arise from a distributive category and the exception monad. These circuits are partial in that they may, based on their state, choose to abort on some inputs. Consequently, certain circuits determine languages, and safety and liveness properties with respect to these languages are captured by circuit equations. Actually, the notions of safety and liveness arise abstractly in any copy category. Extracting the category of circuits which are both safe and live corresponds to the extensive completion of a distributive copy category.Partial circuits coincide with elements of the terminal coalgebra of a specific datatype. The co-induction principle provides mechanisms for the construction of circuits, the normalization of circuit expressions and for the proof of safety and liveness properties.
The InterACT tool is an interactive theorem prover for algebraic specifications emphasizing user-friendliness. InterACT is integrated in the existing ACT environment. The main purpose of InterACT is to teach formal methods in universitary courses about formal specification of software systems. It has already been used successfully in this area.The theoretical and practical concepts underlying InterACT are described in this paper. Ideas for the design of user interfaces for interactive theorem provers can be found.
This paper examines three important topics in computer science: behavioural equivalence, bisimulation, and minimal realisation of automata, and discusses the relationships that hold between them. Central to all three topics is a notion of equivalence of behaviour, and by taking a coalgebraic approach to algebraic specifications we show that bisimulation is 'the same as' behavioural equivalence. Moreover, we show that a particular construction for minimal realisation of behaviour corresponds to a proof technique for proving behavioural equivalence. We also argue that it is useful to consider algebraic specifications of objects as having both algebraic and coalgebraic aspects.
The aim of our work is the modelling and design of information systems in the object-oriented setting. An object-oriented specification covers structural as well as behavioural aspects of the system. A possibility to describe system dynamics is to use a temporal logic as it is done in the formal object-oriented specification language TROLL. Temporal logics is particularly suited to deal with temporal behaviour and evolutionary aspects of systems.Reification techniques have been developed to break down the software design process in pieces with reduced complexity. We support action reification, i.e., actions are reified by complex processes or so-called transactions. Thus, reification corresponds to a change of viewpoint: what has been atomic from the abstract point of view may become compound from the reified point of view. Problems arise when reification is considered in conjunction with temporal logic. Temporal formulae which incorporate action symbols have to be treated carefully under the presence of reification.In this paper we propose the so-called reification logic by extending a linear temporal logic by the concept of transaction. A transaction is a logical unit of a specific abstraction level which is composed of several actions of a more concrete level. We propose an appropriate translation of TROLL concepts in reification logic which is compatible with reification. This way, we establish a framework which has the capability to deal with reification in object-oriented specification.
The paper summarizes the main concepts and paradigms of category theory and explores some of their applications to the area of algebraic specifications. In detail we discuss different approaches to an abstract theory of specification logics. Further we present a uniform framework for developing particular specification logics. We make use of ‘classifying categories’, to present categories of algebras as functor categories and to obtain necessary basic results for particular specification logics in a uniform manner. The specification logics considered are: equational logic for total algebras, conditional equational logic for partial algebras, and rewrite logic for concurrent systems.
The ESPRIT Basic Research Working Group COMPASS has brought together most European scientists in the area of algebraic specification methods in an effort to consolidate and integrate the theoretical basis and apply it to software technology. The algebraic approach treats not just the syntactic aspects of interfaces but supports the precise specification of the semantics of generic reusable system components, providing the formal conceptual basis for their stepwise and correct development.
In this paper we give a new view of the type theory UTT (Uniform theory of dependent types) [5] as a system to formally develop programs from algebraic specifications, comparable to e.g. EML([9]). We will focus our attention on behavioural specifications since they have not been deeply studied in a type theoretical setting, and we describe how to develop proofs about behavioural satisfaction.
