|
A formal language is a set of words, formed on an alphabet of symbols. The theory of formal languages was born out of concern:
- Logicists who wanted to formally define mathematical discourse.
- linguists, who wanted to model natural languages,
- computer scientists who wanted to rigorously specify programming languages.
These initial motivations have led to the development of new mathematical concepts such as grammars and automata that allow the definition of formal languages. Links between these concepts and the more classical notions of logical formulae or algebraic structures (in particular that of semi-groups) have been established.
The theory was then extended to objects more complex than the usual words: infinite words, trees, graphs (finite or infinite), simple complexes, etc.
For each type of description and object we try to determine which properties of languages can be computed and with what efficiency. A generic result for this type of concern would be: given a language L (presented by a finite description "D" of size n), and a property P (in such a class of properties), we can decide, in time O(f(n)), if L verifies P. The comparison of the different description methods is also an objective of the theory. A typical question is the comparison between the class of definable languages in a given logic and the class of languages recognizable by a given class of monoids or automata.
This theory finds new applications in fields close to its origins (computational linguistics, documentary research, for example), and is regularly enriched by contact with problems from other scientific fields: process semantics, parallelism modeling, verification of computer systems, graph theory, combinatorial group theory, topology, genomics, etc.
Problems studied
Here are some of the problems that the Formal Methods team has been particularly concerned with:
- Problems of equivalence of automata on words; extension to the comparison of transductions, trees, graphs.
- Rewriting of words or terms: reduction strategies, descendant language, termination.
- Number sequences (integer or rational) recognised by stacked automata ... of stacks.
- Rational languages in monoids: recognition by automata, closure properties, algorithmic problems on these languages.
- Characterisation of properties of subgroups of free groups by properties of the automata that represent them (Stallings representation)
- Semi-switching and Mazurkiewicz traces: construction of distributed automata, closure problems, algorithmic problems, algebra and logic.
- Equations in monoids: problem of satisfiability, operations on monoids preserving the decidability of systems of equations, decidable fragments of first-order logic.
- Solving the word problem in sub monoids of free profinite monoids.
- Topology of particular profinite monoids: generalisation of properties like Ribes and Zalesskii's (a product of finitely generated subgroups of the free group is closed for the profinite topology).
|
