Résumé : This is the story of two distinct approaches for understanding what are 'languages of words', namely 'algebra' and 'logic'. These two approaches eventually rejoined and now irrigate a vivid community of researchers in computer science. In this talk, I will try to give a broad picture of these two perspectives and intuitions on how they nicely interact. An overview:

- The algebraic point of view: words are element in a free algebra.
The first branch, language theory, is concerned with the description of languages of words seen as elements of the free monoid (generated by some finite set traditionally called the alphabet). As such, words are simply terms in some algebra in the sense of universal algebra. After the seminal works of Kleene and Rabin&Scott, that defined the key notion of regular language, this branch developed toward the analysis of the expressive power of restricted formalisms and machines for describing languages. The leading result here is Schützenberger's theorem which states that being definable by a star-free expression is the same as being recognised by an aperiodic monoid: a brilliant algebraic insight. This algebraic description in language theory nowadays catches up with general algebra and category theory, in particular via the use of monads.

- The model-theoretic point of view: words are relational structures.
The second branch, initiated by Büchi, Elgot, and Trakhtenbrot, is the logical point of view. Words are now seen as labelled chains: linear orders equipped with unary predicates (also called monadic). Now logical sentences are used to express properties over these labelled chains. This time MSO logic (monadic second-order logic, ie first-order logic extended with the ability to quantify over monadic predicates = sets) plays the central role, and turns out to be equivalent to regularity over finite words. But, from the point of view of a logician, there is no reason to restrict our attention to finite words: indeed Büchi soon shows the decidability of MSO over omega-words (ie. labelled chains of order type omega). Rabin then proves the remarkable decidability of MSO over the infinite binary tree, and as a consequence the decidability of MSO over the class of all countable linear chains. The composition method was then introduced by Shelah in a seminal work giving another proof of this decidability over countable linear orders, and establishing at the same time undecidability of the MSO theory over the reals: a brilliant model-theoretic insight. These results were then improved by Gurevitch and Shelah, showing decidability over some restricted forms of uncountable chains, and undecidability without extra set theoretic assumptions (the original result relying on CH).

The two branches have progressively converged and are now actively developed in theoretical computer science, in particular in relation with temporal logics, verification, and algorithmic model theory.

Keywords : logic algebra; decidability; language theory