Abstract

We study domains equipped with algebraic structure for giving CPS interpretations of algebraic computational effects such as non-determinism. We define a notion of ``algebra with coherence'' and prove that for any signature Sigma, the category of (affine, commutative) partial Sigma-algebras and algebra homomorphisms may be embedded in a Cartesian closed category of Sigma-algebras with coherence and conditional homomorphisms.

We then describe a simple continuation-passing-style (CPS) language with binary choice. Any selection of a ``choice algebra'' (cpo-enriched idempotent and self-commutative binary operation) R as answer object induces both an operational and denotational semantics for this language. We show that the notions of testing induced by \emph{commutative} choice algebras are, precisely: may-testing, must-testing, may-and-must-testing and probabilistic testing. We study the completeness properties of these models: firstly for second-order types, by investgating when algebra homomorphisms from R^k to R can be finitely generated by the choice operation from the projections and constants We then show that full abstraction holds at all types for our may-testing, must-testing and may-and-must testing models.