Complete Call-by-Value Calculi of Control Operators, I
Ryu Hasegawa
Graduate School of Mathematical Sciences, The University of Tokyo, Komaba 3-8-1, Meguro-ku, Tokyo 153-8914, Japan

arXiv:1707.02056v1 [cs.LO] 7 Jul 2017

Abstract
We give new call-by-value calculi of control operators that are complete for the continuation-passing style
semantics. Various anticipated computational properties are induced from the completeness. In the first part
of a series of papers, we give the characterization of termination properties using the continuation-passing
style semantics as well as the union-intersection type discipline.
Keywords: λµ-calculus, control operators, call-by-value, normalization, catch/throw

Introduction
After the presentation of the first formal system embodying control operators by Felleisen et al. [15],
and after the striking exposition of its relevance to the classical logic by Griffin [24], the studies of first-class
continuation exploded. Various systems have been proposed by now. If we restrict the search range to
call-by-value calculi, we still find an abundance; [15][12][48] to name a few. In this paper, we add new
systems further to the end of the long list. Our contribution is to present new call-by-value calculi that are
complete and still satisfy good properties, as explained shortly in turn.
The semantics of call-by-value calculi (as well as call-by-name calculi) is traditionally given by the
continuation-passing style (CPS) translation. From its start, it has been used in connection with the
implementation of programming languages [56]. Flanagan et al. suggests relationship to optimization
[17]. With regard to mathematical logic, it corresponds to the Kuroda translation that is a variant of
Gödel’s double negation translation [39][44]. Now the CPS translation is commonly accepted as the standard
semantics.
Given the semantics, completeness is one of the most desirable properties. If a system is not complete,
it suffers a loss of a part of the wealth that is inherited from the target of the semantics. The target of the
CPS semantics is simply the lambda calculus, the βη-reduction of which is the condensation of the essence
of computation. If not complete, thus failing to inherit the essence, the concerned system definitely misses
certain quality that it should intrinsically possess.
The widespread systems are not complete, however. None of the calculi listed in the first paragraph are
complete. Therefore the quest for complete call-by-value systems with control operators are pursued over
many years. After the first system presented by Sabry, a number of systems are proposed in the literature
[58][57][32][33][61][36][18][2][30].
Though many complete call-by-value systems are proposed so far, the computational properties are
hardly explored. Consider the Church-Rosser property or termination of evaluation, for example. Most of
the systems are equational from the beginning, thus hopeless. A few are designed as calculi having evaluation
or reduction rules. As far as the author knows, however, computational properties are scarcely contended
(one exception is confluence in [30]). It seems difficult to design a complete but well-behaved calculus.
One of the reasons why we lack of computational properties is that we must add a number of exotic rules
to a core system to obtain a complete system. For instance, several systems have a rule (λx. E[x])M = E[M ]
Email address: ryu@ms.u-tokyo.ac.jp (Ryu Hasegawa)
Preprint submitted to Elsevier

July 10, 2017

where E[·] is a call-by-value evaluation context. It deviates from the general pattern of reduction rules that
concerns with combination of a few basic constructors. Moreover, if the number of added rules increases,
intricacy of verifying properties is liable to accelerate. In order to obtain anticipated results, therefore, we
must try to (i) restrict the added rules to manageable ones and (ii) find a proof method that overcomes the
difficulty caused by the increasing number of rules.
Our main contribution is to show that a simple (indeed, very simple) modification in the call-by-value
lambda calculus leads us to complete calculi. We add a little “twist” to its syntax. If we view a calculus as a
two-story structure of syntax (terms) and reductions, we modify only the level of syntax. As a consequence,
we have only standard reduction rules found in the literature, achieving the goal (i) above. This contrasts
with previous approaches where the syntax is largely maintained and the reductions are modified.
Making use of our syntax, we verify a sharpened completeness result (Thm. 1.34). It is a kind of
completeness that takes reduction sequences into account, not only equational relations. Similar results
are given for different calculi [59][21][22]. For call-by-value calculi with control operators, this type of
completeness is proven first (as we comment above, most previous systems have no notion of reduction from
the beginning).
The sharpened completeness is a key result. It provides us with a machinery to verify computational
properties. If the target calculus satisfies a certain property, the sharpened completeness informs us how to
reinstall it in the source language. Definitely this type of argument is not our original idea. Fujita especially
uses similar technique extensively [21][22]. We can find a similar approach in de Groote [11], Sabry and
Wadler [59], and Crolard [8] as well. We systematically apply the method to prove various properties. This
way we achieve the goal (ii) above.
We dub this method proof by parasitism. It is the image of depriving nourishment from its host at low
cost. The source language controls the target calculus and let it work hard for him. The properties of the
target calculus are sucked through a channel prepared by completeness.
We apply the method of proof by parasitism to verify desirable syntactic properties. Let [[M ]] denote the
CPS translation of a term M . We first consider an untyped system. We prove the following.
(1) Our calculus enjoys the Church-Rosser property (Thm. 2.1).
(2) M is normalizable if and only if [[M ]] is normalizable (Thm. 2.11).
(3) The call-by-value evaluation of M terminates if and only if [[M ]] is solvable (Thm. 2.31).
Next we turn to type theory. We give a union-intersection type discipline for the CCV λµ-calculus. The
main results are the following type-theoretic characterization of computational properties.
(4) The type system satisfies the subject reduction/expansion property (Thm. 3.31).
(5) A term terminates with respect to the call-by-value evaluation if and only if the term is typeable
(Thm. 3.34, (1)).
(6) A term is weakly normalizing if and only if it has a type judgment that contains neither empty intersection nor empty union (Thm. 3.34, (2)).
For the call-by-name λµ-calculus, van Bakel developped a type system that incorporated union and intersection [64]. Subject reduction/expansion are verified, though computational properties are not explicitly
characterized. As far as the author knows, there has been no attempt to prove the type-theoretic characterization for the call-by-value λµ-calculus.
We have similar results characterizing the strong termination property by the CPS semantics as well
as by types. However, to avoid the paper’s being too long, we decide to discuss strong termination in the
second part of the series of papers.
Finally we disclose the tricks to obtain our complete calculi. Landin introduced the let-construct let x =
M in N in [41, p. 91]. This notation is inherited by Reynolds [56], and is widely accepted through the spread
of programming language ML, probably. In the context of call-by-value lambda calculus, the let notation
is conveniently used. However we notice that, in an earlier influential paper [40], Landin first used the
where-construct N where x = M . It has the same effect as the let-construct, but the body is written first.
Later he turned to preferring the let-construct, saying “The only consideration in choosing let and where
will be relative convenience of writing an auxiliary definition before or after the expression it qualifies” in
[41]. We propose in this paper to return to Landin’s original choice to write the let-binding to the right of
2

its body.
Another leap is audacious identification between terms. It means that we deviate from the standard
tradition that terms are built in the form of trees. We have an analogy in arithmetic. For instance, an
expression 2 + 4 + 6 allows two tree forms, (2 + 4) + 6 and 2 + (4 + 6). However, we, humans, can understand
the expression simultaneously as whichever of these trees, or even as addition of three numbers, with intended
ambiguity. We appeal to this power of humans, who can identify the entities that look similar. While this
ability is not shared by computers, there is no harm, for the behavior of identified terms is indistinguishable
observationally. The main philosophy in our design is to build a system that is usable for humans.
These modifications affect only the structure of the call-by-value lambda calculus. It is orthogonal to
control operators in a sense. So we incorporate control operators into our call-by-value lambda calculus in
two different ways. The first is the λµ-calculus and the second the catch/throw calculus after Crolard [8].
We focus mainly on the former, giving only short discussion for the latter in §4.
1. The CCV λµ-calculus
In this section, we propose a new type-free system of call-by-value λµ-calculus. We call it the CCV
λµ-calculus (CCV is the acronym of “complete call-by-value”). In fact, the calculus is complete for the
standard CPS transformation 1.32. We verify sharpened completeness involving reduction, not only equality,
in Thm. 1.34.
1.1. Syntax
The let-construct after Landin is frequently used in the syntax of languages. Traditionally it is written
in the form let x = M in N . Some authors use it as a syntax sugar of (λx. N )M , while others use it
as a primitive. For example, Moggi’s λc -calculus is an example of the latter [43]. The let-flat rule of the
λc -calculus is
let x = (let y = N in M ) in L

→

let y = N in (let x = M in L)

where we assume that y is not free in L.
We also take the let-construct as a primitive distinct from the lambda-construct. However, we write the
let-binding to the right of its body. We adopt the following syntax:
L ↾ x := M
instead of let x = M in L. Note that the order of L and M is reversed. The two terms of the let-flat rule
above correspond to
L ↾ x := (M ↾ y := N ) and (L ↾ x := M ) ↾ y := N
in the new form. Let us observe that these two terms differ only in associativity of brackets.
The new let-form works in harmony with the µ-binding of the λµ-calculus [50][51]. The call-by-value
variant of the λµ-calculus is given in [48][19]. In the rest of this subsection, we give definition of the CCV
λµ-calculus based on this new form of the let-construct.
Variables are split into two categories: ordinary variables x, y, . . . and continuation variables k, l, . . ..
Definition 1.1. The terms M and jumps J of the CCV λµ-calculus are defined by the following syntax:
M ::= x | λx. M | M M
J ::= [k]M | J ↾ x := M

| M ↾ x := M

|

µk. J

where x ranges over ordinary variables and k over continuation variables. We call the prefix [k] a jumper.

3

The terms and jumps are syntactically separated. For example, λx. [k]M is disallowed. The lambdaabstraction and the mu-abstraction bind the abstracted variables as usual. Moreover, the let-sentences
L ↾ x := M and J ↾ x := M bind the variable x the scopes of which are L and J. Definition of the set FV (M )
or FV (J) of free (ordinary and continuation) variables is standard. For example, FV (M ↾ x := N ) is given
by (FV (M ) − {x}) ∪ FV (N ). The terms and the jumps obey ordinary α-conversion rules. For example,
L ↾ x := M equals L{y/x} ↾ y := M if y is not free in L.
Notation 1.2.
(1) We use curly braces for substitution to avoid too much of the overloading of the square brackets. We use
two ways of substitution notation, {M/x} and {x 7→ M }. We select either from the aspect of readability.
(2) We write x ∈ M in place of x ∈ FV(M ) for simplicity.
As usual, we regard α-convertible terms to be equal. In addition to this, we introduce new identification
rules between terms involving the let notation.
Definition 1.3. We assume the following equality axioms:
L ↾ x := (M ↾ y := N ) = (L ↾ x := M ) ↾ y := N
(µk. J) ↾ x := M
= µk. (J ↾ x := M )
[k](L ↾ x := M )
= ([k]L) ↾ x := M.

if y 6∈ L
if k ∈
6 M

The first rule is the associativity of let-constructs, the second the commutativity between µ and let, and the
third the commutativity between jumper and let. To be precise, the first equality remains valid when y ∈ L
but x = y. However we may assume x 6= y with α-conversion if needed.
Let us consider the first rule of Def. 1.3. In rewriting from left to right, the side condition y 6∈ L does not
actually matter. The violation of the condition disappears if we α-convert the bound variable y with fresh
z as in L ↾ x := (M {z/y} ↾ z := N ). To the contrary, for the rewriting from right to left, the side condition
must be definitely fulfilled. For example, (xy ↾ x := M ) ↾ y := N never equals xy ↾ x := (M ↾ y := N ), since y
spills out of its scope. Similarly, the second equality of the definition is always applicable from left to right,
up to the α-conversion of k if needed. Hence, if we follow the convention that we do α-renaming whenever
needed, we may assume that the brackets are always set as in the right hand sides of Def. 1.3.
Remark 1.4. We often omit brackets as
L ↾ x := M ↾ y := N
µk. J ↾ x := M.
If the side conditions of Def. 1.3 fail, these are forcibly understood to be the right hand sides of the definition.
If the conditions hold, we can regard the bracketing to be in either way. If we must select one for some
reasons, we adopt the convention that the right hand sides are canonical. We omit also brackets between
jump and let as in
[k]L ↾ x := M .
We do not fix which bracketing is canonical for this pattern.
The introduction of equality means that we work on equivalence classes of syntactic trees. There is no
mathematical need to switch the positions of bodies and arguments of let-binding. However, it would be
unbearable to work with equivalences such as [k](let x = M in L) ∼ let x = M in [k]L throughout. Our
syntax makes the equivalence look friendlier to humans as well as it simplifies verification of properties.
We do not need any more the let-flat rule mentioned at the beginning. It is an advantage brought by
the addition of the equality axioms. Likewise we can dispense with a rule flipping the order of µ and let,
4

that implicitly exists in the other systems. For example, the reader may challenge a non-trivial exercise to
prove the corresponding equality (λxµk. J)M = µk. (λx. J)M from the axioms in Tab. 10 of [61, p. 246].
Definition 1.5. A term is a value if it is either a variable x or a lambda abstraction λx. M . Otherwise it
is called a non-value. Letter V is preferably used to denote values, often with no mention.
Definition 1.6. The following are the reduction rules of the CCV λµ-calculus, where the leftmost column
gives the names of rules for future reference:
(ad 1 )
(ad 2 )
(βλ )
(βlet )
(βµ )
(βjmp )
(ηλ )
(ηlet )
(ηµ )

NM
VN
(λx. M )V
M ↾ x := V
M ↾ x := µk. J
[l]µk. J
λx. V x
x ↾ x := M
µk. [k]M

→
→
→
→
→
→
→
→
→

zM ↾ z := N
(N is a non-value)
V z ↾ z := N
(V is a value; N is a non-value)
M ↾ x := V
(V is a value)
M {V /x}
(V is a value)
µk. J{[k] 7→ [k]M ↾ x := }
J{l/k}
V
(V is a value and x 6∈ V )
M
M
(k 6∈ M ).

The first two rules are called administrative rules. In them, z is a fresh variable. The notation J{[k] 7→
[k]M ↾x:=} is a standard context substitution in the λµ-calculus. Each of [k]Q occurring in J is substituted
with [k]M ↾ x := Q, unless that k lies in the scope of another µk in J. This process is done recursively.
Namely, if Q contains [k]R further, the substitution rule is applied to them as well. The substitution J{l/k}
is a shorthand of J{[k] 7→ [l]}.
As usual, substitutions {V /x} and {[k] 7→ [k]M ↾x:=} invoke α-renaming to avoid accidental collisions
of bound variables. We recall that the let-construct binds a variable as well as λ and µ. Hence, for example,
M ↾ y := N ↾ x := y → M {z/y}{y/x} ↾ z := N {y/x},
where we need the renaming of bound y with fresh z to avoid a capture by the substitution {y/x}.
Remark 1.7.
(1) By virtue of α-renaming, substitution operations respect equalities between terms. This warrants the
safety of omission of brackets in Rem. 1.4.
(2) There is ambiguity of the contexts captured by µ-reduction, caused by the equality rules given in Def. 1.3.
For example, let us consider
L ↾ x := M ↾ y := µk. J

(y 6∈ L).

We have two ways of bracketing. If we read it left-associative, µ-reduction captures the context L ↾ x :=
M ↾ y :=  as
µk. J{[k] 7→ [k]L ↾ x := M ↾ y := }.
However, if we regard the let-bindings to be right-associative, µ-reduction captures a partial context
M ↾ y :=  as
L ↾ x := µk. J{[k] 7→ M ↾ y := }.
This ambiguity is intended. Both reductions are allowed in our system. We note that the latter converges
to the former by one more application of rule (βµ ).
Similarly two ways of bracketing in µk. [l]M ↾ x := µh. J with k 6∈ J admit different reductions:
µk. [l]µh. J{[h] 7→ [h]M ↾ x := }
5

and
µh. J{[h] 7→ [h]µk. [l]M ↾ x := }.
These terms converge to a common term if we apply rule (βjmp ) to them.
(3) As derived from the reduction rules, we have
J0 ↾ x := µk. J

∗
−→

J{[k] 7→ J0 ↾ x := }

where J0 and J are jumps. In fact, if J0 has the shape [l]M , the left hand side contracts by rule (βµ ) to
[l]µk. J{[k] 7→ [k]M ↾ x := }, from which we obtain the right hand by rule (βjmp ). If J0 has the shape
J1 ↾ y := M , we transfer it to the shape [l]M ′ by the equality rules of 1.3. We do not need the second
rule exchanging precedence between µ and let, though. (The last miscellaneous comment is returned
later in 1.35.)
The derived rule above corresponds to the second case of rule (µ-ζV ) in [33, Fig. 5, p. 347]. They split
cases by types. Although our system is type-free, the behaviours are different between terms and jumps.
The latter correspond to the case of type ⊥.
Remark 1.8. All rules in Def. 1.6 are totally standard, save our particular syntax of the let-construct.
Two administrative rules are introduced in [43]. The combination of (βλ ) and (βlet ) splits the ordinary
βv -rule after Plotkin [54] into two steps. The combination is found in the core scheme of Flanagan et
al. [17]. Also the call-by-value λ-calculus by Curien and Herbelin [9] have similar rules, though the syntax
is quite different. Rule (βµ ) and (βjmp ) are standard in the λµ-calculus. Rule (ηλ ) is also standard in the
call-by-value lambda calculus. Rule (ηlet ) is found in [43] as well as in [17] in the context of the optimization
transforming to tail recursion. Rule (ηµ ) exists in [48]. These data are by no means exhaustive.
Definition 1.9. The smallest congruence relation containing the reduction rules in Def. 1.6 is denoted by
=ccv , and referred as the CCV equality.
Example 1.10. Many complete systems in the literature [57][58][33][36][2][30] contain the axiom
(λx. E[x])M = E[M ]
where E is the evaluation context of the call-by-value calculus (see Def. 2.15). Understanding the equality
to be =ccv , we can derive this axiom. If E is the void context , the equality is derivable by reduction only,
βλ
βlet
ηlet
ad 2
(λx. x)z ↾ z := M −→
as (λx. x)M −→
x ↾ x := z ↾ z := M −→
z ↾ z := M −→
M , where we assume that M is
a non-value (it is easy if M is a value). The general case is derived from (E[x] ↾ x := M ) =ccv E[M ] that is
verified by induction on the construction of E.
Let us consider two typical examples in the following. We use them as milestones to check the behavior of
the calculus throughout the paper.
Example 1.11. As the fixed-point combinator suitable for the call-by-value calculus, we suggest to use
Y =def λf z. Df Df z,

