Lambda-Calculi for (strict) parallel functions

Abstract

We introduce two λ-calculi and show that they are expressive for two canonical domains of parallel functions. The first calculus is an enrichment of the lazy, call-by-name λ-calculus with call-by-value abstractions and parallel composition, while in the second the usual call-by-name abstractions are disallowed. The corresponding domains are respectively Abramsky′s domain D = (D →⊥D)⊥, a lifted function space, and D = (D →⊥D)⊥, a lifted domain of strict functions. These domains are lattices, and we show that the parallelism is adequately represented by the join operator, while call-by-value abstractions correspond to strict functions. The proofs of the results rely on a completeness theorem for the logical presentation of the semantics. © 1994 Academic Press, Inc.