Narrowing for First Order Functional Logic Programs with Call-Time Choice Semantics

Abstract

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.