Df = λxw. f (λv. xxv)w.

The difference from the ordinary fixed-point combinator à la Curry is that our Y is fully η-expanded.
Hasegawa and Kakutani propose three axioms that the fixed-point combinator in the call-by-value calculus
should satisfy, in the simply typed setting [27]. Among the three, the first two are equational axioms, while
the last axiom has a denotational feature, stated in a conditional phrase. So here we consider the first two
axioms: the fixed-point axiom Y F = λx. F (Y F )x, and the stability axiom Y F = Y (λyx. F yx), in both
of which F is supposed to be a value. We do not mind types here. The encoded Y above satisfies the
6

fixed-point axiom, as Y F = λz. DF DF z = λz. F (λv. DF DF v)z = λz. F (Y F )z, where the equality symbol is
understood to mean =ccv . Also the stability axiom is satisfied since DF =ccv DG holds for G = λyx. F yx.
The η-expansion by z is needed for the fixed-point axiom, the expansion by w for the stability axiom, and the
expansion by v for both. We comment that Plotkin [54] suggests the version where only xx is η-expanded.
We return to this example in 2.22 and 3.8.
Example 1.12. As an example that uses control operators, we take cooperative multitasking. We consider
the case where two agents work in a cooperative manner. The coding below is essentially simplification of
the implementation of coroutine in [1, §17.1].
The following computation demonstrates that Felleisen’s C-operator [15] plays the role of the yield command switching live processes. Let τ̂ be a fixed continuation variable, representing the topmost continuation
point. Let us define
M ⊲qr N

=def

M ↾ q := λrµδ. [τ̂ ]N .

We understand M ⊲qr N to mean that the current agent runs M while the other agent is idle waiting for a
chance to run N that is encapsulated in a closure. Let us say that M is active.
Operator C is used to insert a break-point to switch the active agent. In the λµ-calculus, we can encode
the operator as CM = µk. [τ̂ ]M (λxµδ. [k]x) where δ is a dummy continuation variable. We have the following
reduction sequence:
[τ̂ ]M ↾ q := Cq ⊲qr N

∗
−→
[τ̂ ]M ↾ q := µk. [τ̂ ](λrµδ. [τ̂ ]N )(λqµδ. [k]q)
∗
−→
[τ̂ ](λrµδ. [τ̂ ]N )(λqµδ. [τ̂ ]M )
∗
−→
[τ̂ ]N ⊲rq M

Note that N becomes active. Two occurrences of q in q := Cq refer distinct variables. So we may write
M {q ′ /q} ↾ q ′ := Cq instead. But we use the same variable name deliberately. Intuitively the variable q is
understood to be the channel that passes information from one agent to the other. The variable r is the
channel in the reverse direction.
We can interpret the use of M ↾ q := Cq as inserting a break-point in a process. Namely Cq plays the role
of the yield command in the terminology of multitasking. At the break-point, the current agent pauses and
the rest of computation M is preserved in the closure λqµδ. [τ̂ ]M . The right of execution is conceded to the
other agent who starts N . If a break-point N0 ↾ r := Cr has been built in N , it may be executed eventually.
∗
Then [τ̂ ]N0 ↾ r := Cr ⊲rq M −→
[τ̂ ]M ⊲qr N0 . Namely, the right of execution is returned to the first agent
who restarts the stopped computation from M .
For example, wall = Y (λf q. (f q ↾ q := Cq)) is a program doing nothing whenever invoked and pauses
immediately conceding the right of execution to the other agent. Namely [τ̂ ] wall q ⊲qr N =ccv [τ̂ ]N ⊲rq wall q.
The implementation of multitasking is well-behaved under the condition that there is at most one occurrence of free q in M of M ⊲qr N . It is the programmer’s task to fulfill this constraint. In certain cases, it
will be useful to use multiple occurrences of q. For example, if we implement a board game where players
can retract their moves, we may reinstall the same continuation more than once.
Since our calculus has less features than the SML programming language, we adopt several modifications
and simplifications from the original. Since we consider only two agents, we do not need a queue to record
the processes waiting for restart. Our calculus does not have mutable stores. So we must pass continuation
q explicitly in the yield command Cq. We return to this example in Rem. 2.33 to discuss the call-by-value
evaluation using evaluation contexts and in Rem. 3.9 for typeability.
1.2. CPS translation
In this subsection, we define the continuation-passing style translation of the CCV λµ-calculus and verify
its soundness. It follows the idea of the colon translation to save redundant β-redices [54][59]. For readability,
we use the notation (|M |)[K] instead of M : K. At this stage, we understand K to be an arbitrary lambda
term. However, as we do later, we can restrict the range of K to the terms of particular forms. Namely, it
is a term of sort K given in Def. 1.17.
7

Definition 1.13. We define a new CPS translation [[M ]]. It depends on an auxiliary translations (|M |)[K],
(|J|), and V ∗ .
KV ∗
V1∗ V2∗ K
(|N |)[λy. V ∗ yK]
(|N |)[λx. xV ∗ K]
(|N1 |)[λx. (|N2 |)[λy. xyK]]
(|M |)[λx. (|L|)[K]]
(λk. (|J|))K
(|M |)[k]
(|M |)[λx. (|J|)]

(|V |)[K]
(|V1 V2 |)[K]
(|V N |)[K]
(|N V |)[K]
(|N1 N2 |)[K]
(|L ↾ x := M |)[K]
(|µk. J|)[K]
(|[k]M |)
(|J ↾ x := M |)

:=
:=
:=
:=
:=
:=
:=
:=
:=

x∗
(λx. M )∗

:= x
:= λxk. (|M |)[k]

[[M ]]

:= λk. (|M |)[k]

Herein V is a value and N a non-value. The ordinary variables x and y for three cases of application are
fresh, and the continuation variables k in (λx. M )∗ and [[M ]] are fresh. Other occurrences of variables x and
k share common symbols in the source language and the target language.
In case (|L↾x:=M |)[K], if K contains x as a free variable, we must perform α-conversion as (|M |)[λz. (|L{z/
x}|)[K]] using fresh z. This is a slippery point. The careful reader will find this observation used in proof of
Prop. 1.15.
Now setup is finished. We begin with verifying the soundness of the CPS-translation with respect to the
CCV equality in the source and the βη-equality in the target.
Lemma 1.14.
(1) We have (|M {V /x}|)[K] = (|M |)[K]{V ∗ /x} provided x 6∈ K.
(2) We have (|J{[k] 7→ [k]M ↾ x := }|) = (|J|){k 7→ λx. (|M |)[k]}.
Proof. Easy by compositionality of the colon translation, Def. 1.13



Proposition 1.15. If L =ccv M , then [[L]] = [[M ]] holds with respect to βη-equality.
Proof. We verify (|L|)[K] = (|M |)[K]. Among the axioms in Def. 1.3, both sides yield the same lambda
terms, save the second axiom. For this axiom, the translations of both sides contract to a common term by
β-reduction (no need of η).
Next we consider reduction rules L → M in Def. 1.6. For two administrative rules, both sides translate
∗
into the same terms. For rules βlet , βjmp , ηµ , ηλ , and ηlet , we have (|L|)[K] →
(|M |)[K] by β-reduction or
η-reduction. For the remaining two βλ and βµ , we need β-expansion as well as β-reduction. For example,
the left hand side of βµ is translated into (λk. (|J|))(λx. (|M |)[K]) while the right hand side into (λk. (|J|){k 7→
λx. (|M |)[k]})K by Lem. 1.14, (2). The former β-equals to the latter by reduction followed by expansion. 
Remark 1.16.
(1) A subtle problem is that the equality determined by Def. 1.3 is not strictly respected. As mentioned
in the proof of Prop. 1.15, [[(µk. J) ↾ x := M ]] and [[µk. (J ↾ x := M )]] are not exactly identical, only
β-equal. Hence [[M ]] is determined only up to β-equality. It may cause serious trouble in certain cases.
Fortunately the ambiguity does not injure the proof of the main theorem 1.34 and its applications
presented in this paper. See an analysis in Rem. 1.35.
8

We stress that only the second rule is problematic. The remaining two rules are strictly respected by
the CPS translation.
∗
(2) Suppose L →
M . By inspection of the proof of 1.15, we see that βη-reduction and β-expansion are
needed to obtain (|M |)[K] from (|L|)[K]. We emphasize that η-expansion is not needed. This observation
is used in Thm. 3.31 later.
1.3. Inverse translation
Following the idea of Sabry and Felleisen [58][57], we define the inverse of the CPS translation. Up to
equational theories, the inverse translation actually gives the inverse. We prove a sharpened result taking
into account the orientation of reduction in Thm. 1.34.
Until now, the target calculus of the CPS translation is the ordinary untyped lambda calculus. To define
the inverse translation, however, we regard the target as the sorted lambda calculus.
We prepare four sorts T, Q, W , and K. They are called terms, jumps, values, and continuations, respectively. Moreover, the variables are split to the variables x of sort W and the variables k of sort K.
The former are called ordinary variables and the latter continuation variables. We let T itself represent the
lambda terms of sort T , and likewise for other sorts.
Definition 1.17. The syntax of the target calculus is defined as follows:
Term
Jump
Value
Continuation

T
Q
W
K

::=
::=
::=
::=

λk. Q | W W
KW | T K
x | λx. T
k | λx. Q

where x ranges over ordinary variables and k over continuation variables. We take ordinary βη-reduction as
reduction rules. We comment that each sort is closed under βη-reduction as is straightforward by definition.
It is easy to see that, according to the translations of Def. 1.13, [[M ]] belongs to sort T , both (|M |)[K] and
(|J|) to sort Q, and V ∗ to sort W .
Definition 1.18. The inverse translation (-)−1 is a mapping from the target calculus to the CCV λµcalculus. The definition is given by induction:
T −1 :

(λk. Q)−1 := µk. Q−1
(W1 W2 )−1 := W1−1 W2−1

Q−1 :

(KW )−1
(T K)−1

:= K −1 [W −1 ]
:= K −1 [T −1 ]

W −1 :

x−1
(λx. T )−1

:= x
:= λx. T −1

K −1 :

k −1
(λx. Q)−1

:= [k]
:= Q−1 ↾ x := .

T −1 and W −1 are terms of the CCV λµ-calculus, Q−1 jumps, and K −1 jumps with a single hole . The
notation K −1 [M ] signifies to fill the hole  of K −1 with term M .
Remark 1.19. In view of Def. 1.18, it is clear that application in the translation is restricted to the
shape V V ′ between values. Hence we cannot apply administrative reductions to T −1 etc. Moreover, once
application is restricted so, reduction steps preserve the shape since they send values to values (note that
variables are able to be substituted only with values). So administrative rules can never be applied later on.

9

Definition 1.20. Reduction by non-administrative rule is called practical. For technical reasons, we call
reduction by rule (ηµ ) : µk. [k]M → M vertical.
Lemma 1.21. Vertical reductions are strongly terminating and confluent.
Proof. Easy.



V
P
L −→
M holds where V denotes a one-step vertical reduction and P a
Lemma 1.22. Suppose L′ ←−
one-step practical reduction. There is a term M ′ such that
P

✻

L
V

✻

✻

✻

L′

M

P?

V∗

M′

where the bottom P ? denotes a one-step practical reduction or an equality and the right V ∗ a finite number
of vertical reductions (contrary to the usage in Def. 1.13).
Proof. There are only three patterns of overlapping redices yielding critical pairs: L ↾ x := µk. [k]M and
[l]µk. [k]M where k 6∈ M in either, and µk. [k]µl. J where k 6∈ µl. J. Proof is easy.

Note that Lem. 1.22 excludes administrative reductions. Indeed it fails, since vertical reductions may create
values.
∗

∗

V
P
Corollary 1.23. Suppose L′ ←−
L −→
M where V ∗ denotes a finite number of vertical reductions and P ∗
a finite sequence of practical reductions. There is a term M ′ such that
P∗

✻

L
V∗

✻

✻

✻

L′

M

P∗

V∗

M′ .

Proof. We stack the square diagram of Lem. 1.22 vertically to replace V with V ∗ , then horizontally to
replace P with P ∗ . (Our specific syntactic design notably simplifies the proof here. We do not have to be
bothered by transformation between equivalent terms, as we can identify terms only by ignoring brackets.
It enables verification by simply laying square bricks.)

Corollary 1.23 is used later in Thm. 1.34. Next let us prove (a half of) that the inverse translation is actually
the inverse of the CPS.
Lemma 1.24. Provided x 6∈ K, we have K −1 [L ↾ x := M ] = K −1 [L] ↾ x := M by the equality rules of Def. 1.3
(but with no use of the second rule interchanging µ and let; see 1.35).
Proof. Easy.



Proposition 1.25. Let M be a term of the CCV λµ-calculus. There is a term M † of the calculus such that
A∗
V∗
M −→
M † ←−
[[M ]]−1 (notice the direction). Here A∗ denotes a finite number of administrative reductions
∗
and V a finite number of vertical reductions. As [[M ]] is determined only up to β-equality (Rem. 1.16), we
choose an arbitrary one among those obtained by bracketing between µ and let.
10

Proof. For terms of the form of application define we M † as follows:
(V1 V2 )†
(V N )†
(N V )†
(N1 N2 )†

:=
:=
:=
:=

V1† V2†
V † y ↾ y := N †
xV † ↾ x := N †
xy ↾ y := N2† ↾ x := N1†

where V denotes a value and N a non-value. For terms of other forms and for jumps, definition of M † (and
A∗
J † ) is simply homomorphic. For example, (λx. M )† := λx. M † . By definition, M −→
M † is evident. To
∗
∗
−1 V
†
−1 V
−1
†
verify [[M ]] −→ M , we show ((|M |)[K]) −→ K [M ]. Proof is straightforward. To manipulate the
case M = N1 N2 , we need Lem. 1.24. Since the lemma does not depend on the equality interchanging µ and
V∗
let-binding, [[M ]]−1 −→
M † does not change the chosen bracketing structure. This is why we can choose an
arbitrary bracketing for [[M ]].

Corollary 1.26. [[M ]]−1 =ccv M holds for every CCV λµ-term M .



Remark 1.27.
(1) The term [[M ]]−1 is free from administrative redices by Rem. 1.19. Namely, it is fully let-expanded.
This property corresponds to the main result related to A-normal forms in Flanagan et al. [17, §4]. In
that paper, (kW )−1 is defined as W −1 , the variable k discarded. In our definition, (kW )−1 = [k]W −1 .
Hence we need vertical reductions to collapse µk. [k].
(2) Closely related (and often better) results are proved for different systems in previous works. For example,
∗
Sabry and Felleisen verify [[M ]]−1 −→
M for the call-by-value calculus with no control operators [58,
Thm. 10, p. 310]. Fujita verifies [[M ]]−1 ≡ M for the call-by-name second-order calculus [21, Thm. 32,
p. 204][22, Cor. 17, p. 329].
1.4. Completeness
By virtue of the inverse translation, we can verify completeness of the CPS translation. The completeness
respects reduction, not only equality. The results in this subsection are main vehicles in the rest of this
paper. The β-redices of the target calculus are manipulated in Lem. 1.28 and 1.29, and the η-redices in
Lem. 1.30.
+
(Q{K/k})−1 .
Lemma 1.28. We have ((λk. Q)K)−1 −→

Proof. First we observe that (Q{λx. Q0 /k})−1 is syntactically equal to Q−1 {[k] 7→ Q−1
0 ↾ x := }. Proof
of the lemma is by case splitting. The case of K = k is easy. If K = λx. Q0 , the left hand side equals
−1
Q−1
, which contracts to Q−1 {[k] 7→ Q−1
0 ↾ x := µk. Q
0 ↾ x := } as noted in Rem. 1.7, (3). Now we use
the observation above. In this proof, we use rule (βµ ) and rule (βjmp ) of Def 1.6.

Lemma 1.29.
+
(T {W/x})−1 .
(1) We have ((λx. T )W )−1 −→
−1 +
(2) We have ((λx. Q)W ) −→ (Q{W/x})−1 .
Proof. We show (1). The left hand side equals (λx. T −1 )W −1 , which contracts to T −1 ↾ x := W −1 , then
to T −1 {W −1 /x} since W −1 is a value. It is easy to show T −1 {W −1 /x} = (T {W/x})−1 . (2) is similar. In
this proof, we use rule (βlet ) and rule (βλ ) of Def. 1.6.

Lemma 1.30.
+
T −1 .
(1) We have (λk. T k)−1 −→
11

+
W −1 .
(2) We have (λx. W x)−1 −→
−1 +
(3) We have (λx. Kx) −→ K −1 .

Proof. (1) is an immediate consequence of rule (ηµ ) in Def. 1.6, and (2) of rule (ηλ ). We show (3). We
split cases by the shape of K. The case of K = k is easy. If K = λy. Q, the left side equals Q−1 ↾y :=x↾x:=,
which contracts to Q−1 ↾ y := , i.e., (λy. Q)−1 . In both cases, we use rule (ηlet ) of Def. 1.6. We note that
the equality rules of Def. 1.3 are implicitly used in the proof of (3). However, the interchange law of µ and
let is not used. See 1.35.

+

P
Proposition 1.31. We have P −1 −→
Q−1 in the CCV λµ-calculus, whenever P → Q holds with respect to
βη-reduction in the target calculus. Here P and Q represent lambda terms of all sorts in the target calculus,
P+
and −→
denotes one or more practical reductions.

Proof. It is a consequence of Lem. 1.28, 1.29, and 1.30. No administrative reductions are used, as pointed
out in the proofs of the lemmata.

