2026-06-29T02:09:57Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/531952023-08-11T00:55:51Zcom_20.500.14352_14col_20.500.14352_21

Narrowing for First Order Functional Logic Programs with Call-Time Choice Semantics López-Fraguas, Francisco Rodríguez-Hortalá, Juan Sánchez-Hernández,, Jaime Seipel, D. Hanus, M. Wolf, A. 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. 2023-06-20T13:38:54Z 2023-06-20T13:38:54Z 2023-06-20T13:38:54Z 2009 book part https://hdl.handle.net/20.500.14352/53195 XXXX-XXXX 10.1007/978-3-642-00675-3_14 eng Lecture Notes in Computer Science Spanish projects Merit-Forms-UCM (TIN2005-09207-C03-03) Promesas-CAM (S-0505/TIC/0407) restricted access Springer