An Axiomatic Approach to Adequacy

Torben Braüner

November 1996

Abstract:

This thesis studies adequacy for PCF-like languages in a general categorical framework. An adequacy result relates the denotational semantics of a program to its operational semantics; it typically states that a program terminates whenever the interpretation is non-bottom. The main concern is to generalise to a linear version of PCF the adequacy results known for standard PCF, keeping in mind that there exists a Girard translation from PCF to linear PCF with respect to which the new constructs should be sound. General adequacy results have usually been obtained in order-enriched categories, that is, categories where all hom-sets are typically cpos, maps are assumed to be continuous and fixpoints are interpreted using least upper bounds. One of the main contributions of the thesis is to propose a completely different approach to the problem of axiomatising those categories which yield adequate semantics for PCF and linear PCF. The starting point is that the only unavoidable assumption for dealing with adequacy is the existence, in any object, of a particular ``undefined'' point denoting the non-terminating computation of the corresponding type; hom-sets are pointed sets, and this is the only required structure. In such a category of pointed objects, there is a way of axiomatising fixpoint operators: They are maps satisfying certain equational axioms, and furthermore, satisfying a very natural non-equational axiom called rational openness. It is shown that this axiom is sufficient, and in a precise sense necessary, for adequacy. The idea is developed in the intuitionistic case (standard PCF) as well as in the linear case (linear PCF), which is obtained by augmenting a Curry-Howard interpretation of Intuitionistic Linear Logic with numerals and fixpoint constants, appropriate for the linear context. Using instantiations to concrete models of the general adequacy results, various purely syntactic properties of linear PCF are proved to hold

Available as PostScript, PDF.