RT Book, Section T1 Narrowing for First Order Functional Logic Programs with Call-Time Choice Semantics A1 López-Fraguas, Francisco A1 Rodríguez-Hortalá, Juan A1 Sánchez-Hernández, , Jaime A2 Seipel, D. A2 Hanus, M. A2 Wolf, A. AB In a recent work we have proposed let-rewriting, a simple one-step relation close to ordinary term rewriting but able, via local bindings, to express sharing of computed values. In this way, let-rewriting reflects the call-time choice semantics for non-determinism adopted by modern functional logic languages, where programs are rewrite systems possibly non-confluent and non-terminating. In this paper we extend that work providing 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. Completeness is based on a lifting lemma for let-rewriting similar to Hullot's lifting lemma for ordinary rewriting and narrowing. Our work copes with first order, left linear, constructor-based rewrite systems with no other restrictions about confluence, termination or presence of extra variables in right-hand sides of rules. PB Springer SN 978-3-642-00674-6 YR 2009 FD 2009 LK https://hdl.handle.net/20.500.14352/53195 UL https://hdl.handle.net/20.500.14352/53195 LA eng NO Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40(1), 795–829 (2005)Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. In: Proc. ACM Symposium on Principles of Programming Languages (POPL 1994), pp. 268–279. ACM Press, New York (1994)Antoy, S., Hanus, M.: Overlapping rules and logic variables in functional logic programs. In: ICLP, pp. 87–101 (2006)Braßel, B., Huch, F.: On a tighter integration of functional and logic programming. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 122–138. Springer, Heidelber(2007)Dios, J., López-Fraguas, F.: Elimination of extra variables from functional logic programs. In: Lucio, P., Orejas, F. (eds.) VI Jornadas sobre Programación y Lenguajes (PROLE 2006), pp. 121–135. CINME (2006)Echahed, R., Janodet, J.-C.: Admissible graph rewriting and narrowing. In: Proceedings of the Joint International Conference and Symposium on Logic Programming, Manchester, June 1998, pp. 325–340. MIT Press, Cambridge (1998)Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 279–293. Springer, Heidelberg (2005)González-Moreno, J.C., Hortalá-González, T., López-Fraguas, F., Rodríguez-Artalejo, M.: A rewriting logic for declarative programming. In: Riis Nielson, H.(ed.) ESOP 1996. LNCS, vol. 1058, pp. 156–172. Springer, Heidelberg (1996)González-Moreno, J.C., Hortalá-González, T., López-Fraguas, F., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1), 47–87 (1999)Hanus, M.: Functional logic programming: From theory to Curry. Technical report, Christian-Albrechts-Universität Kiel (2005)Hanus, M.: Multi-paradigm declarative languages. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 45–75. Springer, Heidelberg (2007)Hanus, M. (ed.): Curry: An integrated functional logic language (version 0.8.2) (March 2006),http://www.informatik.uni-kiel.de/report.htmlHullot, J.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)Hussmann, H.: Non-Determinism in Algebraic Specifications and Algebraic Programs. Birkhäuser, Basel (1993)López-Fraguas, F., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: A simple rewrite notion for call-time choice semantics. In: Proc. Principles and Practice of Declarative Programming, pp. 197–208. ACM Press, New York (2007)López-Fraguas, F., Rodríguez-Hortalá, J., Sánchez Hernández, J.: Rewriting and call-time choice: the HO case. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 147–162. Springer, Heidelberg (2008)López-Fraguas, F., Sánchez-Hernández, J.: T OY: A multiparadigm declarative system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp.244–247. Springer, Heidelberg (1999)Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275–317 (1998)Plump, D.: Essentials of term graph rewriting. Electr. Notes Theor. Comput. Sci. 51 (2001)Rodríguez-Hortalá, J.: El indeterminismo en programación lógico-funcional: un enfoque basado en reescritura. Trabajo de Investigación de Tercer Ciclo, Dpto. de Sistemas Informáticos y Computación, Universidad Complutense de Madrid (June 2007)Søndergaard, H., Sestoft, P.: Non-determinism in functional languages. The Computer Journal 35(5), 514–523 (1992)Vado-Vírseda, R.d.: A demand-driven narrowing calculus with overlapping definitional trees. In: Proc. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP 2003), pp. 213–227. ACM Press, New York (2003) NO 17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, Würzburg, Germany, October 4-6, 2007 DS Docta Complutense RD 16 may 2024