# 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*.

BRICS WWW home page