Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-24T01:13:07.490Z Has data issue: false hasContentIssue false
  • English
  • Français

Rewriting and narrowing for constructor systems with call-time choice semantics1

Published online by Cambridge University Press:  30 October 2012

FRANCISCO J. LÓPEZ-FRAGUAS ,
ENRIQUE MARTIN-MARTIN ,
JUAN RODRÍGUEZ-HORTALÁ  and
JAIME SÁNCHEZ-HERNÁNDEZ
FRANCISCO J. LÓPEZ-FRAGUAS
Affiliation:
Departamento de Sistemas Informáticos y ComputaciónUniversidad Complutense de Madrid, Madrid, Spain (e-mail: [email protected], [email protected], [email protected], [email protected])
ENRIQUE MARTIN-MARTIN
Affiliation:
Departamento de Sistemas Informáticos y ComputaciónUniversidad Complutense de Madrid, Madrid, Spain (e-mail: [email protected], [email protected], [email protected], [email protected])
JUAN RODRÍGUEZ-HORTALÁ
Affiliation:
Departamento de Sistemas Informáticos y ComputaciónUniversidad Complutense de Madrid, Madrid, Spain (e-mail: [email protected], [email protected], [email protected], [email protected])
JAIME SÁNCHEZ-HERNÁNDEZ
Affiliation:
Departamento de Sistemas Informáticos y ComputaciónUniversidad Complutense de Madrid, Madrid, Spain (e-mail: [email protected], [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Non-confluent and non-terminating {constructor-based term rewriting systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kinds of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non-trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper, we develop thoroughly the theory for the first-order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing, which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense.

Keywords

term rewriting systemsconstructor-based rewriting logicnarrowingnon-determinismcall-time choice semanticssharinglocal bindings
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 14 , Issue 2 , March 2014 , pp. 165 - 213
Copyright
Copyright © Cambridge University Press 2012 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

This work has been partially supported by the Spanish projects FAST-STAMP (TIN2008-06622-C03-01/TIN), PROMETIDOS-CM (S2009TIC-1465) and GPD-UCM (UCM-BSCH-GR58/08-910502).

References

Albert, E., Hanus, M., Huch, F., Oliver, J. and Vidal, G. 2005. Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40, 1, 795–829.Google Scholar
Alpuente, M., Falaschi, M., Iranzo, P. J. and Vidal, G. 2003. Uniform lazy narrowing. Journal of Logic and Computation 13, 2, 287–312.CrossRefGoogle Scholar
Antoy, S. 2005. Evaluation strategies for functional logic programming. Journal of Symbolic Computation 40, 1, 875–903.CrossRefGoogle Scholar
Antoy, S., Brown, D. and Chiang, S. 2006. On the correctness of bubbling. In 17th International Conference on Rewriting Techniques and Applications (RTA'06), Pfenning, F., Ed. Lecture Notes in Computer Science, vol. 4098. Springer, Berlin, 35–49.Google Scholar
Antoy, S., Brown, D. and Chiang, S. 2007. Lazy context cloning for non-deterministic graph rewriting. Electronic Notes in Theoretical Computer Science 176, 1, 3–23.CrossRefGoogle Scholar
Antoy, S., Echahed, R. and Hanus, M. 1994. A needed narrowing strategy. In 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94), Boehm, H.-J., Lang, B. and Yellin, D. M., Eds. ACM, New York, 268–279.Google Scholar
Antoy, S., Echahed, R. and Hanus, M. 2000. A needed narrowing strategy. Journal of the ACM 47, 4, 776–822.CrossRefGoogle Scholar
Antoy, S. and Hanus, M. 2000. Compiling multi-paradigm declarative programs into prolog. In 3rd International Workshop on Frontiers of Combining Systems (FroCoS'00), Kirchner, H. and Ringeissen, C., Eds. Lecture Notes in Computer Science, vol. 1794. Springer, Berlin, 171–185.Google Scholar
Antoy, S. and Hanus, M. 2006. Overlapping rules and logic variables in functional logic programs. In 22nd International Conference on Logic Programming (ICLP'06), Etalle, S. and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 4079. Springer, Berlin, 87–101.Google Scholar
Ariola, Z. M. and Arvind. 1995. Properties of a first-order functional language with sharing. Theoretical Computer Science 146, 1&2, 69–108.Google Scholar
Ariola, Z. M. and Felleisen, M. 1997. The call-by-need lambda calculus. Journal of Functional Programming 7, 3, 265–301.Google Scholar
Ariola, Z. M., Felleisen, M., Maraist, J., Odersky, M. and Wadler, P. 1995. The call-by-need lambda calculus. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'95), Cytron, R. K. and Lee, P., Eds. ACM, New York, 233–246.Google Scholar
Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, England, UK.CrossRefGoogle Scholar
Barendregt, H. P., Eekelen, M. C. J. D., Glauert, J. R. W., Kennaway, J. R., Plasmeijer, M. J. and Sleep, M. R. 1987. Term graph rewriting. In 1st Parallel Architectures and Languages Europe (PARLE'87), vol. II, Bakker, J. W. de, Nijman, A. J. and Treleaven, P. C., Eds. Lecture Notes in Computer Science, vol. 259. Springer, Berlin, 141–158.Google Scholar
Brassel, B. and Huch, F. 2007. On a tighter integration of functional and logic programming. In 5th Asian Symposium on Programming Languages and Systems (APLAS'07), Shao, Z., Ed. Lecture Notes in Computer Science, vol. 4807. Springer, Berlin, 122–138.CrossRefGoogle Scholar
Caballero, R. and Sánchez, J., Eds. 2006. TOY: A Multiparadigm Declarative Language, version 2.2.3. Technical report, Universidad Complutense de Madrid.Google Scholar
Cheong, P. and Fribourg, L. 1993. Implementation of narrowing: The Prolog-based approach. In Logic Programming Languages: Constraints, Functions, and Objects. MIT Press, Cambridge, MA, USA, 1–20.Google Scholar
DeGroot, D. and Lindstrom, G. Eds. 1986. Logic Programming, Functions, Relations, and Equations. Prentice Hall, Upper Saddle River, NJ, USA.Google Scholar
Dios-Castro, J. and López-Fraguas, F. J. 2007. Extra variables can be eliminated from functional logic programs. Electronic Notes in Theoretical Computer Science 188, 3–19.CrossRefGoogle Scholar
Echahed, R. and Janodet, J.-C. 1997. On Constructor-Based Graph Rewriting Systems. Research Report 985-I, IMAG.Google Scholar
Echahed, R. and Janodet, J.-C. 1998. Admissible graph rewriting and narrowing. In Joint International Conference and Symposium on Logic Programming (JICSLP'98). MIT Press, Cambridge, MA, USA, 325–340.Google Scholar
Escobar, S., Meseguer, J. and Thati, P. 2005. Natural narrowing for general term rewriting systems. In 16th International Conference on Rewriting Techniques and Applications (RTA'05), J. Giesl, Ed. Lecture Notes in Computer Science, vol. 3467. Springer, Berlin, 279–293.Google Scholar
González-Moreno, J. C., Hortalá-González, T., López-Fraguas, F. J. and Rodríguez-Artalejo, M. 1996. A rewriting logic for declarative programming. In 6th European Symposium on Programming (ESOP'96), Nielson, H. R., Ed. Lecture Notes in Computer Science, vol. 1058. Springer, Berlin, 156–172.Google Scholar
González-Moreno, J. C., Hortalá-González, T., López-Fraguas, F. J. and Rodríguez-Artalejo, M. 1999. An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40, 1, 47–87.Google Scholar
González-Moreno, J. C., Hortalá-González, T. and Rodríguez-Artalejo, M. 1997. A higher order rewriting logic for functional logic programming. In 14th International Conference on Logic Programming (ICLP'97). MIT Press, 153–167.Google Scholar
Hanus, M. 1994. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming 19–20, 583–628.Google Scholar
Hanus, M., Ed. 2012. Curry: An Integrated Functional Logic Language (version 0.8.3), September 11, 2012 [online]. http://www.informatik.uni-kiel.de/∼curry/report.html Google Scholar
Hanus, M. 2007. Multi-paradigm declarative languages. In 23rd International Conference on Logic Programming (ICLP'07), Dahl, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 4670. Springer, Berlin, 45–75.Google Scholar
Hanus, M., Kuchen, H. and Moreno-Navarro, J. J. 1995. Curry: A truly functional logic language. In Workshop on Visions for the Future of Logic Programming (ILPS'95), 95–107.Google Scholar
Hullot, J. 1980. Canonical forms and unification. In 5th Conference on Automated Deduction (CADE'80), Bibel, W. and Kowalski, R. A., Eds. Lecture Notes in Computer Science, vol. 87. Springer, Berlin, 318–334.Google Scholar
Hussmann, H. 1993. Non-Determinism in Algebraic Specifications and Algebraic Programs. Birkhäuser Verlag, Berlin.CrossRefGoogle Scholar
Kutzner, A. and Schmidt-Schauss, M. 1998. A non-deterministic call-by-need lambda calculus. In 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Felleisen, M. and Hudak, P., Eds. ACM SIGPLAN Notices 34, 1, 324–335.Google Scholar
Launchbury, J. 1993. A natural semantics for lazy evaluation. In 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'93), Deusen, M. S. Van and Lang, B., Eds. ACM, New York, 144–154.Google Scholar
Loogen, R., López-Fraguas, F. J. and Rodríguez-Artalejo, M. 1993. A demand-driven computation strategy for lazy narrowing. In 5th International Symposium on Programming Language Implementation and Logic Programming (PLILP'93), Bruynooghe, M. and Penjam, J., Eds. Lecture Notes in Computer Science, vol. 714. Springer, Berlin, 184–200.Google Scholar
López-Fraguas, F. J., Martin-Martin, E. and Rodríguez-Hortalá, J. 2010a. Liberal typing for functional logic programs. In 8th Asian Symposium on Programming Languages and Systems (APLAS'10), Ueda, K., Ed. Lecture Notes in Computer Science, vol. 6461. Springer, Berlin, 80–96.CrossRefGoogle Scholar
López-Fraguas, F. J., Martin-Martin, E. and Rodríguez-Hortalá, J. 2010b. New results on type systems for functional logic programming. In 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP'09), Escobar, S., Ed. Revised Selected Papers. Lecture Notes in Computer Science, vol. 5979. Springer, Berlin, 128–144.Google Scholar
López-Fraguas, F. J. and Rodrí-Hortalá, J. 2010. The full abstraction problem for higher order functional-logic programs. In 19th Workshop on Logic-based methods in Programming Environments (WLPE'09), Caballero, R. and Gallagher, J., Eds. CoRR, arXiv:1002:1833.Google Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2007a. Equivalence of two formal semantics for functional logic programs. Electronic Notes in Theoretical Computer Science 188, 117–142.Google Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2007b. A simple rewrite notion for call-time choice semantics. In 9th International Conference on Principles and Practice of Declarative Programming (PPDP'07), Leuschel, M. and Podelski, A., Eds. ACM, New York, 197–208.Google Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2008. Rewriting and call-time choice: The HO case. In 9th International Symposium on Functional and Logic Programming (FLOPS'08), Garrigue, J. and Hermenegildo, M. V., Eds. Lecture Notes in Computer Science, vol. 4989. Springer, Berlin, 147–162.CrossRefGoogle Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2009a. A flexible framework for programming with non-deterministic functions. In 2009 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation (PEPM'09), Puebla, G. and Vidal, G., Eds. ACM, New York, 91–100.Google Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2009b. A fully abstract semantics for constructor based term rewriting systems. In 20th International Conference on Rewriting Techniques and Applications (RTA'09), Treinen, R., Ed. Lecture Notes in Computer Science, vol. 5595. Springer, Berlin, 320–334.CrossRefGoogle Scholar
López-Fraguas, F. J., Rodríguez-Hortalá, J. and Sánchez-Hernández, J. 2009c. Narrowing for first order functional logic programs with call-time choice semantics. In 17th International Conference on Applications of Declarative Programming and Knowledge Management (INAP'07) and 21st Workshop on (Constraint) Logic Programming (WLP'07), Seipel, D., Hanus, M. and Wolf, A., Eds. Revised Selected Papers. Lecture Notes in Artificial Intelligence, vol. 5437, Springer, Berlin, 206–222.Google Scholar
López-Fraguas, F. J. and Sánchez-Hernández, J. 1999. $\mathcal{TOY}$ : A multiparadigm declarative system. In 10th International Conference on Rewriting Techniques and Applications (RTA'99), Narendran, P. and Rusinowitch, M., Eds. Lecture Notes in Computer Science, vol. 1631. Springer, Berlin, 244–247.Google Scholar
López-Fraguas, F. J. and Sánchez-Hernández, J. 2001. Functional logic programming with failure: A set-oriented view. In 8th International Conference on Logic for Programming and Automated Reasoning (LPAR'01), Nieuwenhuis, R. and Voronkov, A., Eds. Lecture Notes in Artificial Intelligence, vol. 2250. Springer, Berlin, 455–469.Google Scholar
Maraist, J., Odersky, M. and Wadler, P. 1998. The call-by-need lambda calculus. Journal of Functional Programming 8, 3, 275–317.Google Scholar
McCarthy, J. 1963. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems. North-Holland, the Netherlands, 33–70.Google Scholar
Moreno-Navarro, J. J. and Rodríguez-Artalejo, M. 1992. Logic programming with functions and predicates: The language Babel. Journal of Logic Programming 12, 189–223.CrossRefGoogle Scholar
Plump, D. 1998. Term Graph Rewriting. Report CSI-R9822, Computing Science Institute, University of Nijmegen.Google Scholar
Plump, D. 2001. Essentials of term graph rewriting. Electronic Notes Theoretical Computer Science 51, 277–289.Google Scholar
Riesco, A. and Rodríguez-Hortalá, J. 2010. Programming with singular and plural non-deterministic functions. In ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'10), Gallagher, J. P. and Voigtländer, J., Eds. ACM, New York, 83–92.Google Scholar
Rodríguez-Artalejo, M. 2001. Functional and constraint logic programming. In Revised Lectures of the International Summer School CCL'99, Comon, H. and Marché, C. and Treinen, R., Eds. Lecture Notes in Computer Science, vol. 2002. Springer, Berlin, 202–270.Google Scholar
Sánchez-Hernández, J. 2004. Una aproximación al fallo constructivo en programación declarativa multiparadigma. PhD thesis, Departamento Sistemas Informáticos y Programación, Universidad Complutense de Madrid.Google Scholar
Sánchez-Hernández, J. 2011. Reduction strategies for rewriting with call-time choice. In 11th Jornadas sobre Programación y Lenguajes (PROLE'11), Arenas, P., Gulías, V. and Nogueira, P., Eds. A Coruña, Spain Google Scholar
Schmidt-Schauss, M. and Machkasova, E. 2008. A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors, and case. In 19th International Conference on Rewriting Techniques and Applications (RTA'08), Voronkov, A., Ed. Lecture Notes in Computer Science, vol. 5117. Springer, Berlin, 321–335.CrossRefGoogle Scholar
Sondergaard, H. and Sestoft, P. 1990. Referential transparency, definiteness and unfoldability. Acta Informatica 27, 6, 505–517.CrossRefGoogle Scholar
Søndergaard, H. and Sestoft, P. 1992. Non-determinism in functional languages. The Computer Journal 35, 5, 514–523.CrossRefGoogle Scholar
Vado-Vírseda, R. D. 2002. Estrategias de estrechamiento perezoso. Trabajo de Investigación de Tercer Ciclo, Dpto. de Sistemas Informáticos y Programación, Universidad Complutense de Madrid.Google Scholar
Vado-Vírseda, R. d. 2003. A demand-driven narrowing calculus with overlapping definitional trees. In 5th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03). ACM, New York, 213–227.Google Scholar
Zartmann, F. 1997. Denotational abstract interpretation of functional logic programs. In 4th International Symposium on Static Analysis (SAS'97), Van Hentenryck, P., Ed. Lecture Notes in Computer Science, vol. 1302. Springer, Berlin, 141–159.Google Scholar
Supplementary material: PDF

Lopez-Freguas supplementary material

Lopez-Freguas supplementary material

Download Lopez-Freguas supplementary material(PDF)
PDF 608.8 KB