{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,20]],"date-time":"2023-09-20T10:50:16Z","timestamp":1695207016727},"reference-count":36,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2008,6,1]],"date-time":"2008-06-01T00:00:00Z","timestamp":1212278400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:p>We present a higher-order call-by-need lambda calculus enriched with constructors,<jats:monospace>case<\/jats:monospace>expressions, recursive<jats:monospace>letrec<\/jats:monospace>expressions, a<jats:monospace>seq<\/jats:monospace>operator for sequential evaluation and a non-deterministic operator<jats:monospace>amb<\/jats:monospace>that is locally bottom-avoiding. We use a small-step operational semantics in the form of a single-step rewriting system that defines a (non-deterministic) normal-order reduction. This strategy can be made fair by adding resources for book-keeping. As equational theory, we use contextual equivalence (that is, terms are equal if, when plugged into any program context, their termination behaviour is the same), in which we use a combination of may- and must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations with respect to normal-order reduction are the same as for fair normal-order reduction. We develop a number of proof tools for proving correctness of program transformations. In particular, we prove a context lemma for both may- and must- convergence that restricts the number of contexts that need to be examined for proving contextual equivalence. Combining this with so-called complete sets of commuting and forking diagrams, we show that all the deterministic reduction rules and some additional transformations preserve contextual equivalence. We also prove a standardisation theorem for fair normal-order reduction. The structure of the ordering \u2264<jats:sub><jats:italic>c<\/jats:italic><\/jats:sub>is also analysed, and we show that \u03a9 is not a least element and \u2264<jats:sub><jats:italic>c<\/jats:italic><\/jats:sub>already implies contextual equivalence with respect to may-convergence.<\/jats:p>","DOI":"10.1017\/s0960129508006774","type":"journal-article","created":{"date-parts":[[2008,6,18]],"date-time":"2008-06-18T13:28:06Z","timestamp":1213795686000},"page":"501-553","source":"Crossref","is-referenced-by-count":26,"title":["A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations"],"prefix":"10.1017","volume":"18","author":[{"given":"DAVID","family":"SABEL","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MANFRED","family":"SCHMIDT-SCHAUSS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2008,6,1]]},"reference":[{"key":"S0960129508006774_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002967"},{"key":"S0960129508006774_ref34","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/35.5.514"},{"key":"S0960129508006774_ref32","unstructured":"Schmidt-Schauss M. , Sch\u00fctz M. and Sabel D. (2004) On the safety of N\u00f6cker's strictness analysis. Frank Report 19, Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t Frankfurt."},{"key":"S0960129508006774_ref31","unstructured":"Schmidt-Schauss M. (2003) FUNDIO: A Lambda-Calculus with a letrec, case, Constructors, and an IO-Interface: Approaching a Theory of unsafePerformIO. Frank Report 16, Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t Frankfurt."},{"key":"S0960129508006774_ref24","first-page":"648","volume-title":"Springer-Verlag Lecture Notes in Computer Science","volume":"944","author":"Natarajan","year":"1995"},{"key":"S0960129508006774_ref23","unstructured":"Moran A. K. (1998) Call-by-name, Call-by-need, and McCarthy's Amb, Ph.D. thesis, Department of Computing Science, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden."},{"key":"S0960129508006774_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.041"},{"key":"S0960129508006774_ref17","first-page":"260","volume-title":"Springer-Verlag Lecture Notes in Computer Science","volume":"1782","author":"Machkasova","year":"2000"},{"key":"S0960129508006774_ref16","first-page":"198","volume-title":"Springer-Verlag Lecture Notes in Computer Science","volume":"1672","author":"Lassen","year":"1999"},{"key":"S0960129508006774_ref15","unstructured":"Lassen S. B. , Levy P. B. and Panangaden P. (2005) Divergence-least semantics of amb is Hoare. Short presentation at the APPSEM II workshop, Frauenchiemsee, Germany. (Available at http:\/\/www.cs.bham.ac.uk\/~pbl\/papers\/.)"},{"key":"S0960129508006774_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.068"},{"key":"S0960129508006774_ref13","unstructured":"Lassen S. B. (1998) Relational Reasoning about Functions and Nondeterminism, Ph.D. thesis, Department of Computer Science, University of Aarhus. (BRICS Dissertation Series DS-98-2.)"},{"key":"S0960129508006774_ref7","volume-title":"Functional Programming \u2013 Application and Implementation","author":"Henderson","year":"1980"},{"key":"S0960129508006774_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.005"},{"key":"S0960129508006774_ref2","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0960129508006774_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"S0960129508006774_ref1","doi-asserted-by":"crossref","unstructured":"Ariola Z. , Felleisen M. , Maraist J. , Odersky M. and Wadler P. (1995) A call-by-need lambda calculus. In: Proc. POPL '95, 22'nd Annual Symposium on Principles of Programming Languages, San Francisco, California, ACM Press.","DOI":"10.1145\/199448.199507"},{"key":"S0960129508006774_ref27","unstructured":"Sabel D. (2003a) A guide through HasFuse. (Available at http:\/\/www.ki.informatik.uni-frankfurt.de\/research\/diamond\/hasfuse\/.)"},{"key":"S0960129508006774_ref30","unstructured":"Santos A. (1995) Compilation by Transformation in Non-Strict Functional Languages, Ph.D. thesis, Glasgow University, Department of Computing Science."},{"key":"S0960129508006774_ref33","unstructured":"Schmidt-Schauss M. , Sch\u00fctz M. and Sabel D. (2005) A complete proof of the safety of N\u00f6cker's strictness analysis. Frank Report 20, Institut f\u00fcr Informatik. J. W. Goethe-Universit\u00e4t Frankfurt."},{"key":"S0960129508006774_ref11","unstructured":"Kutzner A. (2000) Ein nichtdeterministischer call-by-need Lambda-Kalk\u00fcl mit erratic choice: Operationale Semantik, Programmtransformationen und Anwendungen, Dissertation, J. W. Goethe-Universit\u00e4t Frankfurt (in German)."},{"key":"S0960129508006774_ref3","unstructured":"Bois A. R. D. , Pointon R. F. , Loidl H.-W. and Trinder P. W. (2002) Implementing declarative parallel bottom-avoiding choice. In: SBAC-PAD, IEEE Computer Society 82\u201392."},{"key":"S0960129508006774_ref25","volume-title":"Haskell 98 language and libraries: the Revised Report","author":"Peyton Jones","year":"2003"},{"key":"S0960129508006774_ref8","first-page":"177","volume-title":"Functional Programming and its Applications","author":"Henderson","year":"1982"},{"key":"S0960129508006774_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224191"},{"key":"S0960129508006774_ref6","doi-asserted-by":"crossref","unstructured":"Hallgren T. and Carlsson M. (1995) Programming with fudgets. In: Jeuring J. and Meijer E. (eds.) Advanced Functional Programming. Springer-Verlag Lecture Notes in Computer Science 925 137\u2013182.","DOI":"10.1007\/3-540-59451-5_5"},{"key":"S0960129508006774_ref18","volume-title":"A Non-Deterministic Call-by-Need Lambda Calculus: Proving Similarity a Precongruence by an Extension of Howe's Method to Sharing","author":"Mann","year":"2005"},{"key":"S0960129508006774_ref5","first-page":"134","article-title":"Interaction nets with McCarthy's amb: Properties and applications","volume":"10","author":"Fern\u00e1ndez","year":"2003","journal-title":"Nordic J. Comput."},{"key":"S0960129508006774_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"S0960129508006774_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"S0960129508006774_ref29","unstructured":"Sabel D. and Schmidt-Schauss M. (2006) A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Frank Report 24, Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t Frankfurt."},{"key":"S0960129508006774_ref20","unstructured":"Mann M. and Schmidt-Schauss M. (2006) How to prove similarity a precongruence in non-deterministic call-by-need lambda calculi. Frank Report 22, Institut f\u00fcr Informatik. J. W. Goethe-Universit\u00e4t Frankfurt."},{"key":"S0960129508006774_ref10","unstructured":"Jones M. P. and Hudak P. (1993) Implicit and explicit parallel programming in Haskell. Technical Report CT 06520-2158, Department of Computer Science, Yale University."},{"key":"S0960129508006774_ref36","first-page":"88","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"Wells","year":"2003"},{"key":"S0960129508006774_ref28","unstructured":"Sabel D. (2003b) Realising nondeterministic I\/O in the Glasgow Haskell Compiler. Frank Report 17, Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t Frankfurt am Main."},{"key":"S0960129508006774_ref12","doi-asserted-by":"crossref","unstructured":"Kutzner A. and Schmidt-Schauss M. (1998) A nondeterministic call-by-need lambda calculus. In: International Conference on Functional Programming 1998, ACM Press 324\u2013335.","DOI":"10.1145\/289423.289462"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508006774","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T20:59:55Z","timestamp":1684443595000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508006774\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["S0960129508006774"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508006774","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,6]]}}}