Completeness of rewrite rules and rewrite strategies for FP

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Completeness of rewrite rules and rewrite strategies for FP

Full text

Pdf (4.87 MB)

Source

Journal of the ACM (JACM) archive
Volume 37 , Issue 1 (January 1990) table of contents

Pages: 86 - 143

Year of Publication: 1990

ISSN:0004-5411

Authors

Joseph Y. Halpern	IBM Almaden Research Center, San Jose, CA
John H. Williams	IBM Almaden Research Center, San Jose, CA
Edward L. Wimmers	IBM Almaden Research Center, San Jose, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 29, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/78935.78939 What is a DOI?

ABSTRACT

This paper treats languages whose operational semantics is given by a set of rewrite rules. For such languages, it is important to be able to determine that there are enough rules to be able to compute the correct meaning of all expressions, but not so many that the system of rules is inconsistent. A formal framework is developed in which to give a precise treatment of these completeness and soundness issues, which are then investigated in the context of an extended version of the functional programming language FP. The rewrite rules of FP are shown to be sound and complete with respect to three different notions of completeness. The latter half of the paper considers rewrite strategies. In order to implement a language based on rewrite rules, it does not suffice to know that there are “enough” rules in the language; a good strategy for determining the order in which to apply them is also needed. But what is “good”? Corresponding to each notion of completeness, there is a notion of a good rewrite strategy. These notions of goodness are examined and characterized, and examples of a number of natural good strategies are given. Although these results are presented in the context of FP, the techniques (some of which are nontrivial extensions of techniques first used in the context of &lgr;-calculus) should apply well beyond the realm of FP rewriting systems.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
	2	Corrado Böhm, Combinatory foundation of functional programming, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.29-36, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802132]
	3	R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
	4	Walter Dosch , Bernhard Möller>, Busy and lazy FP with infinite objects, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.282-292, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802045]
	5	Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
	6	FRIEDMAN, D., AND WISE, n. Cons should not evaluate its arguments. In Proceedings of the 3rd International Colloquium on Automata, Languages, and Programming. Springer-Verlag, New York, 1976, pp. 257-284.
	7	GOGUEN, J., MESEGUER, J., AND PLAISTED, D. Programming with parameterized abstract objects in OBJ. In Theory and Practice of Software Technology. North-Holland, Amsterdam, 1982.
	8	Joseph Y. Halpern , John H. Williams , Edward L. Wimmers , Timothy C. Winkler, Denotational semantics and rewrite rules for FP, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.108-120, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318623]
	9	Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
	10	Christoph M. Hoffmann , Michael J. O`Donnell, Implementation of an interpreter for abstract equations, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-121, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800522]
	11	Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
	12	MEYER, A.R. What is a model of the X-calculus? Inf. Control 52 (1982), 87-122.
	13	NICKL, F. A denotational semantics for Backus' FP with infinite objects. Tech. Rep. Fakultiit for Mathematik und Informatik. Universitiit Passau, Passau, West Germany, 1985.
	14	Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
	15	PLOTKIN, G.D. LCF considered as a programming language. Theoret. Computer Sci. 5 (1977), 223-255.
	16	PRAWITZ, n. Ideas and results in proof theory. In Proceedings of the 2nd Scandinavian Logic Symposium, J. Fenstad, ed. North-Holland, Amsterdam, 1971.
	17	Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
	18	SMYTH, i. B., AND PLOTKIN, G.n. The category-theoretic solution ofrecursive domain equations. SIAM J. Comput. 11, 4 (1982), 761-783.
	19	Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
	20	TAIT, W.W. Intentional interpretation of functions of finite type I. J. Symb. Logic 32 (1967), 198-212.
	21	TMT, W. W. A realizability interpretation of the theory of species. In Logic Colloquium, R. Parikh, Ed. Springer-Verlag, New York, (1975), pp. 240-251.
	22	TURNER, D.A. A new implementation technique for applicative languages. Softw. Prac. Exp. 9 (1979), 31-49.
	23	WADSWORTH, C.P. The relation between computational and denotational properties of Scott's D=-models of the lambda calculus. SIAM J. Comput. 5 (1976), 488-521.
	24	WADSWORTH, C.P. Approximate reduction and lambda calculus models. SIAM J. Comput. 7 (1978), 337-356.
	25	John H. Williams, Formal Representations for Recursively Defined Functional Programs, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.460-470, April 19-25, 1981
	26	John H. Williams, On the Development of the Algebra of Functional Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.733-757, Oct. 1982 [doi>10.1145/69622.357193]