RT Book, Section
T1 Rewriting and call-time choice: The HO case
A1 López-Fraguas, Francisco Javier
A1 Rodríguez-Hortalá, Juan
A1 Sánchez-Hernández, Jaime
A2 Garrigue, J.
A2 Hermenegildo, M.
AB It is known that the behavior of non-deterministic functions with call-time choice semantics, present in current functional logic languages, is not well described by usual approaches to reduction like ordinary term rewriting systems or A-calculus. The presence of HO features makes things more difficult, since reasoning principles that are essential in a standard (i.e., deterministic) functional setting, like extensionality, become wrong. In this paper we propose HOlet-rewriting, a notion of rewriting with local bindings that turns out to be adequate for programs with HO non-deterministic functions, as it is shown by strong equivalence results with respect to HOCRWL, a previously existing semantic framework for such programs. In addition, we give a sound and complete notion of HO-let-narrowing, we show by a case study the usefulness of the achieved combination of semantic and reduction notions, and finally we prove within our framework that a standard approach to the implementation of HO features, namely translation to FO, is still valid for HO nondeterministic functions.
PB Springer
SN 978-3-540-78968-0
YR 2008
FD 2008
LK https://hdl.handle.net/20.500.14352/53198
UL https://hdl.handle.net/20.500.14352/53198
LA eng
NO Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. J. of Symb. Comp. 40(1), 795–829 (2005)Antoy, S., Brown, D., Chiang, S.: On the correctness of bubbling. In: Pfenning, F.(ed.) RTA 2006. LNCS, vol. 4098, pp. 35–49. Springer, Heidelberg (2006)Antoy, S., Brown, D., Chiang, S.: Lazy context cloning for non-deterministic graph rewriting. In: Proc. Termgraph 2006. ENTCS, vol. 176(1), pp. 61–70 (2007)Antoy, S., Tolmach, A.P.: Typed higher-order narrowing without higher-order strategies. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol. 1722, pp. 335-353.Springer,Heidelberg (1999)Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. In: Proc. POPL 1995, pp. 233–246 (1995)Echahed, R., Janodet, J.-C.: Admissible graph rewriting and narrowing. In: Proc. JICSLP 1998, pp. 325–340. MIT Press, Cambridge (1998)González-Moreno, J., Hortalá-González, M., Rodríguez-Artalejo, M.: A higher order rewriting logic for functional logic programming. In: Proc. ICLP 1997, pp.153–167. MIT Press, Cambridge (1997)González-Moreno, J., Hortalá-González, T., Rodríguez-Artalejo, M.: Polymorphic types in functional logic programming. J. of Functional and Logic Programming 2001/S01, 1–71 (2001) 162 F.J. López-Fraguas, J. Rodríguez-Hortalá, and J. Sánchez-HernándezGonzález-Moreno, J.C.: A correctness proof for warren’s ho into fo translation. In: Proc. GULP 1993, pp. 569–584 (1993)González-Moreno, J.C., Hortalá-González, M.T., Rodríguez-Artalejo, M.: On the completeness of narrowing as the operational semantics of functional logic programming. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 216–230. Springer, Heidelberg (1993)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. J. of Logic Programming 40(1), 47–87 (1999)Hanus, M.: The integration of functions into logic programming: From theory to practice. J. of Logic Programming 19&20, 583–628 (1994)Hanus, M.: Curry mailing list (March, 2007), http://www.informatik.unikiel.de/∼curry/listarchive/0497.htmlHanus, M.: Multi-paradigm declarative languages. In: Dahl, V., Niemelä, I. (eds.)ICLP 2007. LNCS, vol. 4670, pp. 45–75. Springer, Heidelberg (2007)Hanus, M., Prehofer, C.: Higher-order narrowing with definitional trees. J. of Functional Programming 9(1), 33–75 (1999)Hanus, M. (ed.): Curry: An integrated functional logic language (version 0.8.2)(March, 2006), http://www.informatik.uni-kiel.de/∼curry/report.htmlHussmann, 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.: Narrowing for non-determinism with call-time choice semantics. In: Proc. WLP 2007 (2007)López-Fraguas, F., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: A simple rewrite notion for call-time choice semantics. In: Proc. PPDP 2007, 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 (extended version). Tech. Rep. SIC-3-08 (2008), http://gpd.sip.ucm.es/fraguas/papers/flops08long.pdfLó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)Miller, D.: A logic programming language with lambda-abstraction, function variables,and simple unification. J. Log. Comput. 1(4), 497–536 (1991)Nakahara, K., Middeldorp, A., Ida, T.: A complete narrowing calculus for higherorder functional logic programming. In: Leopold, H., Coulson, G., Danthine, A., Hutchison, D. (eds.) COST-237 1994. LNCS, vol. 882, pp. 97–114. Springer, Heidelberg (1994)Peyton Jones, S.L. (ed.): Haskell 98 Language and Libraries. The Revised Report.Cambridge University Press, Cambridge (2003)Plump, D.: Essentials of term graph rewriting. ENTCS 51 (2001)van Raamsdonk, F.: Higher-order rewriting. In: Term Rewriting Systems, Cambridge University Press, Cambridge (2003)Rodríguez-Artalejo, M.: Functional and constraint logic programming. In: Comon, H., Marché, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, pp. 202–270. Springer,Heidelberg (2001)Warren, D.H.: Higher-order extensions to prolog: Are they needed? Machine Intelligence 10, 441–454 (1982)
NO 9th international symposium, FLOPS 2008, Ise, Japan, April 14–16, 2008
DS Docta Complutense
RD 1 may 2024