{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,30]],"date-time":"2024-04-30T22:40:08Z","timestamp":1714516808353},"reference-count":60,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,10,30]],"date-time":"2012-10-30T00:00:00Z","timestamp":1351555200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2014,3]]},"abstract":"Abstract<\/jats:title>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 iscall-time choice<\/jats:italic>, 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.<\/jats:p>","DOI":"10.1017\/s1471068412000373","type":"journal-article","created":{"date-parts":[[2012,10,30]],"date-time":"2012-10-30T13:25:53Z","timestamp":1351603553000},"page":"165-213","source":"Crossref","is-referenced-by-count":3,"title":["Rewriting and narrowing for constructor systems with call-time choice semantics"],"prefix":"10.1017","volume":"14","author":[{"given":"FRANCISCO J.","family":"L\u00d3PEZ-FRAGUAS","sequence":"first","affiliation":[]},{"given":"ENRIQUE","family":"MARTIN-MARTIN","sequence":"additional","affiliation":[]},{"given":"JUAN","family":"RODR\u00cdGUEZ-HORTAL\u00c1","sequence":"additional","affiliation":[]},{"given":"JAIME","family":"S\u00c1NCHEZ-HERN\u00c1NDEZ","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,10,30]]},"reference":[{"key":"S1471068412000373_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_22"},{"key":"S1471068412000373_ref51","first-page":"83","volume-title":"ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'10)","author":"Riesco","year":"2010"},{"key":"S1471068412000373_ref49","volume-title":"Term Graph Rewriting","author":"Plump","year":"1998"},{"key":"S1471068412000373_ref60","first-page":"141","volume-title":"4th International Symposium on Static Analysis (SAS'97)","author":"Zartmann","year":"1997"},{"key":"S1471068412000373_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.01.001"},{"key":"S1471068412000373_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00185-L"},{"key":"S1471068412000373_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6834-2"},{"key":"S1471068412000373_ref20","volume-title":"On Constructor-Based Graph Rewriting Systems","author":"Echahed","year":"1997"},{"key":"S1471068412000373_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.026"},{"key":"S1471068412000373_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.2.287"},{"key":"S1471068412000373_ref27","unstructured":"Hanus M. , Ed. 2012. Curry: An Integrated Functional Logic Language (version 0.8.3), September 11, 2012 [online]. http:\/\/www.informatik.uni-kiel.de\/\u223ccurry\/report.html"},{"key":"S1471068412000373_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.12.007"},{"key":"S1471068412000373_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_23"},{"key":"S1471068412000373_ref53","unstructured":"S\u00e1nchez-Hern\u00e1ndez J. 2004. Una aproximaci\u00f3n al fallo constructivo en programaci\u00f3n declarativa multiparadigma. PhD thesis, Departamento Sistemas Inform\u00e1ticos y Programaci\u00f3n, Universidad Complutense de Madrid."},{"key":"S1471068412000373_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11999-6_9"},{"key":"S1471068412000373_ref57","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/35.5.514"},{"key":"S1471068412000373_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_8"},{"key":"S1471068412000373_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/10720084_12"},{"key":"S1471068412000373_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.05.042"},{"key":"S1471068412000373_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_9"},{"key":"S1471068412000373_ref29","unstructured":"Hanus M. , Kuchen H. and Moreno-Navarro J. J. 1995. Curry: A truly functional logic language. In Workshop on Visions for the Future of Logic Programming (ILPS'95), 95\u2013107."},{"key":"S1471068412000373_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.049"},{"key":"S1471068412000373_ref4","first-page":"35","volume-title":"17th International Conference on Rewriting Techniques and Applications (RTA'06)","author":"Antoy","year":"2006"},{"key":"S1471068412000373_ref56","doi-asserted-by":"publisher","DOI":"10.1007\/BF00277387"},{"key":"S1471068412000373_ref41","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1480945.1480959","volume-title":"2009 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation (PEPM'09)","author":"L\u00f3pez-Fraguas","year":"2009"},{"key":"S1471068412000373_ref9","first-page":"87","volume-title":"22nd International Conference on Logic Programming (ICLP'06)","author":"Antoy","year":"2006"},{"key":"S1471068412000373_ref52","first-page":"202","volume-title":"Revised Lectures of the International Summer School CCL'99","author":"Rodr\u00edguez-Artalejo","year":"2001"},{"key":"S1471068412000373_ref23","first-page":"156","volume-title":"6th European Symposium on Programming (ESOP'96)","author":"Gonz\u00e1lez-Moreno","year":"1996"},{"key":"S1471068412000373_ref22","first-page":"279","volume-title":"16th International Conference on Rewriting Techniques and Applications (RTA'05)","author":"Escobar","year":"2005"},{"key":"S1471068412000373_ref58","unstructured":"Vado-V\u00edrseda R. D. 2002. Estrategias de estrechamiento perezoso. Trabajo de Investigaci\u00f3n de Tercer Ciclo, Dpto. de Sistemas Inform\u00e1ticos y Programaci\u00f3n, Universidad Complutense de Madrid."},{"key":"S1471068412000373_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"S1471068412000373_ref28","first-page":"45","volume-title":"23rd International Conference on Logic Programming (ICLP'07)","author":"Hanus","year":"2007"},{"key":"S1471068412000373_ref30","first-page":"318","volume-title":"5th Conference on Automated Deduction (CADE'80)","author":"Hullot","year":"1980"},{"key":"S1471068412000373_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"S1471068412000373_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80210-X"},{"key":"S1471068412000373_ref45","first-page":"455","volume-title":"8th International Conference on Logic for Programming and Automated Reasoning (LPAR'01)","author":"L\u00f3pez-Fraguas","year":"2001"},{"key":"S1471068412000373_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90034-5"},{"key":"S1471068412000373_ref59","first-page":"213","volume-title":"5th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03)","author":"Vado-V\u00edrseda","year":"2003"},{"key":"S1471068412000373_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S1471068412000373_ref54","volume-title":"11th Jornadas sobre Programaci\u00f3n y Lenguajes (PROLE'11","author":"S\u00e1nchez-Hern\u00e1ndez","year":"2011"},{"key":"S1471068412000373_ref37","volume-title":"19th Workshop on Logic-based methods in Programming Environments (WLPE'09)","author":"L\u00f3pez-Fraguas","year":"2010"},{"key":"S1471068412000373_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78969-7_12"},{"key":"S1471068412000373_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48685-2_19"},{"key":"S1471068412000373_ref18","volume-title":"Logic Programming, Functions, Relations, and Equations","author":"DeGroot","year":"1986"},{"key":"S1471068412000373_ref21","first-page":"325","volume-title":"Joint International Conference and Symposium on Logic Programming (JICSLP'98)","author":"Echahed","year":"1998"},{"key":"S1471068412000373_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"S1471068412000373_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177899"},{"key":"S1471068412000373_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90024-W"},{"key":"S1471068412000373_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10029-8"},{"key":"S1471068412000373_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289462"},{"key":"S1471068412000373_ref17","first-page":"1","volume-title":"Logic Programming Languages: Constraints, Functions, and Objects","author":"Cheong","year":"1993"},{"key":"S1471068412000373_ref25","doi-asserted-by":"crossref","first-page":"153","DOI":"10.7551\/mitpress\/4299.003.0017","volume-title":"14th International Conference on Logic Programming (ICLP'97)","author":"Gonz\u00e1lez-Moreno","year":"1997"},{"key":"S1471068412000373_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"S1471068412000373_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_7"},{"key":"S1471068412000373_ref39","first-page":"197","volume-title":"9th International Conference on Principles and Practice of Declarative Programming (PPDP'07)","author":"L\u00f3pez-Fraguas","year":"2007"},{"key":"S1471068412000373_ref34","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-57186-8_79","volume-title":"5th International Symposium on Programming Language Implementation and Logic Programming (PLILP'93)","author":"Loogen","year":"1993"},{"key":"S1471068412000373_ref46","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003037"},{"key":"S1471068412000373_ref16","volume-title":"TOY: A Multiparadigm Declarative Language","author":"Caballero","year":"2006"},{"key":"S1471068412000373_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00675-3_14"},{"key":"S1471068412000373_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72018-4"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068412000373","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,30]],"date-time":"2024-04-30T21:59:56Z","timestamp":1714514396000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068412000373\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["S1471068412000373"],"URL":"https:\/\/doi.org\/10.1017\/s1471068412000373","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,30]]}}}