The crossroads of categorical algebra and game semantics : an investigation into the application of Kleisli categories and related constructions to the study of Full Abstraction for nondeterministic effects in Algol-like languages

Starting with a Fully Abstract denotational semantics for an Algol-like programming language, we investigate how we can use techniques of categorical algebra to adapt the semantics when the original language is extended with various nondeterministic effects. Our running example for the base denotational semantics is Abramsky and McCusker’s game semantics for Idealized Algol. We give a full presentation of this game semantics, including an alternative proof of Computational Adequacy that uses Laird’s concept of a sequoidal category rather than the combinatorial proof from Abramsky and McCusker’s original paper. We introduce the familiar concepts of monads and Kleisli categories, and prove a Full Abstraction result that shows how the process of passing to certain Kleisli categories corresponds to particular language extensions. We link these language extensions to may-and must-testing for finite and countable nondeterminism, showing how we can construct Fully Abstract models of these effects using Kleisli categories. We introduce a generalization of monads: lax actions, also known as parametric monads. We investigate various corresponding generalizations of Kleisli categories, and prove a Full Abstraction result for one such generalization, showing how it too can be used to construct a model of an extended version of our original Algol-like language. We show how a special case of this construction can be adapted to model a probabilistic language.