×

Algebraic operations and generic effects. (English) Zbl 1023.18006

E. Moggi [in: Proc. LICS ’89, IEEE Press, 14-23 and Inf. Comput. 93, 55-92 (1991; Zbl 0723.68073)] introduced the idea of giving a unified category-theoretic semantics for computational effects, modeling each of them in the Kleisli category of an appropriate strong monad on a base category with finite products. However, the calculus of Moggi’s semantics models does not contain operations, the constructs that actually create the effects. In order to model constructive operations that arise in describing computational effects, the authors consider, given a complete and cocomplete symmetric monoidal closed category \({\mathcal V}\) and a symmetric monoidal \({\mathcal V}\)-category \({\mathcal C}\) with cotensors and a strong \({\mathcal V}\)-monad \(\mathbb{T}\) on \({\mathcal C}\), axioms under which an Ob \({\mathcal C}\)-indexed family of operations of the form \(\alpha_x: (\mathbb{T} x)^v\to(\mathbb{T} x)^w\) provides semantics for algebraic operations on the computational \(\lambda\)-calculus.

MSC:

18C50 Categorical semantics of formal languages
68Q55 Semantics in the theory of computing
03B40 Combinatory logic and lambda calculus
Full Text: DOI