Beschreibung:
<jats:title>Abstract</jats:title><jats:p>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 (<jats:italic>J. Funct. Program.</jats:italic>, 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 <jats:italic>et al</jats:italic>. (<jats:italic>J. Funct. Program.</jats:italic>, 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.</jats:p>