Skip to main content
SpringerLink
Log in

The Existential Fragment of the One-Step Parallel Rewriting Theory

  • Conference paper
Rewriting Techniques and Applications (RTA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5595))

Included in the following conference series:

Abstract

It is known that the first-order theory with a single predicate → that denotes a one-step rewriting reduction on terms is undecidable already for formulae with ∃ ∀ prefix. Several decidability results exist for the fragment of the theory in which the formulae start with the ∃ prefix only. This paper considers a similar fragment for a predicate →p which denotes the parallel one-step rewriting reduction. We show that the first-order theory of →p is undecidable already for formulae with ∃ 7 prefix and left-linear rewrite systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alouini, I., Kirchner, C.: Toward the concurrent implementation of computational systems. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 1–31. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  2. Assmann, U.: Graph rewrite systems for program optimization. ACM Trans. Program. Lang. Syst. 22(4), 583–637 (2000)

    Article  Google Scholar 

  3. Caron, A.-C., Seynhaeve, F., Tison, S., Tommasi, M.: Deciding the satisfiability of quantifier free formulae on one-step rewriting. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 103–117. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Goguen, J., Kirchner, C., Meseguer, J.: Concurrent term rewriting as a model of computation. In: Fasel, J.H., Keller, R.M. (eds.) Graph Reduction 1986. LNCS, vol. 279, pp. 53–93. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  5. Jacquemard, F.: Automates d’arbres et Réécriture de termes. PhD thesis, Université de Paris-Sud (1996)

    Google Scholar 

  6. Limet, S., Réty, P.: A new result about the decidability of the existential one-step rewriting theory. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 118–132. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Levy, J., Veanes, M.: On the undecidability of second-order unification. Information and Computation 159(1-2), 125–150 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  8. Marcinkowski, J.: Undecidability of the first order theory of one-step right ground rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  9. Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. Niehren, J., Pinkal, M., Ruhrberg, P.: On equality up-to constraints over finite trees, context unification and one-step rewriting. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 34–48. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  11. Niehren, J., Treinen, R., Tison, S.: On rewrite constraints and context unification. Information Processing Letters 74(1-2), 35–40 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  12. Seynhaeve, F., Tommasi, M., Treinen, R.: Grid structures and undecidable constraint theories. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 357–368. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Seynhaeve, F., Tison, S., Tommasi, M., Treinen, R.: Grid structures and undecidable constraint theories. Theoretical Computer Science 1-2(258), 453–490 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  14. Tison, S.: Automates comme outil de décision dans les arbres. Dossier d’habilitation à diriger des recherches (December 1990) (in French)

    Google Scholar 

  15. Treinen, R.: The first-order theory of one-step rewriting is undecidable. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 276–286. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  16. Treinen, R.: The first-order theory of linear one-step rewriting is undecidable. Theoretical Computer Science 1-2(208), 149–177 (1998)

    MathSciNet  MATH  Google Scholar 

  17. Vorobyov, S.: The first-order theory of one step rewriting in linear noetheran systems is undecidable. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 254–268. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Vorobyov, S.: The undecidability of the first-order theories of one step rewriting in linear canonical systems. Inf. Comput. 174, 1–32 (2002)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, Warsaw University, ul. Banacha 2, 02-097, Warsaw, Poland

    Aleksy Schubert

  2. SoS Group NIII Faculty of Science, University of Nijmegen, The Netherlands

    Aleksy Schubert

Authors
  1. Aleksy Schubert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS, Université Paris Diderot - Paris 7, CNRS, Paris, France

    Ralf Treinen

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schubert, A. (2009). The Existential Fragment of the One-Step Parallel Rewriting Theory. In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02348-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02347-7

  • Online ISBN: 978-3-642-02348-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation