[TYPES] Lambda calculus with callcc and Moggi's monadic metalanguage
emakarov
emakarov at cs.indiana.edu
Sun Jul 23 23:05:10 EDT 2006
I am studying simply-typed call-by-value (CBV) lambda calculus with
Felleisen's control operator C, or with Scheme's call/cc. For my goal
(removing useless subterms of singleton type) I need beta reductions which
are more general than CBV ones, namely, which allow a function's argument to
be any "pure" term and not necessarily a value. Here "pure" means that the
term does not invoke control operators, i.e., does not cause side effects.
I think that it would be convenient to translate this lambda calculus into
Moggi's monadic metalanguage (MML) which explicitly separates terms with
side effects from pure terms. Terms with side effects have type (M sigma)
where M is a new type constructor, and they have to be evaluated using a
special construct do x <- t1; t2 (computational reductions). Pure terms, on
the other hand, admit arbitrary beta reductions.
However, I believe that just defining the translation does not solve
anything. One has to actually prove that beta reductions on pure term do not
change the program's answer. So one has to prove something like bisimulation
between computational and beta reductions.
I am wondering if somebody has defined this translation from lambda calculus
with control operators into MML and proved the corresponding properties.
More precisely, I'd like to know if
(1) there is a translation which inserts the least number of M's (for
example, it should *not* change every function type sigma1 -> sigma2 into
sigma1 -> M sigma2). Ideally, only terms with side effects should have type
starting with M.
(2) it is proved that arbitrary beta reductions do not change the program's
answer.
Thank you for your help.
Yevgeniy
More information about the Types-list
mailing list