Computer Science – Programming Languages
Scientific paper
2009-07-27
Computer Science
Programming Languages
29 pages
Scientific paper
We present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen. The natural semantics are big-step and use global heaps, where evaluation is suspended and memorized. The reduction semantics are small-step and evaluation is suspended and memorized locally in let-bindings. Thus two styles of formalization describe the call-by-need strategy from different angles. The natural semantics for the acyclic calculus is revised from the previous presentation by Maraist et al. and its adequacy is ascribed to its correspondence with the reduction semantics, which has been proved equivalent to call-by-name by Ariola and Felleisen. The natural semantics for the cyclic calculus is inspired by that of Launchbury and Sestoft and we state its adequacy using a denotational semantics in the style of Launchbury; adequacy of the reduction semantics for the cyclic calculus is in turn ascribed to its correspondence with the natural semantics.
Hasegawa Masahito
Nakata Keiko
No associations
LandOfFree
Small-step and big-step semantics for call-by-need does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Small-step and big-step semantics for call-by-need, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Small-step and big-step semantics for call-by-need will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-246134