Processes, Terms and Cycles: Steps on the Road to Infinity

Frontmatter

The Spectra of Words

Abstract

The k-spectrum of a word is the multiset of its non-contiguous subwords of length k. For given k, how small can n be for a pair of different words of length n to exist, with equal k- spectra? From the Thue-Morse word we find that n is at most 2 ^k . The construction of this paper decreases this upper bound to θ ^k , where \(\bumpeq\) is the golden ratio; the construction was found, though not published, over thirty years ago. Recently the bound has been further reduced, but remains considerably greater than the greatest known lower bound.

Robin Milner

On the Undecidability of Coherent Logic

Abstract

Through a reduction of the halting problem for register machines we prove that it is undecidable whether or not a coherent formula is a logical consequence of a coherent theory. We include a simple completeness proof for coherent logic. Although not published in the present form, these results seem to be folklore. Therefore we do not claim originality. Given the undecidability of the halting problem for register machines the presentation is self-contained.

Marc Bezem

Löb’s Logic Meets the μ-Calculus

Abstract

In this paper, we prove that Löb’s Logic is a retract of the modal μ-calculus in a suitable category of interpretations. We show that various salient properties like decidability and uniform interpolation are preserved over retractions. We prove a generalization of the de Jongh-Sambin theorem.

Albert Visser

A Characterisation of Weak Bisimulation Congruence

Abstract

This paper shows that weak bisimulation congruence can be characterised as rooted weak bisimulation equivalence, even without making assumptions on the cardinality of the sets of states or actions of the processes under consideration.

Rob J. van Glabbeek

Böhm’s Theorem, Church’s Delta, Numeral Systems, and Ershov Morphisms

Abstract

In this note we work with untyped lambda terms under β-conversion and consider the possibility of extending Böhm’s theorem to infinite RE (recursively enumerable) sets. Böhm’s theorem fails in general for such sets \(\mathcal{V}\) even if it holds for all finite subsets of it. It turns out that generalizing Böhm’s theorem to infinite sets involves three other superficially unrelated notions; namely, Church’s delta, numeral systems, and Ershov morphisms. Our principal result is that Böhm’s theorem holds for an infinite RE set \(\mathcal{V}\) closed under beta conversion iff \(\mathcal{V}\) can be endowed with the structure of a numeral system with predecessor iff there is a Church delta (conditional) for \(\mathcal{V}\) iff every Ershov morphism with domain \(\mathcal{V}\) can be represented by a lambda term.

Richard Statman, Henk Barendregt

Explaining Constraint Programming

Abstract

We discuss here constraint programming (CP) by using a proof-theoretic perspective. To this end we identify three levels of abstraction. Each level sheds light on the essence of CP.

In particular, the highest level allows us to bring CP closer to the computation as deduction paradigm. At the middle level we can explain various constraint propagation algorithms. Finally, at the lowest level we can address the issue of automatic generation and optimization of the constraint propagation algorithms.

Krzysztof R. Apt

Sharing in the Weak Lambda-Calculus

Abstract

Despite decades of research in the λ-calculus, the syntactic properties of the weak λ-calculus did not receive great attention. However, this theory is more relevant for the implementation of programming languages than the usual theory of the strong λ-calculus. In fact, the frameworks of weak explicit substitutions, or computational monads, or λ-calculus with a let statement, or super-combinators, were developed for adhoc purposes related to programming language implementation. In this paper, we concentrate on sharing of subterms in a confluent variant of the weak λ-calculus. We introduce a labeling of this calculus that expresses a confluent theory of reductions with sharing, independent of the reduction strategy. We finally state that Wadsworth’s evaluation technique with sharing of subterms corresponds to our formal setting.

Tomasz Blanc, Jean-Jacques Lévy, Luc Maranget

Term Rewriting Meets Aspect-Oriented Programming

Abstract

We explore the connection between term rewriting systems (TRS) and aspect-oriented programming (AOP). Term rewriting is a paradigm that is used in fields such as program transformation and theorem proving. AOP is a method for decomposing software, complementary to the usual separation into programs, classes, functions, etc. An aspect represents code that is scattered across the components of an otherwise orderly decomposed system. Using AOP, such code can be modularized into aspects and then automatically weaved into a system.

Aspect weavers are available for only a handful of languages. Term rewriting can offer a method for the rapid prototyping of weavers for more languages. We explore this claim by presenting a simple weaver implemented as a TRS.

We also observe that TRS can benefit from AOP. For example, their flexibility can be enhanced by factoring out hardwired code for tracing and logging rewrite rules. We explore methods for enhancing TRS with aspects and present one application: automatically connecting an interactive debugger to a language specification.

Paul Klint, Tijs van der Storm, Jurgen Vinju

Observing Reductions in Nominal Calculi Via a Graphical Encoding of Processes

Abstract

The paper introduces a novel approach to the synthesis of labelled transition systems for calculi with name mobility. The proposal is based on a graphical encoding: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph).

Ranked graphs are naturally equipped with a few algebraic operations, and they are proved to form a suitable (bi)category of cospans. Then, as proved by Sassone and Sobocinski, the synthesis mechanism based on relative pushout, originally proposed by Milner and Leifer, can be applied. The resulting labelled transition system has ranked graphs as both states and labels, and it induces on (encodings of) processes an observational equivalence that is reminiscent of early bisimilarity.

Fabio Gadducci, Ugo Montanari

Primitive Rewriting

Abstract

Undecidability results in rewriting have usually been proved by reduction from undecidable problems of Turing machines or, more recently, from Post’s Correspondence Problem. Another natural candidate for proofs regarding term rewriting is Recursion Theory, a direction we promote in this contribution.

We present some undecidability results for “primitive” term rewriting systems, which encode primitive-recursive definitions, in the manner suggested by Klop. We also reprove some undecidability results for orthogonal and non-orthogonal rewriting by applying standard results in recursion theory.

Nachum Dershowitz

Infinitary Rewriting: From Syntax to Semantics

Abstract

Rewriting is the repeated transformation of a structured object according to a set of rules. This simple concept has turned out to have a rich variety of elaborations, giving rise to many different theoretical frameworks for reasoning about computation. Aside from its theoretical importance, rewriting has also been a significant influence on the design and implementation of real programming languages, most notably the functional and logic programming families of languages. For a theoretical perspective on the place of rewriting in Computer Science, see for example [14]. For a programming language perspective, see for example [16].

Richard Kennaway, Paula Severi, Ronan Sleep, Fer-Jan de Vries

Reducing Right-Hand Sides for Termination

Abstract

We propose two transformations on term rewrite systems (TRSs) based on reducing right-hand sides: one related to the transformation order and a variant of dummy elimination. Under mild conditions we prove that the transformed system is terminating if and only if the original one is terminating. Both transformations are very easy to implement, and make it much easier to prove termination of some TRSs automatically.

Hans Zantema

Reduction Strategies for Left-Linear Term Rewriting Systems

Abstract

Huet and Lévy (1979) showed that needed reduction is a normalizing strategy for orthogonal (i.e., left-linear and non-overlapping) term rewriting systems. In order to obtain a decidable needed reduction strategy, they proposed the notion of strongly sequential approximation. Extending their seminal work, several better decidable approximations of left-linear term rewriting systems, for example, NV approximation, shallow approximation, growing approximation, etc., have been investigated in the literature. In all of these works, orthogonality is required to guarantee approximated decidable needed reductions are actually normalizing strategies. This paper extends these decidable normalizing strategies to left-linear overlapping term rewriting systems. The key idea is the balanced weak Church-Rosser property. We prove that approximated external reduction is a computable normalizing strategy for the class of left-linear term rewriting systems in which every critical pair can be joined with root balanced reductions. This class includes all weakly orthogonal left-normal systems, for example, combinatory logic CL with the overlapping rules pred ·(succ ·x) →x and succ ·(pred ·x) →x, for which leftmost-outermost reduction is a computable normalizing strategy.

Yoshihito Toyama

Higher-Order Rewriting: Framework, Confluence and Termination

Abstract

Equations are ubiquitous in mathematics and in computer science as well. This first sentence of a survey on first-order rewriting borrowed again and again characterizes best the fundamental reason why rewriting, as a technology for processing equations, is so important in our discipline [10]. Here, we consider higher-order rewriting, that is, rewriting higher-order functional expressions at higher-types. Higher-order rewriting is a useful generalization of first-order rewriting: by rewriting higher-order functional expressions, one can process abstract syntax as done for example in program verification with the prover Isabelle [27]; by rewriting expressions at higher-types, one can implement complex recursion schemas in proof assistants like Coq [12].

Jean-Pierre Jouannaud

Timing the Untimed: Terminating Successfully While Being Conservative

Abstract

There have been several timed extensions of ACP-style process algebras with successful termination. None of them, to our knowledge, are equationally conservative (ground-)extensions of ACP with successful termination. Here, we point out some design decisions which were the possible causes of this misfortune and by taking different decisions, we propose a spectrum of timed process algebras ordered by equational conservativity ordering.

J. C. M. Baeten, M. R. Mousavi, M. A. Reniers

Confluence of Graph Transformation Revisited

Abstract

It is shown that it is undecidable in general whether a terminating graph rewriting system is confluent or not—in contrast to the situation for term and string rewriting systems. Critical pairs are introduced to hypergraph rewriting, a generalisation of graph rewriting, where it turns out that the mere existence of common reducts for all critical pairs of a graph rewriting system does not imply local confluence. A Critical Pair Lemma for hypergraph rewriting is then established which guarantees local confluence if each critical pair of a system has joining derivations that are compatible in that they map certain nodes to the same nodes in the common reduct.