Similar results are proved by Sabry and Felleisen [58, Thm. 13, p. 312][57, Thm. 3.11, p. 45] and by Fujita
[21, Prop. 27, p. 203][22, Lem. 18, p. 330] for different systems with no control operators.
Corollary 1.32. If [[M1 ]] = [[M2 ]] holds up to βη-equality in the target calculus, then M1 =ccv M2 holds.
Proof. Applying Prop. 1.31 to a zigzag of βη-reductions, we have [[M1 ]]−1 =ccv [[M2 ]]−1 . We have also
Mi =ccv [[Mi ]]−1 by Cor. 1.26.

Corollary 1.32 refers only to equality. We show sharpened completeness with regard to reductions in
Thm. 1.34.
Definition 1.33. We let M ↓ denote the normal form with respect to vertical reductions for each term M
of the CCV λµ-calculus. Existence of the normal form comes from Lem. 1.21.
Before stating the theorem, we recall ambiguity in definition of the CPS translation [[M ]] discussed in
Rem. 1.16, (i). If we choose different bracketing between µ and let, we obtain different [[M ]].
∗
Theorem 1.34. Let M be a term of the CCV λµ-calculus. If [[M ]] →
N with respect to βη-reduction in the
∗
−1 ↓
target calculus, M → (N ) holds in the CCV λµ-calculus. Here we understand [[M ]] to mean arbitrarily
chosen one among those obtained by bracketing between µ and let.

Proof. By Prop. 1.31 and 1.23, we have M ′ satisfying
P∗

V∗

✻

✻
P∗

✻

M†

N −1

✻

[[M ]]−1

V∗

M′

where M † is introduced in Prop. 1.25 that is valid irrelevant of the choice of bracketing. We can replace M ′
∗
∗
with (N −1 )↓ , performing further vertical reductions if needed. Thence we have M −→
M † −→
(N −1 )↓ . 
Similar results are verified by Sabry and Wadler for Moggi’s λc -calculus [59, Thm 8.2, p. 130], and by Fujita
for the second-order call-by-name λµ-calculus [22, Thm. 1, p. 330].
12

Remark 1.35. The equality axioms in Def. 1.3 are the key for Thm. 1.34. So let us analyze where the
axioms are used throughout the proof. They are used in Prop. 1.25 (through Lem. 1.24), Lem. 1.28 (through
Rem. 1.7, (3)), and Lem. 1.30. As commented in these parts, only the first and the third axioms are used
among three axioms of 1.3. The second axiom interchanging µ and let is never used.
This is not strange, since the second axiom is derivable from others if the equality is our concern, the
orientation of the reduction being ignored. Let us assume that the interchange axiom between jumper
and let is valid. Then we derive the second axiom as µk. (J ↾ z := M ) = µk (([k](µk. J)) ↾ z := M ) =
µk. ([k]((µk. J) ↾ z := M )) = (µk. J) ↾ z := M where three equalities are the reverse of βjmp , the interchange
law of jumper and let, and ηµ , respectively.
As an alternative choice, therefore, we may take the reduction rule
(µk. J) ↾ x := M

→

µk. (J ↾ x := M )

in place of the equality axiom. Here we assume that k is not free in M . We do α-renaming otherwise.

2. Proof by Parasitism
The rest of the paper is mostly devoted to the applications of the sharpened completeness theorem 1.34.
It succeeds in dealing with reduction, not only with equality.
The target calculus of the CPS translation is just the ordinary lambda calculus except that it is equipped
with sorts. We have a stock of the results on the lambda calculus through a long history of research. By
the sharpened completeness, we can reflect the properties of the lambda calculus to the CCV λµ-calculus.
We coin the term “proof by parasitism” to describe the technique to obtain syntactic properties through
completeness. A parasite (the source calculus) infests a host (the target calculus) to suck the nurture from
the latter. The nurture in this case is a desired syntactic property. Through completeness the source calculus
can take over the target calclus and make it work hard to provide for him. Fruits are collected by the host
and the free-loader robs them at the lowest cost.
In this section, we demonstrate several samples of the results that uses the proof by parasitism. We do
not claim that this type of argument is original at all. For instance, de Groote [11, Prop. 3.2,Lem. 4.2],
Sabry and Wadler [59, Prop. 7.1.2, p. 126] Crolard [8, Thm. 3.5.1], and Fujita [21, Cor. 34,35][22, Cor. 19]
use the same approaches to prove some of their results. Here we deploy the outfit systematically.
2.1. Proof by parasitism, I: Church-Rosser property
We start with the Church-Rosser property. Its proof is a typical example of an advantage of the technique.
Theorem 2.1. The CCV λµ-calculus enjoys the Church-Rosser property.
Proof. Suppose M1 =ccv M2 . By soundness 1.15 concerning equality, we have [[M1 ]] = [[M2 ]] up to βηequality. Since the lambda calculus fulfills Church-Rosser with respect to βη-reduction (thus the target
∗
∗
calculus does) [4, Thm. 3.3.9], there is a term N such that [[M1 ]] −→
N ←−
[[M2 ]] in the target calculus.
∗
−1 ↓ ∗

Now Thm. 1.34 yields M1 −→ (N ) ←− M2 .
Remark 2.2. The fragment of our system with no µ-operators is essentially the same as Moggi’s λc -calculus
[43]. If we identify M ↾ x := N with let x = N in M , the reduction rules are quite similar, except that the
λc -calculus has the let-flat rule for associativity of the let-construct, while our calculus has it as one of the
equality rules 1.3. This type of relation of the complete call-by-value calculus to the λc -calculus is first
pointed out in [57][58].
With respect to equational theories, the CCV λµ-calculus is a conservative extension of the λc -calculus,
up to the identification of the let-constructs. It is a consequence of the Church-Rosser property 2.1. Although
the λc -calculus is defined as a typed system, let us ignore the typing here. Let =λc denote the equational
theory generated from the reduction rules in Def. 6.2 of [43]. We show that L =λc M is equivalent to
13

L =ccv M . By the Church-Rosser, L =ccv M is derivable only by reduction from L and M . Since L and M
are supposed to have no µ or jumpers, the reduction paths use the rules for λ, applications, and let only.
Therefore L =λc M holds. The converse is trivial.
2.2. Proof by parasitism, II: Weak normalization
In this subsection, we verify that M is normalizable iff [[M ]] is normalizable. First we give a partial
characterization of the normal forms in the CCV λµ-calculus. It is said to be partial, since it does not
exclude the redices of the η-type in Def. 1.6, that is, λx. V x, x ↾ x := M , or µk. [k]M .
Definition 2.3. A term or a jump in the CCV λµ-calculus is quasi-normal if it contains none of the first
six redices in Def. 1.6 (viz., only η-type redices are allowed). If a term or a jump contracts to a quasi-normal
form with no use of the η-type rules, we say that it is quasi-normalizable.
A quasi-normal form may contain a redex λx. V x of rule ηλ . However, if the value V is a lambda abstraction
λy. L, the subterm V x = (λy. L)x is a forbidden β-type redex. Hence only the form λx. yx is allowed.
Definition 2.4. We define four classes M, B, N, and V of CCV λµ-terms, and a class H of jumps by the
following syntax:
M
H
B
N
V

::=
::=
::=
::=
::=

B | µk. H
[k]B
V | N | B ↾ x := N
xV
x | λx. M

where x ranges over ordinary variables and k continuation variables. Here we assume the bracketing convention in Rem. 1.4.
Remark 2.5.
(1) It is easy to see that the terms and jumps defined by the syntax of 2.4 are quasi-normal.
(2) Conversely, quasi-normal terms are correctly characterized by Def. 2.4. To this end, we adopt the
canonical bracketing rules in Rem. 1.4. Between jumper and let, we suppose that [k](L ↾ x := M ) is
canonical.
If a quasi-normal term has the form of application M1 M2 , both Mi must be values so that it does not
form a redex of the administrative rules. Moreover, value M1 must be a variable for otherwise it is a
lambda-abstraction, forming a βλ -redex (λx. M )V . Hence the term must be of the form N = xV where
V is a quasi-normal value. If a quasi-normal term is L ↾ x := M , then M is neither a value nor a µ-term.
Hence M must be an application N. There is no restriction to the form of L. However, by canonical
bracketing rules, we can assume that L is not a µ-term. Hence the term must be of the form B ↾ x := N.
For a quasi-normal jump [k]M , the term M does not start with µ. Hence it is of the form [k]B. The
other cases are similar.
Lemma 2.6. A term or a jump of the CCV λµ-calculus is normalizable if it is quasi-normalizable.
Proof. It suffices to show that quasi-normal terms reduce to quasi-normal forms. Proof is strightforward.


Definition 2.7. The β-normal forms in the target calculus are characterized by the following:
TNF

::= λk. QNF | xWNF
14

QNF ::= xWNF KNF | kWNF
WNF ::= x | λx. TNF
KNF ::= k | λx. QNF .
We remark that β-normalizability in the lambda calculus (thus in the target calculus) is equivalent to
βη-normalizability [4, Cor. 15.1.5].
Now we verify that M is normalizable iff [[M ]] is normalizable. First we prove the if-part, and then the
only-if part. Verification is done by simple comparison of quasi-normal forms and β-normal forms.
Lemma 2.8. If N is a β-normal term in the target calculus, N −1 is quasi-normal.
−1
−1
−1
Proof. We make rough use of equality. We verify that TNF
= M, Q−1
NF = H, WNF = V, and KNF [N] =
H by induction on the construction of the grammar in Def. 2.7. For example, if TNF = xWNF , then
−1
(xWNF )−1 = xWNF
= xV by induction hypothesis. Thence (xWNF )−1 = xV = N = B = M.


Proposition 2.9. Let M be a term of the CCV λµ-calculus. If [[M ]] is normalizable, M is normalizable.
∗
N where N is β-normal in the target calculus. TheoProof. Let us take a reduction sequence [[M ]] →
∗
−1 ↓
rem 1.34 implies M → (N ) in the source calculus. By Lem. 2.8, N −1 is quasi-normal. Thus, by Lem. 2.6,
(N −1 )↓ is normal.


Proposition 2.10. If M is a normalizable CCV λµ-term, [[M ]] is normalizable
Proof. If M1 =ccv M2 then [[M1 ]] = [[M2 ]] by the equational soundness 1.15. Since the lambda calculus
satisfies the Church-Rosser property, normalizability of [[Mi ]] implies that of the other. Hence, from the
beginning, we may assume that M is normal. We show that λk. (|M |)[k] is normalizable in case M = M.
To this end, we verify (|M|)[k], (|H|), (|B|)[k], and (|N|)[KNF ] contract to QNF by β-reductions. Moreover, we
show V∗ contracts to WNF . The proof is by simultaneous induction on construction of Def. 2.4 (up to the
renaming of continuation variables). If M = µl. H, then (|µl.H|)[k] = (λl. (|H|))k → (|H{k/l}|) by β-reduction.
This is the only part we need β-reduction essentially. The rest are easy. We take the case of B. If B = V,
then (|V|)[k] = kV∗ = kWNF = QNF . If B = (B ↾ x := N), we have (|B ↾ x := N|)[k] = (|N|)[λx. (|B|)[k]] =
(|N|)[λx. QNF ] = (|N|)[KNF ] that contracts to QNF by induction hypothesis.

Theorem 2.11. Let M be a term of the CCV λµ-calculus. Then M is normalizable if and only if [[M ]] is
normalizable.
Proof. By Prop. 2.9 and 2.10.



Remark 2.12. The converse of Lem. 2.6 is true, but it is not trivial, contrary to the appearance. In the
ordinary lambda calculus, βη-normalizability implies β-normalizability (it is not trivial) [4, Cor. 15.1.5][62,
§3]. We use this fact.
Remark 2.13. Conceptually, Thm. 2.11 has an idea common to the reduction-free normalization by Berger
and Schwichtenberg [6]. Both methods extract a normal form by the inverse of the interpretation. They use
a full model on lambda terms while we use the CPS semantics. The reduction-free normalization interweaves
the process to find a normal form in the construction of reification-reflection pairs defined by induction on
types. In our case, we consign the task to the target calculus. If a normal form of [[M ]] is found by chance,
a normal form of M is obtained from its inverse translation. If we combine the inverse translation with the
method by Berger and Schwichtenberg, we can give a reduction-free normalization for the CCV λµ-calculus.
This idea will be pursued in a forthcoming paper.
15

2.3. Proof by parasitism, III: Termination of the call-by-value evaluation
In this subsection, we give the operational semantics using evaluation contexts for the CCV λµ-calculus.
We prove that the call-by-value evaluation of M terminates iff [[M ]] is solvable.
The operational semantics using evaluation contexts are introduced by Plotkin [54] for the lambda
calculus on the relation to the execution by an abstract machine. Thereafter the evaluation contexts are
used as a standard technique to give handy operational semantics of calculi. For example, Felleisen et al. [15]
gives the operational semantics of the calculus with control operators C and A. Here we apply the technique
to the CCV λµ-calculus.
The operational semantics gives a canonical order of evaluation. The evaluation context is used to point
which is the next redex to be contracted. We should be sensitive to the scope of each subterm. Hence,
when we speak of the operational semantics, we stop the ellipses of brackets in 1.4 and follow the rule in
Rem. 2.14.
This switch of convention reflects differences of focused targets. The calculus in this paper is designed so
as to be usable for humans. The ellipses of brackets is introduced because tracking them is a cumbersome
task to us. If we talk about implementation, however, we have to fix the order of computation in any case.
The revival of brackets is aimed at doing this. We stress that, though the operational semantics distinguishes
the terms that are different in the positions of brackets, the underlying theory to discuss its properties is
still based on the original system. See Rem. 2.34.
Remark 2.14. Restricted to the case we speak of the operational semantics, we take the following convention. We distinguish (µk. J) ↾ x := M from µk. (J ↾ x := M ), as well as (L ↾ x := M ) ↾ y := N from
L↾x:=(M ↾y :=N ). For jumper and let, we keep on omitting brackets. However, we understand [k]M ↾x:=N
to mean [k](M ↾ x := N ).
Definition 2.15. The evaluation contexts E in the CCV λµ-calculus are defined by the following syntax:
E ::= 

| E[V ] | E[M ] | E[M ↾ x := ]

where, for example, E[V ] is understood to fill a unique hole  in E by V .
Remark 2.16.
(1) We may define the evaluation contexts as E ::=  | V E | EM | M ↾ x := E. This style is more usual.
Since the evaluation contexts are compositional, either definition works. Indeed, we may define even
E ::= 

| E[V E] | E[M E] | E[M ↾ x := E]

combining both styles. We use this remark in Lem. 2.28.
(2) Each term is decomposed into the form of either E[V ] or E[µk. J]. Indeed, if a subterm is neither a
value nor µ-abstraction, we can dismantle it further by a clause of Def. 2.15.
We define the call-by-value evaluation semantics as rewriting rules. It is called E-rewriting. Beforehand
we introduce the E0 -rewriting rules. This relation rewrites terms of the form either E[V ] or E[µk. J] with
non-void evaluation context E.
E0
is defined by the following five rules:
Definition 2.17. The rewriting relation −→

E[(µk. J)M ]
E[V (µk. J)]
E[(λx. M )V ]
E[M ↾ x := V ]
E[M ↾ x := µk. J]

E0
−→
E0
−→
E0
−→
E0
−→
E0
−→

E[zM ↾ z := µk. J]
E[V z ↾ z := µk. J]
E[M ↾ x := V ]
E[M {V /x}]
E[µk. J{[k] 7→ [k]M ↾ x := }]

In the first two rules, z is a fresh variable. The first two rules are called administrative.
16

Remark 2.18.
(1) Each term is decomposed into a unique one of the left hand sides of Def. 2.17 if any. Hence the
computation path by the E0 -rewriting is uniquely determined.
(2) A term E[xV ] has the shape of E ′ [V ] with non-void evaluation context E ′ = E[x]. However, there
is no rewriting from E[xV ]. In this case the computation stalls. It is the only situation where the
evaluation procedure deadlocks.
(3) A value V does not have a shape of E[V ] or E[µk. J] with non-void E. So the E0 -computation terminates
if a value is encountered. Contrary to the case above, we regard this as successful termination. Likewise
the E0 -computation terminates if µk. J is reached. However, the latter may be computed more by the
E-rewriting introduced below. See (1) of Rem. 2.20.
(4) No terms of the left hand sides of Def. 2.17 start with µ. However, for example, (µk. J) ↾ x := V may
occur. Recall that we are sensitive to bracketing in speaking of the operational sematnics.
E
Definition 2.19. The rewriting relation −→
is defined by the following three derivation rules:

E
µk.[l]µm. J −→
µk. J{l/m}

E0
M
L −→
E
L −→ M

E0
M
L −→
E
µk. [l]L −→ µk. [l]M

We comment that it is uniquely determined which rule is applicable, if any, by (4) of Rem. 2.18.
Remark 2.20.
(1) If a term starts with µk1 . [l1 ]µk2 . [l2 ] · · · µkn . [ln ], the E-computation first collapses the pairs of a jump
and a µ-binder, until we reach µk. [l]M where M does not start with µ. Then E0 -rewriting is applied
to M . Afterwards, if the resulting term starts again with a sequence of the two or more pairs of µki
and [li ], we collapse them. Therefore the computation path by the E-rewriting is unique, by (1) of
Rem. 2.18.
(2) We see that the E-computation is classified into three cases, viewing (2) and (3) of Rem. 2.18. First it
normally terminates returning either a value V or µk. [l]V . Second the computation stalls with E[xV ]
or µk. [l]E[xV ] where x is free. Third it may never terminate.
(3) If a term M is closed, the E-computation from M either normally terminates or runs for good. It never
stalls. If the system contains constants c, deadlock E[cV ] may happen.
Definition 2.21.
(1) An E-normal form is a term admitting no E-rewriting. By remark (2) of 2.20, an E-normal form is one
of V , µk. [l]V , E[xV ], and µk. [l]E[xV ]. We note that the definition does not exclude the stalling cases.
E∗
(2) The call-by-value evaluation from M terminates if there is an E-rewriting sequence M −→
N such that
N is E-normal.
Example 2.22.
(1) Let us recall definition of the fixed-point combinator Y in 1.11. For variables f and z, it is easy to see
E∗
Y f z −→
f (λv. Df Df v)z, which is an E-normal form. The call-by-value evaluation from Y f z terminates.
(2) In contrast, if we set Df = λx. f (xx) in definition of Y = λf z. Df Df z, we have an infinite rewriting
E∗
E∗
E∗
sequence Y f z −→
f (Df Df )z −→
f (f (Df Df ))z −→
· · ·.
First we relate (1) of Def. 2.21 to its CPS semantics. It is an easy task. The characterization of (2) is given
later.

