We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

The context of this article is the programme to develop monoidal bicategories with a feedback operation as an algebra of processes, with applications to concurrency theory. The objective here is to study reachability, minimization and minimal realization in these bicategories. In this setting the automata are 1-cells, in contrast with previous studies where they appeared as objects. As a consequence, we are able to study the relation of minimization and minimal realization to serial composition of automata using (co)lax (co)monads. We are led to define suitable behaviour categories and prove minimal realization theorems that extend classical results.

We give a negative answer to the question of whether every partial combinatory algebra can be completed. The explicit counterexample will be an intricately constructed term model. The construction and the proof that it works depend heavily on syntactic techniques. In particular, it provides a nice example of reasoning with elementary diagrams and descendants. We also include a domain-theoretic proof of the existence of an incompletable partial combinatory algebra.

We present an interdisciplinary effort in the field of global environmental change, related to the understanding of the concept of ‘vulnerability’. We have used functional programming to capture the generic aspects of the myriad of definitions of vulnerability, and have used the resulting formalization to learn something new about vulnerability and to write some better software for vulnerability assessment. In the process, we have also found out something about formalization in general, about the advantages and disadvantages of dependent types, and about the role of computing science in the larger intellectual landscape.

In this paper, we describe three distinct monoids over domains, each with a commutative analog, which define bag domain monoids. Our results were inspired by work by Varacca (Varacca 2003), and they lead to a constructive approach to his Hoare indexed valuations over a continuous poset $P$. We use our constructive approach to describe an analog of the probabilistic power domain, and the laws that characterise it, that forms a Scott-closed subset of Varacca's construct. We call these the Hoare random variables over$P$.

Using the concept of a generalised priority constraint satisfaction problem, we previously found a way to introduce priority queries into fuzzy relational databases. The results were PFSQL (Priority Fuzzy Structured Query Language) together with a database independent interpreter for it. In an effort to improve the performance of the resolution of PFSQL queries, the aim of the current paper is to formalise PFSQL queries by obtaining their interpretation in an existing fuzzy logic. We have found that the ŁΠ logic provides sufficient elements. The SELECT line of PFSQL queries is semantically a formula of some fuzzy logic, and we show that such formulas can be naturally expressed in a conservative extension of the ŁΠ logic. Furthermore, we prove a theorem that gives the PSPACE containment for the complexity of finding a model for a given ŁΠ logic formula.

On December 5, 1997, a small conference was held at McGill on the occasion of Jim Lambek's 75th birthday. Subsequently it was decided to publish two volumes of papers contributed in his honour to mark this occasion: this issue of Mathematical Structures in Computer Science is one of the volumes; the other is Volume 6 of the journal Theory and Applications of Categories. At the December 1997 conference, a brief biographical essay was presented by Michael Barr and appears in the TAC volume. However, we wish to make some further remarks here.

Jim completed his Ph.D. at McGill under Hans Zassenhaus in 1950, and has remained at McGill since then. But it is of interest to note that Jim wrote two theses: the second involved biquaternions in mathematical physics, and so foreshadows a significant feature of his career: Jim has consistently shown a remarkable range of interests, from physics to linguistics, from algebra to logic, from the history and philosophy of mathematics to the theory of computing science (although he never touches a computer, to this day!). Let us just review a small sample of his more than 100 published papers.

Weakest precondition transformers are useful tools in program verification. One of their key properties is composability, that is, the weakest precondition predicate transformer (wppt for short) associated to program $f;\;g$ should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy composability as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg–Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the nonempty powerset monad, the counter monad, or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.

We define an extension of pure type systems with explicit substitution. We show that the type systems with explicit substitution are strongly normalizing iff their ordinary counterparts are. Subject reduction is shown to fail in general but a weaker, though still useful, subject reduction property is established. A more complicated extension is proposed for which subject reduction does hold in general.

Certain ‘Finite Structure Conditions’ on a geometric theory are shown to be sufficient for its classifying topos to be a presheaf topos. The conditions assert that every homomorphism from a finite structure of the theory to a model factors via a finite model, and they hold in cases where the finitely presentable models are all finite.

