Special Issue: Selected Papers of the Conference ''International Colloquium on Automata, Languages and Programming 2008''

2008 Editors: Giuseppe Castagna, Igor Walukiewicz,Andrzej Tarlecki

This special issue of Logical Methods in Computer Science contains the revised and extended versions of five articles selected from those presented at the Track B of the 35th International Colloquium on Automata, Languages and Programming (ICALP 2008). The meeting took place in Reykjavik, Iceland form July the 6th to the 13th, 2008. The ICALP colloquium is the main annual meeting of the European Association for Theoretical Com- puter Science (EATCS). Among the three tracks of the conference, Track B is devoted to logic, semantics, and theory of programming.

The article *On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases* by Bernard Boigelot, Julien Brusten, and Véronique Bruyère gives precise characterization of the sets of real numbers that are recognizable in multiple bases, and provides a theoretical justification to the use of weak automata as symbolic representations of sets.

The article *Tree languages defined in first-order logic with one quantifier alternation* by Mikolaj Bojanczyk and Luc Segoufin shows an effective characterization of tree and forest languages definable in Δ2 fragment of first-order logic.

The article *A Theory of Explicit Substitutions with Safe and Full Composition* by Delia Kesner solves an old problem of finding a system with explicit substitutions that enjoys all the good properties one expects from such a system, namely, full composition, faithfulness of the representation of β-conversion, strong normalisation and confluence.

The article *A Type System For Call-By-Name Exceptions* by Sylvain Lebresne presents a type system for a polymorphic call-by-name language with exceptions whose central idea is to enrich the type system with an operator for corruption. Using corruption, and an appropriate subtyping system, one obtains a rather flexible type system whose soundness is proved by resorting to realizability semantics.

The article *Weighted Logics for Nested Words and Algebraic Formal Power Series* by Christian Mathissen exhibits characterizations of algebraic formal power series in terms of weighted logics.

We thank the authors for their contributions. For inclusion in this special issues all articles underwent a new and complete reviewing process. We are grateful to the reviewers for their valuable feedback. We also thank the members of the Program Committee of ICALP 2008 and their sub-referees who contributed to the selection and the refereeing process.

Giuseppe Castagna and Igor Walukiewicz
Guest Editors

1. Tree Languages Defined in First-Order Logic with One Quantifier Alternation

Mikolaj Bojanczyk ; Luc Segoufin.

We study tree languages that can be defined in \Delta_2 . These are tree languages definable by a first-order formula whose quantifier prefix is forall exists, and simultaneously by a first-order formula whose quantifier prefix is . For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. We provide an effective characterization of tree and forest languages definable in \Delta_2 . This characterization is in terms of algebraic equations. Over words, the class of word languages definable in \Delta_2 forms a robust class, which was given an effective algebraic characterization by Pin and Weil.

2. A Theory of Explicit Substitutions with Safe and Full Composition

Delia Kesner.

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.

3. A Type System For Call-By-Name Exceptions

Sylvain Lebresne.

We present an extension of System F with call-by-name exceptions. The type system is enriched with two syntactic constructs: a union type for programs whose execution may raise an exception at top level, and a corruption type for programs that may raise an exception in any evaluation context (not necessarily at top level). We present the syntax and reduction rules of the system, as well as its typing and subtyping rules. We then study its properties, such as confluence. Finally, we construct a realizability model using orthogonality techniques, from which we deduce that well-typed programs are weakly normalizing and that the ones who have the type of natural numbers really compute a natural number, without raising exceptions.

4. On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases

Bernard Boigelot ; Julien Brusten ; Veronique Bruyere.

This article studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak deterministic automata, used as symbolic set representations in actual applications. In previous work, it has been established that the sets of numbers that are recognizable by weak deterministic automata in two bases that do not share the same set of prime factors are exactly those that are definable in the first order additive theory of real and integer numbers. This result extends Cobham's theorem, which characterizes the sets of integer numbers that are recognizable by finite automata in multiple bases. In this article, we first generalize this result to multiplicatively independent bases, which brings it closer to the original statement of Cobham's theorem. Then, we study the sets of reals recognizable by Muller automata in two bases. We show with a counterexample that, in this setting, Cobham's theorem does not generalize to multiplicatively independent bases. Finally, we prove that the sets of reals that are recognizable by Muller automata in two bases that do not share the same set of prime factors are exactly those definable in the first order additive theory of real and integer numbers. These sets are thus also recognizable by weak deterministic automata. This result leads to a precise characterization of the sets of real numbers that are recognizable in […]

5. Weighted Logics for Nested Words and Algebraic Formal Power Series

Christian Mathissen.

Nested words, a model for recursive programs proposed by Alur and Madhusudan, have recently gained much interest. In this paper we introduce quantitative extensions and study nested word series which assign to nested words elements of a semiring. We show that regular nested word series coincide with series definable in weighted logics as introduced by Droste and Gastin. For this we establish a connection between nested words and the free bisemigroup. Applying our result, we obtain characterizations of algebraic formal power series in terms of weighted logics. This generalizes results of Lautemann, Schwentick and Therien on context-free languages.