Abstract Modularity

  • Michael Abbott
  • Neil Ghani
  • Christoph Lüth
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


Modular rewriting seeks criteria under which rewrite systems inherit properties from their smaller subsystems. This divide and conquer methodology is particularly useful for reasoning about large systems where other techniques fail to scale adequately. Research has typically focused on reasoning about the modularity of specific properties for specific ways of combining specific forms of rewriting.

This paper is, we believe, the first to ask a much more general question. Namely, what can be said about modularity independently of the specific form of rewriting, combination and property at hand. A priori there is no reason to believe that anything can actually be said about modularity without reference to the specifics of the particular systems etc. However, this paper shows that, quite surprisingly, much can indeed be said.


Disjoint Union Algebraic Theory Initial Object Left Adjoint Variable Binding 
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.
    Adámek, J., Rosický, J.: Paragon. London Mathematical Society Lecture Note Series, vol. 189. Cambridge University Press, Cambridge (1994)zbMATHCrossRefGoogle Scholar
  2. 2.
    Barr, M., Wells, C.: Toposes, Triples and Theories. In: Grundlehren der mathematischen Wissenschaften, vol. 278, Springer, Heidelberg (1985)Google Scholar
  3. 3.
    Ghani, N., Lüth, C.: Rewriting via coinserters. Nordic Journal of Computing 10, 290–312 (2004)Google Scholar
  4. 4.
    Ghani, N., Lüth, C., de Marchi, F.: Solving algebraic equations using coalgebra. Journal of Theoretical Informatics and Applications 37, 301–314 (2003)zbMATHCrossRefGoogle Scholar
  5. 5.
    Ghani, N., Lüth, C., de Marchi, F.: Monads of coalgebras: Rational terms and term graphs. To appear in Mathematical Structures in Computer ScienceGoogle Scholar
  6. 6.
    Ghani, N., Uustalu, T.: Explicit substitutions and higher-order syntax (extended abstract). In: Honsell, F., Miculan, M., Momigliano, A. (eds.) Proc. of 2nd ACM SIGPLAN Wksh. on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2003, pp. 1–7. ACM Press, New York (2003)CrossRefGoogle Scholar
  7. 7.
    Ghani, N., Uustalu, T.: Coproducts of ideal monads. Journal of Theoretical Informatics and Applications 38, 321–342 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Hamana, M.: Term rewriting with variable binding: an initial algebra approach. In: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 148–159. ACM Press, New York (2003)CrossRefGoogle Scholar
  9. 9.
    Klop, J.W., Middeldorp, A., Toyama, Y., de Vrijer, R.: A simplified proof of Toyama’s theorem. Information Processing Letters 49, 101–109 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Kurihara, M., Kaji, I.: Modular term rewriting systems and the termination. Information Processing Letters 34(1), 1–4 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Lüth, C.: Categorical Term Rewriting: Monads and Modularity. PhD thesis, University of Edinburgh (1998)Google Scholar
  12. 12.
    Lüth, C., Ghani, N.: Monads and modular term rewriting. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 69–86. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Lüth, C., Ghani, N.: Monads and modularity. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 18–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1971)Google Scholar
  15. 15.
    Manes, E.G.: Algebraic Theories. Graduate Texts in Mathematics. Springer, Heidelberg (1976)zbMATHGoogle Scholar
  16. 16.
    Marchiori, M.: Modularity of completeness revisited. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 2–10. Springer, Heidelberg (1995)Google Scholar
  17. 17.
    Middeldorp, A.: Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit te Amsterdam (1990)Google Scholar
  18. 18.
    Middeldorp, A., Toyama, Y.: Completeness of constructor systems. Technical Report CS-R9058, Centrum voor Wiskunde en Informatica, Amsterdam (1990)Google Scholar
  19. 19.
    Ohlebusch, E.: On the modularity of termination of term rewriting systems. Theoretical Computer Science 136, 333–360 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Ohlenbusch, E.: On the modularity of confluence of constructor-sharing term rewriting systems. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, Springer, Heidelberg (1994)Google Scholar
  21. 21.
    Robinson, E.: Variations on algebra: monadicity and generalisations of equational theories. Manuscript. Available at (1994),
  22. 22.
    Rusinowitch, M.: On the termination of the direct sum of term-rewriting systems. Information Processing Letters 26(2), 65–70 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM 34(1), 128–143 (1987)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Michael Abbott
    • 1
  • Neil Ghani
    • 1
  • Christoph Lüth
    • 2
  1. 1.Department of Mathematics and Computer ScienceUniversity of Leicester 
  2. 2.FB 3 – Mathematik und InformatikUniversität Bremen 

Personalised recommendations