Computational Effects and Operations: An Overview
---
paper_title: Semantics for Algebraic Operations

paper_content:

Abstract Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form αx:(Tx)n → Tx provides a definitive semantics for algebraic operations added to the computational λ-calculus. We recall a definition for which we have elsewhere given adequacy results for both big and small step operational semantics, and we show that it is equivalent to a range of other possible natural definitions of algebraic operation. We outline examples and non-examples and we show that our definition is equivalent to one for call-by-name languages with effects, too.
---
paper_title: Notions of Computation Determine Monads

paper_content:

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
---
paper_title: Notions of computation and monads

paper_content:

Abstract The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values ) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations , that provide a correct basis for proving equivalence of programs for a wide range of notions of computation .
---
paper_title: Combining Computational Effects: Commutativity and Sum

paper_content:

We seek a unified account of modularity for computational effects, using the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi’s side-effects monad transformer. And we give a theory for the sum of computational effects, which in particular yields Moggi’s exceptions monad transformer.
---
paper_title: Adequacy for Algebraic Effects

paper_content:

Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λc, a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with-- and without--recursion, an extension of λc with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: nondeterminism and probabilistic nondeterminism.
---
paper_title: Call-by-Push-Value: A Subsuming Paradigm

paper_content:

Call-by-push-value is a new paradigm that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can be seen as arising, via translations that we will provide, from similar semantics for call-by-observable. ::: ::: To explain call-by-observable, we first discuss general operational ideas, especially the distinction between values and computations, using the principle that "a value is, a computation does". Using an example program, we see that the lambda-calculus primitives can be understood as push/pop commands for an operand-stack. ::: ::: We provide operational and denotational semantics for a range of computational effects and show their agreement. We hence obtain semantics for call-by-name and call-by-value, of which some are familiar, some are new and some were known but previously appeared mysterious.
---
paper_title: Combining Computational Effects: Commutativity and Sum

paper_content:

We seek a unified account of modularity for computational effects, using the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi’s side-effects monad transformer. And we give a theory for the sum of computational effects, which in particular yields Moggi’s exceptions monad transformer.
---
paper_title: Semantics for Algebraic Operations

paper_content:

Abstract Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form αx:(Tx)n → Tx provides a definitive semantics for algebraic operations added to the computational λ-calculus. We recall a definition for which we have elsewhere given adequacy results for both big and small step operational semantics, and we show that it is equivalent to a range of other possible natural definitions of algebraic operation. We outline examples and non-examples and we show that our definition is equivalent to one for call-by-name languages with effects, too.
---
paper_title: Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads

paper_content:

A right adjoint functor is said to be of descent type if the counit of the adjunction is pointwise a coequalizer. Building on the results of Tholen's doctoral thesis, we give necessary and sufficient conditions for a composite to be of descent type when each factor is so. We apply this to show that every finitary monad on a locally-finitely-presentable enriched category A admits a presentation in terms of basic operations and equations between derived operations, the arties here being the finitely-presentable objects of A.
---
paper_title: Notions of Computation Determine Monads

paper_content:

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
---
paper_title: A powerdomain construction

paper_content:

We develop a powerdomain construction, $\mathcal{P}[ \cdot ]$, which is analogous to the powerset construction and also fits in with the usual sum, product and exponentiation constructions on domains. The desire for such a construction arises when considering programming languages with nondeterministic features or parallel features treated in a nondeterministic way. We hope to achieve a natural, fully abstract semantics in which such equivalences as $(p\textit{ par } p) = (q\textit{ par }p)$ hold. The domain ($D \to $ Truthvalues) is not the right one, and instead we take the (finitely) generable subsets of D. When D is discrete they are ordered in an elementwise fashion. In the general case they are given the coarsest ordering consistent, in an appropriate sense, with the ordering given in the discrete case. We then find a restricted class of algebraic inductive partial orders which is closed under $\mathcal{P}[ \cdot ]$ as well as the sum, product and exponentiation constructions. This class permits the...
---
paper_title: A probabilistic powerdomain of evaluations

paper_content:

A probabilistic power domain construction is given for the category of inductively complete partial orders. It is the partial order of continuous
---
paper_title: Notions of Computation Determine Monads

paper_content:

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
---
paper_title: Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads

paper_content:

A right adjoint functor is said to be of descent type if the counit of the adjunction is pointwise a coequalizer. Building on the results of Tholen's doctoral thesis, we give necessary and sufficient conditions for a composite to be of descent type when each factor is so. We apply this to show that every finitary monad on a locally-finitely-presentable enriched category A admits a presentation in terms of basic operations and equations between derived operations, the arties here being the finitely-presentable objects of A.
---
paper_title: Notions of Computation Determine Monads

paper_content:

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
---
paper_title: A probabilistic powerdomain of evaluations

paper_content:

A probabilistic power domain construction is given for the category of inductively complete partial orders. It is the partial order of continuous
---
paper_title: Algebraic Theory Of Processes

paper_content:

