Fall 2016

Compositionally, Adequacy, and Full Abstraction

Monday, Dec. 5, 2016 10:00 am10:35 am PST

Add to Calendar


Calvin Lab Auditorium

We consider compositionality, adequacy, and full abstraction from an algebraic point of view. A denotational semantics d is compositional if the denotation of a phrase is a function of the denotations of its (immediate) parts. Modelling a language as an initial  algebra over a finitary signature, compositionality is then that the image of the denotation function d can be turned into an algebra. Thus d becomes a homomorphism — indeed an epimorphism. So  we can factor the denotation function d through a compositional denotation function h, i.e., an algebra homomorphism. 

What can we do if the given denotation function d is not compositional? Say that a  compositional denotation semantics h is adequate with respect to the given denotation function if it factors through d. Then is there a best available adequate semantics? In [Hod] Wilfrid Hodges gave a construction, which can be phrased as dividing the syntax out by the “full abstraction” equivalence (actually congruence) relation, where two phrases P and Q are equivalent in this sense if, and only if, they have the same denotation in all language contexts.  This is  the final adequate semantics, as long as we restrict ourselves to epimorphisms.

In this talk we see that this pattern extends to other cases, but, perhaps surprisingly, not all. In the first we look at languages with variable-binding, following ideas of Peter Aczel for the appropriate notion of algebra. In the second, we look at the standard framework for the denotational semantics of programming languages, namely omega cpos (i.e., partial orders with lubs of increasing omega chains). In all these cases one can work with any algebra, not just free ones. However, and perhaps surprisingly, there are cases where the pattern fails, for example if we allow function symbols with countable arities there may be no final adequate semantics. An open problem emerges: to classify the categories of algebras where the final adequate denotation functions exist.  In the case of the category of sets, we see that such T-algebras exist for any finitary monad T; it may even be that a converse holds.

[Hod] Wilfrid Hodges, Formal Features of Compositionality, Journal of Logic, Language and Information, 10(1), 7-28,2001.