The conditions are shown to hold for the theory of strongly algebraic (or SFP) information systems and some variants, as well as for some other theories already known to be classified by presheaf toposes.

The work adheres to geometric constructivism throughout, and in consequence provides ‘topical’ categories of domains (internal in the category of toposes and geometric morphisms) with an analogue of Plotkin's double characterization of strongly algebraic domains, by sets of minimal upper bounds and by sequences of finite posets.

Is the current formulation of multiset theory, which is based on sets and multiplicities of their elements, adequate? We exhibit both mathematical and metamathematical reasons which should cause one to rethink the definition. Some problems with multiset theory in its accepted formulation concern even the basic operations of union, intersection, and complement; others, more deeply rooted, concern Cartesian products, relations, or morphisms. We compare current definitions and conclude that the problems of multiset theory need to be resolved at the fundamental level of sets and mappings (or equivalent constructs) with multiplicities introduced only as a secondary concept. As a consequence, we propose to define multisets as families. A mapping establishes the connection to the familiar theory of multisets. Without losing anything, our proposal is simple and provides for an elegant mathematical theory.

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

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.

We present a categorical model for intuitionistic linear logic in which objects are polynomial diagrams and morphisms are simulation diagrams. The multiplicative structure (tensor product and its adjoint) can be defined in any locally cartesian closed category, but the additive (product and coproduct) and exponential (-comonoid comonad) structures require additional properties and are only developed in the category Set, where the objects and morphisms have natural interpretations in terms of games, simulation and strategies.

We prove a full completeness theorem for MLL without the Mix rule. This is done by interpreting a proof as a dinatural transformation in a *-autonomous category of reflexive topological abelian groups first studied by Barr, denoted [Rscr ][Tscr ][Ascr ]. In Section 2, we prove the unique interpretation theorem for a binary provable MLL-sequent. In Section 3, we prove a completeness theorem for binary sequents in MLL without the Mix rule, where we interpret formulas in the category [Rscr ][Tscr ][Ascr ]. The theorem is proved by investigating the concrete structure of [Rscr ][Tscr ][Ascr ], especially that arising from Pontrjagin's work on duality.

A Gentzen sequent calculus for Lax Logic is presented, the proofs in which correspond naturally in a 1–1 way to the normal natural deductions for the logic. The propositional fragment of this calculus is used as the basis for another calculus that uses a history mechanism in order to give a decision procedure for propositional Lax Logic.

We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

We consider the well-known Coordinated Attack Problem, where two generals have to decide on a common attack, when their messengers can be captured by the enemy. Informally, this problem represents the difficulties to agree in the presence of communication faults. We consider here only omission faults (loss of message), but contrary to previous studies, we do not to restrict the way messages can be lost, i.e., we make no specific assumption, we use no specific failure metric. In the large subclass of message adversaries where the double simultaneous omission can never happen, we characterize which ones are obstructions for the Coordinated Attack Problem. We give two proofs of this result. One is combinatorial and uses the classical bivalency technique for the necessary condition. The second is topological and uses simplicial complexes to prove the necessary condition. We also present two different Consensus algorithms that are combinatorial (resp. topological) in essence. Finally, we analyze the two proofs and illustrate the relationship between the combinatorial approach and the topological approach in the very general case of message adversaries. We show that the topological characterization gives a clearer explanation of why some message adversaries are obstructions or not. This result is a convincing illustration of the power of topological tools for distributed computability.

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe’s method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga’s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga’s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga’s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

The aim of the research domain known as process mining is to use process discovery to construct a process model as an abstract representation of event logs. The goal is to build a model (in terms of a Petri net) that can reproduce the logs under consideration, and does not allow different behaviours compared with those shown in the logs. In particular, process mining aims to verify the accuracy of the model design (represented as a Petri net), basically checking whether the same net can be rediscovered. However, the main mining methods proposed in the literature have some drawbacks: the classical α-algorithm is unable to rediscover various nets, while the region-based approach, which can mine them correctly, is too complex.

In this paper, we compare different approaches and propose some ideas to counter the weaknesses of the region-based approach.