12 - Stability

Summary

The theory of stable functions is originally due to Berry [Ber78]. It has been rediscovered by Girard [Gir86] as a semantic counterpart of his theory of dilators. Similar ideas were also developed independently and with purely mathematical motivations by Diers (see [Tay90a] for references).

Berry discovered stability in his study of sequential computation (cf. theorem 2.4) and of the full abstraction problem for PCF (cf. section 6.4). His intuitions are drawn from an operational perspective, where one is concerned, not only with the input-output behaviour of procedures, but also with questions such as: ‘which amount of the input is actually explored by the procedure before it produces an output’. In Girard's work, stable functions arose in a construction of a model of system F (see chapter 11); soon after, his work on stability paved the way to linear logic, which is the subject of chapter 13.

In section 12.1, we introduce the conditionally multiplicative functions, which are the continuous functions preserving binary compatible glb's. In section 12.2, we introduce the stable functions, focusing on minimal points and traces. Stability and conditional multiplicativity are different in general, but are equivalent under a well-foundedness assumption. They both lead to cartesian closed categories. The ordering on function spaces is not the pointwise ordering, but a new ordering, called the stable ordering.

We next develop the theory on algebraic cpo's, as in chapter 5. In Section 12.3, we introduce Berry's dI-domains, which are Scott domains satisfying two additional axioms.