Rigid Reachability

  • Harald Ganzinger
  • Florent Jacquemard
  • Margus Veanes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)


We show that rigid reachability, the non-symmetric form of rigid E-unification, is undecidable already in the case of a single constraint. From this we infer the undecidability of a new rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are P-complete in the equational case become EXPTIME-complete when symmetry is absent. By applying automata-theoretic methods, simultaneous monadic rigid reachability with ground rules is shown to be in EXPTIME.


Function Symbol Ground Rule Ground Term Tree Automaton Ground Instance 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.Google Scholar
  2. 2.
    J.-L. Coquidé and R. Gilleron. Proofs and reachability problem for ground rewrite systems. In Proc. of the 6th International Meeting of Young Computer Scientists, volume 464 of LNCS, pages 120–129, 1990.Google Scholar
  3. 3.
    J.L. Coquidé, M. Dauchet, R. Gilleron, and S. Vágvölgyi. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science, 127:69–98, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    V. Cortier. PSPACE-completeness of monadic simultaneous rigid reachability. Unpublished manuscript, july 1998.Google Scholar
  5. 5.
    M. Dauchet. Rewriting and tree automata. In H. Comon and J.P. Jouannaud, editors, Term Rewriting (French Spring School of Theoretical Computer Science), volume 909 of Lecture Notes in Computer Science, pages 95–113. Springer Verlag, Font Romeux, France, 1993.Google Scholar
  6. 6.
    Max Dauchet, Thierry Heuillard, Pierre Lescanne, and Sophie Tison. The confluence of ground term rewriting systems is decidable. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, 1988.Google Scholar
  7. 7.
    A. Degtyarev, Yu. Gurevich, P. Narendran, M. Veanes, and A. Voronkov. The decidability of simultaneous rigid E-unification with one variable. In T. Nipkow, editor, Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 181–195. Springer Verlag, 1998.CrossRefGoogle Scholar
  8. 8.
    A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995.Google Scholar
  9. 9.
    N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–309. North Holland, Amsterdam, 1990.Google Scholar
  10. 10.
    J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406–451, 1970.zbMATHMathSciNetCrossRefGoogle Scholar
  11. 11.
    W.M. Farmer. Simple second-order languages for which unification is undecidable. Theoretical Computer Science, 87:25–41, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Thom Frühwirth, Ehud Shapiro, Moshe Y.Vardi, and Eyal Yardemi. Logic programs as types for logic programs. In 6th IEEE Symp. Logic In Computer Science, pages 300–309, 1991.Google Scholar
  13. 13.
    J.H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338–346. IEEE Computer Society Press, July 1988.Google Scholar
  14. 14.
    J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338–346. IEEE Computer Society Press, 1987.Google Scholar
  15. 15.
    W.D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Y. Gurevich and M. Veanes. Partisan corroboration, and shifted pairing. Research Report MPI-I-98-2-014, Max-Planck-Institut für Informatik, September 1998.Google Scholar
  17. 17.
    Y. Gurevich and A. Voronkov. Monadic simultaneous rigid E-unification and related problems. In P. Degano, R. Corrieri, and A. Marchetti-Spaccamella, editors, Automata, Languages and Programming, 24th International Colloquium, ICALP’97, volume 1256 of Lecture Notes in Computer Science, pages 154–165. Springer Verlag, 1997.Google Scholar
  18. 18.
    D. Kozen. Complexity of finitely presented algebras. In Proc. 9th STOC, pages 164–177, 1977.Google Scholar
  19. 19.
    J. Levy. Decidable and undecidable second-order unification problems. In T. Nipkow, editor, Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March/April 1998, Proceedings, volume 1379 of Lecture Notes in Computer Science, pages 47–60. Springer Verlag, 1998.Google Scholar
  20. 20.
    J. Levy and M. Veanes. On the undecidability of second-order unification. Submitted to Information and Computation, 1998.Google Scholar
  21. 21.
    Helmut Seidl. Haskell overloading is dexptime-complete. Inf. Process. Letters, 52:57–60, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    J.W. Thatcher and J.B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57–81, 1968.CrossRefMathSciNetGoogle Scholar
  23. 23.
    M. Veanes. The relation between second-order unification and simultaneous rigid E-unification. In Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science, June 21–24, 1998, Indianapolis, Indiana (LICS’98), pages 264–275. IEEE Computer Society Press, 1998.Google Scholar
  24. 24.
    Margus Veanes. On computational complexity of basic decision problems of finite tree automata. Technical Report 133, Computing Science Department, Uppsala University, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Harald Ganzinger
    • 1
  • Florent Jacquemard
    • 1
  • Margus Veanes
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany

Personalised recommendations