Detlef Plump

Compositional Reasoning for Probabilistic Finite-State Behaviors

Abstract

We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s simple probabilistic automata. We consider strong bisimulation and observational equivalence, and provide complete axiomatizations for a language that includes parallel composition and (guarded) recursion. The presence of the parallel composition introduces various technical difficulties and some restrictions are necessary in order to achieve complete axiomatizations.

Yuxin Deng, Catuscia Palamidessi, Jun Pang

Finite Equational Bases in Process Algebra: Results and Open Questions

Abstract

Van Glabbeek (1990) presented the linear time/branching time spectrum of behavioral equivalences for finitely branching, concrete, sequential processes. He studied these semantics in the setting of the basic process algebra BCCSP, and tried to give finite complete axiomatizations for them. Obtaining such axiomatizations in concurrency theory often turns out to be difficult, even in the setting of simple languages like BCCSP. This has raised a host of open questions that have been the subject of intensive research in recent years. Most of these questions have been settled over BCCSP, either positively by giving a finite complete axiomatization, or negatively by proving that such an axiomatization does not exist. Still some open questions remain. This paper reports on these results, and on the state-of-the-art in axiomatizations for richer process algebras with constructs like sequential and parallel composition.

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Bas Luttik

Skew and ω-Skew Confluence and Abstract Böhm Semantics

Abstract

Skew confluence was introduced as a characterization of non-confluent term rewriting systems that had unique infinite normal forms or Böhm like trees. This notion however is not expressive enough to deal with all possible sources of non-confluence in the context of infinite terms or terms extended with letrec. We present a new notion called ω-skew confluence which constitutes a sufficient and necessary condition for uniqueness. We also present a theory that can lift uniqueness results from term rewriting systems to rewriting systems on terms with letrec. We present our results in the setting of Abstract Böhm Semantics, which is a generalization of Böhm like trees to abstract reduction systems.

Zena M. Ariola, Stefan Blom

A Mobility Calculus with Local and Dependent Types

Abstract

We introduce an ambient-based calculus that combines ambient mobility with process mobility, uses group names to collect ambients with homologous features, and exploits co-moves and runtime type checking to implement flexible policies for controlling process activities. Types rely on group names and, to support dynamicity, may depend on group variables. Policies can dynamically change also through installation of co-moves. The compliance with ambient policies can be checked locally to the ambients and requires no global assumptions. We prove that the type assignment system and the operational semantics of the calculus are ‘sound’, and define a sound and complete type inference algorithm which, when applied to terms whose type decorations only express the desired policies, computes the minimal type annotations required for their execution. As an application of our calculus, we present a couple of examples and linger on the setting up of policies for controlling the activities of the entities involved.

Mario Coppo, Federico Cozzi, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, Rosario Pugliese

Model Theory for Process Algebra

Abstract

We present a first-order extension of the algebraic theory about processes known as ACP and its main models. Useful predicates on processes, such as deadlock freedom and determinism, can be added to this theory through first-order definitional extensions. Model theory is used to analyse the discrepancies between identity in the models of the first-order extension of ACP and bisimilarity of the transition systems extracted from these models, and also the discrepancies between deadlock freedom in the models of a suitable first-order definitional extension of this theory and deadlock freedom of the transition systems extracted from these models. First-order definitions are material to the formalization of an interpretation of one theory about processes in another. We give a comprehensive example of such an interpretation too.

Jan A. Bergstra, C. A. (Kees) Middelburg

Expression Reduction Systems and Extensions: An Overview

Abstract

Expression Reduction Systems is a formalism for higher-order rewriting, extending Term Rewriting Systems and the lambda-calculus. Here we give an overview of results in the literature concerning ERSs. We review confluence, normalization and perpetuality results for orthogonal ERSs. Some of these results are extended to orthogonal conditional ERSs. Further, ERSs with patterns are introduced and their confluence is discussed. Finally, higher-order rewriting is translated into equational first-order rewriting. The technique develops an isomorphic model of ERSs with variable names, based on de Bruijn indices.

John Glauert, Delia Kesner, Zurab Khasidashvili

Axiomatic Rewriting Theory I: A Diagrammatic Standardization Theorem

Abstract

By extending nondeterministic transition systems with concurrency and copy mechanisms, Axiomatic Rewriting Theory provides a uniform framework for a variety of rewriting systems, ranging from higher-order systems to Petri nets and process calculi. Despite its generality, the theory is surprisingly simple, based on a mild extension of transition systems with independence: an axiomatic rewriting system is defined as a 1-dimensional transition graph \(\mathcal{G}\) equipped with 2-dimensional transitions describing the redex permutations of the system, and their orientation. In this article, we formulate a series of elementary axioms on axiomatic rewriting systems, and establish a diagrammatic standardization theorem.

Paul-André Melliès

Backmatter