López-Fraguas, FranciscoRodríguez-Hortalá, JuanSánchez-Hernández,, JaimeSeipel, D.Hanus, M.Wolf, A.2023-06-202023-06-202009978-3-642-00674-610.1007/978-3-642-00675-3_14https://hdl.handle.net/20.500.14352/5319517th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, Würzburg, Germany, October 4-6, 2007In 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.engbook parthttp://www.springerlink.com/content/k28128067038q01m/fulltext.pdfhttp://www.springerlink.com/restricted access004.43Lenguajes de programación1203.23 Lenguajes de Programación