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 17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, Würzburg, Germany, October 4-6, 2007
DS Docta Complutense
RD 11 abr 2025