The specificity rule for lazy pattern-matching in ambiguous term rewrite systems
- 394 Downloads
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.
KeywordsNormal Form Function Symbol Functional Program Functional Language Ambiguous Term
- 1.A. Augustsson. A compiler for Lazy ML, ACM Conf. on Lisp and Functional Programming, 1984.Google Scholar
- 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
- 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.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.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.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.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.K. Hammond. Implementing Functional Languages for Parallel Machines, Ph.D. thesis, School of Information Systems, University of East Anglia, 1988.Google Scholar
- 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.P. Hudak et al. Report on the Functional Programming Language Haskell. Draft Proposed Standard, 1988.Google Scholar
- 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.J.W. Klop. Term rewriting systems: a tutorial, Bull. EATCS, no.32, 143–182, June 1987.Google Scholar
- 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.A. Laville. Lazy pattern matching in the ML language, INRIA report 664, 1987.Google Scholar
- 16.A. Laville. Comparison of priority rules in pattern matching and term rewriting, INRIA report 878, 1988.Google Scholar
- 17.M.J. O'Donnell. Equational Logic as a Programming Language, MIT Press, 1985.Google Scholar
- 18.N. Perry. Hope+. Internal report, Department of Computing, Imperial College, London, 1988.Google Scholar
- 19.S. Thompson. Lawful functions and program verification in Miranda, Science of Computer Programming, to appear, 1989.Google Scholar
- 20.D.A. Turner. SASL language manual. University of St. Andrews, 1979.Google Scholar
- 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.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.D.A. Turner. Miranda language manual. Research Software Ltd., Canterbury, U.K., 1987Google Scholar