8 - Values and computations

Summary

When considering the λ-calculus as the kernel of a programming language it is natural to concentrate on weak reduction strategies, that is, strategies where evaluation stops at λ-abstractions. In presenting the semantic counterpart of these calculi it is useful to emphasize the distinction between value and computation. A first example coming from recursion theory relies on the notions of total and partial morphism. In our jargon a total morphism when given a value always returns a value whereas a partial morphism when given a value returns a possibly infinite computation. This example suggests that the denotation of a partial recursive algorithm is a morphism from values to computations, and that values are particular kinds of computations.

In domain theory the divergent computation is represented by a bottom element, say ⊥, that we add to the collection of values. This can be seen as the motivation for the shift from sets to flat domains. More precisely, we have considered three categories (cf. definition 1.4.17).

• The category Dcpo in which morphisms send values to values, say D → E. This category is adapted to a framework where every computation terminates.

• The category pDcpo which is equivalent to the one of cpo's and strict functions, and in which morphisms send values to computations, say D → (E)_⊥. This category naturally models call-by-value evaluation where functions' arguments are evaluated before application.

• […]