Rewriting and narrowing for constructor systems with call-time choice semantics
| Autor: | Juan Rodríguez-Hortalá, Enrique Martin-Martin, Francisco Javier López-Fraguas, Jaime Sánchez-Hernández |
|---|---|
| Rok vydání: | 2014 |
| Předmět: |
FOS: Computer and information sciences
Semantics (computer science) Computer science computer.software_genre Lenguajes de programación Theoretical Computer Science Artificial Intelligence Computer Science::Logic in Computer Science Equivalence (formal languages) Soundness Sistemas expertos Computer Science - Programming Languages Programming language Term (logic) Abstract semantic graph TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Hardware and Architecture Conservative extension Completeness (logic) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages Rewriting computer Software Programming Languages (cs.PL) |
| Zdroj: | E-Prints Complutense: Archivo Institucional de la UCM Universidad Complutense de Madrid E-Prints Complutense. Archivo Institucional de la UCM instname |
| Popis: | Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind 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 (..) To appear in Theory and Practice of Logic Programming (TPLP). 89 pages, 6 figures. To appear in Theory and Practice of Logic Programming (TPLP). Corrected typos |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|