Lazy Evaluation and Delimited Control
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a nove...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2010-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1013/pdf |
| _version_ | 1797268748313296896 |
|---|---|
| author | Ronald Garcia Andrew Lumsdaine Amr Sabry |
| author_facet | Ronald Garcia Andrew Lumsdaine Amr Sabry |
| author_sort | Ronald Garcia |
| collection | DOAJ |
| description | The call-by-need lambda calculus provides an equational framework for
reasoning syntactically about lazy evaluation. This paper examines its
operational characteristics. By a series of reasoning steps, we systematically
unpack the standard-order reduction relation of the calculus and discover a
novel abstract machine definition which, like the calculus, goes "under
lambdas." We prove that machine evaluation is equivalent to standard-order
evaluation. Unlike traditional abstract machines, delimited control plays a
significant role in the machine's behavior. In particular, the machine replaces
the manipulation of a heap using store-based effects with disciplined
management of the evaluation stack using control-based effects. In short, state
is replaced with control. To further articulate this observation, we present a
simulation of call-by-need in a call-by-value language using delimited control
operations. |
| first_indexed | 2024-04-25T01:37:24Z |
| format | Article |
| id | doaj.art-288b247bbaed4145a323bd6e6e50330a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:24Z |
| publishDate | 2010-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-288b247bbaed4145a323bd6e6e50330a2024-03-08T09:12:33ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742010-07-01Volume 6, Issue 310.2168/LMCS-6(3:1)20101013Lazy Evaluation and Delimited ControlRonald GarciaAndrew Lumsdainehttps://orcid.org/0000-0002-9153-6622Amr Sabryhttps://orcid.org/0000-0002-1025-7331The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine evaluation is equivalent to standard-order evaluation. Unlike traditional abstract machines, delimited control plays a significant role in the machine's behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control. To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operations.https://lmcs.episciences.org/1013/pdfcomputer science - programming languagesd.3.1 |
| spellingShingle | Ronald Garcia Andrew Lumsdaine Amr Sabry Lazy Evaluation and Delimited Control Logical Methods in Computer Science computer science - programming languages d.3.1 |
| title | Lazy Evaluation and Delimited Control |
| title_full | Lazy Evaluation and Delimited Control |
| title_fullStr | Lazy Evaluation and Delimited Control |
| title_full_unstemmed | Lazy Evaluation and Delimited Control |
| title_short | Lazy Evaluation and Delimited Control |
| title_sort | lazy evaluation and delimited control |
| topic | computer science - programming languages d.3.1 |
| url | https://lmcs.episciences.org/1013/pdf |
| work_keys_str_mv | AT ronaldgarcia lazyevaluationanddelimitedcontrol AT andrewlumsdaine lazyevaluationanddelimitedcontrol AT amrsabry lazyevaluationanddelimitedcontrol |