López-Fraguas, Francisco JavierRodríguez-Hortalá, JuanSánchez-Hernández, JaimeGarrigue, J.Hermenegildo, M.2023-06-202023-06-202008978-3-540-78968-010.1007/978-3-540-78969-7 12https://hdl.handle.net/20.500.14352/531989th international symposium, FLOPS 2008, Ise, Japan, April 14–16, 2008It 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.engbook parthttp://www.springerlink.com/content/h882302u488l838q/fulltext.pdfhttp://www.springerlink.com/restricted access004.43Lenguajes de programación1203.23 Lenguajes de Programación