2008

Editors: Giuseppe Castagna, Igor Walukiewicz,Andrzej Tarlecki

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.

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.

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.

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 multiple bases, and […]

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.