Catálogo de publicaciones - libros

The -spectrum of a word is the multiset of its non-contiguous subwords of length . For given , how small can be for a pair of different words of length to exist, with equal - spectra? From the Thue-Morse word we find that is at most 2. The construction of this paper decreases this upper bound to , where 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.

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.

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.

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.

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 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 closed under beta conversion iff can be endowed with the structure of a numeral system with predecessor iff there is a Church delta (conditional) for iff every Ershov morphism with domain can be represented by a lambda term.

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.

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

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.

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

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.