Ground reducibility is EXPTIME-complete

Autor: Hubert Comon, Florent Jacquemard
Přispěvatelé: Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Verification in databases (DAHU), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), INRIA, Jacquemard, Florent
Rok vydání: 2003
Předmět:
Polynomial
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES
Computational complexity theory
2-EXPTIME
Deterministic algorithm
[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]
EXPTIME
0102 computer and information sciences
02 engineering and technology
computational complexity
01 natural sciences
tree automata
Theoretical Computer Science
Combinatorics
Deterministic automaton
term rewriting
0202 electrical engineering
electronic engineering
information engineering
Two-way deterministic finite automaton
Tree automaton
Mathematics
Discrete mathematics
Linear bounded automaton
ground reducbility
Pushdown automaton
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
16. Peace & justice
Computer theorem-proving
Computer Science Applications
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
010201 computation theory & mathematics
020201 artificial intelligence & image processing
Tree (set theory)
inductive theorem proving
complexity
Alternating Turing machine
Computer Science::Formal Languages and Automata Theory
rewriting systems
Information Systems
Zdroj: LICS
Information and Computation
Information and Computation, 2003, 187 (1), pp.123-153
[Research Report] RR-3800, INRIA. 1999, pp.26
Information and Computation, Elsevier, 2003, 187 (1), pp.123-153
ISSN: 0890-5401
1090-2651
DOI: 10.1016/s0890-5401(03)00134-2
Popis: We prove that ground reducibility is EXPTIME-complete in the general case. EXPTIME-hardness is proved by encoding the computations of an alternating Turing machine whose space is polynomially bounded. It is more difficult to show that ground reducibility belongs to DEXPTIME. We associate first an automaton with disequality constraints A/sub R,t/ to a rewrite system R and a term t. This automaton is deterministic and accepts a term u if and only if t is not ground reducible by R. The number of states of A/sub R,t/ is O(2/sup /spl par/R/spl par//spl times//spl par/t/spl par//) and the size of the constraints are polynomial in the size of R,t. Then we prove some new pumping lemmas, using a total ordering on the computations of the automaton. Thanks to these lemmas, we can give an upper bound to the number of distinct subtrees of a minimal successful computation of an automaton with disequality constraints. It follows that emptiness of such an automaton can be decided in time polynomial in the number of its states and exponential in the size of its constraints. Altogether, we get a simply exponential deterministic algorithm for ground reducibility.
Databáze: OpenAIRE
Externí odkaz: