arXiv subjects

Geraud Senizergues

Publications and source records attributed to Geraud Senizergues.

2 recordsLinked to original sources

arXiv2015

Equations over free inverse monoids with idempotent variables

We introduce the notion of idempotent variables for studying equations in inverse monoids. It is proved that it is decidable in singly exponential time (DEXPTIME) whether a system of equations in idempotent variables over a free inverse monoid has a solution. The result is proved by a direct reduction to solve language equations with one-sided concatenation and a known complexity result by Baader and Narendran: Unification of concept terms in description logics, 2001. We also show that the problem becomes DEXPTIME hard , as soon as the quotient group of the free inverse monoid has rank at least two. Decidability for systems of typed equations over a free inverse monoid with one irreducible variable and at least one unbalanced equation is proved with the same complexity for the upper bound. Our results improve known complexity bounds by Deis, Meakin, and Senizergues: Equations in free inverse monoids, 2007. Our results also apply to larger families of equations where no decidability has been previously known.

cs.LO↗

arXiv2013

Bottom-up rewriting for words and terms

For the whole class of linear term rewriting systems, we define \emph{bottom-up rewriting} which is a restriction of the usual notion of rewriting. We show that bottom-up rewriting effectively inverse-preserves recognizability and analyze the complexity of the underlying construction. The Bottom-Up class (BU) is, by definition, the set of linear systems for which every derivation can be replaced by a bottom-up derivation. Membership to BU turns out to be undecidable, we are thus lead to define more restricted classes: the classes SBU(k), k in N of Strongly Bottom-Up(k) systems for which we show that membership is decidable. We define the class of Strongly Bottom-Up systems by SBU = U_{k in \} SBU(k). We give a polynomial sufficient condition for a system to be in $\SBU$. The class SBU contains (strictly) several classes of systems which were already known to inverse preserve recognizability: the inverse left-basic semi-Thue systems (viewed as unary term rewriting systems), the linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems.

cs.FL↗