@UNPUBLISHED{Moran:Sands:Need-Extended,
  author = {A. K. Moran and David Sands},
  title = {Improvement in a Lazy Context: An Operational Theory for
                  Call-By-Need (Extended Version)},
  note = {Extended version of \cite{Moran:Sands:Need}},
  year = {1998},
  month = {November},
  url_Paper = {http://www.cse.chalmers.se/~dave/papers/cbneed-theory-extended.pdf},
  abstract = {The standard implementation technique for lazy functional languages is
call-by-need, which ensures that an argument to a function in any  given call
is evaluated at most once. A significant problem with  call-by-need is that it
is difficult - even for compiler writers - to  predict the effects of program
transformations. The traditional  theories for lazy functional languages are
based on call-by-name  models, and offer no help in determining which
transformations do  indeed optimize a program.

In this article we present an operational theory for call-by-need, based upon
an improvement ordering on programs: M is improved by N if in all
program-contexts C, when C[M] terminates then C[N] terminates at least as
cheaply.

We show that this improvement relation satisfies a "context lemma", and
supports a rich inequational theory, subsuming the call-by-need lambda calculi
of Ariola \emph{et al}.  The reduction-based call-by-need calculi are
inadequate as a theory of lazy-program transformation since they only permit
transformations which speed up programs by at most a constant factor (a claim
we substantiate); we go beyond the various reduction-based calculi for
call-by-need by providing powerful proof rules for recursion, including
syntactic continuity - the basis of fixed-point-induction style reasoning, and
an Improvement Theorem, suitable for arguing the safetey and correctness of
recursion-based program transformations.
},
}

{"_id":"7dA6RjPzhmN7Aktak","bibbaseid":"moran-sands-improvementinalazycontextanoperationaltheoryforcallbyneedextendedversion-1998","downloads":0,"creationDate":"2017-02-03T08:24:26.832Z","title":"Improvement in a Lazy Context: An Operational Theory for Call-By-Need (Extended Version)","author_short":["Moran, A. K.","Sands, D."],"year":1998,"bibtype":"unpublished","biburl":"http://www.cse.chalmers.se/~dave/davewww2016.bib","bibdata":{"bibtype":"unpublished","type":"unpublished","author":[{"firstnames":["A.","K."],"propositions":[],"lastnames":["Moran"],"suffixes":[]},{"firstnames":["David"],"propositions":[],"lastnames":["Sands"],"suffixes":[]}],"title":"Improvement in a Lazy Context: An Operational Theory for Call-By-Need (Extended Version)","note":"Extended version of i̧teMoran:Sands:Need","year":"1998","month":"November","url_paper":"http://www.cse.chalmers.se/~dave/papers/cbneed-theory-extended.pdf","abstract":"The standard implementation technique for lazy functional languages is call-by-need, which ensures that an argument to a function in any given call is evaluated at most once. A significant problem with call-by-need is that it is difficult - even for compiler writers - to predict the effects of program transformations. The traditional theories for lazy functional languages are based on call-by-name models, and offer no help in determining which transformations do indeed optimize a program. In this article we present an operational theory for call-by-need, based upon an improvement ordering on programs: M is improved by N if in all program-contexts C, when C[M] terminates then C[N] terminates at least as cheaply. We show that this improvement relation satisfies a \"context lemma\", and supports a rich inequational theory, subsuming the call-by-need lambda calculi of Ariola \\emphet al. The reduction-based call-by-need calculi are inadequate as a theory of lazy-program transformation since they only permit transformations which speed up programs by at most a constant factor (a claim we substantiate); we go beyond the various reduction-based calculi for call-by-need by providing powerful proof rules for recursion, including syntactic continuity - the basis of fixed-point-induction style reasoning, and an Improvement Theorem, suitable for arguing the safetey and correctness of recursion-based program transformations. ","bibtex":"@UNPUBLISHED{Moran:Sands:Need-Extended,\n author = {A. K. Moran and David Sands},\n title = {Improvement in a Lazy Context: An Operational Theory for\n Call-By-Need (Extended Version)},\n note = {Extended version of \\cite{Moran:Sands:Need}},\n year = {1998},\n month = {November},\n url_Paper = {http://www.cse.chalmers.se/~dave/papers/cbneed-theory-extended.pdf},\n abstract = {The standard implementation technique for lazy functional languages is\ncall-by-need, which ensures that an argument to a function in any given call\nis evaluated at most once. A significant problem with call-by-need is that it\nis difficult - even for compiler writers - to predict the effects of program\ntransformations. The traditional theories for lazy functional languages are\nbased on call-by-name models, and offer no help in determining which\ntransformations do indeed optimize a program.\n\nIn this article we present an operational theory for call-by-need, based upon\nan improvement ordering on programs: M is improved by N if in all\nprogram-contexts C, when C[M] terminates then C[N] terminates at least as\ncheaply.\n\nWe show that this improvement relation satisfies a \"context lemma\", and\nsupports a rich inequational theory, subsuming the call-by-need lambda calculi\nof Ariola \\emph{et al}. The reduction-based call-by-need calculi are\ninadequate as a theory of lazy-program transformation since they only permit\ntransformations which speed up programs by at most a constant factor (a claim\nwe substantiate); we go beyond the various reduction-based calculi for\ncall-by-need by providing powerful proof rules for recursion, including\nsyntactic continuity - the basis of fixed-point-induction style reasoning, and\nan Improvement Theorem, suitable for arguing the safetey and correctness of\nrecursion-based program transformations.\n},\n}\n\n\n\n","author_short":["Moran, A. K.","Sands, D."],"key":"Moran:Sands:Need-Extended","id":"Moran:Sands:Need-Extended","bibbaseid":"moran-sands-improvementinalazycontextanoperationaltheoryforcallbyneedextendedversion-1998","role":"author","urls":{" paper":"http://www.cse.chalmers.se/~dave/papers/cbneed-theory-extended.pdf"},"downloads":0},"search_terms":["improvement","lazy","context","operational","theory","call","need","extended","version","moran","sands"],"keywords":[],"authorIDs":[],"dataSources":["SBHWXKotbthoEYKJv"]}