Article ID Journal Published Year Pages File Type
426084 Information and Computation 2013 19 Pages PDF
Abstract

We consider the problem of establishing a relationship between two interpretations of base type terms of a λcλc-calculus extended with algebraic operations. We show that the given relationship holds if it satisfies a set of natural conditions. We apply this result to 1) comparing two monadic semantics related by a strong monad morphism, and 2) comparing two monadic semantics of fresh name creation: Starkʼs new name creation monad and the global counter monad. We also consider the same problem, relating semantics of computational effects, in the presence of recursive functions. We apply this additional by extending the previous monad morphism comparison result to the recursive case.

Keywords
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,