When two interpretations of a programming language are given, we are naturally interested in the problem of establishing a relationship between these interpretations. A representative case is the computational adequacy of PCF, which compares the denotational semantics and the operational semantics of PCF. Problems of this sort are also seen in monadic representations of computational effects. They vary a lot depending on the combination of a computational effect, two monadic representations of it and a relationship between these monadic representations. For instance, 1. A simple problem is to compare two monadic representations of nondeter-ministic computations using the powerset monad and the list monad. 2. Filinski gave a formal relationship between the monadic representation and the CPS representation of call-by-value programs. This is to compare representations of computational effects by a monad T and the continuation monad (- ⇒ TR) ⇒ TR. 3. Wand and Vaillancourt compared two monadic representations of backtracking computations using the stream monad and the 2-CPS monad.
展开▼
