We define a language for second-order arithmetic using the (positive) connectives ∧ and ∨, the (positive) quantifiers ∀ and ∃, and with negation ‘pushed to the atoms’ under the form of atomic formula t[esdot ]u, t≠u, t∈X, t∈X where t and u stand for first-order terms and X for a second-order variable.

We define and study the translation from this language to the more usual implicational language containing the entailment connective →. We also study the converse translation. Next we define the appropriate notion of syntactical truth predicate for this language (such a notion has been introduced for the implicational language in Colson and Grigorieff (1998)). We establish using the previous translations that the existence of such a predicate for this language is equivalent to the the existence of such a predicate for the implicational language. This result is established in a predicative formal system. We conclude by discussing some elementary attempts to construct such a truth predicate by a fixed point technique.

Mixins are modules that may contain deferred components, that is, components not defined in the module itself; moreover, in contrast to parameterised modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we defined a syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatisation.

Graph transitions represent an extension of the DPO approach to graph transformation for the specification of reactive systems. In this paper, we develop the theory of concurrency for graph transitions. In particular, we prove a local Church–Rosser theorem and define a notion of shift-equivalence that allows us to represent both intra-concurrency (within the specified subsystem) and inter-concurrency (between subsystem and environment). Via an implementation of transitions in terms of DPO transformations with context rules, a second, more restrictive notion of equivalence is defined that captures, in addition, the extra-concurrency (between operations of the environment). As a running example and motivation, we show how the concepts of this paper provide a formal model for distributed information systems.

This special issue of Mathematical Structures in Computer Science contains the final Proceedings of the Tutorial Workshop on Realizability Semantics and Applications, which was held between June 30 and July 1, 1999 in Trento, Italy, as one of the satellite workshops associated to the Federated Logic Conference.

A categorical framework for equational logics is presented, together with axiomatizability results in the style of Birkhoff. The distinctive categorical structures used are inclusion systems, which are an alternative to factorization systems in which factorization is required to be unique rather than unique ‘up to an isomorphism’. In this framework, models are any objects, and equations are special epimorphisms in [Cfr ], while satisfaction is injectivity. A first result says that equations-as-epimorphisms define exactly the quasi-varieties, suggesting that epimorphisms actually represent conditional equations. In fact, it is shown that the projectivity/freeness of the domain of epimorphisms is what makes the difference between unconditional and conditional equations, the first defining the varieties, as expected. An abstract version of the axiom of choice seems to be sufficient for free objects to be projective, in which case the definitional power of equations of projective and free domain, respectively, is the same. Connections with other abstract formulations of equational logics are investigated, together with an organization of our logic as an institution.

This special issue of Mathematical Structures in Computer Science is devoted to the theory and applications of graph transformations. This research area dates back to the early seventies and is based on mathematical techniques from graph theory, algebra, logic and category theory. The theory of graph transformations has become attractive as a modelling and programming paradigm for complex graphical structures in a large variety of areas in computer science and for applications to other fields. During the Joint APPLIGRAPH/GETGRATS Workshop on Graph Transformation Systems (GRATRA 2000) – a satellite of ETAPS 2000 in Berlin – 35 lectures were presented by participants from all over the world. The authors of presentations that stressed the theoretical point of view were invited to submit a full version of their presentation to Mathematical Structures in Computer Science. After a careful refereeing process nine papers have been accepted, seven of which are included in this special issue.

The paper by Ehrenfeucht, Petre, Prescott and Rozenberg connects the important new area of DNA computing in vivo to our area of graph transformation. An application of hypergraph constructions to the static analysis of concurrent systems is presented by König, and normal forms for context-free node rewriting hypergraph grammars by Klempien-Hinrichs. The construction of pushout complements for ‘partly total algebras’ generalising attributed graphs is presented by Burmeister, Llabrés and Roselló. Finally, Courcelle and Makowsky present operations on relational structures (generalising different kinds of graphs and hypergraphs) that are compatible with monadic second order logic. Four other accepted papers could not be included in this special issue because of space limitations.

They will appear in regular issues of MSCS:

— R. Heckel, M. Llabrés, H. Ehrig and F. Orejas: Concurrency and loose semantics of open graph transformation systems.

— L. Helouet, C. Jard and B. Caillaud: An event structure based semantics for high-level message sequence charts.

— J. Larossa and G. Valiente: Constraint satisfaction algorithms for graph pattern matching.

— N. Verlinden and D. Janssens: Algebraic properties for Local Action Systems.

We are most grateful to all the referees of these papers, to Olga Runge and Claudia Ermel for technical support, and to Giuseppe Longo and Cambridge University Press for fruitful cooperation in editing this special issue.

The purpose of this short paper is to sketch the development of a few basic topics in the history of realizability. The number of topics is quite limited and reflects very much my own personal taste, prejudices and area of competence.

The connections between formal topology and domain theory are surveyed and various types of continuous domains are represented as formal spaces through locally Stone and locally Scott formal topologies.

This paper details a partial order semantics for families of scenarios represented by High-Level Message Sequence Charts (HMSCs): graph grammars generating event structures are used to represent HMSCs. A decision procedure for HMSC equivalence is then described. This can be considered as a first step towards the formal manipulation of scenarios.

Ciliates have developed a unique nuclear dualism, having two nuclei of different functionality: the germline micronucleus and the somatic macronucleus. The way that ciliates assemble the macronuclear genes after cell mating constitutes one of the most intricate DNA processings in living organisms. This processing is also very interesting from the computational point of view. In this paper, we investigate the operations of loop excision and hairpin excision/reinsertion used in the assembly process. In particular, we consider three levels of formalization of this process, culminating in graph reduction systems.

