Rewriting and narrowing for constructor systems with call-time choice semantics
Francisco J. Lòpez-Fraguas
Enrique Martin-Martin
Juan Rodrìguez-Hortalà, and
Jaime Sànchez-Hernàndez
(Universidad Complutense de Madrid, Spain)
Abstract
Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of speci cation and programming. In particular, existing functional logic languages use such kind of rewrite systems to de ne 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 rst order version of letrewriting, 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 letrewriting. 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.
Bibtex (Use it for references)
@article{KEYWORD,
journal = {Theory and Practice of Logic Programming},
publisher = {Cambridge University Press},
author = {Francisco Javier L{\’o}pez-Fraguas and
Enrique Martin-Martin and
Juan Rodr\'{\i}guez-Hortal{\’a} and
Jaime S{\’a}nchez-Hern{\’a}ndez},
title = {Rewriting and narrowing for constructor systems with call-time
choice semantics},
volume = {14},
number = {2},
year = {2014},
pages = {165-213}
}