We axiomatize permutation equivalence in term rewriting systems and Klop’s orthogonal Combinatory Reduction Systems (Klop 1980). The axioms for the former are provided by the general approach proposed by Meseguer (Meseguer 1992). The latter need extra axioms modelling the interplay between reductions and the operation of substitution.

As a consequence of this work, the definition of permutation equivalence is rid of residual calculi, which are heavy in general.

In this paper, we propose a new and elegant definition of the class of recursive functions, which is analogous to Kleene's definition but differs in the primitives taken, thus demonstrating the computational power of the concurrent programming language introduced in Walters (1991), Walters (1992) and Khalil and Walters (1993).

The definition can be immediately rephrased for any distributive graph in a countably extensive category with products, thus allowing a wide, natural generalization of computable functions.

The π-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, which fails in the ordinary π-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

Using the well-known categorical notion of ‘functor’, one may define the concept of datatype (algebra) without being forced to introduce a signature (that is, names and typings for the individual sorts (types) and operations involved). This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra.

The categorical notion of ‘transformer’ developed in this paper allows the same approach to laws: without using signatures one can define the concept of law for datatypes (lawful algebras), and investigate the equational specification of datatypes in a syntax-free manner. A transformer is a special kind of functor and also a natural transformation on the level of dialgebras. Transformers are quite expressive, satisfy several closure properties, and are related to naturality and Wadler'' Theorems For Free Theorem. In fact, any colimit is an initial lawful algebra.

We continue our study of the negation-free structure of multiplicative linear logic, as represented by the structure of weakly distributive categories, to consider the ‘exponentials’! and ? in the weakly distributive context. In addition to the usual triple and cotriple structure that one would expect on each of the two operators, there must be some connection between them to replace the de Morgan relationship found in the linear logic context. This turns out to be the notion of tensorial strength. We analyze coherence for this situation, using a modification of the usual nets due to Danos, which is a form suitable for linear logic with exponentials but without negation.

We establish sufficient and necessary conditions for a natural sink to be a colimit in DCPO. Based on these conditions, we show how to construct a colimit for any functor F from a small category Ω into the category DCPO. This demonstrates that the category DCPO is cocomplete. We also investigate under what conditions the colimit object is algebraic.

Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

We show that a set of finite graphs of tree-width at most k is recognizable (with respect to the algebra of graphs with an unbounded number of sources) if and only if it is recognizable with respect to the algebra of graphs of tree-width at most k with at most k sources.

It is well known that every algorithmic problem definable by a formula of first-order logic can be solved in polynomial time, since all these problems are in L (see Aho and Ullman (1979) and Immerman (1987)). Using an old technique of Hanf (Hanf 1965) and other techniques developed to prove the decidability of formal theories in mathematical logic, it is shown that an arbitrary FO-problem over relational structures of bounded degree can be solved in linear time.

A polynomial-time algorithm is presented for deciding bisimulation equivalence of so-called Basic Parallel Processes: multisets of elementary processes combined by a commutative parallel-composition operator.

In this paper we try to shed some light on the similarities and differences in the different approaches denning the notions of implementation and implementation correctness. For obvious reasons, we do not discuss all existing approaches individually. Instead, a formal framework is introduced in order to discuss the most important ones. Additionally, we discuss some issues, which in our opinion are often misunderstood, concerning transitivity of implementation correctness and its role in the software development process. In particular, on the one hand, we show that for reasonable notions of implementation, it is almost impossible to prove transitivity of implementation correctness at the specification level. On the other hand, we show that this is not really important if the programming language satisfies the properties of horizontal and vertical composition.

Argumentation is a proof theoretic paradigm for reasoning under uncertainty. Whereas a ‘proof’ establishes its conclusion outright, an ‘argument’ can only lend a measure of support. Thus, the process of argumentation consists of identifying all the arguments for a particular hypothesis φ, and then calculating the support for φ from the weight attached to these individual arguments. Argumentation has been incorporated as the inference mechanism of a large scale medical expert system, the ‘Oxford System of Medicine’ (OSM), and it is therefore important to demonstrate that the approach is theoretically justified. This paper provides a formal semantics for the notion of argument embodied in the OSM. We present a categorical account in which arguments are the arrows of a semilattice enriched category. The axioms of a cartesian closed category are modified to give the notion of an ‘evidential closed category’, and we show that this provides the correct enriched setting in which to model the connectives of conjunction (&) and implication (⇒).

Finally, we develop a theory of ‘confidence measures’ over such categories, and relate this to the Dempster-Shafer theory of evidence.

This paper considers two main aspects of the lower power locale PL(X): first, its relation to the symmetric topos construction of Bunge and Carboni; and second, its points, which, it is shown, are equivalent to the weakly closed sublocales of X with open domain. This is done as part of a more general discussion of arbitrary weakly closed sublocales, including a new characterization using suplattice homomorphisms from o(X) to Sub(1), and a new proof of a theorem of Jibladze relating them to Ω-nuclei.

We consider the relationship between three ways of defining graph derivability. That the traditional double-pushout approach and Banach's inward version are equivalent in the case of injective left-hand sides is proved in a purely categorical setting. In the case of noninjective left-hand sides, equivalence can be shown in special categories if the right-hand side is injective. Both approaches have the same generative power in the category of graphs if the pushout connecting the outward production with the inward one is a pullback as well. Finally, it is shown that Banach's point of view establishes a close relationship between the categorical approach and Kaplan's Δ-grammars, allowing a slight generalization of Δ-grammars and making them an operational description of the categorical approach.

We study a natural generalization of System Fω with intersection types, establishing basic structural properties and constructing a semantic model based on partial equivalence relations to prove the soundness of typing. As an application of this calculus, we define a simple typed model of object-oriented programming with multiple inheritance.

An analysis of relationships between Craig-style interpolation, compactness, and other related model-theoretic properties is carried out in the softer framework of categories of pre-institutions. While the equivalence between sentence interpolation and the Robinson property under compactness and Boolean closure is well known, a similar result under different assumptions (not involving compactness) is newly established for presentation interpolation. The standard concept of naturality of model transformation is enriched by a new property, termed restriction adequacy, which proves useful for the reduction of interpolation along pre-institution transformations. A distinct reduction theorem for the Robinson property is presented as well. A variant of the ultraproduct concept is further introduced, and the related closure property for pre-institutions is shown to be equivalent to compactness

This paper presents several basic results about the non-existence of reflexive objects in cartesian closed topological categories of Hausdorff spaces. In particular, we prove that there are no non-trivial countably compact reflexive objects in the category of Hausdorff k-spaces and, more generally, that any non-trivial reflexive Tychonoff space in this category contains a closed discrete subspace corresponding to a numeral system in the sense of Wadsworth. In addition, we establish that a reflexive Tychonoff space in a cartesian-closed topological category cannot contain a non-trivial continuous image of the unit interval. Therefore, if there exists a non-trivial reflexive Tychonoff space, it does not have a nice geometric structure.

We establish functional completeness of Locally Cartesian Closed Categories by axiomatising the theory of LCCC's in a constructive style. As a consequence we show that there is essentially only one interpretation of Martin-Löf's theory of types with extensional equality in the theory of LCCC's.