17

Definition 2.23. The head normal form in the target calculus is defined by the following syntax:
THN ::= λk. QHN | xW
QHN ::= kW | xW K
where K and W are as in Def. 1.17.
Lemma 2.24. If N is in the head normal form in the target calculus, N −1 is E-normal.
−1
Proof. Let us see Q−1
= [l]W −1 . On the other hand, (xW K)−1 is equal to [l]xW −1 or
HN . We have (lW )
−1
Q−1 ↾y :=xW −1 according to K’s shape, l or λy. Q. Therefore THN
is one of xW −1 , µk. [l]W −1 , µk. [l]xW −1 ,
and µk. Q−1 ↾ y := xW −1 . Since W −1 is a value, these are all E-normal by (2) of Rem. 2.20. The last case
−1
may need more comments. For example, if Q = (λm. Q0 )l, it is equal to µk. ([l](µm. Q−1
).
0 ) ↾ y := xW
The E-computation does not collapse [l]µm, contrary to the appearance. By the convention in Rem. 2.14,
the term should read µk. [l]((µm. Q0−1 ) ↾ y := xW −1 ). Hence [l] and µm do not face each other.


Lemma 2.25. If a term M is E-normal in the CCV λµ-calculus, [[M ]] is solvable.
Proof. [[M ]] is almost in head normal form. We need a single step of head reduction in certain cases.
First we claim that, if N is a non-value, (|E[N ]|)[K] = (|N |)[KE ] holds for suitably defined continuation
KE . It is defined by induction on construction of E in Def. 2.15. (i) K = K. (ii) KE[V ] = λy. V ∗ yKE . (iii)
KE[M] equals λx. xV ∗ KE if M is a value V . If M is a non-value, KE[M] equals λx. (|M |)[λy. xyKE ]. (iv)
KE[M↾x:=] = λx. (|M |)[KE ]. Proof of the claim is immediate from definition of the colon translation 1.13.
Since KE depends on given continuation K, we write KE,K below.
We prove that [[M ]] = λk. (|M |)[k] belongs to THN in Def. 2.23 up to head reduction. We split cases by
the shape of E-normal M . If M equals E[xV ], the claim above yields (|M |)[k] = (|xV |)[KE,k ] = xV ∗ KE,k =
QHN . If M equals µk. [l]E[xV ], then we have (λk. (|E[xV ]|)[l])k, that is, (λk. xV ∗ KE,l )k. This contracts to
xV ∗ KE,l = QHN by one-step head reduction. In either case, [[M ]] =β λk. QHN = THN . If M = V , then
[[V ]] = λk. kV ∗ = THN . If M = µk. [l]V , one-step head-reduction yields λk. lV ∗ = THN .

From Lem. 2.25 and soundness 1.15, it is immediate to see that if the call-by-value evaluation of M terminates
then [[M ]] is solvable. The converse is true as is verified below.
E
Lemma 2.26. If T0 → T1 is a head reduction of sort T terms in the target calculus, T0−1 −→
T1−1 holds
∗
where E denotes a finite sequence of E-rewriting with no use of the administrative rules in Def. 2.17
∗

Proof. We return to Prop. 1.31. As remarked in Rem. 1.19, the administrative rules are never applicable
to the term obtained by the inverse translation. There are only four patterns for the head redices of
sort T terms: (λx. T )W , λk. (λx. Q)W , λk. (λm. Q)K, and λk. (λx. T )W K. We verify the lemma for the
third pattern. If K = l, the inverse is µk. [l]µm. Q−1, which is by 2.19 rewritten to µk. Q−1 {l/m}, viz.,
(λk. Q{l/m})−1. If K = λy. Q0 , the inverse is µk. (Q0−1 ↾ y := µm. Q−1 ). Since Q−1
0 has the form of [l]M0 , we
have µk. [l](M0 ↾ y := µm. Q−1 ). (We need re-bracketing as commented in the proof of Lem. 2.24.) By the Erewriting it is rewritten to µk. [l]µm.Q−1 {[m] 7→ [m]M0 ↾ y := }, then to µk. Q−1 {[m] 7→ [l]M0 ↾ y := }.
The last equals to the inverse of λk. Q{m 7→ λy.Q0 }. The remaining patterns are similar.

∗

E
Corollary 2.27. There is a rewriting sequence [[M ]]−1 −→
N to some E-normal N , whenever [[M ]] is
solvable. Here E ∗ denotes a finite number of E-rewriting with no use of the administrative rules in Def. 2.17.
∗
Proof. By solvability, there is a head reduction sequence [[M ]] →
T where T is in head normal form.
Apply Lem. 2.26 and 2.24.


18

Hence we know that the call-by-value evaluation of [[M ]]−1 terminates if [[M ]] is solvable. We want to transfer
A∗
V∗
the evaluation of [[M ]]−1 to the evaluation of M . To this end, we recall that we have M −→
M † ←−
[[M ]]−1
∗
by Prop. 1.25. Let us analyze the interaction of E-rewriting with administrative reductions A and vertical
reductions V ∗ .
In Prop. 1.25 the arrow labeled with V ∗ is in actuality a mixture of true vertical reductions and applications of equality axioms save the second axiom (see Lem. 1.24). As the E-rewriting is sensitive to bracketing,
V∗
we must take care of this fact. In the following lemmata, we should understand −→
to mean such a mixture.
Lemma 2.28. In the following, V ∗ and A∗ denote finite sequences of vertical reduction and administrative
reduction respectively.
∗

V
(1) If N −→
N ′ and N is E-normal, then N ′ is E-normal.
A∗
(2) Suppose N −→
N ′ . Then N is E-normal if N ′ is E-normal.

Proof. (1) Vertical reduction µk. [k]M → M preserves the property of being a value or E[xV ]. Moreover,
the first and the third equality axioms of Def. 1.3 respect E-normal forms. (2) It suffices to manipulate
A
one-step administrative reduction. We consider ad 1 -reduction C[N M ] −→
C[zM ↾ z := N ]. The case of
ad 2 -reduction is similar. We suppose that C[zM ↾ z :=N ] is E-normal. Recall (2) of Rem. 2.20 for the shapes
of E-normal forms. Interested cases are E[xV ] and µk. [l]E[xV ]. We consider the former. The essential case
is E = E ′ [zM ↾ z := E ′′ ] so that C[zM ↾ z := N ] is equal to E ′ [zM ↾ z := E ′′ [xV ]]. Then C[N M ] is equal to
E ′ [E ′′ [xV ]M ] that is E-normal.

We first show that the E-rewriting commutes with vertical reductions. Second we verify that administrative
reductions can be postponed.
∗

∗

V
E
M −→
N holds (pay attention to the directions of arrows) and N is E-normal,
Lemma 2.29. If M ′ ←−
′
there is an E-normal term N such that
E∗

V∗

✻

✻

✻

M′

N

✻

M

E∗

V∗

N′

where E ∗ a finite sequence of E-rewriting with no use of administrative rules in Def. 2.17. For V ∗ , see the
comment immediately before Lem. 2.28.
∗

V
Proof. N ′ is E-normal by Lem. 2.28, (1). Although −→
is a mixture, we can shuffle the order so that
first true vertical reductions are applied, then equality axioms. So we first prove the lemma for pure vertical
reductions. It is easy. (However we comment that the lemma fails if administrative E-rewriting is included,
since vertical reduction creates a value in case µk. [k]V → V .) Second we prove that if M1 = M2 save the
E∗
E∗
N2 with N1 = N2 . A crucial case is
N1 to an E-normal form N1 , then M2 −→
second axiom and if M1 −→
E[(L ↾ x := M ) ↾ y := µk. J] = E[L ↾ x := (M ↾ y := µk. J)]. The one-step E-rewriting from the former splits
into two steps from the latter.


∗

∗

E
A
N1 holds, (compare the directions of arrows with those in 2.29), then
Lemma 2.30. If M −→
M1 −→
A∗

E∗

✻

✻

✻

N

M1

✻

M

A∗

E∗

N1
19

for some N . Here A∗ denotes a finite sequence of administrative reduction of Def. 1.6, and E ∗ a finite
sequence of E-rewriting. We stress that administrative rules of Def. 2.17 are allowed in E ∗ here.
A
Proof. We follow the standard parallel reduction argument. We define parallel reduction =⇒
allowing
A
E∗
simultaneous administrative reduction. We verify the following: ∗if M =⇒ M1 −→ N1 holds, there is a term
A
A
E∗
A∗
N such that M −→
N =⇒
N1 . Then we use equivalence of L =⇒
L1 and L −→
L1


Theorem 2.31. Let M be a term of the CCV λµ-calculus. The call-by-value evaluation of M terminates
if and only if [[M ]] is solvable.
∗

E
Proof. We verify the if-part. By Cor. 2.27, we have [[M ]]−1 −→
N for E-normal N where E ∗ does not
A∗
† V∗
use the administrative rules. By Prop. 1.25, we have M −→ M ←− [[M ]]−1 . Hence Lem. 2.29, (1), gives
E-normal N ′ satisfying
E∗

✻

[[M ]]−1
V∗

✻
M†

✻

A∗

✻

✻

M

N

E∗

V∗

N′ .
∗

∗

∗

A
E
A
Deferring the administrative reductions M −→
M † by Cor. 2.30, we finally obtain M −→
N ′′ −→
N ′ . By
′′
(2) of Lem. 2.28, N is E-normal.


Corollary 2.32. If the call-by-value evaluation of M terminates returning N , and if M =ccv M ′ , the callby-value evaluation of M ′ terminates returning some N ′ . Moreover the E-normal forms satisfy N =ccv N ′ .
Proof. By soundness 1.15, [[M ]] = [[M ′ ]] holds. If the evaluation of M terminates, [[M ]] is solvable by
Thm. 2.31. Since solvability is closed under βη-equality [4, Thm. 15.1.7], [[M ′ ]] is solvable. Hence the
evaluation of M ′ terminates by the theorem. The last part of the corollary is immediate since M =ccv N
and M ′ =ccv N ′ .

From Cor. 2.32, we know that the operational meaning of a term does not change if we transfer it to another
term by CCV-equality.
Example 2.33. We return to the implementation of the cooperative multitasking in 1.12. The call-byvalue evaluation of [τ̂ ](M ↾ q := Cq) ⊲qr N proceeds to [τ̂ ](µδ. [τ̂ ]N ) ↾ r := λq. (µδ. [τ̂ ](M ↾ q := q)), which
is not accurately equal [τ̂ ]N ⊲rq M . However, Cor. 2.32 ensures that, if the call-by-value evaluation of
either halts, the other halts, and they yield the E-normal forms equal up to =ccv . So it is safe to regard
[τ̂ ](M ↾ q := Cq) ⊲qr N to have the effect of switching a live process by invoking [τ̂ ]N ⊲rq M .
Remark 2.34. We can dynamically change the scopes of let and mu bindings during execution. Suppose
E∗
L −→
M and M = M ′ where the latter is by re-bracketing following the rules in Def. 1.3. By Cor. 2.32,
then, L terminates iff M ′ terminates, and they return equal results. Repeatedly doing so does not damage
the terminating situation (by König’s lemma). This ensures the safety of optimization by changing scopes,
such as let-flattening [52]. We note that our equality enables optimization by oppositely narrowing the scope
of let-bindings.
Remark 2.35. Theorem 2.31 is an extension of [54, p. 148, Thm. 2]. Results closely related to Cor. 2.32 are
proved in [54, p. 142, Cor. 1] for the call-by-value lambda calculus and in [15, p. 231, Cor. 4.9] for the calculus
with control operators C and A. Since completeness fails in these calculi, the proof strategy is different.
They appeal to the standardization theorem to shuffle the order of computation. We use completeness. We
need only the restricted shuffle patterns in Lem. 2.30.
20

3. Type-Theoretic Characterization
In the theory of the ordinary lambda calculus, various computational properties are characterized by
the intersection type discipline. A well-known theorem by Barendregt, Coppo, and Dezani-Ciancaglini
exhibits that weak normalizability and solvability are reduced to certain typeability problems [5]. In the
previous section, we have verified (Thm. 2.11, 2.31) that these two properties exactly correspond to weak
normalizability and the termination of call-by-value evaluation in the CCV λµ-calculus. It is, therefore,
natural to think of extending the type-theoretic characterization to the CCV λµ-calculus.
In this section, we develop the union-intersection type discipline for the CCV λµ-calculus. We verify
the following two theorems in 3.34: (i) the call-by-value evaluation of a CCV λµ-term M terminates if and
only if M is typeable; (ii) M is normalizable if and only if M is typeable and the typing judgement of M
contains neither empty intersection nor empty union. The results are verified by reflecting the intersection
type discipline of the target calculus.
3.1. Union-intersection type discipline
We introduce the union-intersection type discipline for the CCV λµ-calculus. There are plenty of works
discussing type systems having both union and intersection, e.g., [28][53][3]. Later we give comparison with
some of type systems, limited to call-by-value calculi, in §3.5. For call-by-name λµ-calculus, van Bakel gives
a type system equipped with union and intersection, verifying subject reduction/expansion [64]. Indeed, our
type system is inspired by this.
Definition 3.1. We define raw types R, subsidiary types S, and types T by the following syntax:
R ::= T
α | S→T
S ::= S R
T ::=
S
T
where α ranges over atomic types.
R denotes a finite formal intersection of raw types, R1 ∩ R2 ∩ · · · ∩ Rn .
S
If n = 0, we write ω. Likewise S is a finite formal union S1 ∪ S2 ∪ · · · ∪ Sn . If n = 0, we write (agemo?).
We ignore differences by associativity and commutativity of ∩ and of ∪.
ω

Remark 3.2. In Def. 3.1, case n = 1 is allowed in S = R1 ∩ R2 ∩ · · · ∩ Rn . Hence each raw type is a
subsidiary type. Likewise each subsidiary type is a type.
Definition 3.3. The subtype relation ≤ is defined by the following derivation rules:
α≤α

S′ ≤ S
T ≤ T′
′
S → T ≤ S → T′

S ≤ S′
S ∩ S ′′ ≤ S ′

[ S ≤ Si ]i
T
S ≤ i Si

T ≤ T′
T ≤ T ′′ ∪ T ′

[ T ≤ T ]i
Si
i Ti ≤ T .

The notation [ S ≤ Si ]i should be understood to mean a sequence of derivations where i ranges over a finite
index set. [ Ti ≤ T ]i is similar. Taking an empty index set, we have ≤ T and S ≤ ω. From the latter, we
further obtain T ≤ ω by use of the last inference rule.
ω

The subtype relation is a quasi-order. For example T and T ∪ T are comparable to each other, but not
equal.
We deliberately omit the reflexivity law and the transitivity law:
21

T ≤T

T ≤ T′
T ≤ T ′′

T ′ ≤ T ′′

(both for types and subsidiary types) from the table in Def. 3.3. As is verified in Lem 3.4, these rules are
redundant. We can add them with no change of power. A similar result is asserted in Dunfield and Pfenning
[14, Lem. 1, §5] in a more general setting.
Lemma 3.4. If T ≤ T ′ is derived in the system having the inference rules for reflexivity and transitivity in
addition to those of Def. 3.3, then T ≤ T ′ is derived in the pure system of Def. 3.3.
′
Proof. For distinction, let us write
and transitivity. We
S T ≤1 T ifSwe use′ the system including reflexivity
f
define the third relation ≤2 . First i∈I Si ≤2 j∈J Sj if there is a mapping I −→ J such that Si ≤2 Sf′ (i)
T
T
f
for every i. Second i∈I Ri ≤2 j∈J Rj′ if there is a mapping J −→ I such that Rf (j) ≤2 Rj′ for every j.
′
′
Finally R ≤2 R if both R and R are the same atomic type or R = S → T and R′ = S ′ → T ′ with S ′ ≤2 S
and T ≤2 T ′ . Now it is easy to verify that T ≤1 T ′ implies T ≤2 T ′ by induction on the construction of the
derivation trees. It is also easy to show that T ≤2 T ′ implies T ≤ T ′ . (As a consequence, all of ≤, ≤1 and
≤2 turn out to be the same.)


Definition 3.5. We give the inference rules of typing judgements. A typing judgement has the form Γ ⊢
M : T | ∆. Here the typing environment Γ is a finite sequence of xi : Si , and the typing environment ∆ is
a finite sequence of kj : Tj . As usual, we assume that all variables in the typing environments are distinct
from each other. We stress that only subsidiary types are assigned to ordinary variables while continuation
variables have no limitation. We assume a special type ⊥
⊥ for typing jumps. The following are inference
rules:
Γ, x : S ⊢ x : S | ∆
[ Γ, x : Si ⊢ M : Ti | ∆ ]i
T
Γ ⊢ λx. M : i (Si → Ti ) | ∆
S T
Γ ⊢ M : i j (Sij → T ) | ∆
Γ ⊢ MN : T | ∆
[ Γ, x : Si ⊢ M : T | ∆ ]i
Γ ⊢ M ↾ x := N : T | ∆

[Γ ⊢ N:

Γ ⊢ N:

S

Γ ⊢ N:

S

i

S

j

Sij | ∆ ]i

Si | ∆

Γ ⊢ J :⊥
⊥ | ∆, k : T
Γ ⊢ µk. J : T | ∆
Γ ⊢ M : T | ∆, k : T
Γ ⊢ [k]M : ⊥
⊥ | ∆, k : T
[ Γ, x : Si ⊢ J : ⊥
⊥ | ∆ ]i
Γ ⊢ J ↾ x := N : ⊥
⊥ | ∆
Γ ⊢ M :T | ∆
Γ ⊢ M : T′ | ∆

i

Si | ∆

T ≤ T′

The last inference
rule is called the inheritanceS
rule. TEach suffix (i or j) ranges over a finite set. For instance,
S T
the type i j (Sij → T ) is understood to be i∈I j∈J(i) (Sij → T ). where I and each J(i) are finite sets.
The notation [· · ·]i denotes a finite sequence of judgements. We understand that the parts without suffix i
are common to all the judgements therein. InSeach rule, the corresponding suffixes range over the same set.
For example, in the right premise [ Γ ⊢ N : j Sij | ∆ ]i of the S
third
T rule, the suffix i ranges over I and
the suffix j in the i-th judgement ranges over J(i) as they do so in i j (Sij → T ). Moreover, Γ, N , and ∆
are common to all judgements in the sequence.
22

The simply typed CCV λµ-calculus is defined by limiting all intersections and unions to range over singleton
sets.
Remark 3.6.
(1) Note that the valuesSare typed by subsidiary types in the first two inference rules of Def. 3.5. Hence, if
a value V has type Si , it must be obtained by an application of the inheritance rule. So V has type
Si for some i, viewing the characterization of the subtype relation by ≤2 in the proof of 3.4.
(2) Not all terms have type ω. However, every value can have type ω. For variable x, we use the inheritance
rule since S ≤ ω. For lambda abstraction λx. M , let i range over an empty set. In general, a term can
have type ω if and only if it is typeable.
(3) Since indices may range over an empty set, the sequences [· · ·]i are able to be void. Hence a term may
be typed even if not all of free variables occur in the typing environments. In such a case, we may
implicitly regard x : ω and k : .
ω

Example 3.7. The typing of the call/cc operatorT is suggestive. The operator is encoded as call/cc M =
µk. [k]M (λxµδ. [k]x). Provided that M has type ( j (Sj → )) → T , we have
S
call/cc M : T ∪ j Sj .
ω

Here can be replaced with any other type. TheStype of call/cc M is naturally understood in the aspect
of side-effects: T is the type of a normal exit and Si of non-local exits. The union over i corresponds
to
S T
possible multiple locations where
non-local
exits
are
raised.
We
can
generalize
the
type
of
M
to
((
(S
→
ij
i
j
S
)) → T ) with call/cc M : T ∪ ij Sij , if it is meaningful.
ω

ω

Example 3.8. Let us recall definition of the call-by-value fixed-point combinator Y in Def.1.11. We show
that f : ω → , z : S ⊢ Y f z : T where S is an arbitrary subsidiary type and T is an arbitrary type. The
key is that Df = λxw. f (λv. xxv)w has type ω → S → T and type ω. The latter is obvious by Rem.3.6,
(2). For the former, λv. xxv has type ω by the same remark. Thus f (λv. xxv) has type . Since is an
empty union, f (λv. xxv)z can have arbitrary type T , irrelevant of the type of z, by letting i range over an
empty set in the inference rule for application of Def. 3.5. From the two types of Df , we have Df Df z : T .
Therefore Y f z : T .
In contrast, if we change Df to λx. f (xx), then Y f z is not typeable. It is a consequence of nontermination discussed in Example 2.22, (2), and the theorem verified later in 3.34, (1).
ω

ω

ω

Remark 3.9. The implementation of multitasking in 1.12 was done in the type-free calculus. We have
trouble if we want to provide types. Let us work in the simple types. Let α be the type of the topmost
continuation τ̂ . In M ↾ q ′ := Cq, if q ′ has type Q, then the type of q is (Q → α) → α. Moreover, in M ⊲qr N
(viz., M ↾q:=λrµδ. [τ̂ ]N ), the type of r is Q → α. To say simply, we need one nesting of (-) → α, proportional
to the number of message-passing through channels. For example, we cannot type wall in Example 1.12 even
if we have typed fixed-point combinator, since it allows an unbounded number of message passing.
An open question is whether this is an essential phenomenon. Possibly there is no well-typed implementation of multitasking that repeats stop-and-go in an unbounded number of times, unless mutable stores are
allowed. Incidentally, as far as the author knows, all implementation of multitasking and coroutine in the
literature uses mutable stores [29][1][13]1 .
Remark 3.10.
1 The implementation of iterators in [35] does not use mutable stores. However, two processes, an iterator and its caller, are
not symmetric.

23

(1) Nishizaki gives the translation of the call-by-value calculus with the call/cc operator into the linear logic
[47]. If we take correspondences between modalities and union-intersection by ! ! ∩ and ? ! ∪, his
′
translation
T
S Tis ′coincidental to ours. For instance, the implication type is translated to ! R ⊸ ? ! R and
R→
R , respectively. This is not surprising. The modalities in the linear logic are the reflection
of duplication or deletion of variables [23]. The union-intersection types are transplanted from the
intersection types of the lambda calculus, and the latter also reflects multiple occurrences of variables
[5][7].
(2) The λc -calculus by Moggi is designed so as to be sound and complete for the Kleisli category of strong
monads T [43]. The CPS semantics of the call-by-value lambda calculus is simply a special case where
T is a continuation monad ¬¬(-). As discussed in Rem. 2.2, the call-by-value lambda calculus has the
same equational theories as the λc -calculus. Hence the continuation monad has a special status among
strong monads. This single strong monad represents the calculus that works for all strong monads.
An analysis behind this phenomenon is given by Filinski [16]. In a nutshell, every monad embeds into a
codensity monad [42, Exer. 7.3], that is defined using right Kan extension. The codensity monads share
common structures with the continuation monad. In fact, if we assume the second-order lambda calculus
satisfying the parametricity condition, the codensity monad associated with T is written ∀α. (X →
T α) → T α (see [26] for the Kan extensions via parametricity), while the continuation monad is (X →
⊥
⊥) → ⊥
⊥. This type of fact is rediscovered in a different context [68]. See also [31].
We file an elementary property of the type system in Def. 3.5. We verify that the inheritance rule can be
limited to values.
Definition 3.11. We introduce Γ ⊢′ M : T | ∆. This judgement is defined as follows. We substitute all ⊢
in Def. 3.5 with ⊢′ . Moreover, we replace the inheritance rule by the following restricted one:
Γ ⊢′ V : S | ∆
Γ ⊢′ V : T | ∆

S≤T

where V is a value, S a subsidiary type and T a type.
Let us write Γ ≤ Γ′ if the typing environments Γ and Γ′ contains the same set of ordinary variables x and
if S ≤ S ′ holds for x : S and x : S ′ occurring in Γ and Γ′ . Likewise we define ∆ ≤ ∆′ .
Lemma 3.12. If Γ ⊢ M : T | ∆ holds, Γ− ⊢′ M : T + | ∆+ holds for any typing environments and types
satisfying Γ− ≤ Γ, ∆ ≤ ∆+ , and T ≤ T + . (The notation T + is irrelevant of that in Def. 3.21; here we use
it simply as a meta-symbol representing a type.)
Proof. Easy induction on the derivation of Γ ⊢ M : T | ∆. We need the transitivity of the subtype
relation. It is verified in Lem. 3.4.

Corollary 3.13. The following holds
Γ ⊢ M :T | ∆

⇐⇒

Γ ⊢′ M : T | ∆.



Remark 3.14. Typing respects equality. That is to say, if M = N holds with respect to the equality
axioms in Def. 1.3. and if Γ ⊢ M : T | ∆ holds, then we have Γ ⊢ N : T | ∆. This is easily seen if we use ⊢′ ,
viewing Cor. 3.13.
Lemma 3.15. Except for values, the inversion of inference rules holds. For instance, if Γ ⊢ M ↾x:=N
S :T |∆
holds, there is a finite set of subsidiary types Si such that Γ, x:Si ⊢ M :T |∆ for every i and Γ ⊢ N : i Si |∆.
Proof. Immediate from Cor. 3.13. This lemma is used later in Lem. 3.29.
24



3.2. Type system of the target calculus
The type system for the target calculus is the classic intersection type discipline. It is used to give the
type-theoretic characterization of syntactic properties of the lambda calculus [5][7]. The most significant
property of the discipline is the subject-expansion. Namely, if M → N by β-reduction and N has type τ ,
then M has type τ , too. Later van Bakel simplified the system introducing the strict type assignment [63].
It is, however, inconvenient to use the type systems in the literature as they actually are, by the following
two reasons. First the target calculus has η-reduction. The system by van Bakel is not sound with respect
to the η-reduction [63, p. 145]. Despite this, we want to take the benefit of the strict type assignment of
that system. So we revive the inheritance rule that has been eliminated in van Bakel’s. Second our target
calculus has sorts. In case we utilize the subject expansion, the induced typing must follow the constraints
imposed by the sorts. It is not immediate how to ensure it if we take results in the literature.
One of the simplest ways to clear the obstruction is to tailor a system from fabric, not by the adjustment
of ready-made results. We develop the intersection type system of the target calculus from scratch. We
follow the standard argument, but take care of sorts. A similar approach is taken by van Bakel et al. to
build a filter model for the call-by-name λµ-calculus [67] Verification of properties is sketched in Appendix
Appendix A.
Notation 3.16. As a special atomic type we prepare ⊥
⊥. We write ¬(-) in place of (-) → ⊥
⊥. To separate
strict types from types, we write underbars for types.
We define τ -types, κ-types, and σ-types corresponding to sort T , K, and W of the target calculus 1.17. The
atomic type ⊥
⊥ corresponds to sort Q.
Definition 3.17. We define strict types τ, κ, σ and types κ, σ by the following syntax:
T
σ ::= T σ
σ ::= α | σ → τ
κ ::= ¬σ
κ ::=
κ
τ ::= ¬κ
T
where α represents atomic types. The notation κ signifies finite formal intersection κ1 ∩ κ2 ∩ · · · ∩ κn
where case n = 0, 1 is included.
T We do not distinguish a strict type of class κ with a type of κ with n = 1.
Similar remarks applies to σ. We manipulate associativity and commutativity of intersection implicitly.
An empty intersection is written ω.
We note that the right side of the arrow type σ → τ is limited to a strict type τ . Moreover, in ¬σ = σ → ⊥
⊥,
type ⊥
⊥ is strict. Hence we follow the restriction of van Bakel [63].
Definition 3.18. We define the subtype relation ≤ for the target calculus. Each row of the following table
gives the definition of the relation between σ, κ, and τ , respectively.
α≤α

σ′ ≤ σ
τ ≤ τ′
′
σ → τ ≤ σ → τ′

σ ≤ σ′
σ ∩ σ′′ ≤ σ ′

[ σ ≤ σ i ]i
T
σ ≤ i σi

σ′ ≤ σ
¬σ ≤ ¬σ ′

κ ≤ κ′
κ ∩ κ′′ ≤ κ′

[ κ ≤ κi ]i
T
κ ≤ i κi

κ′ ≤ κ
¬κ ≤ ¬κ′

where the notation [· · ·]i denote a finite sequence of derivations (void sequences inclusive).
Remark 3.19.
to ≤2 in the proof of Lem. 3.4. For example, we define
T We′ have a characterization similar
T
f
κ
iff
there
is
a
mapping
J
−→
I
such
that κf (i) ≤2 κ′i for every i. In particular, we can
κ
≤
2
j∈J j
i∈I i
add reflexivity and transitivity to 3.18 with no change of power.
25

Definition 3.20. We give the inference rules of the typing judgements of the target calculus. A typing
judgement has two typing environments Π and Θ. The former is a finite sequence of x : σ and the latter of
k : κ. The variables occurring in the typing environments are distinct from each other. The following is the
table of the inference rules:
Π, Θ, k : κ ⊢s Q : ⊥
⊥
Π, Θ ⊢s λk. Q : ¬κ
Π, Θ ⊢s W1 : σ → τ
Π, Θ ⊢s W1 W2 : τ

[ Π, Θ ⊢s W2 : σi ]i

Π, Θ ⊢s K : ¬σ
Π, Θ ⊢s KW : ⊥
⊥

[ Π, Θ ⊢s W : σi ]i

Π, Θ ⊢s T : ¬κ
Π, Θ ⊢s T K : ⊥
⊥

[ Π, Θ ⊢s K : κi ]i

Π, x : σ ∩ σ ′ , Θ ⊢s x : σ

Π, x : σ, Θ ⊢s T : τ
Π, Θ ⊢s λx. T : σ → τ

Π, Θ, k : κ ∩ κ′ ⊢s k : κ

⊥
Π, x : σ, Θ ⊢s Q : ⊥
Π, Θ ⊢s λx. Q : ¬σ

T
T
where we assume σ = i σi and κ = i κi . The notation [· · ·]i represents a finite sequence of derivations.
Moreover we have the following three inheritance rules:
Π, Θ ⊢s T : τ
Π, Θ ⊢s T : τ ′
Π, Θ ⊢s W : σ
Π, Θ ⊢s W : σ ′

τ ≤ τ′

Π, Θ ⊢s K : κ
Π, Θ ⊢s K : κ′

κ ≤ κ′

σ ≤ σ′

Only strict types are given to terms in the typing judgements. The suffix of ⊢s signifies this. The inference
rules are standard. We emphasize, however, that the inheritance rules are included. This makes contrast to
the system by van Bakel [63]. The reason is that also η-reduction is our concern. Our type system goes in
between the system by Barendregt et al. [5] and the one by van Bakel.
3.3. Soundness and completeness of type systems
Definition 3.5 gives the union-intersection type system for the CCV λµ-calculus. Definition 3.20 gives
the intersection type system for the target calculus. In this subsection, we show that the former is sound
and complete with respect to the latter under the CPS translation.
We start with soundness. Toward this, we need to extend the CPS translation to types.
Definition 3.21. We define S ∗ , T + , and [[T ]] (referring to Def. 3.1). These three belong to categories σ, κ,
and τ of Def. 3.17, respectively. The definition is inductively given as follows:
T
T
∗
αS
= α, T (S → T )∗ = S ∗ → [[T ]],
( R)∗ = R∗
( S)+ = ¬S ∗
[[T ]] = ¬T + .
Lemma 3.22. If T0 ≤ T1 holds, [[T0 ]] ≤ [[T1 ]] holds. Here the first subtype relation is given in Def. 3.3, and
the second in Def. 3.18.
Proof. Simultaneously we verify that T0 ≤ T1 implies T1+ ≤ T0+ and that S0 ≤ S1 implies S0∗ ≤ S1∗ . Proof
is easy.

26

We associate typing environments Γ∗ and ∆+ to Γ and ∆. Definition is straightforward. To each x : S is
associated x : S ∗ , and to each k : T is associated k : T + . First we show soundness.
Proposition 3.23. The following holds:
Γ ⊢ M :T | ∆

=⇒

Γ∗ , ∆+ ⊢s [[M ]] : [[T ]].

S
Proof. We use the following fact repeatedly. Suppose that Γ∗ , ∆+ , k : ( Si )+ ⊢s (|M |)[k] : ⊥
⊥ holds.
Moreover, we suppose [ Γ∗ , ∆+ ⊢s K : ¬Si∗ ]i . Then Γ∗ , ∆+ ⊢s (|M |)[K] : ⊥
⊥ is derivable. To prove this
fact, we see Γ∗ , ∆+ ⊢s (λk. (|M |)[k])K : ⊥
⊥ is derivable, and use the subject reduction A.6 for β.
We simultaneously verify two assertions: (i) Γ∗ , ∆+ , k : T + ⊢s (|M |)[k] : ⊥
⊥ whenever Γ ⊢ M :
T | ∆; (ii) Γ∗ , ∆+ ⊢s (|J|) : ⊥
⊥ whenever Γ ⊢ J : ⊥
⊥ | ∆. From the first assertion, the proposition
follows immediately. Proof is by induction on the construction of derivation trees. We show the case
of application
N . Let us see the corresponding inference ruleTin Def. 3.5. By induction hypothesis,
T MT
∗
∗
⊢s (|N |)[k] : ⊥
⊥ for every i. We
→ [[T ]]) ⊢s (|M |)[k] : ⊥
⊥ and Γ∗ , ∆+ , k : j ¬Sij
Γ∗ , ∆+ , k : i ¬ j (Sij
T ∗
∗
, and k : T + , we can
recall (|M N |)[k] = (|M |)[λx. (|N |)[λy. xyk]]. From the typing x : j (Sij → [[T ]]), y : Sij
∗
derive xyk : ⊥
⊥. So λy. xyk : ¬Sij
for every j. T
Thus (|N |)[λy. xyk] : ⊥
⊥ by the fact mentioned in the preceding
∗
→ [[T ]]). This holds for every i. Therefore (|M N |)[k] : ⊥
⊥
paragraph. Consequently λx. (|N |)[λy. xyk] : ¬ j (Sij
using the fact again. If either M or N is a value, (|M N |)[k] is obtained by β-reduction of the non-value case.
The subject reduction A.6 is applied. For the inheritance rule, we use Lem. 3.22. Other cases are similar.

We turn to completeness. It is verified in Thm. 3.30. First we extend the inverse translation to types.
Definition 3.24. We define σ −1 , κ−1 , and τ −1 as well as σ −1 and κ−1 in the following way:
−1
αT
= T
α
(T σ)−1 = S σ −1
( κ)−1 =
κ−1

(σ → τ )−1 = σ −1 → τ −1
= σ −1
(¬σ)−1
−1
= κ−1
(¬κ)

The first row defines σ −1 , the second row σ −1 and κ−1 , and the third row κ−1 and τ −1 . From the first row
in turn, they are raw types, subsidiary types, and types in the sense of Def. 3.1.
Lemma 3.25.
(1) We have (S ∗ )−1 = S, (T + )−1 = T , and [[T ]]−1 = T .
(2) The following hold:
τ0 ≤ τ1
κ0 ≤ κ1
σ0 ≤ σ1

=⇒
=⇒
=⇒

τ0−1 ≤ τ1−1
κ1−1 ≤ κ0−1
σ0−1 ≤ σ1−1 .

We note that the order is flipped in case of κ.
Proof. Easy.



We prepare several lemmata needed to prove completeness. They are the properties of the source-side type
systems.
Lemma 3.26. Let V be a value T
of the CCV λµ-calculus. If Γ ⊢ V : Si | ∆ holds for a finite family of
subsidiary types Si , then Γ ⊢ V : i Si | ∆.
27

Proof. Easy.



Lemma 3.27. Let K be a term of sort K in the target calculus. Moreover, let us take a finite set of
subsidiary types Si in the source side.
T
⊥ | ∆ holds, and if Γ ⊢ V : Si | ∆ holds for every i where V is a value, then
(1) If Γ,  : Si ⊢ K −1 : ⊥
Γ ⊢ K −1 [V ] : ⊥
⊥ | ∆ holds.
S
(2) If Γ,  : Si ⊢ K −1 : ⊥
⊥ | ∆ holds for every i, and if Γ ⊢ M : Si | ∆ holds, then Γ ⊢ K −1 [M ] : ⊥
⊥|∆
holds.
T
Proof. (1) By Lem. 3.26, Γ ⊢ V : Si | ∆ holds. Now the lemma is easy.
(2) We split cases by the
shape of K. If K = k, the typing environment ∆ S
is of the form ∆0 , k :T . Since Γ, :Si ⊢ [k]:⊥
⊥ | ∆0 , k :T
is assumed, we have Si ≤ T for every i. Hence Si ≤ T . Thus Γ ⊢ M : T | ∆0 , k : T by the inheritance
rule. From this, the lemma is immediate. If K = λx. Q, we have Γ,  : Si ⊢ Q−1 ↾ x :=  : ⊥
⊥ | ∆ for every
i. Now Γ ⊢ Q−1 ↾ x := M : ⊥
⊥ | ∆ is a direct application of an inference rule.

Proposition 3.28. The following hold:
Π,
Π,
Π,
Π,

Θ
Θ
Θ
Θ

⊢s
⊢s
⊢s
⊢s

T :τ
Q:⊥
⊥
W :σ
K:κ

=⇒
=⇒
=⇒
=⇒

Π−1
Π−1
Π−1
Π−1 ,

⊢ T −1 : τ −1 | Θ−1
⊢ Q−1 : ⊥
⊥ | Θ−1
−1
⊢ W : σ −1 | Θ−1
 : κ−1 ⊢ K −1 : ⊥
⊥ | Θ−1

where Π−1 and Θ−1 are naturally defined. Namely, Π−1 is the sequence of x : σ −1 for x : σ occurring in Π,
and Θ−1 is the sequence of k : κ−1 for k : κ occurring in Θ.
Proof. Proof is by straightforward induction on the derivation. We pick up several cases. For readability,
let us write Γ, ∆ in place of Π−1 , Θ−1 . (i) Derivation of W1 WT
2 by the second rule. By induction hypothesis,
Γ ⊢ W2−1 : σi−1 | ∆ for each i. By Lem. 3.26, Γ T⊢ W2−1 : σi−1 | ∆ for W2−1 is a value. By induction
hypothesis, Γ ⊢ W1−1 : σ −1 → τ | ∆ where σ −1 = σi−1 . Hence Γ ⊢ W1−1 W2−1 : τ −1 | ∆ is inferred by the
application rule of Def. 3.5. (ii) Derivations of KW and T K are manipulated by (1) and (2) of Lem. 3.27
respectively.
(iii) The inheritance rule for κ, that is, the last rule save one in Def. 3.20. By induction
hypothesis, Γ,  : κ−1 ⊢ K −1 : ⊥
⊥ | ∆. Now κ ≤ κ′ implies κ′−1 ≤ κ−1 by Lem. 3.25, (2). Hence Lem. 3.12
′−1
and Cor. 3.13 imply Γ,  : κ
⊢ K −1 : ⊥
⊥ | ∆. Other cases are easy and left to the reader.

Let us see the part dealing with W1 W2 in the proof of Prop. 3.28. To produce the type of (W1 W2 )−1 =
W1−1 W2−1 , we use the application rule, that is, the third rule in the table of Def. 3.5. We note, however,
that the full-fledged potential of the rule is not used. The type of W1−1 is preceded by neither of intersection
and union. The full power is needed in the following lemma, which asserts the subject reduction property
for vertical reductions and the subject expansion property for administrative reductions.
Lemma 3.29.
(1) Suppose L → M by vertical reduction (Def. 1.20). If Γ ⊢ L : T | ∆ holds Γ ⊢ M : T | ∆ holds.
(2) Suppose L → M by administrative reduction (Def. 1.6). If Γ ⊢ M : T | ∆ holds Γ ⊢ L : T | ∆ holds.
Proof. (1) Immediate.
(2) By Lem. 3.15, we can apply the inversion of inference except to values.
This makes our proof slightly simple. In this proof, the typing context ∆ plays no role. So let us omit
it completely. There are two cases. We verify the case of (ad 2 ) V N → V z ↾ z := N where z is fresh.
Let us suppose Γ ⊢ V z ↾ z := N : T . By inversion, there
is a finite family of strict types Si such that
S
Γ, z : Si ⊢ V zS: T
holds
for
every
i
and
Γ
⊢
N
:
S
holds.
The former is, by inversion, obtained
Si
T
from Γ ⊢ V : j k (S̃ijk → T ) and [ Γ, z : Si ⊢ z : k S̃ijk ]j . By Rem. 3.6, (1), there is j such that
28

T
Γ ⊢ V : k (S̃ijk → T ). Let us Tfix such j = j(i) for each i. By the same remark, for each i, there is
k such that
S T ) ≤ Si → T . This holds for each i. So Lem 3.26 yields
T Si ≤ S̃ijk . Thence k (S̃ijk →
Γ ⊢ V : i (Si → T ). By this and Γ ⊢ N : Si , we conclude Γ ⊢ V N : T . The case of (ad 1 ) is similar. 
Now we are in the position to prove completeness for type systems.
Theorem 3.30. Let M be a term of the CCV λµ-calculus. We have
Π, Θ ⊢s [[M ]] : τ

=⇒

Π−1 ⊢ M : τ −1 | Θ−1 .

Proof. By Prop.3.28, we have Π−1 ⊢ [[M ]]−1 : τ −1 | Θ−1 . Let us recall, by Prop. 1.25, that vertical
reductions from [[M ]]−1 yield M † , from which we recover M by administrative expansions. Therefore two
statements of Lem. 3.29 yield Π−1 ⊢ M : τ −1 | Θ−1 .

3.4. Type-theoretic characterization of syntactic properties
Here is the main part of this section. We verify that the union-intersection type system of the CCV
λµ-calculus satisfies the subject reduction as well as a weak form of the subject expansion (Thm. 3.31).
Moreover, we give the type-theoretic characterization of the termination of call-by-value evaluation as well
as of normalizability (Thm. 3.34).
∗
Theorem 3.31. Let us suppose L −→
M in the CCV λµ-calculus.

(1) If Γ ⊢ L : T | ∆ holds, Γ ⊢ M : T | ∆ holds.
(2) If Γ ⊢ M : T | ∆ holds, there are Γ′ , ∆′ and T ′ such that Γ′ ⊢ L : T ′ | ∆′ holds.
Proof. (1) By Prop. 3.23, Γ∗ , ∆+ ⊢s [[L]] : [[T ]]. As commented in Rem. 1.16, we need only βη-reduction
and β-expansion (but no η-expansion) to obtain [[M ]] from [[L]]. Hence Prop. A.6 and Prop. A.7, (1), imply
Γ∗ , ∆+ ⊢s [[M ]] : [[T ]]. Thus by Thm. 3.30 we have (Γ∗ )−1 ⊢ M : [[T ]]−1 | (∆+ )−1 . Finally, Lem. 3.25, (1),
shows (Γ∗ )−1 = Γ, (∆+ )−1 = ∆ and [[T ]]−1 = T .
(2) To obtain [[L]] from [[M ]], we need η-expansion in
addition. We apply Prop. A.7, (2).

Remark 3.32. We need the change of typing environments and types in Thm. 3.31, (2), only in the ηλ expansion of V to λx. V x. Recall the proof of soundness 1.15, in which the η-rule of the target calculus is
involved only to handle ηλ and ηlet . However, for the latter, the used η-rule is λx. Kx → K of the sort K.
The subject expansion for η of this sort causes no problem as mentioned in the proof of Prop. A.7. Hence
the change is needed only for ηλ . If V has an atomic type α, we replace it by an arbitrary raw type S → T .
Remark 3.33. The rules for application and let-construct in Def. 3.5 are essentially the union-elimination
rule. It is reported in [3, §2] that, for the call-by-name system, the subject reduction/expansion property
fails if we include the union-elimination rule. The counter-example to the subject expansion is x(yz)(yz) : C
where x has type (A → A → C) ∩ (B → B → C), y type D → (A ∪ B), and z type D. The one to the
subject reduction is similar. We comment that the counter-examples are not applicable to our call-by-value
system. Indeed, x(yz)(yz) is unable to have type D, whereas xuu ↾ u := yz has. Note that the latter term
has no redution to the former in the call-by-value calculus. In exchange, the intersection-introduction rule
must be restricted in our system (see Example 3.38, (2)), contrary to the case of call-by-name.
Theorem 3.34. Let M be a CCV λµ-term.
(1) The call-by-value evaluation of M terminates if and only if typing judgement Γ ⊢ M : T | ∆ is derivable
for some Γ, ∆, and T .
29

(2) M is normalizable if and only if typing judgement Γ ⊢ M : T | ∆ is derivable for some Γ, ∆, and T ,
all these three containing neither ω nor .
ω

Proof. (1) By Thm. 2.31, the call-by-value evaluation of M terminates iff [[M ]] is solvable. The latter
is equivalent to existence of typing Π, Θ ⊢s [[M ]] : τ by Prop. A.8. Now the if-part is a consequence of
Prop. 3.23, and the only-if part of Thm. 3.30.
(2) Proof is similar. We use Thm. 2.11 and Prop. A.9
instead. The condition that Γ, ∆, and T contain neither ω nor corresponds to the condition that Π, Θ,
and τ do not contain ω, by Def. 3.21 and 3.24.

ω

We remark that, in Thm. 3.34, (2), ω and are prohibited only in the lowermost typing judgement of the
derivation tree. They may appear elsewhere.
ω

3.5. Conservative extension
Recall definition of types in Def. 3.1. The places of union and intersection are constrained. For example,
in the arrow type S → T , the left hand S cannot start with union. This kind of type system is relatively
exotic. No restriction is imposed, or different constraints are placed, in the union-intersection types appearing
in the literature.
In this subsection, we give a conservative extension of our former type system. The restriction on types
is removed. We can write union and intersection wherever we want. The extension itself is not difficult at
all. The motivation we think of it for all that lies in building a platform for comparison with related works.
We define the set of types A with no restriction forced in their construction:
T
S
A ::= α | A → A |
A |
A
T
where
S α ranges over atomic types. Moreover A denotes finite intersection A1 ∩ A2 ∩ · · · ∩ An , and likewise
for A. Case n = 0 is included.
For the subtype relation, in addition to the standard rules, we take the following supplementary axioms:
S
S
≤ Si (A ∩ Bi )
(sup 1 )
A ∩ i Bi
T
(sup 2 )
i (Ai → B) ≤ ( i Ai ) → B.
Specifically the standard rules are those of Def. 3.3 where we discard distinction among raw types, subsidiary
types and types, understanding S and T to range over all types A. Furthermore, we add the inference rules
of reflexivity and transitivity. For distinction, let us write A ≤ext B for the subtype relation of the extended
system.
S T
By the distributivity
law (sup 1 ), each type A is equivalent to a disjunctive normal form i j Aij .
S T
Namely A ∼ext i j Aij where
≤ext B and B ≤ext A. Moreover, by the second rule
S A ∼ext B means AT
(sup 2 ), each T → T ′ with T = i Si is equivalent to i (Si → T ′ ). Therefore each type A is equivalent to a
type T subject to the formation rule of Def. 3.1.
Lemma 3.35. We suppose A ∼ext T as well as A′ ∼ext T ′ where T and T ′ are subject to the rule of
Def. 3.1. Then A ≤ext A′ implies T ≤ T ′ where the latter is by the subtype relation defined in 3.3.
Proof. For each A we can find canonical T satisfying A ∼ext T by the translation from inside out. First
we verify T ≤ T ′ for canonical T and T ′ . The general case is inferred from this.

Next we give the extended typing judgement Γ ⊢ext M : A | ∆. In the typing environment Γ, we allow
x : A where A is a general type, contrary to the restriction to subsidiary types in the former system 3.5. The
inference rules include those in Def. 3.5 where we ignore distinction between subsidiary types and types,
regarding S and T to range over all types A. As an effect of allowing arbitrary A, we can simplify the rule
of application:
30

S
Γ ⊢ext M : i (Ai → A′ ) | ∆
Γ ⊢ext M N : A′ | ∆

[ Γ ⊢ext N : Ai | ∆ ]i
.

Furthermore, we add the following inference rule introducing union in typing environments:
Γ, x : A1 ⊢ext M : B | ∆
Γ, x : A2 ⊢ext M : B | ∆
Γ, x : A1 ∪ A2 ⊢ext M : B | ∆

We want to show that the extended type system is conservative. Since each type A is equivalent S
to T , we
may assume, from the beginning, that the judgement is Γ ⊢ext M : T | ∆ where Γ consists of xk : ik Sk ik
(k = 1, 2, . . . , n) for Sk ik and T subject to the formation rule of 3.1. Also the types assigned in ∆ are
supposed to be of the form T . Let us suppose that each ik ranges over an index set Ik . We associate a
family of |I1 | × |I2 | × · · · × |In | typing judgements:
[ x1 : S1 i1 , x2 : S2 i2 , . . . , xn : Sn in ⊢ M : T | ∆ ]i1 ,···,in
of the former type system. Now we have the following conservativity result.
Proposition 3.36. Typing judgement Γ ⊢ext M : T | ∆ is derived in the extended system if and only if all
of x1 : S1 i1 , x2 : S2 i2 , . . . , xn : Sn in ⊢ M : T | ∆ are derived in the system of Def. 3.5.
Proof. The only-if part is easy induction on derivations for ⊢ext . We use Lem. 3.35 to deal with the
inheritance rule. For the if-part, we observe that derivations for ⊢ are literally interpreted as derivations for
⊢ext . We employ the added inference rule several times to bring them together into a single derivation. 
Corollary 3.37. If Γ ⊢ext M : T | ∆ holds where Γ and ∆ are the typing environments allowed in Def. 3.5,
then Γ ⊢ M : T | ∆ holds.

Remark 3.38. Let us compare our type system with related systems in the literature. We take the conservative extension above as a workbench. We focus on call-by-value calculi having both union and intersection.
(1) Dunfield and Pfenning propose a functional language having both union and intersection (and more),
and verified basic properties such as type preservation and progress [14]. No control operators are
considered. The subtype relation coincides with the one defined in Def. 3.3. The two supplementary
axioms are not contained. Related to the intersection type, the following inference rules are considered
Γ ⊢ V :A
Γ ⊢ V :B
Γ ⊢ V :A∩B

Γ ⊢ V :ω

where symbols are changed for the sake of comparison. We note that the rules are applied only to value
V . In [10], it is mentioned that the subject reduction fails if they are extended to non-values, under
existence of mutable stores. The rules are derivable in our system viewing 3.26 and 3.36 (the latter is
tacitly used below repeatedly). For union types, the following inference rules are considered.
Γ ⊢ M :A∪B
Γ ⊢ E[M ] : C

Γ, x : A ⊢ E[x] : C

Γ, x : B ⊢ E[x] : C

Γ ⊢ M:
Γ ⊢ E[M ] : C

ω

These rules are derivable in our system. Let us consider the first. From two hypotheses for E[x], we
have λx. E[x] : (A → C) ∩ (B → C) by the inference rule for lambda abstraction in 3.5. Then the rule
for application yields (λx. E[x])M : C. Now we have (λx. E[x])M =ccv E[M ] as seen in Example 1.10.
Thus the subject reduction/expansion 3.31 yields Γ ⊢ E[M ] : C. (Since ηλ is not needed in 1.10, we
need no change of types or typing environments as commented in Rem. 3.32.) The second rule is similar,
noticing λx. E[x] has type ω. So the union-intersection fragment of their system is a subsystem of ours.
31

(2) Ishihara and Kurata propose type system TA and slightly weaker system TA− [34]. They define a class
of call-by-value lambda models called TA-models, and show that TA is sound while TA− is complete
with respect to certain denotational models. No control operator exists. Their subtype relation contains
all the rules of ours, including the supplementary axioms introduced in this subsection. The typing rule
related to union is
Γ ⊢ V :A∪B
Γ, x : A ⊢ M : C
Γ ⊢ M {V /x} : C

Γ, x : B ⊢ M : C
.

(In TA− , the value V is restricted to a variable.) This rule is derivable in our system as well. Indeed,
from λx. M : (A → C) ∩ (B → C), we obtain (λx. M )V : C. Now the subject reduction 3.31 yields
Γ ⊢ M {V /x} : C. Hence the rules related to union is simulated in our system.
However, the manipulation of intersection is different. Their system contains axiom (A → B) ∩ (A →
C) ≤ A → B ∩ C. Accordingly it contains an inference rule
Γ ⊢ M :A
Γ ⊢ M :B
Γ ⊢ M :A∩B

for arbitrary M , not restricted to values. Let us see what happens with this rule. We take types so
that A 6∼ext (A ∩ B) 6∼ext B. Let us suppose a : A, b : B, and f : ((X → X) → ω → X) ∩ (ω →
(X → X) → X) where X is arbitrary for it plays no role. Moreover, let l be of type X. We consider
M = µk. [l]f (λxµδ. [k]a)(λxµδ. [k]b). The term M has type A. For this, we let the type of λxµδ. [k]b
be ω (see Rem 3.6, (2)). Symmetrically M has type B. However M does not have type A ∩ B in our
system, since f cannot have type ω → ω → X. If we naturally extend their system to the λµ-calculus,
therefore, it is a non-conservative extension of ours. (System TA has no ω but has ν behaving similarly.)
Furthermore, the extension violates the subject reduction property. Let us set A = α → β and B = β.
If we take zz ↾ z := M for M above, it is typeable. But it contracts to µk. [l]f (λxµδ. [k]aa)(λxµδ. [k]bb)
that is not typeable at aa as well as bb.
(3) Palsberg and Pavlopoulou establish a link between polyvariant flow analyses and union-intersection
type systems [49]. They show equivalence between flow-safety and typeability. Although their types
are infinite regular trees for their purpose, here we ignore that aspect, and formally compare their type
systems presented in §3. The types are restricted to disjunctive normal forms. So axiom (sup 1 ) is
implicitly needed. The rules of the acceptable type ordering Def. 3.2, p. 278, are derivable from our
subtype relation. AlsoTthe axioms of a specific
acceptable
type ordering in §3.6, p. 284, are derivable.
S
S
To derive axiom (21) i (Ai → Bi ) ≤ ( i Ai ) → ( i Bi ) therein, we need axiom (sup 2 ). The typing
rules for the lambda-calculus fragment in p. 279 are the same as our
S rules 3.5 except for application.
The rule for application is the restriction of ours where the union i is not involved. Therefore their
system is a subsystem of ours.
(4) Van Bakel gives union-intersection type systems for the λµµ̃-calculus and the calculus X based on the
classical sequent calculus [65][66]. Both of these calculus include the call-by-name and the call-by-value
fragments. Since the syntax is quite different from the λµ-calculus, relation is not clear at this stage.
We leave comparison to the future work.

4. Call-by-value catch/throw calculus: a chain of parasitism
We can make a chain of parasitism. We have defined the CCV λµ-calculus, and verified several properties
using proof by parasitism. Now we can take the calculus as the new target of a translation of a calculus.
Namely, we cascade proof by parasitism for creation of new complete calculi.
In this section, we give a call-by-value version of Crolard’s catch/throw calculus λct [8]. We verify the
completeness with respect to the translation into the CCV λµ-calculus as a demonstration of a chain of
parasitism.

32

Definition 4.1. We separate ordinary variables x and continuation variables k. The terms M of the callby-value catch/throw calculus are defined by
M ::= x

| λx. M

|

MM

| M ↾ x := M

|

εk. M

|

raise k M .

The construct εk binds the continuation variable k, so that it obeys α-convertibility. The displayed occurrence of k in raise k M is free. We note that continuation variables are used only in this form.
We change notations from [8]. Binding operator εk builds a new exception block tagged by identifier k.
Construct raise k throws an exception that is caught by the encapsulating block tagged by k. Since εk is
subject to α-conversion, the calculus gives the static catch/throw mechanism.
Definition 4.2. We introduce the following equality rules between terms:
L ↾ x := (M ↾ y := N ) = (L ↾ x := M ) ↾ y := N
(εk. M ) ↾ x := N
= εk. (M ↾ x := N )
(raise k M ) ↾ x := N
= raise k (M ↾ x := N )

if y 6∈ L
if k ∈
6 N

We usually omit brackets as in the CCV λµ calculus (see Rem. 1.4). For the reduction rules, we replace
βµ , βjmp , and ηµ in Def. 1.6 by the following seven rules:
εδ. M
εk. raise k M
M ↾ x := raise k N
raise l raise k N
M ↾ x := εk. N
raise l εk. M
εlεk. M

→
→
→
→
→
→
→

M
εk. M
raise k N
raise k N
εk. M ↾ x := N {raise k  7→ raise k M ↾ x := }
raise l M {l/k}
εl. M {l/k}

where δ is a dummy continuation variable that does not occur free in M . The notation {raise k  7→
raise k M ↾ x := } denotes the structural substitution similar to the one in the λµ-calculus. We notice
that the substitution is applied recursively. Moreover {l/k} is the abbreviation of structural substitution
{raise k  7→ raise l }.
Continuation variables k are, unlike ordinary variables, never substituted with values. They behave only as
placeholders to mark the positions to insert continuations as in the λµ-calculus.
Remark 4.3.
(1) The operational semantics of call/cc is different from that of catch. The former creates a continuation object at each call, whilst the latter simply waits for an exception to be raised [45]. Though
called catch/throw for historical reasons, our calculus equally simulates the first-class continuation. The
following encoding is found in [8, p. 646]:
call/cc M

:= εk. M (λx. raise k x).

Let τ̂ be a fixed continuation variable representing the topmost context. Let us use the equality symbol
for the congruence relation generated from the equality and reduction rules in Def. 4.2. Then we have
raise τ̂ E[ call/cc M ] = raise τ̂ E[εk. M (λx. raise k x)]
= raise τ̂ E[x] ↾ x := εk. M (λx. raise k x)
= raise τ̂ E[M (λx. raise τ̂ E[x])]
(see 1.10 for the second equality). In particular, if E has the form L ↾ x := , the first contracts to the
last. Hence, if we regard raise τ̂ as the abort operator A, we regain the ordinary operational semantics
33

of the call/cc-operator. Therefore εk is much like a control operator than a simple catch mechanism. In
fact, the abstract machine model in [8] copies the stack environment at each call of catch.
The little twist in the encoding of call/cc above is caused by the character of the calculus that the continuation variables are unable to be substituted. The first-class continuation is not directly materialized
in our calculus. In view of call/cc(λy. L) = εk. L ↾ y := λx. raise k x, we observe that the continuation k
is passed to the ordinary variable y by making the first-class closure λx. raise k x, the essence of which
is k itself. We may say that continuations in our calculus are quasi-first-class.
(2) Sato defines a calculus of catch/throw in [60], simplifying Nakano’s calculus [46]. The catch operator
catchk M has disjunction type A ∨ B where A is the type of M representing a normal exit while the
type B of k is for non-local exits. (In [60], symbol ? is used for catch and ! for throw.) In the
classical propositional logic, A ∨ B is equivalent to (B → A) → A. Two injections are represented by
inl M = λf. M and inr M = λf. f M . Let us adopt the following encoding:
catchk M
:= λf εγ. f (εk. raise γ M )
throwk M
:= raise k M
tapply(M, k) := M (λx. raise k x)
where γ is a fresh continuation variable. If we develop the simply typed system appropriately, catchk M
has type (B → A) → A. The six reduction rules in [37, p. 230] are
L ↾ x := throwk M
catchk M
catchk throwk M
tapply(inl M, k)
tapply(inr M, k)
tapply(catchk M, l)

→
→
→
→
→
→

throwk M
inl M
inr M
M
throwk M
M {l/k}

(if k 6∈ M )
(if k ∈
6 M)

where the first rule is replaced since we are concerned with call-by-value. In our favor, the last replacement serves to get rid of the non-confluence example (p. 229, ibid.). These reduction rules are then
realized by one or more steps of contractions in our calculus. Therefore their catch-throw calculus is a
subsystem of ours.
(3) Next we consider de Groote’s system [12]. We encode the exception handling block as
let k in M handle kx ⇒ N

:=

εγ. N ↾ x := εk. raise γ M

where γ is a fresh continuation variable. We note that it is equal to (catchk M )(λx. N ) using the
encoding of the catch above. For the raise operator, we identify raise(kM ) in the original with raise k M
and avoid using tag-less raise. Then the reduction rules in Tab. 2, p. 206 are simulated after appropriate
modification. Unlike the case of Sato’s system, the orientation of the reduction is not preserved. We
are content to show that two sides of the reduction rules are equal. The most essential is the following
rule called (handle/raise):
let k1 in
let k2 in
..
.
let kn in
raise (k1 V )
handle kn x ⇒ Nn
..
.
handle k2 x ⇒ N2
handle k1 x ⇒ N1

let k1 in
let k2 in
..
.
→

let kn in
N1 {V /x}
handle kn x ⇒ Nn
..
.
handle k2 x ⇒ N2
handle k1 x ⇒ N1

where Ni may contain k1 , k2 , . . . , ki−1 . The translations of the two sides contract to a common term
34

εγ. N1 {x 7→ V θn · · · θ2 θ1 } where θi = {raise k i  7→ raise γ Ni ↾ x := }.
(4) The catch/throw-related part of Krebbers’ system [38] is easily simulated by identifying catch k with εk
and throw k with raise k.
We show that our call-by-value catch/throw calculus is sound and complete. We take the CCV λµ-calculus
as the target language.
Definition 4.4. The translation [[-]] from the call-by-value catch/throw calculus into the CCV λµ-calculus
and the inverse translation (-)−1 are defined. For the control operators, we define as follows:
[[εk. M ]]
= µk. [k][[M ]]
[[raise k M ]] = µδ. [k][[M ]]

(µk. J)−1 = εk. J −1
([k]M )−1 = raise k M −1

where δ is a dummy continuation variable. For the other constructs, the translations are homomorphic
except that for application we set
[[N1 N2 ]]
[[N V ]]
[[V N ]]
[[V1 V2 ]]

=
=
=
=

zw ↾ w := [[N2 ]] ↾ z := [[N1 ]]
z[[V ]] ↾ z := [[N ]]
[[V ]]z ↾ z := [[N ]]
[[V1 ]][[V2 ]]

where V is a value and N a non-value. This definition is chosen to ensure that [[M ]] becomes an administrative
normal form. Except this technical point, the essentially same translations are found in [8] and [37].
∗
∗
Lemma 4.5. If [[M ]] −→
N holds in the CCV λµ-calculus, then M −→
(N −1 )↓ holds, where (-)↓ means to
take the normal form with respect to vertical reductions.

Theorem 4.6. The call-by-value catch/throw calculus satisfies the Church-Rosser property.
Proof. Proceed along the same line as in Thm. 2.1, using completeness 4.5 and the Church-Rosser property
of the target 2.1.

To avoid that the paper is too long, we stop here. The results in previous sections are extended in a relatively
simple way. We refer the reader to [55].
5. Conclusion
We present a new call-by-value λµ-calculus and a catch/throw calculus that are complete for the continuation-passing style semantics. A key idea is to deviate from the standard convention that terms should be
syntactic trees. If we are to accept this deviation, we can have simple but complete systems.
The calculi satisfy a certain form of completeness with respect to reduction. Cultivating the completeness, we verify a number of anticipated properties by pulling back the corresponding ones in the ordinary
lambda calculus. This method is called proof by parasitism. Although the idea itself is not new, we persistently pursue its benefits. We succeed in showing Church-Rosser, and in characterizing normalizability and
termination of call-by-value evaluation in terms of the CPS translation for the call-by-value λµ-calculus. We
also give a union-intersection type system, and verifies that various syntactic properties are chracterized by
typeability.
Related works are mentioned in the relevant parts of this paper. We do not repeat all. Here we review the
previous results on the completeness of lambda calculi and their extensions, focusing largely on call-by-value
systems having control operators. We comment that almost all previous systems are presented as equational
theories. The computational properties are scarcely explored.
35

As far as the author knows, the first work establishing completeness of the call-by-value lambda calculus is
done by Sabry et al. [58][57] The inverse of the CPS translation is first introduced in their papers. The rules
of the call-by-value lambda calculus in [58, Fig. 2, p. 311] are sound and complete for the CPS translation.
They consider reduction rules, not only equalities. Reduction sequences are preserved and reflected by
the CPS translation. Furthermore, they extend the call-by-value lambda calculus by adding the control
operators, call/cc and abort. The rules of Fig. 4 (p. 319) are sound and complete. For the extended system,
only equalities are considered. If we encode the control operators as call/cc M = µk. [k]M (λxµδ. [k]x) and
abort M = µδ. [τ̂ ]M using a fixed special continuation variable τ̂ , the rules of their calculus are derived from
our CCV λµ-calculus up to equality.
Hofmann deals with Felleisen’s C-operator and abort [32]. The equational theory is defined in Def. 1
in p. 465. It is sound and complete for the categorical model introduced in Def. 5 (p. 470). The proof of
completeness is by construction of the term model. The calculus has especially the initial type 0. The rules
involving the abort operator depend on types. If M is of type 0, we have rule AM = M called (A0 -Id). The
rules save this one are derived in the CCV λµ-calculus if we encode CM = µk. [τ̂ ]M (λxµδ. [k]x). Later the
system is simplified in [33, §5.3].
Führmann and Thielecke simplify Hofmann’s calculus [18]. As a new rule they introduce λk. k(CV ) = V
called rule (C-Delay). Completeness is verified in Thm. 40 (p. 261), Thm. 45 (p. 263), and Cor. 71 (p.274)
in various settings. The type of operator C is ((A → O) → O) → A where O is the initial type. We warn
that rule (C-delay) is not valid in the CCV λµ-calculus, if we take the encoding of C above, that can have
type ((A → B) → B) → A for arbitrary B. The rule heavily depends on the fact that O is initial. To make
the rule valid in the call-by-value λµ-calculus, we must regard ⊥
⊥ as an atomic type and add rules related
to the continuation variables of type ⊥
⊥ as done in [61].
Hofmann and Streicher discuss both the call-by-name and the call-by-value λµ-calculus [33]. Terms and
jumps are not separated. For the call-by-value language, Fig. 5 in p. 347 gives the equational theory. It
is sound and complete for the categorical model in Def. 5.1 (p. 346). The calculus contains several rules
involving the initial type 0. Except these, all rules are derivable from ours.
Selinger’s theory of the call-by-value λµ-calculus is essentially the same as ours, though that paper deals
with only equalities [61, Tab. 10]. The theory is sound and complete for the categorical model, called the
co-control category (§.4.2). His system contains also tensor, unit and finite coproducts. As minor differences,
the let-construct let x = M in N is an abbreviation of (λx. N )M , and terms and jumps are not separated.
Herbelin and Zimmermann give a reduction system, called the λµtpCBV -calculus, which is complete for
the CPS semantics [30]. Their system uses the let-notation as a primitive. It contains the rule of type
let x = M in E[x] → E[M ] as well as the let-flat rule. This calculus satisfies confluence (Prop. 9, p. 152).
The idea is to disallow E[V ] as the evaluation context if V is a lambda abstraction, allowing only E[x]
for variable x. The contexts that are able to be captured by µ are restricted accordingly.
If we extend the range to delimited control operators, we can find the axiomatization by Kameyama and
Hasegawa [36]. It deals with equational theories of shift/reset and the delimited call/cc. Completeness for
the CPS translation is verified by the inverse translation. Moreover, Ariola et al. gives several calculi having
delimited control operators [2]. The calculus in §7.5 (p. 262) is complete with respect to the KameyamaHasegawa’s theory. Although the system is given with reduction rules, the completeness result is obtained
for equational theories.
The above is an overview for the complete call-by-value calculi. For the call-by-name, the pioneering
paper [54] by Plotkin already verifies completeness of the λ-calculus in Thm. 6 (p. 153). The proof is by
simulation relations. It is extended by de Groote to the call-by-name λµ-calculus [11]. Fujita establishes
completeness by the inverse translation [20][21]. He manages to deal with reduction using an idea similar to
ours. Also Hofmann-Streicher [33] and Selinger [61] show completeness with respect to categorical models.
Acknowledgement
We are grateful to Kazunori Tobisawa for letting the author notice the importance of Cor. 2.32, especially
in the context of the coding of cooperative multitasking 2.33.
36

Appendix A. Properties of the type system for the target calculus
We collect several results of the intersection type system for the target calculus defined in §3.2. The
argument follows the standard one that uses filter domains [5][7]. So we omit proof mostly.
We need subject reduction/expansion for the type system in Def. 3.20. The results in the literature
are not directly applicable, though our system is a subsystem of [5] if we forget about sorts. The reason
is that the types of terms are constrained relative to their sorts. For example, a type of term K must be
of the form ¬σ, i.e, σ → ⊥
⊥. The right hand of the arrow is restricted to ⊥
⊥. We must ensure that the
subject reduction/expansion remain to hold under the constraint. We extend the standard arguments to
many-sorted languages.
T
τ.
We extend the types in Def. 3.17 by introducing τ ::=
Definition A.1. A T -filter d is a non-empty set of types τ satisfying the ordinary filter conditions: (i)
τ ∩ τ ′ ∈ d whenever τ , τ ′ ∈ d; (ii) τ ′ ∈ d whenever τ ∈ d and τ ≤ τ ′ . Similarly we define a K-filter and a
⊥}.
W -filter by replacing τ with κ and σ. We can define also a Q-filter as a filter on the singleton set {⊥
Definition A.2. Filter domain T is the set of all T -filters. It forms an algebraic complete partial order
(CPO) [25] in regard to inclusion. Similarly filter domains K, W, and Q are defined. We comment that Q
is the Sierpı́nski space consisting of two filters {ω} and {ω, ⊥
⊥}.
As usual, we let [D → D′ ] denote the CPO of all Scott continuous maps of D into D′ , partially-ordered by
the pointwise ordering. We let ↑ X denote the smallest filter containing the set X.
Definition A.3. We define six continuous maps:
FT
[K → Q],
T −→
←−
G
T

FK
[W → Q],
K −→
←−
G
K

FW
[W → T ],
W −→
←−
G
W

these defined as follows:
FT (d) = λe. ↑{⊥
⊥ | ∃κ ∈ e. ¬κ ∈ d}
FK (d) = λe. ↑{⊥
⊥ | ∃σ ∈ e. ¬σ ∈ d}
FW (d) = λe. ↑{τ | ∃σ ∈ e. (σ → τ ) ∈ d}
GT (f ) = ↑{¬κ | ⊥
⊥ ∈ f (↑ κ)}
GK (f ) = ↑{¬σ | ⊥
⊥ ∈ f (↑ σ)}
GW (f ) = ↑{σ → τ | τ ∈ f (↑ σ)}.
In the last three, for example, ↑ σ denotes the principal filter generated by σ (namely, an abbreviation of
↑{σ}). We remark that the sets occurring here are upward-closed for strict types. Hence ↑{· · ·} means
taking the closure with respect to finite intersection, especially, adding ω forcibly.
The interpretation of terms of the target calculus, [[T ]]ξ etc., is naturally defined. An environment ξ assigns
a W-filter e to each ordinary variable x and a K-filter d to each continuation variable k. We have [[T ]]ξ ∈ T ,
[[K]]ξ ∈ K, [[W ]]ξ ∈ W, and [[Q]]ξ ∈ Q. The definition of the interpretation is standard. For example,
[[λk. Q]]ξ := GT (λd. [[Q]]ξ{d/k}) and [[W1 W2 ]]ξ := FW ([[W1 ]]ξ)([[W2 ]]ξ).
To understand relation between the filter domains and the intersection types, it is convenient to formally
introduce the environments associating filters to variables, x : d and k : e where d ∈ W and e ∈ K. We let
Πfil denote an environment of x : d and Θfil an environment of k : e. As usual, the variables occurring in the
environments should be distinct from each other.
Definition A.4. We introduce the typing judgement Πfil , Θfil ⊢s T : τ . We interpret this judgement as
there are Π and Θ satisfying the following three conditions: (i) Supposed that Πfil is x1 :d1 , x2 :d2 , . . . , xm :dm ,
37

the typing environment Π is of the form x1 : σ 1 , x2 : σ 2 , . . . , xm : σ m where each σ i is a member of filter di . (ii)
Supposed that Θfil is k1 :e1 , k2 :e2 , . . . , kn :en , the typing environment Θ is of the form k1 :κ1 , k2 :κ2 , . . . , kn :κn
where each κi is a member of filter ei . (iii) Π, Θ ⊢s T : τ holds. Similar for other sorts.
Proposition A.5. To each environment ξ associate we the filtering environments Πfil = Πξ and Θfil = Θξ
in a natural manner. Namely, we take x : d if ξ(x) = d and k : e if ξ(k) = e. The following hold:
τ ∈ [[T ]]ξ
⊥
⊥ ∈ [[Q]]ξ
σ ∈ [[W ]]ξ
κ ∈ [[K]]ξ

⇐⇒
⇐⇒
⇐⇒
⇐⇒

Πξ ,
Πξ ,
Πξ ,
Πξ ,

Θξ
Θξ
Θξ
Θξ

⊢s
⊢s
⊢s
⊢s

T :τ
Q:⊥
⊥
W :σ
K : κ.

Next two propositions establish subject reduction/expansion of the target calculus. For η-reduction, we
have only a weak form of subject expansion.
Proposition A.6. We suppose T → T ′ by β-reduction. Then we have
Π, Θ ⊢s T : τ

⇐⇒

Π, Θ ⊢s T ′ : τ .

Similar for other sorts.
Proof. The filter model is sound in regard to β-conversion since Fa ◦ Ga = id where a = T, W, K.



Proposition A.7. We suppose T → T ′ by η-reduction. The following hold:
(1) If Π, Θ ⊢s T : τ holds, Π, Θ ⊢s T ′ : τ holds.
(2) If T ′ is typeable for some typing environments, so is T .
Similar for other sorts.
Proof. We note GW (FW (d)) = ↑{σ → τ | σ → τ ∈ d}. Hence GW (FW (d)) ⊆ d. So η-reduction preserves
types whereas η-expansion does not in case of λx. W x. Specifically, if W has atomic type α, then λx. W x
is not provided with the same type. However, we can substitute the atomic type α with an arbitrary type
of the form σ → τ . Then both W and λx. W x have this type. Since single W may have two or more typing
judgements, we apply the substitution repeatedly if needed. Hence η-expansion preserves typeability. On the
other hand, Ga (Fa (d)) = d for a = T, K. Hence, for the η-rule of other sorts, subject reduction/expansion
actually holds.

Now we characterize solvability and normalizability in the target calculus by typeability. We adapt results
in [5] to our setting.
Proposition A.8. Term T is solvable if and only if there are Π, Θ, and τ such that Π, Θ ⊢s T : τ . Similar
for other sorts.
In the next proposition, we should assume that there is at least one atomic type for otherwise there are no
derivations satisfying the assumption.
Proposition A.9. Term T is normalizable if and only if Π, Θ ⊢s T : τ holds for some Π, Θ, and τ , all of
these three not containing ω. Similar for other sorts. We emphasize that the typing judgements except the
lowermost in the derivation tree may contain ω.
38

References
[1] A. W. Appel, Compiling with Continuations, Cambridge University Press, 1992.
[2] Z. M. Ariola, H. Herbelin, and A. Sabry, A type-theoretic foundation of delimited continuations, Higher-Order Symbolic
Comput. 22(3):233–273, 2009.
[3] F. Barbanera, M. Dezani-Ciancaglini, and U. de’Liguoro, Intersection and union types: Syntax and semantics, Inform.
Comput. 119(2):202–230, 1995.
[4] H. P. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics,
Volume 103, Revised Edition, North-Holland, 1984.
[5] H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment,
J. Symbolic Logic, 48(4):931–940, 1983.
[6] U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed lambda calculus, Proceedings of
the Sixth Annual Symposium on Logic in Computer Science, LICS ’91, Amsterdam, The Netherlands, July, 1991, pages
203–211, IEEE, 1991.
[7] M. Coppo, D. Dezani-Ciancaglini, and M. Zacchi, Type theories, normal forms, and D∞ -lambda models, Inform. Comput.,
72(2):85–116, 1987.
[8] T. Crolard, A confluent λ-calculus with a catch/throw mechanism, J. Func. Program. 9(6):625–647, 1999.
[9] P.-L. Curien and H. Herbelin, The duality of computation, Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming, ICFP ’00, M. Odersky, P. Wadler, eds., Montreal, Canada, Sep. 2000, pages
233–243, ACM Press, 2000.
[10] R. Davies and F. Pfenning, Intersection types and computational effects, Proceedings of the Fifth International Conference
on Functional Programming, ICFP ’00, P. Wadler, ed., Montreal, Canada, Sep. 2000, pages 198–208, ACM Press, 2000.
[11] P. de Groote, A CPS-translation of the λµ-calculus, Proceedings of the 19th International Colloquium on Trees in Algebra
and Programming, CAAP ’94, S. Tison, ed., Edinburgh, U.K., April, 1994, Lecture Notes in Computer Science 787, pages
85–99, Springer, 1994.
[12] P. de Groote, A simple calculus of exception handling, Second International Conference on Typed Lambda Calculi and
Applications, TLCA ’95, M. Dezani-Ciancaglini, G. Plotkin, eds., Edinburgh, U.K., Lecture Notes in Computer Science
902, pages 201–215, Springer, 1995.
[13] A. L. de Moura and R. Ierusalimschy, Revisiting coroutines, ACM Trans. Program. Lang. Syst., 31(2): 2009.
[14] J. Dunfield and F. Pfenning, Type assignment for intersections and unions in call-by-value languages, 6th International
Conference on Foundations of Software Science and Computational Structures, FoSSaCS 2003, A. D. Gordon ed., Warsaw,
Poland, Apr. 2003, pages 250–266, Lecture Notes in Computer Science 2620, (Springer, 2003).
[15] M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba, A syntactic theory of sequential control, Theoret. Comput.
Sci., 52(3):205–237, 1987.
[16] A. Filinski, Representing monads, 21st ACM Symposium on ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, POPL 1994, H. J. Boehm, B. Lang, D. M. Yellin, eds., Portland, Oregon, U.S.A., Jan. 1994,
pages 446–457, ACM Press, 1994.
[17] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen, The essence of compiling with continuations, Proceedings of the
ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, R. Cartwright, ed.,
Albuquerque, New Mexico, U.S.A., Jun. 1993, pages 237–247, ACM Press, 1993.
[18] C. Führmann and H. Thielecke, On the call-by-value CPS transform and its semantics, Inform. Comput. 188(2):241–283,
2004.
[19] K. Fujita, Domain-free λµ-calculus, RAIRO Theoret. Inform. Appl., 34(6):433–466, 2001.
[20] K. Fujita, A sound and complete CPS-translation for λµ-calculus, Proc. 6th International Conference on Typed Lambda
Calculi and Applications TLCA 2003, M. Hofmann, ed., Valencia, Spain, June, 2003, Lecture Notes in Computer Science
2701, pages 120–134, Springer, 2003.
[21] K. Fujita, Galois embedding from polymorphic lambda types into existential types, Proc. 7th International Conference
on Typed Lambda Calculi and Applications, TLCA 2005, P. Urzyczyn, ed., Nara, Japan, April, 2005, Lecture Notes in
Computer Science 3461, pages 194–208, Springer, 2005.
[22] K. Fujita, CPS-translation as adjoint, Theoret. Comput. Sci. 411:324–340, 2010.
[23] J.-Y. Girard, Linear Logic, Theoret. Comput. Sci. 50(1):1–102, 1987.
[24] T. G. Griffin, A formulae-as-types notion of control, The Seventeenth Annual ACM Symposium on Principles of Programming Languages, POPL 1990, San Francisco, Calif., U.S.A., Jan. 1990. pages 47–58, ACM Press, 1990.
[25] C. A. Gunter, Semantics of Programming Languages; Structures and Techniques, MIT Press, 1992.
[26] R. Hasegawa, Relational limits in general polymorphism, Publ. Research Inst. Math. Sci. 30(4):535–576, 1994.
[27] M. Hasegawa and Y. Kakutani, Axioms for recursion in call-by-value, Higher-Order Symbolic Comput. 15(2-3):235–264,
2002.
[28] S. Hayashi, Singleton, union and intersection types for program extraction, International Conference TACS ’91, Theoretical Aspects of Computer Software, T. Ito and A. R. Meyer, eds., Sendai, Japan, Sep. 1991, Lecture Notes in Computer
Science 526, pages 701–730, Springer, 1991.
[29] C. T. Haynes, D. P. Friedman, and M. Wand, Continuations and coroutines, Proceedings of the 1984 ACM Symposium
on Lisp and Functional Programming, LFP ’84, Austin, Texas, U.S.A., Aug. 1984, pages 293–298, ACM 1984.
[30] H. Herbelin and S. Zimmermann, An operational account of call-by-value minimal and classical λ-calculus in “natural
deduction” form, 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, P.-L. Curien,
ed., Brasilia, Brazil, Jul. 2009, Lecture Notes in Computer Science 5608, pages 142–156, Springer, 2009.

39

[31] R. Hinze, Kan extensions for program optimisation, or: Art and Dan explain an old trick, 11th International Conference
on Mathematics of Programming Construction, MPC 2012, J. Gibbons, P. Nogueira, eds., Madrid, Spain, Jun. 2012,
Lecture Notes in Computer Science 7342, pages 324–362, Springer, 2012.
[32] M. Hofmann, Sound and complete axiomatisations of call-by-value control operators, Math. Struct. Comput. Sci.,
5(4):461–482, 1995.
[33] M. Hofmann and T. Streicher, Completeness of continuation models for λµ -calculus, Inform. Comput., 179(2):332–355,
2002.
[34] H. Ishihara and T. Kurata, Completeness of intersection and union type assignment systems for call-by-value λ-models,
Theoret. Comput. Sci. 272(1-2):197–221, 2002.
[35] R. P. James and A. Sabry, Yield: Mainstream delimited continuations, Theory and Practice of Delimited Continuations,
TPDC 2011, Novi Sad, Serbia, May, pages 20–32.
[36] Y. Kameyama and M. Hasegawa, A sound and complete axiomatization of delimited continuation, Proceedings of the
Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP’03, C. Runciman, O. Shivers, eds.,
Uppsala, Sweden, Aug. 2003, pages 177–188, ACM Press, 2003.
[37] Y. Kameyama and M. Sato, Strong normalizability of the non-deterministic catch/throw calculi, Theoret. Comput. Sci.,
272(1–2):223–245, 2002.
[38] R. Krebbers A call-by-value λ-calculus with lists and control, Proceedings Fourth Workshop on Classical Logic and
Computation, H. Geuvers, U. de’Liguoro, eds., Warwick, U.K., Jul. 2012, Electronic Proceedings in Theoretical Computer
Science 97, pages 19–34.
[39] S. Kuroda, Intuitionistische Untersuchungen der formalistischen Logik, Nagoya Math. J., 2: 35–47, 1951.
[40] P. J. Landin, The mechanical evaluation of expressions, Computer J. 6(4):308–320, 1964.
[41] P. J. Landin, A correspondence between ALGOL 60 and Church’s lambda-notation: Part I, Comm. ACM, 8(2):89–101,
1965.
[42] S. Mac Lane, Categories for the working mathematician, Springer, 1971.
[43] E. Moggi, Computational lambda-calculus and monads, preprint, LFCS Report Series, Laboratory for Foundations of
Computer Science, Department of Computer Science, The University of Edinburgh, Oct., 1988.
[44] C. Murthy, Extracting constructive content from classical proofs, Ph.D Thesis, Department of Computer Science, Cornell
University, 1990.
[45] H. Nakano, A constructive formalization of the catch and throw mechanism, Seventh Annual IEEE Symposium on Logic
in Computer Science, LICS 1992, Santa Cruz, CA, U.S.A., Jun. 1992, pages 82–82, IEEE, 1992
[46] H. Nakano, The non-deterministic catch and throw mechanism and its subject reduction property, Logic, Language and
Computation, Festscrhift in Honor of Satoru Takasu, N. D. Jones, M. Hagiya, M. Sato, eds., Lecture Notes in Computer
Science 792, pages 61–72, Springer, 1994
[47] S. Nishizaki, Programs with continuations and linear logic, Sci. Comput. Program. 21(2):165–190, 1993.
[48] C.-H. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, The 24th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, P. Lee, F. Henglein, N. D. Jones,
eds., Paris, France, Jan. 1997, pages 215–227, ACM Press, 1997.
[49] J. Palsberg and C. Pavlopoulou, From polyvariant flow information to intersection and union types, J. Func. Program.
11(3):263–317, 2001.
[50] M. Parigot, λµ-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated
Reasoning, 4th International Conference LPAR ’92, A. Voronkov, ed., St. Petersburg, Russia, Jul. 1992, Lecture Notes
in Artificial Intelligence 624, pages 190–201, Springer, 1992.
[51] M. Parigot, Classical proofs as programs, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC
’93 G. Gottlob, A. Leitsch, D. Mundici, eds., Brno, Czech, Aug. 1993, Lecture Notes in Computer Science 713, pages
263–276, Springer 1993.
[52] S. Peyton Jones, W. Partain, and A. Santos, Let-floating: moving bindings to give faster programs, ACM SIGPLAN
notices 31(6):1–12, 1996.
[53] B. Pierce, Programming with intersection types, union types, and polymorphism, Preprint, CMU-CS-91-105, School of
Computer Science, Carnegie Mellon University, 1991.
[54] G. D. Plotkin, Call-by-name, call-by-value and the λ-calculus, Theoret. Comput. Sci. 1(2):125–159, 1975.
[55] B. Ponwilawan, A Call-by-value Catch/throw Calculus and its Union-Intersection Type System Characterizing Normalizability, , Master Thesis, Graduate School for Mathematical Sciences, The University of Tokyo, 2014.
[56] J. C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the 25th ACM Annual
Conference, Volume 2, J. J. Donovan, R. Shields, eds., Oct. 1972, pages 717–740, 1972; Reprinted in Higher-Order
Symbolic Comput. 11(4):363–397, 1998.
[57] A. A. Sabry, The Formal Relationship between Direct and Continuation-Passing Style Optimizing Compilers: A Synthesis
of Two Paradigms, Doctoral Thesis, Rice University, 1994.
[58] A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style, Lisp Symbolic Comput. 6(3-4):289–
360, 1993.
[59] A. Sabry and P. Wadler, A reflection on call-by-value, ACM Trans. Program. Lang. Systems 19(6): 916–941, 1997.
[60] M. Sato, Intuitionistic and classical natural deduction systems with the catch and the throw rules, Theoret. Comput. Sci.
175(1):75–92, 1997.
[61] P. Selinger, Control categories and duality: On the categorical semantics of the lambda-mu calculus, Math. Struct.
Comput. Sci. 11(2):207–260, 2001.
[62] M. Takahashi, Parallel reductions in λ-calculus, Inform. Comput. 118(1):120–127, 1995.

40

[63] S. van Bakel, Complete restrictions of the intersection type discipline, Theoret. Comput. Sci., 102(1):135–163, 1992.
[64] S. van Bakel, Sound and complete typing for λµ, Proceedings Fifth Workshop on Intersection Types and Related Systems,
ITRS ’10, E. Pimentel, B. Venneri, J. Wells, eds., Edinburgh, Scotland, Jul. 2010, Electronic Proceedings in Theoretical
Computer Science 45, pages 31–44.
[65] S. van Bakel, Completeness and partial soundness results for intersection and union typing for λµµ̃, Ann. Pure Appl.
Logic 161(11):1400–1430, 2010.
[66] S. van Bakel, Completeness and soundness results for X with intersection and union types, Fund. Inform. 121(1–4):1–41,
2012.
[67] S. van Bakel, F. Barbanera, and U. de Liguoro, A filter model for λµ, 10th International Conference on Typed Lambda
Calculi and Applications, TLCA 2011, Novi Sad, Serbia, L. Ong, ed., Jun. 2011, Lecture Notes in Computer Science 6690,
pages 213–228, Springer, 2011.
[68] J. Voigtländer, Asymptotic improvement of computations over free monads, 9th International Conference on Mathematics
of Programming Construction, MPC 2008, P. Audebaud, C. Paulin-Mohring, eds., Marseille, France, Jul. 2008, Lecture
Notes in Computer Science 5133, pages 388–403, Springer 2008.

41

