Term Rewriting Systems
For a Turing-complete computational model such as term rewriting, it is natural to ask about the decidability (in the general case or in specific cases) of certain properties, such as the accessibility of a given term from another by rewriting, strong termination (all rewriting sequences terminate), or confluence (two divergent rewriting sequences can always converge to the same term).
Ground reducibility is one of the few properties that can be decided for all rewriting systems. This property is central to certain approaches to automatic inductive theorem proving. We studied its resolution by reduction to decision problems for tree automata with local constraints with Hubert Comon and established its exact complexity (EXPTIME-completeness) later LICS’97 and IC’03.
Furthermore, I have resolved (negatively) the open problem of the decidability of accessibility and confluence for flat term rewriting systems, using a reduction that was later improved here. Guillem Godoy and I have shown, using tree automaton techniques, that the problem of uniqueness of normal forms, which expresses that a given term rewriting system, viewed as a computational procedure, is functional, is decidable for flat and linear systems and undecidable for flat and right-linear systems.
The problem of rigid unification was introduced to extend proof methods in first-order logic with equality, such as tables and matings. The idea is that the variables in equations are no longer assumed to be universally quantified as in classical unification procedures in proof and logic programming, but are rigid, in the sense that each variable can only be instantiated once in a proof (it is non-rewritable, i.e., the different instantiations of variables in a proof must be consistent). Together with Harald Ganzinger, Margus Veanes, we introduced the problem of rigid accessibility, which generalizes the previous one by orienting the direction of application of the equations (which corresponds in a way to the transition from equation reasoning to calculation). We conducted an in-depth study of the boundary between decidability and undecidability of simultaneous and non-simultaneous variants of the problem (ASIAN’98, ICALP’99, IJFCS’00), which proved to be more difficult than rigid unification. The cases of decidability were established using tree automata techniques.
Numerous studies deal with the closure of standard tree automata languages by rewriting, like this contribution during my thesis. Together with Francis Klay and Camille Vacher (LATA’09 and IC’11), we analyzed the closure of rigid tree automata by rewriting, with an algorithm for deciding membership in this closure. We also studied the problem of regular model checking in the case of applying rewriting with specific strategies. With Andrea Gascon and Guillem Godoy, we have shown the unexpected result that the application of the innermost strategy, which is analogous to call-by-value in functional languages, gives better results for regular model checking than standard rewriting: the closure of a tree automaton language by a flat rewriting system is a tree automaton language with local constraints of a simple type, having good properties.
We also studied with Masahiko Sakai and Yoshiharu Kojima the control of term rewriting by contextual conditions expressed by tree automata, i.e., the selection of rewriting positions using automata computation. This study was motivated by the problems of analyzing updates and XML access control policies presented, insofar as in practice, update application positions are generally selected by XPath expressions.