Circular splicing has been very recently introduced to model a specific recombinant behaviour of circular DNA, continuing the investigation initiated with linear splicing. In this paper we restrict our study to the relationship between regular circular languages and languages generated by finite circular splicing systems and provide some results towards a characterization of the intersection between these two classes. We consider the class of languages X*, called here star languages, which are closed under conjugacy relation and with X being a regular language. Using automata theory and combinatorial techniques on words, we show that for a subclass of star languages the corresponding circular languages are (Paun) circular splicing languages. For example, star languages belong to this subclass when X* is a free monoid or X is a finite set. We also prove that each (Paun) circular splicing language L over a one-letter alphabet has the form L = X+ ∪ Y, with X,Y finite sets satisfying particular hypotheses. Cyclic and weak cyclic languages, which will be introduced in this paper, show that this result does not hold when we increase the size of alphabets, even if we restrict ourselves to regular languages.

This paper is the first step in thesolution of the problem of finite completion of comma-free codes.We show that every finite comma-free code is included in afinite comma-free code of particular kind, which we called, for lack of a better term, canonical comma-free code. Certainly, finite maximal comma-free codesare always canonical. The final step of the solution which consistsin proving further that every canonical comma-free code is completedto a finite maximal comma-free code, is intended to be published in a forthcomingpaper.

In 1978, Courcelle asked for a complete set of axioms and rules for the equational theory of (discrete regular) words equipped with the operations of product, omega power and omega-op power. In this paper we find a simple set of equations and prove they are complete. Moreover, we show that the equational theory is decidable in polynomial time.

This paper is a sequel to anearlier paper of the present author, in which it was proved thatevery finite comma-free code is embedded into a so-called (finite)canonical comma-free code. In this paper, it is proved that every(finite) canonical comma-free code is embedded into a finite maximal comma-freecode, which thus achieves the conclusion that every finite comma-freecode has finite completions.


The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces $\boldsymbol{\Lambda_\mu^+}$, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

We give a linear time algorithm which, given a simply connected figure of the plane divided into cells, whose boundary is crossed by some colored inputs and outputs, produces non-intersecting directed flow lines which match inputs and outputs according to the colors, in such a way that each edge of any cell is crossed by at most one line. The main tool is the notion of height function, previously introduced for tilings. It appears as an extension of the notion of potential of a flow in a planar graph.

We exhibit a new class of grammars with the help of weightfunctions. They are characterized by decreasing the weight during the derivation process. A decision algorithm for the emptiness problem is developed. This class contains non-contextfree grammars. The corresponding language class is identical to the class of ultralinear languages.

We present a description of asymptotic behaviour of languages of bi-infinite words obtained by iterating morphisms defined on free monoids.

We show that the class of groups which have monoid presentations by means of finite special [λ]-confluent string-rewriting systems strictly contains the class of plain groups (the groups which are free products of a finitely generated free group and finitely many finite groups), and that any group which has an infinite cyclic central subgroup can be presented by such a string-rewriting system if and only if it is the direct product of an infinite cyclic group and a finite cyclic group.

The question of how to combine monads arises naturally in many areas with much recent interest focusing on the coproduct of two monads. In general, the coproduct of arbitrary monads does not always exist. Although a rather general construction was given by Kelly  [Bull.  Austral. Math. Soc.22 (1980) 1–83], its generality is reflected in its complexity which limits the applicability of this construction. Following our own research [C. Lüth and N. Ghani, Lect. Notes Artif. Intell.2309 (2002) 18–32], and that of Hyland, Plotkin and Power [IFIP Conf. Proc.223 (2002) 474–484], we are looking for specific situations when simpler constructions are available. This paper uses fixed points to give a simple construction of the coproduct of two ideal monads.

This paper investigates one possible model of reversible computations, animportant paradigm in the context of quantum computing. Introduced byBennett, a reversible pebble game is anabstraction of reversible computation that allows to examine the space andtime complexity of various classes of problems. We present a techniquefor proving lower and upper bounds on time and space complexity for severaltypes of graphs. Using this technique we show that the time needed toachieve optimal space for chain topology is Ω(nlgn) for infinitelymany n and we discusstime-space trade-offs for chain. Further we show a tight optimalspace bound for the binary tree of height h of the form h + Θ(lg*h)and discuss space complexity for the butterfly. These results give anevidence that reversible computations need more resources than standardcomputations. We also show an upper bound on time and space complexity ofthe reversible pebble game based on the time and space complexity of thestandard pebble game, regardless of the topology of the graph.

We study the complexity of the infinite word uβ associated with theRényi expansion of 1 in an irrational base β > 1.When β is the golden ratio, this is the well known Fibonacci word,which is Sturmian, and of complexity C(n) = n + 1.For β such thatdβ(1) = t1t2...tm is finite we provide a simple description ofthe structure of special factors of the word uβ . When tm =1we show thatC(n) = (m - 1)n + 1. In the cases when t1 = t2 = ... tm-1 ort1 > max{t2,...,tm-1 } we show that the first differenceof the complexity function C(n + 1) - C(n ) takes value in{m - 1,m} for every n, and consequently we determine thecomplexity of uβ . We show thatuβ is an Arnoux-Rauzy sequence if and only ifdβ(1) = tt...t1. On the example ofβ = 1 + 2cos(2π/7), solution of X3 = 2X2 + X - 1, we illustratethat the structure of special factors is more complicated fordβ (1) infinite eventually periodic.The complexity for this word is equal to 2n+1.

We provide alternative proofs and algorithms for results proved by Sénizergues on rational and recognizable free group languages. We consider two different approaches to the basic problem of deciding recognizability for rational free group languages following two fully independent paths: the symmetrification method (using techniques inspired by the study of inverse automata and inverse monoids) and the right stabilizer method (a general approach generalizable to other classes of groups). Several different algorithmic characterizations of recognizability are obtained, as well as other decidability results.

We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog.
Succinctness of the languages is closely related to the combined and parameterised complexity of query evaluation for these languages.

We introduce the notion of a differentiation function of a context-free grammar which gives the number of terminal words that can be derived in a certain number of steps. A grammar is called narrow (or k-narrow) iff its differentiation function is bounded by a constant (by k). We present the basic properties of differentiation functions, especially we relate them to structure function of context-free languages and narrow grammars to slender languages. We discuss the decidability of the equivalence of grammars with respect to the differentiation function and structure function and prove the decidability of the k-narrowness of context-free grammars. Furthermore, we introduce languages representing the graph of the differentiation and structure function and relate these languages to those of the Chomsky hierarchy.

This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations.

This paper establishes computational equivalence of two seemingly unrelated concepts: linear conjunctive grammars and trellis automata. Trellis automata, also studied under the name of one-way real-time cellular automata, have been known since early 1980s as a purely abstract model of parallel computers, while linear conjunctive grammars, introduced a few years ago, are linear context-free grammars extended with an explicit intersection operation. Their equivalence implies the equivalence of several other formal systems, including a certain restricted class of Turing machines and a certain type of language equations, thus giving further evidence for the importance of the language family they all generate.

We add a sufficient condition for validity of Propo- sition 4.10 in the paper Frougny et al. (2004). This condition is not a necessary one, it is nevertheless convenient, since anyway most of the statements in the paper Frougny et al. (2004) use it.