Abstract
In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations which specify (the order in) which subterms are evaluated. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index enables the evaluation of an argument whereas a negative index means “evaluate on-demand”. While strategy annotations containing only natural numbers have been implemented and received some recent investigation endeavor (regarding, e.g., termination and completeness), fully general annotations (also called on-demand strategy annotations), which have been proposed to support laziness in OBJ-like languages, are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. Then, we propose a solution to these problems which is based on a suitable extension of the E-evaluation strategy of OBJ-like languages (that only considers annotations given as natural numbers) to on-demand strategy annotations. Our strategy incorporates a better treatment of demandness and also exhibits good computational properties; in particular, we show how to use it for computing (head-)normal forms. We also introduce a transformation for proving termination of the new evaluation strategy by using standard techniques.
Work partially supported by CICYT TIC2001-2705-C03-01, Acciones Integradas HI2000-0161, HA2001-0059, HU2001-0019, and Generalitat Valenciana GV01-424.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Alpuente, S. Escobar, and S. Lucas. Correct and complete (positive) strategy annotations for OBJ. Electronic Notes in Theoretical Computer Science, volume 71. Elsevier Sciences, to appear 2002.
M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Specialization of Lazy Functional Logic Programs. Sigplan Notices, 32(12):151–162, ACM Press, New York, 1997.
S. Antoy and S. Lucas. Demandness in rewriting and narrowing. Electronic Notes in Theoretical Computer Science, volume 76. Elsevier Sciences, to appear 2002.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. Electronic Notes in Theoretical Computer Science, volume 4. Elsevier Sciences, 1996.
S. Eker. Term rewriting with operator evaluation strategies. Electronic Notes in Theoretical Computer Science, volume 15. Elsevier Sciences, 1998.
K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proc. of the 12th Annual ACM Symposium on Principles of Programming Languages, POPL’85, pages 52–66. ACM Press, 1985.
W. Fokkink, J. Kamperman, and P. Walters. Lazy rewriting on eager machinery. ACM Transactions on Programming Languages and Systems, 22(1):45–86, 2000.
K. Futatsugi and A. Nakagawa. An overview of Cafe specification environment-an algebraic approach for creating, verifying, and maintaining formal specification over networks-. In Proc. of 1st International Conference on Formal Engineering Methods, 1997.
B. Gramlich and S. Lucas. Modular termination of context-sensitive rewriting. In C. Kirchner, editor, Proc. of 4th International ACM SIG-PLAN Conference on Principles and Practice of Declarative Programming, PPDP’02, Pittsburg, USA, 2002. ACM Press, New York. To appear, 2002.
Jürgen Giesl and Aart Middeldorp. Transformation techniques for context-sensitive rewrite systems. Aachener Informatik-Berichte (AIBs) 2002-02, RWTH Aachen, 2002.
J. A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.P. Jouannaud. Introducing OBJ. In Joseph A. Goguen and Grant Malcolm, editors, Software Engineering with OBJ: algebraic specification in action. Kluwer, 2000.
S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998:1–61, 1998.
S. Lucas. Termination of on-demand rewriting and termination of OBJ programs. In Harald Sondergaard, editor, Proc. 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), pages 82–93, Firenze, Italy, September 2001. ACM Press, New York.
S. Lucas. Context-sensitive rewriting strategies. Information and Computation, to appear, 2002.
S. Lucas. Lazy rewriting and context-sensitive rewriting. Electronic Notes in Theoretical Computer Science, volume 64. Elsevier Sciences, to appear, 2002.
S. Lucas. Termination of (canonical) context-sensitive rewriting. In Sophie Tison, editor, Proc. 13th International Conference on Rewriting Techniques and Applications, RTA’02, LNCS 2378:296–310, Springer-Verlag, Berlin, 2002.
J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: the Language BABEL. Journal of Logic Programming, 12(3):191–223, 1992.
T. Nagaya. Reduction Strategies for Term Rewriting Systems, PhD Thesis. School of Information Science, Japan Advanced Institute of Science and Technology, 1999.
M. Nakamura and K. Ogata. The evaluation strategy for head normal form with and without on-demand flags. Electronic Notes in Theoretical Computer Science, volume 36. Elsevier Sciences, 2001.
K. Ogata and K. Futatsugi. Operational semantics of rewriting with the on-demand evaluation strategy. In Proc of 2000 International Symposium on Applied Computing, SAC’00, pages 756–763. ACM Press, 2000.
H. Zantema. Termination of context-sensitive rewriting. In Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97, pages 172–186. Springer-Verlag, LNCS 1232, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alpuente, M., Escobar, S., Gramlich, B., Lucas, S. (2002). Improving On-Demand Strategy Annotations. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_1
Download citation
DOI: https://doi.org/10.1007/3-540-36078-6_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00010-5
Online ISBN: 978-3-540-36078-0
eBook Packages: Springer Book Archive