We offer a short tour into the interactive interpretation of sequential programs. We emphasize streamlike computation — that is, computation of successive bits of information upon request. The core of the approach surveyed here dates back to the work of Berry and the author on sequential algorithms on concrete data structures in the late seventies, culminating in the design of the programming language CDS, in which the semantics of programs of any type can be explored interactively. Around one decade later, two major insights of Cartwright and Felleisen on one hand, and of Lamarche on the other hand gave new, decisive impulses to the study of sequentiality. Cartwright and Felleisen observed that sequential algorithms give a direct semantics to control operators like call-cc and proposed to include explicit errors both in the syntax and in the semantics of the language PCF. Lamarche (unpublished) connected sequential algorithms to linear logic and games. The successful program of games semantics has spanned over the nineties until now, starting with syntax-independent characterizations of the term model of PCF by Abramsky, Jagadeesan, and Malacaria on one hand, and by Hyland and Ong on the other hand.
Two important models of functions that have been constructed since turned out to be the extensional collapse (i.e. the hereditary quotient equating sequential algorithms computing the same function, i.e. (in the affine case) two algorithms @math and @math such that @math ): Bucciarelli and Ehrhard's model of strongly stable functions @cite_3 @cite_16 , and Longley's model of sequentially realizable functionals @cite_10 . The first model arose from an algebraic characterization of sequential (first-order) functions, that carries over to all types. The second one is a realizability model over a combinatory algebra in which the interaction at work in sequential algorithms is encoded.
@cite_16 @cite_10 @cite_3
2038883640 1985955425 1963626918
In the previous chapter, we saw how the model PC offers a maximal class of partial computable functionals strictly extending SF (in the sense of the poset ( J ( N _ ) ) of Subsection 3.6.4). In the present chapter, we show that SF can also be extended in a very different direction to yield another class SR of computable functionals which is in some sense incompatible with PC. This class was first identified by Bucciarelli and Ehrhard [45] as the class of strongly stable functionals; later work by Ehrhard [69], van Oosten [294] and Longley [176] established the computational significance of these functionals, investigated their theory in some detail, and provided a range of alternative characterizations. We prove that, in the hierarchy of simple types based on the type of natural numbers, any finite strongly stable function is equal to the application of the semantics of a PCF-definable functional to some strongly stable (generally not PCF-definable) functionals of type two. Applying a logical relation technique, we derive from this result that the strongly stable model of PCF is the extensional collapse of its sequential algorithms model. We investigate the minimization of Newton's functional for the problem of the body of minimal resistance with maximal height @math cite butt in the class of convex developable functions defined in a disc. This class is a natural candidate to find a (non-radial) minimizer in accordance with the results of cite lrp2. We prove that the minimizer in this class has a minimal set in the form of a regular polygon with @math sides centered in the disc, and numerical experiments indicate that the natural number @math is a non-decreasing function of @math . The corresponding functions all achieve a lower value of the functional than the optimal radially symmetric function with the same height @math .