Rewriting and narrowing for constructor systems with call-time choice semantics1. Issue 2 (30th October 2012)

• Record Type: Journal Article
• Authors: LÓPEZ-FRAGUAS, FRANCISCO J.; MARTIN-MARTIN, ENRIQUE; RODRÍGUEZ-HORTALÁ, JUAN; SÁNCHEZ-HERNÁNDEZ, JAIME
• Is Part Of: Theory and practice of logic programming. Volume 14:Issue 2(2014)
• Page Start: 165
• Page End: 213
• Publication Date: 2012-10-30
• Subjects: term rewriting systems, -- constructor-based rewriting logic, -- narrowing, -- non-determinism, -- call-time choice semantics, -- sharing, -- local bindings; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068412000373
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: Non-confluent and non-terminating {constructor-based term rewriting systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kinds of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non-trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper, we develop thoroughly the theory for the first-order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide 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. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense.