Axioms for Recursion in Call-by-Value.
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.
Introduction
While the equational theories of xpoint operators in call-by-name programming
languages and in domain theory have been extensively studied
and now there are some canonical axiomatizations (including the
iteration theories [1] and Conway theories, equivalently traced cartesian
categories [12] { see [27] for the latest account), there seems no such
widely-accepted result in the context of call-by-value (cbv) programming
languages, possibly with side eects. Although the implementation of
recursion in \impure" programming language has been well-known, it
seems that the underlying semantic nature of recursive computation in
the presence of side-eects has not been studied at a suciently general
level. Regarding the widespread use of call-by-value programming
languages and the importance of recursion in real life programming, it
is desirable to have theoretically motivated and justied principles for
reasoning about recursive computation in a call-by-value setting.
In this paper we propose a candidate of such an axiomatization,
which consists of three simple axioms, including a uniformity principle
analogous to that in the call-by-name setting. Our axiomatization, of
stable uniform call-by-value xpoint operators to be introduced below,
is justied by the following two main results:
y An extended abstract of this work appeared in Proc. Foundations of Software
Science and Computation Structures (FoSSaCS 2001), Springer LNCS Vol. 2030.
Hasegawa and Kakutani
1. The  c -calculus (computational lambda calculus) [18] with a stable
uniform cbv xpoint operator is sound and complete for the models
based on the notion of uniform T -xpoint operators of Simpson and
Plotkin [27].
2. In the call-by-value -calculus [25] (= the  c -calculus plus rst-
class continuations) there is a bijective correspondence between
stable uniform cbv xpoint operators and uniform iterators, via
Filinski's construction of recursion from iteration [5].
The notion of uniform T-xpoint operators arose from the context of
Axiomatic Domain Theory [7, 26]. By letting T be a lifting monad on
a category of predomains, a uniform T-xpoint operator amounts to
a uniform xpoint operator on domains (the least xpoint operator in
the standard order-theoretic setting). In general, T can be any strong
monad on a category with nite products, thus a uniform T-xpoint
operator makes sense for any model of the computational lambda calculus
in terms of strong monads [18], and Simpson and Plotkin [27]
suggest the possibility of using uniform T-xpoint operators for modelling
call-by-value recursion. This line of considerations leads us to
our rst main result. In fact, we distill our axioms from the uniform
T-xpoint operators.
A surprise is the second one, in that the axioms precisely account for
Filinski's cbv xpoint operator derived from an iterator (innite loop
constructor) and rst-class continuations, provided that we rene Filin-
ski's notion of uniformity, for which the distinction between values and
eect-insensitive programs (characterised by the notion of centrality)
[22, 28, 10] is essential. Using our axioms, we establish the bijectivity
result between xpoint operators and iterators. Therefore here is an
interesting coincidence of a category-theoretic axiomatics (of Simpson
and Plotkin) with a program construction (of Filinski).
However, we also show that, after sorting out the underlying categorical
semantics, Filinski's construction combined with the Continuation-Passing
Style (CPS) transformation can be understood within the abstract
setting of Simpson and Plotkin. The story is summarised as
follows. As noted by Filinski, the CPS-transform of an iterator is a
usual (call-by-name) xpoint operator on the types of the form R A in
the target -calculus, where R is the answer type. If we let T be the
continuation monad R R (
, then the uniform T-xpoint operator precisely
amounts to the uniform xpoint operator on the types R A . Since
our rst main result is that the stable uniform cbv xpoint operator is
sound and complete for such uniform T-xpoint operators, it turns out
that Filinski's construction combined with the CPS transformation can
be regarded as a consequence of the general categorical axiomatics; by
Axioms for Recursion in Call-by-Value 3
specialising it to the setting with a continuation monad, we obtain a
semantic version of the second main result.
Construction of this paper
In Section 2 we recall the  c -calculus and the call-by-value -calculus,
which will be used as our working languages in this paper. In Section
3 we introduce our axioms for xpoint operators in these calculi (De-
nition and give basic syntactic results. Section 4 demonstrates how
our axioms are used for establishing Filinski's correspondence between
recursion and iteration (which in fact gives a syntactic proof of the
second main result). Up to this section, all results are presented in an
entirely syntactic manner. In Section 5 we start to look at the semantic
counterpart of our axiomatization, by recalling the categorical models
of the  c -calculus and the call-by-value -calculus. We then recall the
notion of uniform T-xpoint operators on these models in Section 6,
and explain how our axioms are distilled from the uniform T-xpoint
operators (Theorem 2, the rst main result). In Section 7, we specialise
the result in the previous section to the models of the call-by-value -
calculus, and give a semantic proof of the second main result (Theorem
4). Section 8 gives some concluding remarks.
2. The Call-by-Value Calculi
The  c -calculus (computational lambda calculus) [18], an improvement
of the call-by-value -calculus [21], is sound and complete for
1. categorical models based on strong monads (Moggi [18])
2. Continuation-Passing Style transformation into the -calculus
(Sabry and Felleisen [23])
and has proved useful for reasoning about call-by-value programs. In
particular, it can be seen as the theoretical backbone of (the typed
version of) the theory of A-normal forms [8], which enables us to
optimise call-by-value programs directly without performing the CPS
transformation.
For these reasons, we take the  c -calculus as a basic calculus for
typed call-by-value programming languages. We also use an extension
of the  c -calculus with rst-class continuations, called the call-by-
value -calculus, for which the soundness and completeness results
mentioned above have been extended by Selinger [25].
4 Hasegawa and Kakutani
2.1. The  c -calculus
The syntax, typing rules and axioms on the well-typed terms of the
c -calculus are summarised in Figure 1. The types, terms and typing
judgements are those of the standard simply typed lambda calculus
(including the unit > and binary products ). 1 c  ranges over the
constants of type . As an abbreviation, we write let x  be M in N for
denotes the set of free variables in M . (As long as
there is no confusion, we may use italic small letters for both variables
and values. Capital letters usually range over terms, though we may
also use some capital letters like F , G, H for higher-order functional
values.) The crucial point is that we have the notion of values, and the
axioms are designed so that the above-mentioned completeness results
hold. Below we may call a term a value if it is provably equal to a value
dened by the grammar. We write g  f for the composition x:g (f x)
of values f and g, and id  for the identity function x  :x.
In the sequel, we are concerned not just about the pure  c -calculus
but also about its extensions with additional constructs and axioms.
A  c -theory is a typed equational theory on the well-typed expressions
of the  c -calculus (possibly with additional constructs) which is
a congruence on all term constructions and contains the axioms of the
c -calculus. A  c -theory can be typically specied by the additional
axioms (as the congruence generated from them), or as the equational
theory induced by a model in the sense of Section 5, i.e. '
Centre and focus
In call-by-value languages, we often regard values as representing eect-
(nished or suspended) computations. While this intuition is valid,
the converse may not always be justied; in fact, the answer depends
on the computational eects under consideration.
DEFINITION 1 (centre, focus). In a  c -theory, we say that a term
central if it commutes with any other computational eect,
that is,
let x  be M in let y  be N in be N in let x  be M in L :
holds for any N :  and L : , where x and y are not free in M and
N . In addition, we say that it is central and moreover
copyable and discardable, i.e., let x  be M in hx;
and let x  be M in
1 We do not include the \computation types" T and associated constructs, as
they can be dened by
Axioms for Recursion in Call-by-Value 5
Types ranges over base types
Terms
Typing Rules:
Axioms:
let x  be V in
let x  be M in
let y  be (let x  be L in M) in be L in let y  be M in N
be M in let x  be N in f x
be M in let y  be N in hx; yi
where let x  be M in N stands for

Figure

1. The c-calculus
It is worth emphasising that a value is always focal, but the converse
is not true (see Section 7.3). A detailed analysis of these concepts in
several  c -theories is found in [10]; see also discussions in Section 5.
2.2. The call-by-value -calculus
Our call-by-value -calculus, summarised in Figure 2, is the version
due to Selinger [25]. We regard it as an extension of the  c -calculus
with rst-class continuations and sum types (the empty type ? and
binary sums +). We write : for the type
The typing judgements take the form '
is a sequence of names (ranged over by , ,. )
with their types. A judgement
represents a well-typed term M with at most m free
We write FN(M) for
6 Hasegawa and Kakutani
Types
Terms
Additional Typing Rules:
Additional Axioms:
be M in [; ]x

Figure

2. The call-by-value -calculus
the set of free names in M . In this judgement, M can be thought of
as a proof of the sequent  or the proposition
in the classical propositional
logic. Among the additional axioms, the rst one involves the mixed
substitution M [C( )=[]( )] for a term M , a context C( ) and a name
, which is the result of recursively replacing any subterm of the form
[]N by C(N) and any subterm of the form [
or further details on these
syntactic conventions.
Remark 1. We have chosen the cbv -calculus as our working language
rstly because we intend the results in this paper to be compatible
with the duality result of the second author [15] (see Section 7)
which is based on Selinger's work on the -calculus [25], and secondly
because it has a well-established categorical semantics, again thanks to
Selinger. However our results are not specic to the -calculus; they
apply also to any other language with similar semantics { for example,
we could have used Hofmann's axiomatization of control operators [13].
Also, strictly speaking, the inclusion of sum types (coproducts) is not
Axioms for Recursion in Call-by-Value 7
necessary in the main development of this paper, though they enable
us to describe iterators more naturally (as general feedback operators,
see Remark 3 in Section 4) and are also used in some principles on
iterators like diagonal property (see Section 8), and crucially needed
for the duality result in [25, 15].
Example 1. As an example, we can dene terms for the \double-
negation elimination" and the \initial map":
One can check that these combinators satisfy Hofmann's axioms in [13].
Also, we can use C (as will be done
in the programming example in SML/NJ in Section 4).
Centre and focus
In the presence of rst-class continuations, central and focal terms
coincide [28, 25], and enjoy a simple characterisation (thunkability [28]).
LEMMA 1. In a cbv -theory, the following conditions on a term
are equivalent.
1. M is central.
2. M is focal.
3. (thunkability) let x  be M in u >
We also note that central terms and values agree at function types [25].
LEMMA 2. In a cbv -theory, a term M :  !  is central if and
only if it is a value, i.e., (with x not free in M) holds.
3. Axioms for Recursion
Throughout this section, we work in a  c -theory.
3.1. Rigid functionals
The key in our axiomatization of call-by-value xpoint operators is
the notion of uniformity. In the call-by-name setting, we dene the
8 Hasegawa and Kakutani
uniformity for xpoint operators with respect to the strict maps, i.e.,
those that preserve the bottom element (divergence). In a call-by-value
setting, however, we cannot dene uniformity via this particular notion
of strict maps, simply because everything is strict { if an input does not
terminate, the whole program cannot terminate. Instead we propose to
dene the uniformity principle with respect to a class of functionals
that use their argument functions in a constrained way.
called rigid if H (x:M holds for any M :  !  , where
x and y are not free in H and M .
The word \rigid" was coined by Filinski in [5] (see discussions in Section
7.3). Intuitively, a rigid functional uses its argument exactly once, and
it does not matter whether the argument is evaluated beforehand or
evaluated at its actual use.
LEMMA 3.
are rigid, so is H 0
LEMMA 4. If H
holds (where f and y are not free in H).
Example 2. The reader may want to see rigid functionals in more
concrete ways. In the case of settings with rst-class continuations, we
have such a characterisation of rigid functionals, see Section 7.3. In
general cases, a rigid functional typically takes the following form:
:let x be f (h y) in N
the following property: h v is central for any
{ later, such an h will be called \total" (Denition 4). N can
be any term, possibly with side eects. It is easily seen that such an H
y in any  c -theory. On the other hand,
in the presence of side eects, many purely functional terms fail to be
rigid { e.g., constant functionals, as well as functionals like f:f  f .
3.2. Axioms for recursion
Now we are ready to state the main denition of this paper: our axiomatization
of the call-by-value xpoint operators.
Axioms for Recursion in Call-by-Value 9
DEFINITION 3 (stable uniform call-by-value xpoint operator). A type-indexed
family of closed values x v
is called a stable uniform call-by-value xpoint operator if the following
conditions are satised:
1. (cbv xpoint) For any value F
(where x is not free in F )
2. (stability) For any value F
(where f , x are not free in F )
3. (uniformity) For values F
holds, then H
F
G
The rst axiom is known as the call-by-value xpoint equation; the
eta-expansion in the right-hand-side means that x v
F is equal to
a value. The second axiom says that, though the functionals F and
may behave dierently, their xpoints, when applied to
values, satisfy the same xpoint equation and cannot be distinguished.
The last axiom is a call-by-value variant of Plotkin's uniformity prin-
ciple; here the rigid functionals play the r^ole of strict functions in the
uniformity principle for the call-by-name xpoint operators. Our uniformity
axiom can be justied by the fact that H (x v
same xpoint equation as x v
holds:
xpoint equation for x v
The following consideration conrms that the rigidness assumption cannot
be dropped from the uniformity axiom. Let H
be any value so that holds. Take any term M of type
Hasegawa and Kakutani
by be M in y:H f y (with f , g not free
in M ). Then we have H  H, and the uniformity would ask
G to be hold; it is easily seen that x v
and x v y, hence H must be rigid.
Remark 2. As easily seen, the uniformity implies that any rigid functional
preserves the xpoints of the identity maps: H
. It is tempting to
dene a notion of \call-by-value strictness" as this preservation of the
xpoints of identities. In the pure functional settings (like the call-by-
value PCF) where the divergence is the only eect, this call-by-value
strictness actually coincides with the rigidness (this can be veried by
inspecting the standard domain-theoretic model; see also Section 6).
However, in the presence of other eects (in particular the case with
rst-class continuations which we will study in the Section 4), rigidness
is a much stronger requirement than this call-by-value strictness; for
instance, the constant functional f:x v
id as well as the \twice" functional
are call-by-value strict (hence rigid in a pure functional
setting), but they are not rigid in many  c -theories and cannot be used
in the uniformity principle.
3.3. On the axiomatizations of uniformity
There are some alternative ways of presenting the axioms of stable
uniform cbv xpoint operators. In particular, in [5] Filinski proposed a
single uniformity axiom which amounts to our stability and uniformity
axioms.
LEMMA 5. For values F
and g, y are not free in G).
F
G
Proof.
Axioms for Recursion in Call-by-Value 11
PROPOSITION 1. The stability axiom and uniformity axiom are equivalent
to the following Filinski's uniformity axiom [5]:
For
(with x, f not free in F ), then H G.
G
Proof. Stability and uniformity imply Filinski's uniformity, because,
stability
Conversely, Filinski's uniformity implies stability and uniformity. First,
for a value F
is rigid, by Filinski's uniformity
we have the stability x v
For uniformity, suppose that we have values F
holds. Then, by Lemma 5, we have H  (f:x:F f
(g:y:G g y)  H. By applying Filinski's uniformity axiom, we obtain
Since we have already seen that stability follows from Filinski's unifor-
mity, it follows that x v
we have H
4. Recursion from Iteration
For grasping the r^ole of our axioms, it is best to look at the actual
construction in the second main result: the correspondence of recursors
and iterators in the presence of rst-class continuations due to Filinski
[5]. So we shall describe this syntactic development before going into
the semantic investigation which is the main issue of this paper. In this
section we work in a call-by-value -theory, unless otherwise stated.
12 Hasegawa and Kakutani
4.1. Axioms for iteration
As the case of recursion, we introduce a class of functions for determining
the uniformity principle for an iterator.
DEFINITION 4 (total value). In a  c -theory, a value
called is central for any value v : .
The word \total" is due to Filinski [5], though in his original denition
h v is asked to be a value rather than a central term. 3
DEFINITION 5 (uniform iterator). A type-indexed family of closed values
called a uniform iterator if the following
conditions are satised:
1. (iteration) For any value f
(i.e. loop
2. (uniformity) For values
is total and h
f
h, we have (loop
So it is natural to expect that (loop g)  h behaves in the same way as
loop f for \well-behaved" h. The uniformity axiom claims that this is
the case when h is total.
It seems that this totality assumption is necessary. For example, let
always-jumping function which
is not total); then (loop g) performs the jump to the label
, while loop f just diverges.
3 We shall warn that there is yet another use of the word \total" by Filinski [4]
where a term is called total when it is discardable (in the sense of Denition 1); see
[29] for a detailed analysis on this concept. Another possible source of confusion is
that our notion of totality does not correspond to the standard notions of \total
relations" or \total maps (in domain theory)". However, in this paper we put our
priority on the compatibility with Filinski's development in [5].
Axioms for Recursion in Call-by-Value 13
Remark 3. Despite of its very limited form, the expressive power of
an iterator is not so weak, as we can derive a general feedback operator
from an iterator using sums and rst-class continuations, which satises
(with a syntax sugar for sums)
case f a of (in 1 x
for
4.2. The construction
Surprisingly, in the presence of rst-class continuations, there is a bijective
correspondence between the stable uniform cbv xpoint operators
and the uniform iterators. We recall the construction which is
essentially the same as that in [5].
The construction is divided into two parts. For the rst part, we
introduce a pair of contravariant constructions:
Note that here we need rst-class continuations to implement step ;
(it has \classical" type). One can easily verify that
LEMMA 6.
holds.
pets holds.
LEMMA 7.
For values
is rigid or F is total.
pets
The following observation implies that the two notions of uniformity
for recursors and iterators are intimately related by this contravariant
correspondence.
14 Hasegawa and Kakutani
LEMMA 8. step bijective correspondence
between rigid functionals of total functions of  !  .
Proof. The only non-trivial part is that step ; ( ) sends a rigid
functional to a total function (the other direction and the bijectivity
follow immediately from Lemma 4 and Lemma 6). Suppose that H :
rigid. We show that step
central. This can be veried as follows:
let u be :H (y:[]y) x in let v be M in N
be M in N))x
be M in []N) x
let v be M in let u be :H (y:[]y) x in N
let v be M in :H (u:[]N) x
:(let v be M in H (u:[]N) x)
be M in u:[]N) x
Since H is rigid, it follows that
H (u:let v be M in []N) be M in u:[]N) x:We are then able to see that, if loop is a uniform iterator, the
composition
loop   step
yields a stable uniform xpoint operator restricted on the negative
types :. The cbv xpoint axiom is veried as (by noting the equation
(loop   step ;
The stability axiom holds as step (f:x:F f . The uniformity
axiom follows from Lemma 7 and Lemma 8. If H :!: F
G :!: H :!: and H is rigid (hence total by Lemma 4), the rst half
of Lemma 7 implies (step
Since step ; H is total by Lemma 8, by the uniformity of loop we have
loop ; (step
Axioms for Recursion in Call-by-Value 15
Conversely, if x v is a stable uniform xpoint operator,
gives a uniform iterator:
Again, the uniformity is a consequence of Lemma 7 and Lemma 8. One
direction of the bijectivity of these constructions is guaranteed by the
stability axiom (while the other direction follows from step ; pets
So we have established
PROPOSITION 2. There is a bijective correspondence between uniform
iterators and stable uniform cbv xpoint operators restricted on
negative types.
The second part is to reduce xpoints on an arrow type  !  to
those on a negative type This is possible because we can
implement a pair of isomorphisms between these types (again using
rst-class continuations):
switch 1
It is routinely seen that both switch 1
switch
hold. It is also easy to verify (by direct
calculation or by applying Proposition 8 in Section 7) that
LEMMA 9. switch ; and switch 1
are rigid.
By applying the uniformity axiom to the trivial equation switch ;
(switch 1
PROPOSITION 3. There is a bijective correspondence between stable
uniform cbv xpoint operators restricted on negative types and those on
general function types.
Hasegawa and Kakutani
Proof. From a stable uniform cbv xpoint operator restricted on
negative types, one can dene that on general function types by taking
the equation above as denition; because of the uniformity, this in fact
is the unique possibility of extending the operator to that on all function
types. The only nontrivial point is that the uniformity axiom on this
dened xpoint operator on general function typed can be derived from
the uniformity axiom on the xpoint operator on negative types, which
we shall spell out below. Suppose that we have values F
such that H holds. Since rigid functionals are closed under
composition (Lemma 3) and switch and switch 1 are rigid (Lemma 9),
switch 1  H  switch is also rigid. By applying the uniformity axiom
(on negative types) to the equation
(switch 1
(switch 1
we obtain
switch 1
which implies (by applying switch  to both sides of the equation)
In summary, we conclude that, in the presence of rst-class continu-
ations, stable uniform cbv xpoint operators are precisely those derived
from uniform iterators, and vice versa:
THEOREM 1. There is a bijective correspondence between uniform
iterators and stable uniform cbv xpoint operators.
switch
loop
code written in SML/NJ [17, 11] is found in Figure 3.
Axioms for Recursion in Call-by-Value 17
(* an empty type "bot" with an initial map A : bot -> 'a *)
datatype
fun A (VOID
(* the C operator, C : (('a -> bot) -> bot) -> 'a *)
(* basic combinators *)
fun step F
fun switch l
(* an iterator, loop : ('a -> 'a) -> 'a -> bot *)
(* recursion from iteration *)

Figure

3. Coding in SML/NJ (versions based on SML '97 [17])
5. Categorical Semantics
The rest of this paper is devoted to investigating the semantic counterpart
of our stable uniform cbv xpoint operators and for giving
our two main results in a coherent way. In this section we recall some
preliminaries on the underlying categorical structures which will be
used in our semantic development.
5.1. Models of the  c -calculus
Let C be a category with nite products and a strong monad
and  are the unit and multiplication of the monad
T , and  is the tensorial strength with respect to the nite products of C
(see e.g. [18, 19] for these category-theoretic concepts). We write C T for
the Kleisli category of T , and for the associated left adjoint
explicitly, J is the identity on objects and sends f 2 C (X; Y )
to  Y  f 2 C T (X; Y We assume that C has Kleisli
exponentials, i.e., for every X in C the functor J((
Hasegawa and Kakutani
has a right adjoint X This gives the structure for
modelling computational lambda calculus [18]. Specically, we x an
object for each base type b and dene the interpretation of types
as well-typed
interpreted inductively as a morphism of
once we x the interpretations of constants; see


Appendix

A for a summary. Following Moggi, we call such a structure
a computational model.
PROPOSITION 4. [18] The computational models provide a sound
and complete class of models of the computational lambda calculus.
In fact, we can use the  c -calculus as an internal language of a computational
model { up to the choice of the base category C (which
may correspond to either syntactically dened values, or more semantic
values like thunkable terms, or even something between them; see [10]
for a detailed consideration on this issue) { in a similar sense that
the simply typed lambda calculus is used as an internal language of a
cartesian closed category [16].
5.2. Models of the call-by-value -calculus
Let C be a distributive category, i.e., a category with nite products and
coproducts so that preserves nite coproducts for each
A. We call an object R a response object if there exists an exponential
R A for each A, i.e., C (  A; R) ' C ( ; R A ) holds. Given such a
structure, we can model the cbv -calculus in the Kleisli category C T
of the strong monad
[25]. A term ' M :  j  is interpreted
as a morphism of C T ([[]];
for The interpretation is in fact a typed
version of the call-by-value CPS transformation [21, 25], as sketched in


Appendix

B. Following Selinger, we call C a response category and the
Kleisli category C T a category of continuations and write R C for C T
(though in [25] a category of continuations means the opposite of R C ).
PROPOSITION 5. [25] The categories of continuations provide a sound
and complete class of models of the cbv -calculus.
As the case of the  c -calculus, we can use the cbv -calculus as an
internal language of a category of continuations [25].
Axioms for Recursion in Call-by-Value 19
5.3. Centre and focus
We have already seen the notion of centre and focus in the  c -calculus
and the cbv -calculus in a syntactic form (Denition 1). However,
these concepts originally arose from the analysis on the category-theoretic
models given as above. Following the discovery of the premonoidal
structure on the Kleisli category part C T (R C ) of these models [22],
Thielecke [28] proposed a direct axiomatization of R C not depending
on the base category C (which may be seen as a chosen category of
\values") but on the subcategory of \eect-free" morphisms of R C ,
which is the focus (equivalently centre) of R C . Fuhrmann [10] carries
out further study on models of the  c -calculus along this line.
DEFINITION 6 (centre, semantic denition). Given a computational
model with the base category C and the strong monad T , an arrow
called central if, for any g :
compositions (Y  g)  (f
Note that the products are not necessarily bifunctorial on C T ; they
form premonoidal products in the sense of [22] (the reader familiar
with this notion might prefer to
use
instead of  for indicating that
they are not cartesian products). This notion of centrality amounts to
the semantic version of centrality in Denition 1.
In this paper we do not go into the further details of these semantic
analyses. However, we will soon see that these concepts naturally arise
in our analysis of the uniformity principles for recursors and iterators.
In particular, a total value (equivalently the term x :  '
precisely corresponds to the central morphisms in the semantic
models. In the case of the models of the cbv -calculus, the centre
can be characterised in terms of the category of algebras, for which our
uniformity principles are dened; that is, we have
PROPOSITION 6. f central if and only
if its counterpart in C is an algebra morphism from the algebra (R B
to (R A ; R  A ).
We discuss more about this in Section 7; there this observation turns
out to be essential in relating the uniformity principles for recursion
and iteration in the cbv -theories. We note that this result has been
observed in various forms in [28, 25, 10].
4 In terms of C , f 2 C T (X; Y
holds for any g 2 C T (X are the
left-rst and right-rst pairings (Appendix A).
20 Hasegawa and Kakutani
6. Uniform T -Fixpoint Operators
In this section we shall consider a computational model with the base
category C and a strong monad T .
6.1. Uniform T-Fixpoint Operators
We rst recall the notion of uniform T -xpoint operator of Simpson
and Plotkin [27], which arose from considerations on xpoint operators
in Axiomatic Domain Theory (ADT) [7, 26]. In ADT, we typically
start with a category C of predomains, for example the category of
!-complete partial orders (possibly without bottom) and continuous
functions. Then we consider the lifting monad T on C , which adds a
bottom element to !-cpo's. Then objects of the form TX are pointed
cpo's (!-cpo's with bottom), on which we have the least xpoint op-
erator. It is also easily checked that such a pointed cpo has a unique
T -algebra structure (in fact any T -algebra arises in this way in this
setting, though we will soon see that this is not the case if we take a
continuation monad as T ), and an algebra morphism is precisely the
bottom-preserving maps, i.e., the strict ones. As is well known, the least
xpoint operator enjoys the uniformity principle with respect to such
strict maps. By abstracting this situation we have:
DEFINITION 7 (uniform T-xpoint operator [27]). A T-xpoint operator
on C is a family of functions
such that, for any f : holds. It is called
uniform if, for any f :
imply
TTY TY TY TY
f
Thus a T-xpoint operator is given as a xpoint operator restricted
on the objects of the form TX. One may easily check that, in the
domain-theoretic example sketched as above, the condition h
Th says that h is a strict map.
Axioms for Recursion in Call-by-Value 21
This limited form of xpoint operators, however, turns out to be
sucient to model a call-by-value xpoint operator. To see this, suppose
that we are given an object A with a T -algebra structure  :
(that is, we ask
we have   (  f
Therefore we can extend a T-xpoint operator ( )  to be a xpoint
objects with T -algebra structure by dening f
Moreover, given a uniform T-xpoint operator ( )  , it is easy to see
that this extended xpoint operator ( )  on T -algebras is uniform in
the following sense: for T -algebras
h is a T -algebra morphism) and g
f
Furthermore, such a uniform extension is unique: given a uniform
xpoint operator ( )  on objects with T -alpgebra structure, by applying
this uniformity to   (  f
completely
determined by its restriction on free algebras (TX;X ), i.e., a uniform
T-xpoint operator.
In particular, Kleisli exponentials X ) Y t in this scheme, where
the T -algebra structure given as the
adjoint mate (currying) of
(see

Appendix

A for notations). Since we interpret a function type as
a Kleisli exponential, this fact enables us to use a uniform T-xpoint
operator for dealing with a xpoint operator on function types.
We note that   corresponds to
an eta-expansion in the  c -calculus. That is, if a term '
represents an arrow f
22 Hasegawa and Kakutani
LEMMA 10. For any ' M :  !  ,
holds.
Proof.
This observation is frequently used in distilling the axioms of the stable
uniform cbv xpoint operators below.
6.2. Axiomatization in the  c -calculus
Using the  c -calculus as an internal language of C T , the equation f
f  f  on X ) Y can be represented as
The side condition means that F corresponds
to an arrow in C (X
the operator ( can be
equivalently axiomatized by a slightly dierent operator
subject to f z = X;Y  f  f z , with an additional condition f
X;Y  f) z . In fact, we can dene such a ( ) z as ( X;Y  ( ))  and
conversely and it is easy to see that these are in
bijective correspondence. The condition f equivalently
z , is axiomatized in the  c -calculus as (by recalling
that   X;Y  ( ) gives an eta-expansion)
which is precisely the cbv xpoint axiom. The additional condition
f) z is axiomatized as
F is a value
This is no other than the stability axiom. We thus obtain the rst two
axioms of our stable uniform cbv xpoint operators, which are precisely
modelled by T-xpoint operators.
Axioms for Recursion in Call-by-Value 23
6.3. Uniformity axiom
Next, we shall see how the uniformity condition on T-xpoint operators
can be represented in the  c -calculus. Following the previous discus-
sions, we consider H it is an algebra
morphism from (X ) Y; X;Y ) to (X 0 Spelling out this
condition, we ask H to satisfy H  equivalently
In terms of the  c -calculus,
this means that an eta-expansion commutes with the application of H;
therefore, in the  c -calculus, we to be a
value such that
holds for any M : We have called such an H rigid, and dened
the uniformity condition with respect to such rigid functionals.
Remark 4. Actually the uniformity condition obtained by the argument
above is as follows, which is slightly weaker than stated in
Denition 3:
For
G.
However, thanks to Lemma 5, we can justify the uniformity axiom in
Denition 3.
6.4. Soundness and completeness
Now we give one of the main result of this paper.
THEOREM 2. The computational models with a uniform T -xpoint
operator provide a sound and complete class of models of the computational
lambda calculus with a stable uniform call-by-value xpoint
operator.
5 A characterisation of rigid functions (on computation types) in the same spirit
is given in Filinski's thesis [6] (Section 2.2.2) though unrelated to the uniformity of
Hasegawa and Kakutani
This extends Proposition 4 with the stable uniform call-by-value
xpoint operator and uniform T-xpoint operators. Most part of soundness
follows from a routine calculation. However, the interpretation of
the stable uniform call-by-value xpoint operator and the verication
of the axioms do require some care: we need to consider a parameterized
xpoint operator (with parameterized uniformity) for interpreting
the free variables. Thus we have to parameterize the considerations in
Section 6.1. This can be done along the line of Simpson's work [26].
Below we outline the constructions and results needed for our purpose.
PROPOSITION 7. A uniform T -xpoint operator uniquely extends to
a family of functions
where X ranges over objects of C and
such that
1. (parameterized xpoint) For
f
holds
2. (parameterized uniformity) For
Th   X;A and h  h X;A imply g
ThX;A
A
Here we only give the construction of f
A and omit the proof (which largely consists of lengthy
diagram chasings and we shall leave it for interested readers { see also
[26]). Let
(recall that is the T -algebra structure on
Using , we dene dfe
Axioms for Recursion in Call-by-Value 25
Finally we have f
A. By trivialising
the parameterization and by considering just the free algebras, one can
recover the original uniform T-xpoint operator. The uniqueness of the
extension follows from the uniformity (essentially in the same way as
described in Section 6.1).
Using this parametrically uniform parameterized xpoint operator,
now it is not hard to interpret a stable uniform call-by-value xpoint
operator in a computational model with a uniform T-xpoint operator
and check that all axioms are validated.
Completeness is shown by constructing a term model, for which
there is no diculty. Since the uniform T-xpoint operator on this
term model is directly dened by the stable uniform call-by-value x-
point operator on the types also because we have
already observed that rigid functionals are characterized as the algebra
morphisms in this model, this part is truly routine.
7. Recursion from Iteration Revisited
7.1. Iteration in the category of continuations
Let C be a response category with a response object R. An iterator
on the category of continuations R C is a family of functions (
R C
Spelling out this denition in C , to give an iterator on R C is to give a
family of functions ( (R A ; R A
holds for f 2 C (R A ; R A ). Thus an iterator on R C (hence in the cbv -
calculus) is no other than a xpoint operator on C (hence the target
call-by-name calculus) restricted on objects of the form R A (\negative
objects").
Example 3. We give a simple-minded model of the cbv -calculus
with an iterator. Let C be the category of !-cpo's (possibly without
bottom) and continuous maps, and let R be an !-cpo with bottom.
Since C is a cartesian closed category with nite coproducts, it serves
as a response category with the response object R. Moreover there is
a least xpoint operator on the negative objects R A because R A has
a bottom element, thus we have an iterator on R C (which in fact is a
unique uniform iterator in the sense below).
Remark 5. A careful reader may notice that we actually need a parameterized
version of the iterator for interpreting free variables as
well as free names: should be dened as a function from R C (X
A+Y ) to R C (X  A; Y ). However, this parameterization, including
26 Hasegawa and Kakutani
that on uniformity discussed below, can be done in the same way as in
the previous section (and is much easier); a uniform iterator uniquely
extends to a parametrically uniform parameterized iterator { we leave
the detail to the interested reader.
7.2. Relation to uniform T-fixpoint operators
For any object A, the negative object R A canonically has a T -algebra
structure
:x A :m (f R A
for the monad
. Thus the consideration on the uniform T -
xpoint operators applies to this setting: if this computational model
has a uniform T-xpoint operator, then we have a xpoint operator on
negative objects, hence we can model an iterator of the cbv -calculus
in the category of continuations.
Conversely, if we have an iterator on R C , then it corresponds to a
xpoint operator on negative objects in C , which of course include
objects of the form
. Therefore we obtain a T-xpoint
operator. It is then natural to expect that (along the consideration
in Section 6.1), if the iterator satises a suitable uniformity condition,
then it bijectively corresponds to a uniform T-xpoint operator. This
uniformity condition on an iterator must be determined again with respect
to algebra morphisms. So we regard h 2 R C
as \strict" when its counterpart in C (R B ; R A ) is an algebra morphism
from (R to (R A ; A ), i.e., h
holds in C . We
say that an iterator ( )  on R C is uniform if f holds for
THEOREM 3. Given a response category C with a response object R,
to give a uniform R R (
-xpoint operator on C is to give a uniform
iterator on R C .
Proof. Immediate, since a uniform R R (
-xpoint operator uniquely
extends to a uniform xpoint operator on negative objects (hence a
uniform iterator) { the uniqueness of the extension follows from the
uniformity (by the same argument as given in Section 6.1). 2
Axioms for Recursion in Call-by-Value 27
Fortunately, the condition to be an algebra morphism is naturally
represented in a cbv -theory. A value h : A!B represents an algebra
morphism if and only if
holds { in fact, the CPS transformation (see Appendix B) of this equation
is no other than the equation h
. By Lemma 1, in
a cbv -theory, this requirement is equivalent to saying that hx is a
central term for each value x (this also implies Proposition 6 in Section
5), hence h is total. Therefore we obtain the uniformity condition for
an iterator in Section 4. This is remarkable, as it says that the idea of
dening the uniformity principle of xpoint operators with respect to
algebra morphisms (from ADT) and the idea of dening the uniformity
principle of iterators with respect to eect-free morphisms (from Filin-
ski's work) coincide in the presence of rst-class continuations, despite
their very dierent origins; technically, this is the substance of the left-
to-right implication of Proposition 6. In summary, we have semantically
shown Theorem 1:
THEOREM 4 (Theorem 1 restated). In a cbv -theory, there is a bijective
correspondence between the stable uniform cbv xpoint operators
and the uniform iterators.
In a sense, the syntactic proof in Section 4 gives an example of direct
style reasoning, whereas this semantic proof provides a continuation-passing
style reasoning on the same result. We can choose either stable
uniform xpoint operators (in syntactic, direct style) or uniform T -
xpoint operators (in semantic, monadic or continuation-passing style)
as the tool for reasoning about recursion in call-by-value setting; they
are as good as the other (thanks to Theorem 2).
7.3. On Filinski's uniformity
In [5] Filinski introduced uniformity principles for both cbv xpoint
operators and iterators, for establishing a bijective correspondence between
them. While his denitions turn out to be sucient for his
purpose, in retrospect they seem to be somewhat ad hoc and are strictly
weaker than our uniformity principles. Here we give a brief comparison.
First, Filinski calls a value is a value for
each value v : . However, while a value is always central, the converse
is not true. Note that, while the notion of centre is uniquely determined
for each cbv -theory (and category of continuations), the notion
of value is not canonically determined (a category of continuations
28 Hasegawa and Kakutani
can arise from dierent response categories [25]). Since the uniformity
principle is determined not in terms of the base category C but in terms
of the category of algebras, it seems natural that it corresponds to the
notion of centre which is determined not by C but by C T .
Second, Filinski calls a value H
there are total  such that
holds (cf. Example 2). It is easily checked that if H is rigid in the sense
of Filinski, it is also rigid in our sense { but the converse does not
hold, even if we change the notion of total values to ours (for instance,
switch ; in Section 4 is not rigid in the sense of Filinski). By closely
inspecting the correspondence of rigid functionals and total functions
via the step/pets and switch constructions, we can strengthen Filinski's
formulation to match ours:
PROPOSITION 8. In a cbv
if and only if there are total
such that
holds.
Proof. By pre- and post-composing switch and switch 1 , rigid functionals
of are in bijective correspondence with
those of :( are, by Lemma 8, in bijective
correspondence with the total functions of
the step/pets construction. A total function of (
is equal to hy; ki:hh 2 hy; ki; h 1
total functions We note
that total functions of are in bijective correspondence
with those of
we take hy; ki:x:k (g y
In summary, for any rigid functional H
have total  such that
holds. By simplifying the right hand side of this equation, we obtain
the result. 2
This subsumes Filinski's rigid functionals as special cases where h 2 does
not use the second argument.
Axioms for Recursion in Call-by-Value 29
8. Conclusion and Further Work
We have proposed an axiomatization of xpoint operators in typed
call-by-value programming languages, and have shown that it can be
justied in two dierent ways: as a sound and complete axiomatization
for uniform T-xpoint operators of Simpson and Plotkin [27], and also
by Filinski's bijective correspondence between recursion and iteration
in the presence of rst-class continuations [5]. We also have shown that
these results are closely related, by inspecting the semantic structure
behind Filinski's construction, which turns out to be a special case of
the uniform T-xpoint operators.
We think that our axioms are reasonably simple, and we expect they
can be a practical tool for direct-style reasoning about call-by-value
programs involving recursion, just in the same way as the equational
theory of the computational lambda calculus is the theoretical basis of
the theory of A-normal forms [23, 8].
8.1. Further principles for call-by-value recursion
It is an interesting challenge to strengthen the axioms in some systematic
ways. Below we give some results and perspectives.
Dinaturality, diagonal property, and Iteration Theories
By adding other natural axioms on an iterator in the presence of rst-
class continuations, one may derive the corresponding axioms on the
cbv xpoint operator. In particular, we note that the dinaturality
loop (g
on an iterator loop precisely amounts to the axiom
on the corresponding cbv xpoint operator x v (note that this axiom
implies both the cbv xpoint axiom and the stability axiom). Similarly,
the diagonal property on the iterator
loop (x::[; ](f
corresponds to that on the xpoint operator
These can be seen axiomatizing the call-by-value counterpart of Conway
theories [1, 12]. In [27], Simpson and Plotkin have shown that the
Hasegawa and Kakutani
equational theory induced by a uniform Conway operator (provided it
is consistent) is the smallest iteration theory of Bloom and
Esik [1],
which enjoys very general completeness theorem. Regarding this fact,
we conjecture that our axioms for stable uniform cbv xpoint operators
together with the dinaturality and diagonal property capture all the
valid identities on the cbv xpoint operators, at least in the presence
of rst-class continuations.
Mutual recursion and extensions to product types
One may further consider the call-by-value version of the Bekic property
(another equivalent axiomatization of dinatural and diagonal properties
[12]) along this line, which could be used for reasoning about mutual
recursion. For this purpose it is natural to extend the denition of
xpoint operators on product types of function types, and also extend
the notion of rigid functionals to those with multiple parameters. These
extensions are syntactically straightforward and semantically natural
(as the category of algebras is closed under nite products). Spelling
this out, for , we can (uniquely) extend
the xpoint operator on    0 by (using the idea of Section
property is
stated as, for
. For example, from
Bekic property and uniformity, we can show equations like x v
Fixpoint objects
Another promising direction is the approach based on xpoint objects
[2], as a uniform T-xpoint operator is canonically derived from a x-
point object whose universal property implies strong proof principles.
For instance, in Example 3, a uniform iterator is unique because the
monad R R (
has a xpoint object. For the setting with rst-class con-
tinuations, it might be fruitful to study the implications of the existence
of a xpoint object of continuation monads.
Graphical axioms
Jerey [14] argues the possibility of partial traces as a foundation of
graphical reasoning on recursion in call-by-value languages. Schweimeier
and Jerey [24] demonstrate that such graphical axioms can be used to
Axioms for Recursion in Call-by-Value 31
verify the closure conversion phase of a compiler. Similar consideration
is found in Fuhrmann's thesis [10]. It follows that most of the equalities
proposed in these approaches can be derived (up to some syntactic
dierences) from the axioms for stable uniform call-by-value xpoint
operators with dinatural and diagonal (or Bekic) property; detailed
comparisons, however, are left as a future work.
In a related but dierent direction, Erkok and Launchbury [3] propose
graphical axioms for reasoning about recursion with monadic
eects in lazy functional programming languages. Friedman and Sabry
[9] also discuss about recursion in such settings (\unfolding recursion"
versus \updating recursion") and propose an implementation of \up-
dating recursion" via a monadic eect. Although these approaches have
the common underlying semantic structure as the present work, the
problems cosidered are rather of dierent nature and it is not clear
how they can be compared with our work.
8.2. Relating recursion in call-by-name and call-by-value
The results reported here can be nicely combined with Filinski's duality
[4] between call-by-value and call-by-name languages with rst-class
control primitives. In his MSc thesis [15], the second author demonstrates
that recursion in the call-by-name -calculus [20] exactly corresponds
to iteration in the call-by-value -calculus via this duality,
by extending Selinger's work [25]. Together with the results in this
paper, we obtain a bijective correspondence between call-by-name recursion
and call-by-value recursion (both subject to suitable uniformity
principles)
Recursion in
cbn -calculus , Iteration in
cbv -calculus , Recursion in
cbv -calculus
which seems to open a way to relate the reasoning principles on recursive
computations under these two calling strategies.

Acknowledgements

We thank Shin-ya Katsumata and Carsten Fuhrmann for helpful discussions
and their interests on this work, and the anonymous reviewers
of FoSSaCS 2001 and this submission for numerous insightful sugges-
tions. Part of this work was done while the rst author was visiting
Laboratory for Foundations of Computer Science, University of
Edinburgh.
Hasegawa and Kakutani



--R

Iteration Theories.
New foundations for

Declarative continuations: an investigation of duality in programming language semantics.
Recursion from iteration.
Controlling
Axiomatic Domain Theory in Categories of Partical Maps.
The essence of compiling with continuations.
Recursion is a computational e


Models of Sharing Graphs: A Categorical Semantics of let and letrec.
Sound and complete axiomatisations of call-by-value control operators

Duality between Call-by-Name Recursion and Call-by- Value Iteration
Introduction to Higher Order Categorical Logic.

Computational lambda-calculus and monads
Notions of computation and monads.


Premonoidal categories and notions of computation.
Reasoning about programs in continuation-passing style

Control categories and duality: on the categorical semantics of the lambda-mu calculus
Recursive types in Kleisli categories.
Complete axioms for categorical
Categorical Structure of Continuation Passing Style.
Using a continuation twice and its implications for the expressive power of call/cc.
--TR

--CTR
Yoshihiko Kakutani , Masahito Hasegawa, Parameterizations and Fixed-Point Operators on Control Categories, Fundamenta Informaticae, v.65 n.1-2, p.153-172, January 2005
Atsushi Ohori , Isao Sasano, Lightweight fusion by fixed point promotion, ACM SIGPLAN Notices, v.42 n.1, January 2007
Carsten Fhrmann , Hayo Thielecke, On the call-by-value CPS transform and its semantics, Information and Computation, v.188 n.2, p.241-283, 29 January 2004
Martin Hyland , Paul Blain Levy , Gordon Plotkin , John Power, Combining algebraic effects with continuations, Theoretical Computer Science, v.375 n.1-3, p.20-40, May, 2007
continuations;iteration;categorical semantics;recursion;call-by-value