論文

査読有り
2009年11月

Small-step and big-step semantics for call-by-need

JOURNAL OF FUNCTIONAL PROGRAMMING
  • Keiko Nakata
  • ,
  • Masahito Hasegawa

19
6
開始ページ
699
終了ページ
722
記述言語
英語
掲載種別
研究論文(学術雑誌)
DOI
10.1017/S0956796809990219
出版者・発行元
CAMBRIDGE UNIV PRESS

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 (J. Funct. Program., vol. 7. no. 3, 1997). 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. (J. Fund. Program., vol. 8, no. 3, 1998), 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 (1993) and Sestoft (1997), 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.

リンク情報
DOI
https://doi.org/10.1017/S0956796809990219
J-GLOBAL
https://jglobal.jst.go.jp/detail?JGLOBAL_ID=200902242281139172
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000272196200004&DestApp=WOS_CPL
ID情報
  • DOI : 10.1017/S0956796809990219
  • ISSN : 0956-7968
  • eISSN : 1469-7653
  • J-Global ID : 200902242281139172
  • Web of Science ID : WOS:000272196200004

エクスポート
BibTeX RIS