We use some results of Trnková to show first that subcoalgebras are always closed under finite intersections. Assuming that the type functor F is bounded, we obtain a concrete representation of the terminal F-coalgebra. We also provide several equivalent characterizations of boundedness.

There are two main approaches to obtaining ‘topological’ cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be cartesian closed – for example, the category of sequential spaces. Under the other, one generalises the notion of space – for example, to Scott's notion of equilogical space. In this paper, we show that the two approaches are equivalent for a large class of objects. We first observe that the category of countably based equilogical spaces has, in a precisely defined sense, a largest full subcategory that can be simultaneously viewed as a full subcategory of topological spaces. In fact, this category turns out to be equivalent to the category of all quotient spaces of countably based topological spaces. We show that the category is bicartesian closed with its structure inherited, on the one hand, from the category of sequential spaces, and, on the other, from the category of equilogical spaces. We also show that the category of countably based equilogical spaces has a larger full subcategory that can be simultaneously viewed as a full subcategory of limit spaces. This full subcategory is locally cartesian closed and the embeddings into limit spaces and countably based equilogical spaces preserve this structure. We observe that it seems essential to go beyond the realm of topological spaces to achieve this result.

Graph pattern matching is a central problem in many application fields. Since it is NP-complete, we cannot expect to find algorithms with a good worst-case performance. However, there is still room for general procedures with a good average performance. In this paper we explore four different solving approaches within the constraint satisfaction framework, and introduce a new algorithm, which we call nRF+. The algorithm is a refinement of really full look ahead that takes advantage of the problem structure in order to enhance the look ahead procedure. We give a formal proof that nRF+ is superior to the other approaches in terms of number of visited nodes. An additional contribution of this paper is the introduction of a new benchmark for testing algorithms in this domain. It is formed by a large set of well-defined graphs of very diverse nature. In this benchmark, we show that nRF+ can efficiently solve a broad range of problems, while still leaving many problem instances unsolved. The use of this challenging benchmark is encouraged for future algorithms evaluation.

We present a category of locally convex topological vector spaces that is a model of propositional classical linear logic and is based on the standard concept of Köthe sequence spaces. In this setting, the ‘of course’ connective of linear logic has a quite simple structure of a commutative Hopf algebra. The co-Kleisli category of this linear category is a cartesian closed category of entire mappings. This work provides a simple setting in which typed λ-calculus and differential calculus can be combined; we give a few examples of computations.

We extend the proof-irrelevant model defined in Smith (1988) to the whole of Martin-Löf's logical framework. The main difference here is the existence of a type whose objects themselves represent types rather than proof-objects. This means that the model must now be able to distinguish between objects with different degree of relevance: those that denote proofs are irrelevant whereas those that denote types are not. In fact a whole hierarchy of relevance exists.

Another difference is the higher level of detail in the formulation of the formal theory, such as the explicit manipulation of contexts and substitutions. This demands an equally detailed definition of the model, including interpreting contexts and substitutions.

We are thus led to a whole reformulation of the proof-irrelevant model. We present a model that is built up from an arbitrary model of the untyped lambda calculus. We also show how to extend it when the logical framework itself is enlarged with inductive definitions. In doing so, a variant of Church numerals is introduced.

As in Smith (1988), the model can only be defined in the absence of universes, and it is useful to obtain an elementary proof of consistency and to prove the independence of Peano's fourth axiom.

Confluent node-rewriting hypergraph grammars represent the most comprehensive known method for defining sets of hypergraphs in a recursive way. For a large natural subclass of these grammars, we show that the maximal rank of hyperedges indispensable for generating some set of hypergraphs equals the maximal rank of the hyperedges occurring in the hypergraphs of that set. Moreover, if such a grammar generates a set of graphs, one can construct from that grammar a C-edNCE graph grammar generating the same set of graphs.

The notion of tripos (Hyland et al. 1980; Pitts 1981) was motivated by the desire to explain in what sense Higg's description of sheaf toposes as H-valued sets and Hyland's realizability toposes are instances of the same construction. The construction itself can be seen as the universal solution to the problem of realizing the predicates of a first order hyperdoctrine as subobjects in a logos with effective equivalence relations. In this note it is shown that the resulting logos is actually a topos if and only if the original hyperdoctrine satisfies a certain comprehension property. Triposes satisfy this property, but there are examples of non-triposes satisfying this form of comprehension.

Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly–Mac Lane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.

We present explicit constructions of universal homogeneous objects in categories of domains with stable embedding–projection pairs as arrows. These results make use of a representation of such domains through graph-like structures and apply a generalization of Rado’s result on the existence of the universal homogeneous countable graph. In particular, we build universal homogeneous objects in the categories of coherence spaces and qualitative domains, introduced by Girard (Girard 1987; Girard 1986), and two categories of hypercoherences recently studied by Ehrhard (Ehrhard 1993). Our constructions rely on basic numerical notions. We also show that a suitable random construction of Rado’s graph and its generalizations produces with probability 1 the universal homogeneous structures presented here.

This paper presents a simple implementation of the λ-calculus in the interaction net paradigm. It is based on a two-fold translation. λ-terms are coded (for duplication) or decoded (for execution), and reduction is achieved by switching between these two states: decoding corresponds to head reduction and encoding to left reduction.