An Operational Semantics for Parallel Lazy Evaluation

We present an operational semantics for parallel lazy evaluation that accurately models the parallel behaviour of the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately then combined before proceeding to the next set of reductions. Consequently the semantics has two levels, with transition rules for individual threads at one level and combining rules at the other. Each parallel thread is modelled by a binding labelled with an indication of its activity status. To the best of our knowledge this is the rst semantics that models such thread states. A set of labelled bindings corresponds to a heap and is used to model sharing. The semantics is set at a higher level of abstraction than an abstract machine and is therefore more manageable for proofs about programs rather than implementations. At the same time, it is suciently low level to allow us to reason about programs in terms of parallelism (i.e. the number of processors used) as well as work and run-time with dierent numbers of processors