CTCS 97: Abstracts of Accepted Papers

Proof Principles for Datatypes with Iterated Recursion
by Ulrich Hensel, Bart Jacobs

Data types like trees which are finitely branching and of (possibly) infinite depth are described by iterating initial algebras and terminal coalgebras. We study proof principles for such data types in the context of categorical logic, following and extending the approach of~[HermidaJ95b,JacobsHermidaIndCoind96]. The technical contribution of this paper involves a description of initial algebras and terminal coalgebras in total categories of fibrations for lifted ``datafunctors''. These lifted functors are used to formulate our proof principles. We test these principles by proving some elementary results for four kinds of trees (with finite or infinite breadth or depth) using the proof tool PVS.

When do datatypes commute?
by Paul Hoogendijk, Roland Backhouse

Polytypic programs are programs that are parameterised by type constructors (like List), unlike polymorphic programs which are parameterised by types (like Int). In this paper we formulate precisely the polytypic programming problem of ``commuting'' two datatypes. The precise formulation involves a novel notion of higher order naturality. We demonstrate via a number of examples the relevance and interest of the problem, and we show that all ``regular datatypes'' (the sort of datatypes that one can define in a functional programming language) do indeed commute according to our specification. The framework we use is the theory of allegories, a combination of category theory with the point-free relation calculus.

A factorisation theorem for external derivations
by Paul-Andre Mellies

