Catálogo de publicaciones - libros

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].

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.

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 ·( ·) → and ·( ·) →, for which leftmost-outermost reduction is a computable normalizing strategy.

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 , 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].

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.

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.

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.

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.

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.

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 on group variables. Policies can dynamically change also through installation of co-moves. The compliance with ambient policies can be checked 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.