Algebraic Theory of Processes provides the first general and systematic introduction to the semantics of concurrent systems, a relatively new research area in computer science. It develops the mathematical foundations of the algebraic approach to the formal semantics of languages and applies these ideas to a particular semantic theory of distributed processes. The book is unique in developing three complementary views of the semantics of concurrent processes: a behavioral view where processes are deemed to be equivalent if they cannot be distinguished by any experiment; a denotational model where processes are interpreted as certain kinds of trees; and a proof-theoretic view where processes may be transformed into equivalent processes using valid equations or transformations. It is an excellent guide on how to reason about and relate behavioral, denotational, and proof-theoretical aspects of languages in general: all three views are developed for a sequence of increasingly complex algebraic languages for concurrency and in each case they are shown to be equivalent. Algebraic Theory of Processes is a valuable source of information for theoretical computer scientists, not only as an elegant and comprehensive introduction to the field but also in its discussion of the author's own theory of the behavioral semantics of processes ("testing equivalence") and original results in example languages for distributed processes, It is self-contained; the problems addressed are motivated from the standpoint of computer science, and all the required algebraic concepts are covered. There are exercises at the end of each chapter.
---
paper_title: Combining Computational Effects: Commutativity and Sum

paper_content:

We seek a unified account of modularity for computational effects, using the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi’s side-effects monad transformer. And we give a theory for the sum of computational effects, which in particular yields Moggi’s exceptions monad transformer.
---
paper_title: A probabilistic powerdomain of evaluations

paper_content:

A probabilistic power domain construction is given for the category of inductively complete partial orders. It is the partial order of continuous
---
paper_title: Adequacy for Algebraic Effects

paper_content:

Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λc, a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with-- and without--recursion, an extension of λc with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: nondeterminism and probabilistic nondeterminism.
---
paper_title: Towards a mathematical operational semantics

paper_content:

We present a categorical theory of 'well-behaved' operational semantics which aims at complementing the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if the operational rules of a programming language can be modelled as a natural transformation of a suitable general form, depending on functorial notions of syntax and behaviour, then one gets the following for free: an operational model satisfying the rules and a canonical, internally fully abstract denotational model which satisfies the operational rules. The theory is based on distributive laws and bialgebras; it specialises to the known classes of well-behaved rules for structural operational semantics, such as GSOS.
---
paper_title: Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads

paper_content:

A right adjoint functor is said to be of descent type if the counit of the adjunction is pointwise a coequalizer. Building on the results of Tholen's doctoral thesis, we give necessary and sufficient conditions for a composite to be of descent type when each factor is so. We apply this to show that every finitary monad on a locally-finitely-presentable enriched category A admits a presentation in terms of basic operations and equations between derived operations, the arties here being the finitely-presentable objects of A.
---
paper_title: Notions of Computation Determine Monads

paper_content:

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
---
paper_title: Combining Computational Effects: Commutativity and Sum

paper_content:

We seek a unified account of modularity for computational effects, using the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi’s side-effects monad transformer. And we give a theory for the sum of computational effects, which in particular yields Moggi’s exceptions monad transformer.
---
paper_title: Adequacy for Algebraic Effects

paper_content:

Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λc, a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with-- and without--recursion, an extension of λc with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: nondeterminism and probabilistic nondeterminism.
---
paper_title: Towards a mathematical operational semantics

paper_content:

We present a categorical theory of 'well-behaved' operational semantics which aims at complementing the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if the operational rules of a programming language can be modelled as a natural transformation of a suitable general form, depending on functorial notions of syntax and behaviour, then one gets the following for free: an operational model satisfying the rules and a canonical, internally fully abstract denotational model which satisfies the operational rules. The theory is based on distributive laws and bialgebras; it specialises to the known classes of well-behaved rules for structural operational semantics, such as GSOS.
---
paper_title: Call-by-Push-Value: A Subsuming Paradigm

paper_content:

Call-by-push-value is a new paradigm that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can be seen as arising, via translations that we will provide, from similar semantics for call-by-observable. ::: ::: To explain call-by-observable, we first discuss general operational ideas, especially the distinction between values and computations, using the principle that "a value is, a computation does". Using an example program, we see that the lambda-calculus primitives can be understood as push/pop commands for an operand-stack. ::: ::: We provide operational and denotational semantics for a range of computational effects and show their agreement. We hence obtain semantics for call-by-name and call-by-value, of which some are familiar, some are new and some were known but previously appeared mysterious.
---

Title: Computational Effects and Operations: An Overview

Section 1: Introduction
Description 1: Introduce the motivation and scope of the paper, including an overview of the semantics of programming languages and computational effects.

Section 2: Enriched Lawvere Theories
Description 2: Introduce the concept of countable enriched Lawvere theories, provide examples, and explain their relationship with monads.

Section 3: Combining Computational Effects
Description 3: Discuss the natural combinations of countable enriched Lawvere theories and the various ways in which computational effects can be combined.

Section 4: Operational Semantics
Description 4: Present a unified structural operational semantics for computational effects using Lawvere theories and discuss its implications.

Section 5: Further Work
Description 5: Outline current work and future questions, including the study of deconstructors, extensions to local phenomena, and relationships with enriched equational theories.