The specificity rule for lazy pattern-matching in ambiguous term rewrite systems

  • Richard Kennaway
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 432)


Many functional languages based on term rewriting (such as Miranda and ML) allow the programmer to write ambiguous rule systems, with the understanding that rules will be matched against a term in the order in which the rules are written, and that the pattern-matching of a rule against a term proceeds from left to right.

This gives a precise semantics to such ambiguous systems, but it has disadvantages. It depends on the textual ordering of the program, whereas the standard theory of term rewriting has no such concept. As a result, equational reasoning is not always valid for this semantics, defeating the primary virtue of functional languages. The semantics also fails to be fully lazy, in that sometimes a non-terminating computation will be performed on a term which has a normal form.

We define a rule, called specificity, for computation in ambiguous term rewrite systems. This rule (really a meta-rule) stipulates that a term rewrite rule of the system can only be used to reduce a term which matches it, if that term can never match any other rule of the system which is more specific than the given rule. One rule is more specific than another if the left-hand side of the first rule is a substitution instance of the second, and the reverse is not true. Specificity captures the intuition underlying the use of ambiguity in ML and Miranda, while also providing lazy pattern-matching.

A natural generalisation of the idea provides a semantics for Miranda's lawful types.


Normal Form Function Symbol Functional Program Functional Language Ambiguous Term 
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.


  1. 1.
    A. Augustsson. A compiler for Lazy ML, ACM Conf. on Lisp and Functional Programming, 1984.Google Scholar
  2. 2.
    J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Priority rewrite rules, Report CS-R8407, Centrum voor Wiskunde en Informatica, Amsterdam, 1982.Google Scholar
  3. 3.
    J.A. Bergstra and J.W. Klop. Conditional rewrite rules: confluence and termination. J. Comp. Sys. Sci., 32, no.3, 323–362, 1986.CrossRefGoogle Scholar
  4. 4.
    G. Berry. Stable models of typed lambda-calculi, in: G. Ausiello and C. Böhm., eds., Proc. 5th Int. Conf. on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol.62 (Springer, 1978)Google Scholar
  5. 5.
    T.H. Brus, M.C.J.D. van Eekelen, M.O. van Leer, and M.J. Plasmeijer. Clean: a language for functional graph rewriting, Report, Computing Science Department, University of Nijmegen, 1987.Google Scholar
  6. 6.
    R.M. Burstall, D.B. MacQueen, and D.T. Sannella. Hope: an experimental applicative language, in: Proc. 1st ACM Lisp Conference, 136–143, Stanford, 1980.Google Scholar
  7. 7.
    A.J. Field, L.S. Hunt, and R.L. While. Best-fit pattern matching for functional languages. Internal report, Department of Computing, Imperial College, London, 1989.Google Scholar
  8. 8.
    J.R.W. Glauert, J.R. Kennaway, and M.R. Sleep. Dactl: a computational model and compiler target language based on graph reduction. ICL Technical Journal, 5, 509–537, 1987.Google Scholar
  9. 9.
    K. Hammond. Implementing Functional Languages for Parallel Machines, Ph.D. thesis, School of Information Systems, University of East Anglia, 1988.Google Scholar
  10. 10.
    R. Harper, R. Milner, and M. Tofte. The definition of Standard ML, Report ECS-LFCS-88-62, Laboratory for Foundations of Computer Science, University of Edinburgh, 1988.Google Scholar
  11. 11.
    P. Hudak et al. Report on the Functional Programming Language Haskell. Draft Proposed Standard, 1988.Google Scholar
  12. 12.
    G. Huet and J.-J. Lévy. Call by need computations in non-ambiguous linear term rewriting systems, INRIA report 359, 1979.Google Scholar
  13. 13.
    J.W. Klop. Term rewriting systems: a tutorial, Bull. EATCS, no.32, 143–182, June 1987.Google Scholar
  14. 14.
    J.W. Klop. Term rewriting systems, in S. Abramsky, D. Gabbay, and T. Maibaum (eds.) Handbook of Logic in Computer Science, (Oxford University Press, in preparation).Google Scholar
  15. 15.
    A. Laville. Lazy pattern matching in the ML language, INRIA report 664, 1987.Google Scholar
  16. 16.
    A. Laville. Comparison of priority rules in pattern matching and term rewriting, INRIA report 878, 1988.Google Scholar
  17. 17.
    M.J. O'Donnell. Equational Logic as a Programming Language, MIT Press, 1985.Google Scholar
  18. 18.
    N. Perry. Hope+. Internal report, Department of Computing, Imperial College, London, 1988.Google Scholar
  19. 19.
    S. Thompson. Lawful functions and program verification in Miranda, Science of Computer Programming, to appear, 1989.Google Scholar
  20. 20.
    D.A. Turner. SASL language manual. University of St. Andrews, 1979.Google Scholar
  21. 21.
    D.A. Turner. Recursion equations as a programming language, in J. Darlington, P. Henderson, and D.A. Turner (eds.) Functional Programming and its Applications: an Advanced Course, Cambridge University Press, 1982.Google Scholar
  22. 22.
    D.A. Turner. Miranda: a non-strict functional language with polymorphic types. In J.-P. Jouannaud (ed.), Proc. ACM Conf. on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, vol.201, Springer-Verlag, 1985.Google Scholar
  23. 23.
    D.A. Turner. Miranda language manual. Research Software Ltd., Canterbury, U.K., 1987Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Richard Kennaway
    • 1
  1. 1.School of Information SystemsUniversity of East AngliaNorwichUK

Personalised recommendations