Completely iterative monads in semantics of coinductive programs

Abstract

Some programs are not merely sets of batch instructions performed in isolation. They interact, either directly with the user, or with other threads and resources. This dissertation tackles the problem of mathematical description (denotational semantics) of the observable behaviour of such programs. In the tradition of denotational semantics and functional programming, one can distinguish between pure computations, which are regarded as mathematical functions, and effectful ones, like those generating behaviour. Both effects in general and behaviour of interactive systems have been thoroughly studied, and they both have elegant category-theoretic explanations: the frameworks of, respectively, monads and coalgebra. The point of this dissertation is to explore the area where the two meet. The thesis of this dissertation is that the right kind of monads to describe the observable behaviour of programs are completely iterative monads (cims), introduced by Elgot and more recently studied by Adamek and others. They are monads equipped with a certain corecursion scheme that allows us to describe the computation in a coinductive, step-wise manner. To support this, we introduce a formal coinductive semantics parametrised with a cim. We study its properties and show that it instantiates to a number of known approaches, based on metric spaces and final coalgebras. Then, we focus on studying properties of cims, especially those important in semantics and programming, like composability. We show that a number of constructions used in denotational semantics to model different aspects of behaviour are instances of the constructions that we introduce. The most important structure that we study are coinductive resumptions, generalising previous results by Moggi or Hyland, Plotkin, and Power. The language of our development is category-theoretic, and so are the properties that we investigate. We are interested in universal properties, distributive laws, algebras, and monadicity. Thus, the results apply not only to semantics and programming, but can be construed as a general investigation of algebraic structures with iteration.