pi-Calculus Characterizations of some Practical lambda-Calculus Reduction Strategies

We give p-calculus encodings of some reduction strategies that have been found useful in the functional programming community: call-byvalue, parallel call-by-value, call-by-need and call-by-process. The ease with which the p-calculus lends itself to expressing these different reduction strategies is remarkable. All four of our encodings can be `mixed and matched' in that different reduction strategies can be applied to different parts of the program, as is routinely done in functional programming systems. 1 Introduction Functional programming systems have reached a state of considerable maturity. While all are ultimately based on the l-calculus, they often differ in their choice of reduction strategy. This diversity originates from the non-determinism in the unconstrained l-calculus as to the choice of the next redex in a given term. Reduction strategies we will consider in this paper are call-by-value, as found in, for example, Standard ML [Mil84], parallel call-by-value , as used in..