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.