Among all the potential computations of a term, some are better than others. In my PhD, I give an algebraic characterisation of the << good >> ones, for instance the leftmost outermost reductions of the lambda-calculus: a derivation e: M -> P is << external >> if e.f: M -> Q is standard for any standard derivation f: P -> Q.
In this short talk, I will show that every derivation d: M -> Q can be factorised as an external derivation from e: M -> P followed by an << internal >> derivation f: P -> Q. Moreover, this epi-mono factorisation is functorial (i.e there is a nice diagram) in the sense of Freyd-Kelly.
Conceptually, the factorisation result means that the good part in a computation can always be separated from the junk. Technically, it is the key step towards the description of stability (semantics) as a syntactic phenomenon. In fact, contrary to usual derivation spaces (see Levy's PhD), external derivation spaces enjoy meets.

A decision algorithm for linear isomorphism of types with complexity O(nlog^2(n)).
by Alexander Andreev, Sergei Soloviev

It is known, that ordinary isomorphisms (associativity and commutativity of ``times'', isomorphisms for ``times'' unit and currying) provide a complete axiomatisation of isomorphism of types in multiplicative linear lambda calculus (isomorphism of objects in a free symmetric monoidal closed category). One of the reasons to consider linear isomorphism of types instead of ordinary isomorphism was that better complexity could be expected. Meanwhile, no upper bounds reasonnably close to linear were obtained. We describe an algorithm deciding if two types are linearly isomorphic with complexity O(nlog^{2}(n)).

by A. Bucalo, G. Rosolini

Lifting is the name with which, in semantics of programming languages, one refers to a representation of partial maps. It relates to the order induced on the representation by the inclusion of graphs of partial maps, which usually adds one element below all others. The problem we want to consider is precisely that of recognizing a lifting functor in a category, possibly lacking part of the structure required to define the representation. We solve it in the general case of a category with a terminal object; this indicates that a lifting functor carries an imprint which distinguishes it, and does not depend, for instance, on having pullbacks in the category.
This approach to partiality seems new in the literature on categories of partial maps since there the central r\^ole is played by the Kleisli category on the monad: the category of total maps is only instrumental, and always recognized as definable from that of partial maps (when this comes with sufficient structure). On the other hand, it is certainly implicit in the computational point of view, and it relates directly to the question of modularity: once the structure of lifting is known, one knows how to mix that with others.
An interesting characterization of lifting is obtained when we specialize our result to categories with finite products.

Shedding New Light in the World of Logical Systems
by Uwe Wolter, Alfio Martini

The notion of an Institution [GB92] is here taken as the precise formulation for the notion of a logical system. By using elementary tools from the core of category theory, we are able to reveal the underlying mathematical structures lying ``behind'' the logical formulation of the satisfaction condition, and hence to acquire a both suitable and deeper understanding of the institution concept. This allows us to systematically approach the problem of describing and analyzing relations between logical systems. Theorem 2.11 redesigns the notion of an institution to a purely categorical level, so that the satisfaction condition becomes a functorial (and natural) transformation from specifications to (subcategories of) models and vice versa. This systematic procedure is also applied to discuss and give a natural description for the notions of institution morphism and institution map. The last technical discussion is a careful and detailed analysis of two examples, which tries, as an outcome, to outline how the new categorical insights could help in guiding the development of a unifying theory for relations between logical systems.

Effectiveness of the Global Modulus of Continuity on Metric Spaces
by Klaus Weihrauch, Xizhong Zheng

Abstract: Let (X,d_X) and (Y,d_Y) be metric spaces. By definition, there is a function h which maps every triple (f,x,\epsilon) to \delta > 0, for any continuous function f from X to Y, element x in X and real \epsilon > 0, such that d_Y(f(x), f(x')) < \epsilon whenever d_X(x,x') < \delta for all x' in X. Such a function h is called the global modulus of continuity on the function space C(X,Y) of continuous functions from X to Y. By a recent result of Repovs and Semenov, there is a continuous global modulus of continuity on C(X,Y), if X is locally compact. Their proof applies the classical Selection Theorem of Michael, i.e., h exists as a selection function of some lower semi continuous set valued function. Thus it is quite ineffective. Based on Weihrauch's frameworks on computable metric space, we effectivize this result. A computable metric space X of Weihrauch's sense is called effectively locally compact, if we can determine effectively from any element x of X a compact neighbourhood B(x ) of x. Our main theorem of this paper says that there is a computable global modulus of continuity on C(X,Y) if X is a effectively locally compact metric space. Our proof is a direct construction of an algorithm which computes the global modulus of continuity.

Monads and Modular Term Rewriting
by Christoph Lueth, Neil Ghani

Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lu96], the usefulness of this semantics was demonstrated by giving a purely categorical proof of the modularity of confluence for the disjoint union of term rewriting systems (Toyama's theorem). This paper provides further support for the use of monads in term rewriting by giving a categorical proof of the most general theorem concerning the modularity of strong normalisation. In the process, we also improve upon some technical aspects of the earlier work.
[Lu96] Compositional Term Rewriting: An algebraic proof of Toyama's theorem. RTA'96, Springer LNCS 1103.

Presheaf Models for the pi-Calculus
by Gian Luca Cattani, Ian Stark, Glynn Winskel

Recent work has shown that presheaf categories provide a general model of concurrency, with an inbuilt notion of bisimulation based on open maps. Here it is shown how this approach can also handle systems where the language of actions may change dynamically as a process evolves. The example is the \pi-calculus, a calculus for `mobile processes' whose communication topology varies as channels are created and discarded. A denotational semantics is described for the \pi-calculus within an indexed category of profunctors; the model is fully abstract for bisimilarity, in the sense that bisimulation in the model, obtained from open maps, coincides with the usual bisimulation obtained from the operational semantics of the \pi-calculus. While attention is concentrated on the `late' semantics of the \pi-calculus, it is indicated how the `early' and other variants can also be captured.

Categorical Modelling of Structural Operational Rules: case studies
by Daniele Turi

This paper aims at substantiating a recently introduced mathematical theory of `well-behaved' operational semantics by applying it to a significant variety of examples. These involve: non-determinism, interaction, side-effects, exceptions, and trace equivalence. Both guarded and unguarded recursive programs are also treated, the former using a novel functorial notion of guardedness and the latter by working in categories of partial maps.

A 2-Categorical Presentation of Term Graph Rewriting
by Andrea Corradini, Fabio Gadducci

It is well-known that a term rewriting system can be represented faithfully as a cartesian 2-category, where horizontal arrows represent terms, and cells represent rewriting sequences. In this paper we propose a similar, original 2-categorical representation for term graph rewriting. Building on a result recently presented by the authors, which shows that term graphs over a given signature are in one-to-one correspondence with arrows of a ps-monoidal category freely generated from the signature, we associate with a term graph rewriting system a ps-monoidal 2-category, and show that cells faithfully represent its rewriting sequences. We also discuss how to deal with garbage collection, and we exploit the categorical framework to relate term graph rewriting and term rewriting. This last point is based on the observation that ps-monoidal (2-)categories can be regarded as "weak" cartesian (2-)categories, where certain naturality axioms have been dropped.

Combining and Representing Logical Systems
by Till Mossakowski, Andrzej Tarlecki, Wieslaw Pawlowski

The paper addresses important problems of building complex logical systems and their representations in universal logics in a systematic way. Following Goguen and Burstall, we adopt the model-theoretic view of logic as captured in the notion of institution and of parchment (a certain algebraic way to present institutions).
We propose a modified notion of parchment together with a notion of parchment morphism and representation, respectively. We lift formal properties of the categories of institutions and their representations to this level: the category of parchments is complete, and parchment representations may be put together using categorical limits as well. However, parchments provide a more adequate framework for systematic combination of logical systems than institutions. We indicate how the necessary invention for proper combination of various logical features may be introduced either on an ad hoc basis (when putting parchments together using limits in the category of parchments) or via representations in a universal logic (when parchment combination is driven by their representations).

General Synthetic Domain Theory -- A Logical Approach (Extended abstract)
by Bernhard Reus, Thomas Streicher

Synthetic Domain Theory (SDT) is a version of Domain Theory where ``all functions are continuous''. In the first author's Thesis there has been developed a logical and axiomatic version of SDT which is special in the sense that it captures the essence of Domain Theory `a la Scott but rules out e.g. Stable Domain Theory as it requires that the order on function spaces is pointwise. In this article we will give a logical and axiomatic account of a general SDT aiming to grasp the structure common to all notions of domains which has been advocated by many authors. As in loc.cit. the underlying logic is a sufficiently expressive version of constructive type theory. We start with a few basic axioms giving rise to a core theory on top of which we study various notions of predomains as e.g. complete and well-complete S-spaces, define the appropriate notion of domain and prove the common induction principles.

Specifying Interaction Categories
by Dusko Pavlovic, Samson Abramsky

We analyse two complementary methods for obtaining models of typed process calculi, in the form of interaction categories. These methods allow adding new features to previously captured notions of process and of type, respectively. By combining them, all familiar examples of interaction categories, as well as some new ones, can be built starting from some simple familiar categories.
Using the presented constructions, interaction categories can be analysed without fixing a set of axioms, merely in terms of the way in which they are specified --- just like algebras are analysed in terms of equations and relations, independently on abstract characterisations of their varieties.

A Calculus for Collections and Aggregates
by Kazem Lellahi, Val Tannen

We present a calculus that should play for database query languages the same role that the lambda calculus plays for functional programming. For the semantic foundations of the calculus we introduce a new concept: monads enriched with algebraic structure. We model collection types through enriched monads and aggregate operations through enriched monad algebras. The calculus derives program equivalences that underlie a good number of the optimizations used in query languages.