14 - Sequentially

Summary

This chapter is devoted to the semantics of sequentiality. At first order, the notion of sequential function is well-understood, as summarized in theorem 6.5.4. At higher orders, the situation is not as simple. Building on theorem 13.3.18, Ehrhard and Bucciarelli have developped a model of strongly stable functions, which we have described in section 13.3. But in the strongly stable model an explicit reference to a concept of sequentiality is lost at higher orders. Here there is an intrinsic difficulty: there does not exist a cartesian closed category of sequential (set theoretical) functions (see theorem 14.1.12). Berry suggested that replacing functions by morphisms of a more concrete nature, and retaining information on the order in which the input is explored in order to produce a given part of the output, could be a way to develop a theory of higher order sequentiality. This intuition gave birth to the model of sequential algorithms of Berry and Curien, which is described in this chapter [BC82, BC85].

In section 14.1, we introduce Kahn and Plotkin's (filiform and stable) concrete data structures and sequential functions between concrete data structures [KP93]. This definition generalizes Vuillemin's definition 6.5.1. A concrete data structure consists of cells that can be filled with a value, much like a PASCAL record field can be given a value. A concrete data structure generates a cpo of states, which are sets of pairs (cell, value), also called events (cf. section 12.3).