A Semantic analysis of control

James David Laird

Abstract:

This thesis examines the use of denotational semantics to reason about control flow in sequential, basically functional languages. It extends recent work in game semantics, in which programs are interpreted as strategies for computation by interaction with an environment.

Abramsky has suggested that an intensional hierarchy of computational features such as state, and their fully abstract models, can be captured as violations of the constraints on strategies in the basic functional model. Non-local control flow is shown to fit into this framework as the violation of strong and weak `bracketing' conditions, related to linear behaviour.

The language muPCF (Parigot's mu_lambda with constants and recursion) is adopted as a simple basis for higher-type, sequential computation with access to the flow of control. A simple operational semantics for both call-by-name and call-by-value evaluation is described. It is shown that dropping the bracketing condition on games models of PCF yields fully abstract models of muPCF.

The games models of muPCF are instances of a general construction based on a continuations monad on Fam(C), where C is a rational cartesian closed category with infinite products. Computational adequacy, definability and full abstraction can then be captured by simple axioms on C.

The fully abstract and universal models of muPCF are shown to have an effective presentation in the category of Berry-Curien sequential algorithms. There is further analysis of observational equivalence, in the form of a context lemma, and a characterization of the unique functor from the (initial) games model, which is an isomorphism on its (fully abstract) quotient. This establishes decidability of observational equivalence for finitary muPCF, contrasting with the undecidability of the analogous relation in pure PCF.

ECS-LFCS-99-409.

This report is available in the following formats:

Previous | Index | Next