[Prev][Next][Index][Thread]
a paper on call-by-value recursion
Dear colleagues,
We wonder if the following paper is of some interest to you -- in
particular to those studying semantics of ML-like typed call-by-value
programming languages (possibly with side effects like first-class
continuations):
------------------------------------------------------------------------
Axioms for Recursion in Call-by-Value
by Masahito Hasegawa and Yoshihiko Kakutani
Abstract:
We propose an axiomatization of fixpoint operators in typed
call-by-value programming languages, and give its justifications in
two ways. First, it is shown to be sound and complete for the notion
of uniform T-fixpoint operators of Simpson and Plotkin. Second, the
axioms precisely account for Filinski's fixpoint operator derived from
an iterator (infinite loop constructor) in the presence of first-class
continuations, provided that we define the uniformity principle on
such an iterator via a notion of effect-freeness (centrality). We then
explain how these two results are related in terms of the underlying
categorical structures.
Keywords:
recursion, iteration, call-by-value, continuations, categorical semantics.
An extended abstract (short version) has appeared in
Proc. Foundations of Software Science and Computation Structures
(FoSSaCS2001), Springer LNCS 2030 (2001) pp.246-260.
A full version will appear in Higher-Order and Symbolic Computation.
Electronic copies of both versions, as well as further information
on this work are available from
http://www.kurims.kyoto-u.ac.jp/~hassei/papers/
------------------------------------------------------------------------
Let us add a few more comments. This work can be read in two ways:
- (for semantics-minded readers) as a syntactic realization of Simpson
and Plotkin's proposal (LICS2000) of using their "uniform T-fixed
point operators" (where T is a strong monad used in the Moggi-style
"monadic" modelling of call-by-value languages) as a semantics of
call-by-value recursion
- (for syntax-minded readers) as a semantic analysis of Filinski's
pioneering work on recursion and iteration in call-by-value
languages in the presence of first-class continuations (Lisp and
Symbolic Computation, 1994)
In fact, as described in the abstract, we offer a unified view on
these readings: the latter is obtained as an instance of the former,
by instantiating the strong monad T to be the continuation monad.
This story was made possible by employing the ideas and results from
the work by Power&Robinson, Thielecke, Fuhrman and Selinger on the
"direct-style" models of call-by-value programming languages.
In particular, it turns out to be crucial to sort out the relationship
between the "effect-freeness" in call-by-value languages and the
"uniformity principle" for call-by-value recursion. To this end, we
propose the notion of "rigid functional" (which is a refinement of the
notion with the same name introduced by Filinski) as a natural notion
of "strictness" in a call-by-value setting.
Best,
Masahito and Yoshihiko.
------------------------------------------------------------------------
Masahito Hasegawa <hassei@kurims.kyoto-u.ac.jp>
Yoshihiko Kakutani <kakutani@kurims.kyoto-u.ac.jp>
Research Institute for Mathematical Sciences, Kyoto University
------------------------------------------------------------------------