Confluence: The Unifying, Expressive Power of Locality

  • Jiaxiang Liu
  • Jean-Pierre Jouannaud
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


Scientific fields undergo successive phases of specialization and unification.

The field of programming languages is in a phase of specialization. Among the main programming paradigms are imperative programming, functional programming, logic programming, object oriented programming, concurrent programming and distributed programming. Each of these fields is further specialized. For example, there are many different paradigms for functional programming: LISP, Mac Carthy’s original functional programming paradigm based on pure lambda-calculus for lists enriched with recursion; ML, Milner’s paradigm based on a typed lambda-calculus enriched with data types, a let construct and recursion which has become a standard; O’Donnel’s paradigm based on orthogonal rewriting; and OBJ, Goguen’s paradigm based on terminating rewriting in first-order algebra to cite a few. Similarly, logic programming has given rise to constraint logic programming, as well as query languages for data bases.


Logic Programming Local Peak Transitive Closure Coloured Version Functional Programming 
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.
    Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society 39, 472–482 (1936)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 243–320. North-Holland (1990)Google Scholar
  3. 3.
    Diaconescu, R., Futatsugi, K.: An overview of cafeobj. Electr. Notes Theor. Comput. Sci. 15, 285–298 (1998)CrossRefzbMATHGoogle Scholar
  4. 4.
    Felgenhauer, B.: Personnal communication (2013)Google Scholar
  5. 5.
    Felgenhauer, B.: Rule labeling for confluence of left-linear term rewrite systems. In: International Workshop on Confluence (2013)Google Scholar
  6. 6.
    Felgenhauer, B., van Oostrom, V.: Proof orders for decreasing diagrams. In: van Raamsdonk, F. (ed.) RTA. LIPIcs, vol. 21, pp. 174–189. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  7. 7.
    Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Jouannaud, J.-P., Li, J.: Church-rosser properties of normal rewriting. In: Cégielski, P., Durand, A. (eds.) CSL. LIPIcs, vol. 16, pp. 350–365. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  9. 9.
    Jouannaud, J.-P., Liu, J.: From diagrammatic confluence to modularity. Theor. Comput. Sci. 464, 20–34 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Jouannaud, J.-P., Okada, M.: A computation model for executable higher-order algebraic specification languages. In: LICS, pp. 350–361. IEEE Computer Society (1991)Google Scholar
  11. 11.
    Jouannaud, J.-P., van Oostrom, V.: Diagrammatic confluence and completion. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 212–222. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Kirchner, C.: Rho-calculi for computation and logic (invited talk). In: Tiwari, A. (ed.) RTA. LIPIcs, vol. 15, pp. 2–4. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  13. 13.
    Klop, J.W.: Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam (1980)Google Scholar
  14. 14.
    Donald, E.: Knuth and Peter B. Bendix. Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Elsevier (1970)Google Scholar
  15. 15.
    Meseguer, J.: Rewriting logic and maude: Concepts and applications. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 1–26. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Meseguer, J.: Maude. In: Padua, D.A. (ed.) Encyclopedia of Parallel Computing, pp. 1095–1102. Springer (2011)Google Scholar
  17. 17.
    Masaki, N., Weiqiang, K., Kazuhiro, O., Kokichi, F.: A specification translation from behavioral specifications to rewrite specifications. IEICE Transactions 91-D(5), 1492–1503 (2008)Google Scholar
  18. 18.
    Pottier, F.: An overview of Calphaml. Electr. Notes Theor. Comput. Sci. 148(2), 27–52 (2006)CrossRefGoogle Scholar
  19. 19.
    Saraswat, V.A.: The paradigm of concurrent constraint programming. In: ICLP, pp. 777–778 (1990)Google Scholar
  20. 20.
    Strub, P.-Y.: Coq modulo theory. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 529–543. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  21. 21.
    Terese: Term rewriting systems. In: Klop, J.W., et al. (eds.) Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)Google Scholar
  22. 22.
    Toyama, Y.: Commutativity of term rewriting systems. Programming of future generation computers II, pp. 393–407 (1988)Google Scholar
  23. 23.
    van Oostrom, V.: Confluence by decreasing diagrams. Theor. Comput. Sci. 126(2), 259–280 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    van Oostrom, V.: Confluence by decreasing diagrams converted. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 306–320. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
    Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. In: Schmidt-Schauß, M. (ed.) RTA. LIPIcs, vol. 10, pp. 377–392. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Jiaxiang Liu
    • 1
    • 2
    • 4
    • 5
  • Jean-Pierre Jouannaud
    • 1
    • 2
    • 3
  1. 1.School of Software and Software ChairTsinghua UniversityBeijingChina
  2. 2.LIX, École PolytechniquePalaiseauFrance
  3. 3.Université Paris-SudOrsayFrance
  4. 4.Key Laboratory for Information System SecurityMinistry of EducationBeijingChina
  5. 5.Tsinghua National Laboratory for Information Science and Technology (TNList)BeijingChina

Personalised recommendations