Logical Methods in Computer Science
Vol. 9(1:14)2013, pp. 1–38
www.lmcs-online.org

Submitted
Published

Jul. 2, 2010
Mar. 28, 2013

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH
INDUCTIVE AND COINDUCTIVE TYPES ∗
DAISUKE KIMURA AND MAKOTO TATSUTA
National Institute of Informatics, 2-1-2 Hitotsubashi, Tokyo 101-8430, Japan
e-mail address: {kmr, tatsuta}@nii.ac.jp

Abstract. This paper extends the dual calculus with inductive types and coinductive types. The paper
first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the
same duality of the original dual calculus, it has the duality of inductive and coinductive types, that is,
the duality of terms and coterms for inductive and coinductive types, and the duality of their reduction
rules. Its strong normalization is also proved, which is shown by translating it into a second-order dual
calculus. The strong normalization of the second-order dual calculus is proved by translating it into
the second-order symmetric lambda calculus. This paper then introduces a call-by-value system and a
call-by-name system of the dual calculus with inductive and coinductive types, and shows the duality
of call-by-value and call-by-name, their Church-Rosser properties, and their strong normalization.
Their strong normalization is proved by translating them into the non-deterministic dual calculus
with inductive and coinductive types.

1. Introduction
Dual Calculus DC given by Wadler [27, 28] is a type system which corresponds to the classical
sequent calculus LK (see, for example, [7]). It represents computation induced by cut elimination
in LK by using its expressions and their reduction. The dual calculus has two nice properties:
computation in classical logic, and duality.
The computation of classical logic has been intensively studied, for example, [2, 4, 8, 9, 20,
21, 23, 27, 28]. They all studied the Curry-Howard correspondence between classical logic and
functional programming languages with sophisticated control structures like catch/throw and firstclass continuations. This correspondence is an extension of the Curry-Howard correspondence
between intuitionistic logic and the typed λ-calculus, which is well established.
The classical sequent calculus LK has nice duality. We have an involution that maps conjunction and disjunction to each other, and maps the left and right rules of conjunction to the right
and left rules of disjunction and vice versa. This involution can be extended to the cut elimination
procedure for LK.
The system DC inherits the duality of the classical sequent calculus LK. Moreover, its proof
terms called terms, coterms, and statements also have duality, since they correspond to proofs in
2012 ACM CCS: [Theory of computation]: Models of computation—Computability—Lambda calculus.
Key words and phrases: Curry-Howard isomorphism, Classical logic, Dual Calculus, Inductive definitions, Coinductive definitions.
∗
The conference version of this paper has appeared in [13].

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-9(1:14)2013

CC

D. Kimura and M. Tatsuta
Creative Commons

2

D. KIMURA AND M. TATSUTA

LK. This implies that its reduction relation can have duality since the reduction relation is induced
by the cut elimination procedure in LK. In this framework, Wadler gave the call-by-value and callby-name strategies in DC, and showed the duality of them [27]. He also showed that the equational
correspondence between DC and Parigot’s λµ-calculus [19], and showed the duality between callby-value and call-by-name of the λµ-calculus using the duality of the dual calculus [28]. Since then,
the dual calculus has been actively studied [26, 12, 13].
Inductive definitions are important in both mathematical logic and computer science. Inductive
definitions strengthen expressiveness of logical systems (for example, See [3]). They are central in
programming and program verification [22, 18, 14] for handling recursive data structures such as
lists and trees, and specification of recursive programs. Coinductive definitions are also important
since they can represent streams, infinite trees, and bisimulation, for example, in [24].
This paper presents Dual Calculus DCµν with inductive types and coinductive types. Our calculus extends the duality of DC to inductive types and coinductive types. The involution in DC is
extended so that it maps inductive types and coinductive types to each other. It also maps the left
and right rules of inductive types to the right and left rules of coinductive types and vice versa. Because of the duality of the proof rules, we will have cut elimination procedure that keeps the duality
of inductive types and coinductive types. This induces the duality of the reduction relations of proof
terms for inductive types and coinductive types.
Our main results are: (1) the duality between inductive types and coinductive types with reduction, (2) strong normalization in DCµν, (3) strong normalization in the second-order Dual Calculus
DC2, (4) the duality between the call-by-value and call-by-name DCµν, and (5) the Church-Rosser
property and strong normalization of the call-by-value and call-by-name DCµν.
We will show strong normalization of DCµν. In order for proving the strong normalization, we
will first show the strong normalization of the second-order Dual Calculus DC2 given by [26] by
interpreting it in second-order symmetric lambda-calculus given in [21]. Then strong normalization
of DCµν is proved by interpreting it in DC2 by using second-order coding of inductive and coinductive
types.
We first introduce the system DCµν that does not have reduction strategies, since it is designed
by the Curry-Howard correspondence for a standard cut elimination procedure in LK. The system
can discuss non-deterministic aspects of computation in classical logic, since the execution of programs in DCµν is non-deterministic. It also works as a base framework for other variants of DCµν
with specific reduction strategies such as call-by-value and call-by-name that will be given later.
The duality between call-by-value and call-by-name is first suggested by Filinski [5]. The dual
calculus gives a clear explanation for this duality by using the logical duality of classical logic. We
will show the duality of call-by-value and call-by-name in the dual calculus extended with inductive
types and coinductive types. We extend the call-by-value DC and the call-by-name DC given in [27]
with inductive types and coinductive types, and introduce the systems CBV DCµν and CBN DCµν. They
are obtained from DCµν by restricting its non-deterministic reduction to the call-by-value or call-byname strategies, and also by adding some strategy-specific reduction rules. In the same way as [27],
we show the duality of call-by-value and call-by-name in the dual calculus with inductive types
and coinductive types. We will show the Church-Rosser property as well as strong normalization
for CBV DCµν and CBN DCµν. The strong normalization will be shown by translating CBV DCµν and
CBN DCµν into DCµν.
In [1], the duality between inductive types and coinductive types in linear logic is studied. Our
system DCµν shows the duality in ordinary sequent calculus LK.
Momigliano and Tiu [16, 17] discussed an intuitionistic sequent calculus with inductive definitions and coinductive definitions and showed its cut elimination theorem. Our system DCµν is

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

3

a classical system and our strong normalization shows the cut elimination theorem of the classical
sequent calculus. Our cut elimination procedure is not closed in an intuitionistic fragment because
it keeps the duality and we have the corresponding proof rule that manipulates a succedent if we
have some proof rule that manipulates an antecedent. So we cannot directly compare our method
and their method.
In category theory, inductive definitions are represented by initial algebras and coinductive
definitions are represented by final coalgebras [6], and their duality in category theory is known.
Our system DCµν enables us to show the duality in a clear syntactic way by using a type system.
Several papers for dual calculus investigated the duality of computation. Wadler showed the
duality between values and continuations, and the duality between call-by-value computation and
call-by-name computation by using the explicit duality of DC [27, 28]. The first author of this paper showed the duality between the call-by-name fixed point operator and the call-by-value loop
operator by extending DC [11]. The first author also showed the duality of reduction between callby-value computation and call-by-name computation in λµ-calculus by using DC [12] to answer the
open question presented in Wadler’s invited talk at RTA2005 [28], which asked whether the duality between call-by-value and call-by-name in his equation systems would be refined in reduction
systems. Tzevelekos [26] investigated the dual calculus given in [27]. He assumed some additional
conditions on reductions, and showed both Church-Rosser property and strong normalization hold
under his conditions. He also investigated the relationship between DC and the symmetric λ-calculus
by Barbanera and Berardi [2]. A second-order extension of DC is also considered in [26].
The system µ̄µ̃ in [4] is a system with implication and subtraction, and also has duality. Their
calculus with negation, conjunction, and disjunction is called µµ̃∧a ∨a ¬ and the correspondence between it and the dual calculus is discussed in [9].
A semantical approach to the duality between call-by-value and call-by-name was studied by
Selinger [23]. He gave a categorical semantics of the λµ-calculus, and explained the duality by using
the categorical duality. This approach is extended to the duality between the fixed point operator
and the loop operator by Kakutani [10].
Section 2 gives a definition of DC and states its duality. Section 3 introduces DCµν and shows
its duality. Section 4 gives examples. In section 5, we give DC2 and show its strong normalization.
Section 6 proves strong normalization for DCµν. Section 7 introduces CBV DCµν and CBN DCµν and
shows their Church-Rosser properties and strong normalization.
2. The Dual Calculus DC
This section defines Dual Calculus DC and states its duality. This system is obtained from the original
Dual Calculus given in [27] by removing reduction strategies in reduction rules. This system gives
us a base framework for several variants of dual calculi.
Definition 2.1 (Types and Expressions of DC). Let X, Y, Z, . . . range over type variables, A, B, . . .
range over types, The symbols x, y, z, . . . range over variables, and α, β, γ, . . . range over covariables.
We assume an involution (−)′ between variables and covariables, which satisfies x′′ = x and α′′ = α.
An expression (denoted by D, E, . . .) is either a term (denoted by M, N, . . .), a coterm (denoted by
K, L, . . .), or a statement (denoted by S , T, . . .). We define them as follows:
Types
A F X | A ∧ A | A ∨ A | ¬A,
Expressions D F M | K | S ,
Terms
M F x | hM, Mi | hMiinl | hMiinr | [K]not | (S ).α,
Coterms
K F α | [K, K] | fst[K] | snd[K] | nothMi | x.(S ),
Statements S F M • K.

4

D. KIMURA AND M. TATSUTA

The term (S ).α binds the covariable α in S . The coterm x.(S ) binds the variable x in S . We write
FV(D) for the set of free variables in D. We also write FCV(D) for the set of free covariables in
D. We will use [ / ] for substitution. For example, the substitution S [M/x] denotes the statement
obtained from S by replacing x by M.
The type A ∧ B denotes a conjunction, A ∨ B denotes a disjunction, and ¬A denotes a negation.
A variable means an ordinary variable. A covariable means an output port and gets some value after
computation. A term represents an ordinary computation which becomes a value or puts values at
output ports after computation. The term hM, Ni means a pair. The terms hMiinl and hMiinr
mean the left injection and the right injection to a disjoint sum, respectively. When [K]not gets
its input, it gives the input to K and computes K. The term (S ).α is an abstraction of S by α. It
computes S and its value is the value at the output port α. A coterm represents continuation which
puts values at output ports after computation when it gets its input. The coterm [K, L] gets an input
of a disjoint sum. If the input is hMiinl, it gives M to K and computes K. If the input is hMiinr,
it gives M to L and computes L. The coterm fst[K] gets an input of a pair. If the input is hM, Ni,
then it gives M to K and computes K. The coterm snd[K] also gets an input of a pair. If the input is
hM, Ni, then it gives N to K and computes K. The coterm nothMi gets a continuation as its input.
It gives M to the continuation and computes the continuation. The coterm x.(S ) is an abstraction of
S by x. If it gets an input, it puts the input in x and computes S . The statement M • K means the
computation of K with the input M that may put values at output ports.
A typing judgment (denoted by J) of DC takes either the form Γ ⊢ ∆ M : A, the form K : A
Γ ⊢ ∆, or the form Γ S ⊢ ∆, where Γ denotes a context x1 : A1 , . . . , xn : An that is a set of variable
declarations, and ∆ denotes a cocontext α1 : B1 , . . . , αm : Bm that is a set of covariable declarations.
We will call M, K, and S a principal expression in those judgments. The domain of Γ (denoted by
dom(Γ)) is the set of variables {x1 , . . . , xn } if Γ is x1 : A1 , . . . , xn : An . The domain of ∆ (denoted by
dom(∆)) is the set of covariables {α1 , . . . , αm } if ∆ is α1 : B1 , . . . , αm : Bm .
We intuitively explain the typing judgments. There can be other ways of intuitive explanation,
for example, [26]. In order to give an intuitive idea in general, we assume an evaluation strategy
for expressions, and a notion of values for the strategy. For example, when we take call-by-name,
the values will be canonical form, and the computation will be lazy evaluation. The focus | is used
only for denoting which part contains a term, a coterm, or a statement in a judgment, and when we
think the corresponding sequent in ordinary sequent calculus, we will erase it. The typing judgment
x1 : A1 , . . . , xn : An ⊢ α1 : B1 , . . . , αm : Bm M : A means that when each xi has a value of type
Ai , and M is computed, then M returns a value of type A or some αi gets a value of type Bi . The
judgment K : A x1 : A1 , . . . , xn : An ⊢ α1 : B1 , . . . , αm : Bm means that when each xi has a value of
type Ai , an input of type A is given to K, and K is computed, then some αi gets a value of type Bi.
The judgment x1 : A1 , . . . , xn : An S ⊢ α1 : B1 , . . . , αm : Bm means that when each xi has a value of
type Ai and S is computed, then some αi gets a value of type Bi . We sometimes use the symbol ⊢DC
instead of the symbol ⊢ that appears in a judgment in order to explicitly show it is a judgment of DC.
That is, we write Γ ⊢DC ∆ M : A for the judgment Γ ⊢ ∆ M : A. Similarly, we write K : A Γ ⊢DC ∆
and Γ S ⊢DC ∆.
The typing rules are given in Figure 1. If we erase terms, coterms, statements, and the symbol
|, the system becomes logically equivalent to a fragment of classical sequent calculus LK, whose
definition is given in, for example, [7].

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

Γ, x : A ⊢ ∆ x : A

(AxR)

α : A Γ ⊢ ∆, α : A

5

(AxL)

Γ⊢∆ M:A Γ⊢∆ N:B
K:A Γ⊢∆ L:B Γ⊢∆
(∧R)
(∨L)
Γ ⊢ ∆ hM, Ni : A ∧ B
[K, L] : A ∨ B Γ ⊢ ∆
Γ⊢∆ M:A
(∨R1)
Γ ⊢ ∆ hMiinl : A ∨ B

K:A Γ⊢∆
(∧L1)
fst[K] : A ∧ B Γ ⊢ ∆

Γ⊢∆ M:B
(∨R2)
Γ ⊢ ∆ hMiinr : A ∨ B

K:B Γ⊢∆
(∧L2)
snd[K] : A ∧ B Γ ⊢ ∆

K:A Γ⊢∆
(¬R)
Γ ⊢ ∆ [K]not : ¬A

Γ⊢∆ M:A
(¬L)
nothMi : ¬A Γ ⊢ ∆

Γ S ⊢ ∆, α : A
(IR)
Γ ⊢ ∆ (S ).α : A

Γ, x : A S ⊢ ∆
(IL)
x.(S ) : A Γ ⊢ ∆

Γ⊢∆ M:A K:A Γ⊢∆
(Cut)
Γ M•K ⊢∆
Figure 1: Typing rules of DC
Definition 2.2 (Reduction). The reduction relation −→DC is defined as the compatible closure of the
following reduction rules:
(β∧1 )
(β∧2 )
(β∨1 )
(β∨2 )
(β¬)
(βR)
(βL)
(ηR)
(ηL)

hM, Ni • fst[K] −→DC M • K,
hM, Ni • snd[K] −→DC N • K,
hMiinl • [K, L] −→DC M • K,
hMiinr • [K, L] −→DC M • L,
[K]not • nothMi −→DC M • K,
(S ).α • K −→DC S [K/α],
M • x.(S ) −→DC S [M/x],
(M • α).α −→DC M,
x.(x • K) −→DC K,

where x and α are fresh in (ηL) and (ηR), respectively.
The rules (ηR) and (ηL) are necessary to get the results of computation of terms and coterms
from computation of statements inside them. We do not include the η-rules for logical connectives
that are given in [28], since these break the confluence property for call-by-value and call-by-name
systems, which we will study in Section 7. In order to study a base framework, we first consider a
non-deterministic rewriting system that does not commit to either the call-by-name or call-by-value
theory.
The system DC we consider first is obtained from the original dual calculus given in [27] by
omitting evaluation strategies, dropping (ς)-rules that provide strong evaluation under call-by-value
and call-by-name strategies, and replacing (ηL) and (ηR)-expansion rules by (ηL) and (ηR)-reduction
rules.
The role of (ηL) and (ηR)-reduction rules are to simplify logical proofs without changing any
proof structure. In the last section, we also give the call-by-value and call-by-name variants of DCµν.
The role of these rules become clearer in that section since they are necessary to obtain a value as
the result of a computation under some strategy.

6

D. KIMURA AND M. TATSUTA

The type of an expression is preserved by reduction.
Proposition 2.3 (Subject reduction of DC). The following claims hold.
(1) If Γ ⊢DC ∆ M : A and M −→DC N, then Γ ⊢DC ∆ N : A holds.
(2) If K : A Γ ⊢DC ∆ and K −→DC L, then L : A Γ ⊢DC ∆ holds.
(3) If Γ S ⊢DC ∆ and S −→DC T , then Γ T ⊢DC ∆ holds.
This proposition is shown by induction on reduction using the following substitution lemma.
Lemma 2.4 (Substitution lemma). The following claims hold.
(1) Suppose Γ ⊢DC ∆ N : A is derivable. Then we have the following.
(1a) If Γ, x : A ⊢DC ∆ M : B, then Γ ⊢DC ∆ M[N/x] : B,
(1b) if K : B Γ, x : A ⊢DC ∆, then K[N/x] : B Γ ⊢DC ∆, and
(1c) if Γ, x : A S ⊢DC ∆, then Γ S [N/x] ⊢DC ∆.
(2) Suppose L : A Γ ⊢DC ∆ is derivable. Then we have the following.
(2a) If Γ ⊢DC ∆, α : A M : B, then Γ ⊢DC ∆ M[L/α] : B,
(2b) if K : B Γ ⊢DC ∆, α : A, then K[L/α] : B Γ ⊢DC ∆, and
(2c) if Γ S ⊢DC ∆, α : A, then Γ S [L/α] ⊢DC ∆.
Proof. The claims (1a),(1b), and (1c) are shown simultaneously by induction on M, K, and S . The
claims (2a),(2b), and (2c) are also shown simultaneously by induction on M, K, and S .
The following duality transformation extends the duality in the sequent calculus LK to terms,
coterms, and statements.
Definition 2.5 (Duality Transformation). The duality transformation (−)◦ from DC into itself is
defined for types and expressions as follows:
(X)◦ = X, (¬A)◦ = ¬(A)◦ ,
(A ∧ B)◦ = (A)◦ ∨ (B)◦ ,
◦
′
◦
(x) = x ,
(α) = α′ ,
◦
◦
◦
(hM, Ni) = [(M) , (N) ], ([K, L])◦ = h(K)◦ , (L)◦ i,
(hMiinl)◦ = fst[(M)◦ ], (fst[K])◦ = h(K)◦ iinl,
(hMiinr)◦ = snd[(M)◦ ], (snd[K])◦ = h(K)◦ iinr,
([K]not)◦ = noth(K)◦ i, (nothMi)◦ = [(M)◦ ]not,
((S ).α)◦ = α′ .((S )◦ ),
(x.(S ))◦ = ((S )◦ ).x′ ,
◦
◦
◦
(M • K) = (K) • (M) .

(A ∨ B)◦ = (A)◦ ∧ (B)◦ ,

Note that a type and a statement are mapped to themselves. A term and a coterm are mapped to
each other.
We also define transformation for judgments. If Γ is x1 : A1 , . . . , xn : An , then (Γ)◦ is defined as (x1 )◦ : (A1 )◦ , . . . , (xn )◦ : (An )◦ . If ∆ is α1 : B1 , . . . , αm : Bm , then (∆)◦ is defined as
(α1 )◦ : (B1 )◦ , . . . , (αm )◦ : (Bm )◦ . The judgment (Γ ⊢ ∆ M : A)◦ is defined as (M)◦ : (A)◦ (∆)◦ ⊢ (Γ)◦ .
The judgment (K : A Γ ⊢ ∆)◦ is defined as (∆)◦ ⊢ (Γ)◦ (K)◦ : (A)◦ . The judgment (Γ S ⊢ ∆)◦ is
defined as (∆)◦ (S )◦ ⊢ (Γ)◦ .
We also define transformation for inference rule names as follows: (AxR)◦ = (AxL), (AxL)◦ =
(AxR), (∨R1)◦ = (∧L1), (∧L1)◦ = (∨R1), (∧R)◦ = (∨L), (∨L)◦ = (∧R), (∨L2)◦ = (∧R2), (∨R2)◦ =
(∧L2), (¬L)◦ = (¬R), (¬R)◦ = (¬L), (IR)◦ = (IL), (IL)◦ = (IR), and (Cut)◦ = (Cut).
This duality transformation preserves substitution of terms and coterms.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

7

Lemma 2.6. The following claims hold.
(1) (D[M/x])◦ = (D)◦ [(M)◦ /x′ ].
(2) (D[K/α])◦ = (D)◦ [(K)◦ /α′ ].
Proof. The claims (1) and (2) are shown by induction on D. We treat the first case of (1): the case
of D is x. (x[M/x])◦ = (M)◦ = x′ [(M)◦ /x′ ] = (x)◦ [(M)◦ /x′ ]. The other cases are straightforwardly
proved by the induction hypothesis.
This duality transformation is shown to preserve typing and reduction, and to be an involution.
This transformation is a homomorphism for this system in the sense that it preserves typing and
reduction. An important feature of DC is its duality by this transformation. A term is dual to a
coterm by this homomorphism.
Proposition 2.7 (Duality of DC). The followings hold.
(1) If J is derived from J1 , . . . , Jn (n = 1 or 2) by an inference rule R, then (J)◦ is derived from
(Jn )◦ , . . . , (J1 )◦ by the inference rule (R)◦ .
(2) D −→DC E implies (D)◦ −→DC (E)◦ .
(3) ((A)◦ )◦ = A, ((D)◦ )◦ = D, and ((J)◦ )◦ = J hold.
Proof. The claim (1) is proved by case analysis of the inference rules. The claim (2) is proved by
induction on the generation of −→DC using Lemma 2.6. The claim (3) is proved by induction on
types and expressions.
Remark 2.8. The (−)◦ transformation maps dual reduction rules to each other. That is, if D −→DC E
is the reduction rules (β∧1 ), (β∧2 ), (β∨1 ), (β∨2 ), (β¬), (βR), (βL), (ηR), and (ηL), then (D)◦ −→DC
(E)◦ is the reduction rules (β∨1 ), (β∨2 ), (β∧1 ), (β∧2 ), (β¬), (βL), (βR), (ηL), and (ηR), respectively.
Implication ⊃ can be defined by ¬ and ∨ in the same way as [27].
Definition 2.9. We write A ⊃ B for ¬A∨B. We also write λx.M for (h[x.(hMiinr•γ)]notiinl•γ).γ.
We also write N@K for [nothNi, K].
The constructor @ simulates the application in λ-calculus together with •. The following holds
from the definition.
Proposition 2.10. The following typing inference rules and reduction rule are derivable.
Γ⊢∆ M:A K:B Γ⊢∆
Γ, x : A ⊢ ∆ M : B
(⊃ R)
(⊃ L)
Γ ⊢ ∆ λx.M : A ⊃ B
M@K : A ⊃ B Γ ⊢ ∆
(β ⊃) λx.M • (N@K) −→DC M[N/x] • K

3. The Dual Calculus DCµν with Inductive and Coinductive Types
In this section, we present DCµν, which is an extension of DC with inductive types and coinductive
types. We first extend the definition of types of DC to inductive types µX.A and coinductive types
νX.A, and then extend expressions and reduction.
In Section 5, we will introduce the second-order system DC2. The system DCµν is worth to be
studied as well as DC2, since DCµν is within a first-order logic.
We first define types, their positive type variables, and their negative type variables. A positive
type variable in a type does not occur negatively in the type in the usual sense. A negative type
variable in a type does not occur positively in the type.

8

D. KIMURA AND M. TATSUTA

Definition 3.1. The set of type variables is written by TyVars. We define the types of DCµν (denoted
by A, B, . . .) and the set Pos(A) of positive type variables in the type A and the set Neg(A) of negative
type variables in the type A as follows:
A F X | A ∧ A | A ∨ A | ¬A | µX.A | νX.A
where µX.A and νX.A are defined when the type variable X is in Pos(A).
Pos(X) = TyVars,
Neg(X) = TyVars \ {X},
Pos(A1 ∧ A2 ) = Pos(A1 ∨ A2 ) = Pos(A1 ) ∩ Pos(A2 ),
Neg(A1 ∧ A2 ) = Neg(A1 ∨ A2 ) = Neg(A1 ) ∩ Neg(A2 ),
Pos(¬B) = Neg(B),
Neg(¬B) = Pos(B),
Pos(µX.B) = Pos(νX.B) = Pos(B) ∪ {X},
Neg(µX.B) = Neg(νX.B) = Neg(B) ∪ {X}.
The types µX.A and νX.A bind X in A.
When we think standard semantics of the propositional logic with inductive and coinductive
definitions, µX.A and νX.A are interpreted by the least fixed point and the greatest fixed point of the
monotone function P respectively, where P is the function which maps a set U to the set A[U/X].
Let µ be µX.A and ν be νX.A. They will have the following properties: (a) A[µ/X] ⊆ µ, (b) A[B/X] ⊆
B implies µ ⊆ B, (c) ν ⊆ A[ν/X], and (d) B ⊆ A[B/X] implies B ⊆ ν. Based on this meaning, we
will introduce terms, coterms, and their reduction for inductive and coinductive types in the same
way as [15].
Definition 3.2. The terms, coterms, and statements of DCµν are defined as follows:
M F x | hM, Mi | hMiinl | hMiinr | [K]not | (S ).α | inµX.AhMi | coitrAx hM, Mi,
K F α | [K, K] | fst[K] | snd[K] | nothMi | x.(S ) | outνX.A[K] | itrαA [K, K],
S F M • K.
The term itrαA [K, L] binds α in K. The coterm coitrAx hM, Ni binds x in M.
The expressions inµX.AhMi and itrαA [K, L] are the expressions for inductive types. The constructor inµX.A maps a term of type A[µX.A/X] to that of µX.A. The coterm itrαB [K, L] is an iterator
having an input of type µX.A where L is a postprocessor after iteration. When it gets the input of
type µX.A, first a value of type A[µX.A/X] is computed according to the input, next a value of type
A[B/X] is computed by recursive invocation of the iterator, then it is given to K and K is computed
to get a value of type B, and finally the value is given to L and L is computed. Dually, outνX.A [K]
and coitrAx hM, Ni are defined for coinductive types. The constructor outνX.A maps a coterm of
type νX.A to that of A[νX.A/X]. When the coterm outνX.A [K] gets the input of type νX.A, first the
input is transformed into a value of type A[νX.A/X], then the value is given to K, and finally K is
computed. The term coitrBx hM, Ni is a coiterator of type νX.A. It transforms N of type B into a
value of νX.A according to M. Type annotations will be necessary for defining reduction rules.
Definition 3.3. The typing rules of DCµν are defined by those of DC and the following rules:
Γ ⊢ ∆ M : A[µX.A/X]
(µR)
Γ ⊢ ∆ inµX.AhMi : µX.A

K : A[B/X] Γ ⊢ ∆, α : B L : B Γ ⊢ ∆
(µL)
itrαB [K, L] : µX.A Γ ⊢ ∆

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

K : A[νX.A/X] Γ ⊢ ∆
(νL)
outνX.A[K] : νX.A Γ ⊢ ∆

9

Γ, x : B ⊢ ∆ M : A[B/X] Γ ⊢ ∆ N : B
(νR)
Γ ⊢ ∆ coitrBx hM, Ni : νX.A

We sometimes use the symbol ⊢DCµν instead of the symbol ⊢ in a judgment in order to explicitly
show it is a judgment of DCµν. That is, we write Γ ⊢DCµν ∆ M : A for the judgment Γ ⊢ ∆ M : A.
Similarly, we write K : A Γ ⊢DCµν ∆ and Γ S ⊢DCµν ∆.
The system DCµν satisfies the following basic lemmas.
Lemma 3.4 (Weakening lemma of DCµν). Let Γ ⊆ Γ′ and ∆ ⊆ ∆′ . Then
(1) if Γ ⊢DCµν ∆ M : A is provable, then Γ′ ⊢DCµν ∆′ M : A holds,
(2) if K : A Γ ⊢DCµν ∆ is provable, then K : A Γ′ ⊢DCµν ∆′ holds, and
(3) if Γ S ⊢DCµν ∆ is provable, then Γ′ S ⊢DCµν ∆′ holds.
Proof. They are shown simultaneously by induction on M, K, and S .
Lemma 3.5. Let Γ′ ⊆ Γ and ∆′ ⊆ ∆. Then the following claims hold in DCµν.
(1) If FV(M) ⊆ dom(Γ′ ) and FCV(M) ⊆ dom(∆′ ), then Γ ⊢ ∆ M : A implies Γ′ ⊢ ∆′ M : A.
(2) If FV(K) ⊆ dom(Γ′ ) and FCV(K) ⊆ dom(∆′ ), then K : A Γ ⊢ ∆ implies K : A Γ′ ⊢ ∆′ .
(3) If FV(S ) ⊆ dom(Γ′ ) and FCV(S ) ⊆ dom(∆′ ), then Γ | S ⊢ ∆ implies Γ′ | S ⊢ ∆′ .
Proof. They are shown simultaneously by induction on M, K, and S .
Lemma 3.6 (Substitution lemma of DCµν). The following claims hold.
(1) Suppose Γ ⊢DCµν ∆ N : A is derivable. Then the following hold.
(1a) If Γ, x : A ⊢DCµν ∆ M : B, then Γ ⊢DCµν ∆ M[N/x] : B,
(1b) if K : B Γ, x : A ⊢DCµν ∆, then K[N/x] : B Γ ⊢DCµν ∆, and
(1c) if Γ, x : A S ⊢DCµν ∆, then Γ S [N/x] ⊢DCµν ∆.
(2) Suppose L : A Γ ⊢DCµν ∆ is derivable. Then the following hold.
(2a) If Γ ⊢DCµν ∆, α : A M : B, then Γ ⊢DCµν ∆ M[L/α] : B,
(2b) if K : B Γ ⊢DCµν ∆, α : A, then K[L/α] : B Γ ⊢DCµν ∆, and
(2c) if Γ S ⊢DCµν ∆, α : A, then Γ S [L/α] ⊢DCµν ∆.
Proof. The claims (1a), (1b), and (1c) are shown simultaneously by induction on M, K, and S . The
claims (2a), (2b), and (2c) are also shown simultaneously by induction on M, K, and S .
The duality transformation can be extended from DC to DCµν.
Definition 3.7 (Duality Transformation). The duality transformation for types, terms, coterms,
statements, and inference rule names of DCµν is defined by those of DC and the following equations:
(µX.A)◦ = νX.(A)◦ ,

(νX.A)◦ = µX.(A)◦ .
◦

(inµX.AhMi)◦ = outνX.(A) [(M)◦ ],
◦
(outνX.A[K])◦ = inµX.(A) h(K)◦ i,
◦
◦ , (L)◦ i,
(itrαA [K, L])◦ = coitr(A)
α′ h(K)
(A)◦
A
◦
(coitrx hM, Ni) = itrx′ [(M)◦ , (N)◦ ].
(µR)◦ = (νL),
(νL)◦ = (µR),
(µL)◦ = (νR),
The above duality transformation is well-defined.

(νR)◦ = (µL).

10

D. KIMURA AND M. TATSUTA

Lemma 3.8. The type (A)◦ is defined, and Pos(A) = Pos((A)◦ ) and Neg(A) = Neg((A)◦ ) hold.
Proof. These claims are shown by induction on A. We consider the cases of µX.B and νX.B. The
other cases are straightforwardly proved by the induction hypothesis.
The case of µX.B: Suppose that µX.B is defined. Then we have X is in Pos(B). By the induction
hypothesis, (B)◦ is defined and X occurs positively in (B)◦ . Therefore νX.(B)◦ is defined, and we
have Pos(µX.B) = Pos(νX.(B)◦ ) and Neg(µX.B) = Neg(νX.(B)◦ ) by the induction hypothesis.
The case of νX.B can be shown in the similar way to the case of µX.B.
This duality transformation alternates free variables and free covariables that occur in terms
and coterms. Let V be a set of variables, and C be a set of covariables. Then a set of covariables
(V)◦ is defined by {x′ | x ∈ V}. A set of variables (C)◦ is also defined by {α′ | α ∈ C}.
Lemma 3.9. Let D be an expression of DCµν. Then FV((D)◦ ) = (FCV(D))◦ and FCV((D)◦ ) =
(FV(D))◦ hold.
Proof. The claims are shown by induction on D.
This duality transformation preserves substitution of types, terms, and coterms.
Lemma 3.10. Let A and B be types, D be an expression, M be a term, and K be a coterm of DCµν.
Then the following hold.
(1) (A[B/X])◦ = (A)◦ [(B)◦ /X].
(2) (D[M/x])◦ = (D)◦ [(M)◦ /x′ ].
(3) (D[K/α])◦ = (D)◦ [(K)◦ /α′ ].
Proof. The claim (1) is shown by induction on A. The claims (2) and (3) are shown by induction on
D.
The extended duality transformation preserves typing, and is an involution in DCµν.
Proposition 3.11. The following claims hold.
(1) If J is derived from J1 , . . . , Jn (n = 1 or 2) by an inference rule R, then (J)◦ is derived from
(Jn )◦ , . . . , (J1 )◦ by the inference rule (R)◦ .
(2) ((A)◦ )◦ = A, ((D)◦ )◦ = D, and ((J)◦ )◦ = J hold for any type A, expression D, and judgment J of
DCµν.
Proof. The claim (1) is shown by case analysis of the inference rules of DCµν using Lemma 3.10
(1). The claim (2) is shown by induction on types and expressions.
Our reduction rules for inductive and coinductive types will be defined so that they correspond
to cut elimination procedures in the classical sequent calculus LK extended with inductive definitions and coinductive definitions. In the following proof figures, we will write µ, ν, and A[B] for
µX.A, νX.A, and A[B/X] respectively. In the logical system, when the cut formula is an inductive
type, the cut elimination procedure reduces the proof
..
..
..
..
..
..
Γ ⊢ ∆, A[µ]
A[B], Γ ⊢ ∆, B B, Γ ⊢ ∆
(µR)
(µL)
Γ ⊢ ∆, µ
µ, Γ ⊢ ∆
(Cut)
Γ⊢∆

to the proof

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

..
..
Γ ⊢ ∆, A[µ]
(Wk)
Γ ⊢ ∆, B, A[µ]

..
..
..
..
A[B], Γ ⊢ ∆, B B, Γ ⊢ ∆, B
(µL)
A[B], Γ ⊢ ∆, B
µ, Γ ⊢ ∆, B
(mono)
A[µ], Γ ⊢ ∆, B
(Cut)
Γ ⊢ ∆, B
Γ⊢∆

..
..
B, Γ ⊢ ∆

11

(Cut)

We can intuitively understand the rule (mono) as follows: µ ⊢ B implies A[µ] ⊢ A[B], so we have
A[µ] ⊢ B by combining it with A[B] ⊢ B. This rule will be formally shown in Lemma 3.14 (2a).
This reduction changes the cut formula from µ to A[µ]. We do not have to count the cut formula B,
since that cut is auxiliary. When the cut formula is a coinductive type, the cut elimination procedure
reduces a proof in a dual way to the above reduction.
When we have a function λx.M from A to B and the variable X is in Pos(C), we can define
the function from C[A/X] to C[B/X] by extending λx.M. We will use monoX.C
A,B,x.M {N} so that this
X.C
X.C
function maps z to monoA,B,x.M {z}. We will define monoA,B,x.M {N} by induction on the measure ||C||X
for a type C and a type variable X, which is defined by induction on C as follows: If X is not free in
A, then ||A||X = 0. In the other cases, we assume that some X occurs in A and we define
||X||X = 1,
||A ∧ B||X = ||A ∨ B||X = ||A||X + ||B||X + 1,
||¬A||X = ||A||X + 1,
||µY.A||X = ||νY.A||X = ||A||X + ||A||Y + 1.
Note that if X is not free in B and we have X , Y, then k A kX = k A[B/Y] kX .
The number ||A||X will also be used for evaluating the size of monoX.C
A,B,x.M {N} by using M, N,
and C (see Lemma 6.2). If we replaced ||A||X + ||A||Y + 1 by ||A||X + 1 in the definition of ||µY.A||X
and ||νY.A||X , it would not work for this purpose.
Definition 3.12. Assume a type variable X and types A, B, C are given and X is not free in A and B.
For a variable x and terms M and N, we define the term monoX.C
A,B,x.M {N} by induction on k C kX as
follows:
monoX.X
A,B,x.M {N} = (N • x.(M • α)).α,
monoX.C
A,B,x.M {N} = N

(X does not occur in C),

X.C
X.D
monoX.C∧D
A,B,x.M {N} = h monoA,B,x.M {(N • fst[α]).α}, monoA,B,x.M {(N • snd[β]).β} i,
X.C
X.D
monoX.C∨D
A,B,x.M {N} = (N • [ y.(hmono A,B,x.M {y} iinl • γ), z.(hmono A,B,x.M {z} iinr • γ) ]).γ,
X.¬C
monoA,B,x.M
{N} = [ z.(N • noth monoX.C
B,A,x.M {z} i ) ]not,
X.µY.C
monoA,B,x.M
{N} = ( N • itrαµY.C[B/X] [ z.( inµY.C[B/X] h monoX.C[µY.C[B/X]/Y]
{ z } i • α ), β ] ).β,
A,B,x.M
X.νY.C
{ (z • outνY.C[A/X] [α]).α }, N i.
monoA,B,x.M
{N} = coitrzνY.C[A/X] h monoX.C[νY.C[A/X]/Y]
A,B,x.M

For a covariable α and coterms K and L, we also define
◦

X.(C)
◦ ◦
monoX.C
A,B,α.K {L} = (mono(B)◦ ,(A)◦ ,α′ .(K)◦ {(L) }) .

Note that ||µY.C||X > ||C[µY.C[B/X]/Y]||X and ||νY.C||X > ||C[νY.C[A/X]/Y]||X hold since X is
not free in µY.C[B/X] and νY.C[A/X]. We cannot replace C[µY.C[B/X]/Y] by C in the definiX.µY.C
tion of monoA,B,x.M {N} because of the type annotation for in. For readability, we sometimes write
X.C
X.C
X.C
monoX.C
A,B,x {M, N} and monoA,B,α{K, L} for monoA,B,x.M {N} and monoA,B,α.K {L}, respectively.

12

D. KIMURA AND M. TATSUTA

The paper [17] studied an intuitionistic logical system with strictly-positive inductive definitions, and on the other hand we study a classical logical system with positive inductive definitions.
Our cut elimination for inductive types is the same as theirs, and on the other hand our cut elimination for coinductive types is different from theirs. They can avoid the use of mono. However, we
cannot straightforwardly compare our method and their method, since our system is strictly larger
than their system.
Our method works only for classical logic and does not work for an intuitionistic logic. This
is because our cut elimination procedure keeps the duality and we have the corresponding proof
rule that manipulates a succedent if we have some proof rule that manipulates an antecedent. In
particular, we define the operator mono for coterms as the dual of the operator mono for terms.
Roughly speaking, in the proof of the next lemma, when we show the properties of mono for negation
by using the derivation
A⊢B
A, ¬B ⊢
¬B ⊢ ¬A,
we need the following derivation in order to show the properties of its dual:
B⊢A
⊢ A, ¬B
¬A ⊢ ¬B
which uses a non-intuitionistic sequent.
Lemma 3.13. The following claims hold.
(1a) FV(monoX.C
A,B,x {M, N}) ⊆ (FV(M) \ {x}) ∪ FV(N).
X.C {M, N}) ⊆ FCV(M) ∪ FCV(N).
(1b) FCV(monoA,B,x

(2a) FV(monoX.C
A,B,α{K, L}) ⊆ FV(K) ∪ FV(L).
(2b) FCV(monoX.C
A,B,α{K, L}) ⊆ (FCV(K) \ {α}) ∪ FCV(L).
Proof. The claims (1a) and (1b) are shown by induction on k C kX . The claims (2a) and (2b) are
shown by using (1a), (2b), and Lemma 3.9.
Lemma 3.14. Assume X is in Pos(C) and Neg(D). Then the following hold:
(1a) Γ, x : A ⊢ ∆ | M : B and Γ ⊢ ∆ | N : C[A] implies Γ ⊢ ∆ | monoX.C
A,B,x.M {N} : C[B],
(1b) Γ, x : B ⊢ ∆ M : A and Γ ⊢ ∆ N : D[A] implies Γ ⊢ ∆ monoX.D
A,B,x.M {N} : D[B],
(2a) K : A Γ ⊢ ∆, α : B and L : C[B] Γ ⊢ ∆ implies monoX.C
A,B,α.K {L} : C[A] Γ ⊢ ∆,
(2b) K : B Γ ⊢ ∆, α : A and L : D[B] Γ ⊢ ∆, implies monoX.D
A,B,α.K {L} : C[A] Γ ⊢ ∆,
where C[A] and D[A] are abbreviations of C[A/X] and D[A/X], respectively.
Proof. The claims (1a) and (1b) are shown simultaneously by induction on ||C||X and ||D||X . The
claims (2a) and (2b) are shown by using (1a), (1b), and Proposition 3.11.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

13

The following proposition is obtained as a special case of the above lemma.
Proposition 3.15. Assume X is in Pos(C). The following are derivable:
Γ, x : A ⊢ ∆ | M : B
K : A Γ ⊢ ∆, α : B
X.C
X.C
Γ, z : C[A] ⊢ ∆ | monoA,B,x.M {z} : C[B]
monoA,B,α.K {β} : C[A] Γ ⊢ ∆, β : C[B]
Definition 3.16. We define the one-step reduction relation −→DCµν of DCµν as the compatible closure
of the reduction rules of DC and the following reduction rules:
X.C
(βµ) inµX.C hMi • itrαA [K, L] −→DCµν (M • monoµX.C,A,β
{ itrαA [K, β], K }).α • L,
A
(βν) coitrAx hM, Ni • outνX.C [K] −→DCµν N • x.(monoX.C
A,νX.C,z { coitrx hM, zi, M } • K).

This system has subject reduction.
Proposition 3.17 (Subject reduction of DCµν). The following claims hold.
(1) If Γ ⊢DCµν ∆ M : A and M −→DCµν N, then Γ ⊢DCµν ∆ N : A holds.
(2) If K : A Γ ⊢DCµν ∆ and K −→DCµν L, then L : A Γ ⊢DCµν ∆ holds.
(3) If Γ S ⊢DCµν ∆ and S −→DCµν T , then Γ T ⊢DCµν ∆ holds.
Proof. They are shown simultaneously by induction on the generation of −→DCµν using Lemma 3.4,
3.5, 3.6, and 3.14. We consider the cases of (βµ) and (βν).
Case of (βµ). Assume Γ inµX.C hMi • itrαA [K, L] ⊢ ∆ is derivable in DCµν. We use µ and C[A]
as abbreviations of µX.C and C[A/X], respectively. The last rule of the derivation must be (Cut)
rule. Then Γ ⊢ ∆ inµX.C hMi : D and itrαA [K, L] : D Γ ⊢ ∆ are derivable for some type D. Since
the last rules of these derivations must be (µR) and (µL), we obtain D is µX.C, and the derivations
of Γ ⊢ ∆ M : C[µ], the judgment K : C[A] Γ ⊢ ∆, α : B, and L : A Γ ⊢ ∆, α : B. Hence we have
X.C { itrA [K, β], K } : C[µ] Γ ⊢
itrαA [K, β] : µ Γ ⊢ ∆, β : A by (AxL) and (µL) rules, and then monoµ,A,β
α
X.C
{ itrαA [K, β], K }).α•L ⊢ ∆
∆, α : A is derivable by Lemma 3.14. Therefore we have Γ (M•monoµ,A,β
by using (IR), (Cut) rules.
The case of (βν) is shown similarly to the case of (βµ).
The other cases are straightforwardly proved by the induction hypothesis.
The duality transformation (−)◦ preserves reduction.
Theorem 3.18 (Duality of DCµν). D −→DCµν E implies (D)◦ −→DCµν (E)◦ for any expressions D
and E.
Proof. This is proved by induction on the generation of −→DCµν .
Proposition 3.19. If D −→DCµν E is the rules (βµ) and (βν), then (D)◦ −→DCµν (E)◦ is (βν) and (βµ)
respectively.
We have shown the duality of inductive types and coinductive types. Proposition 3.11 and
Theorem 3.18 show that the duality transformation is a homomorphic involution. The description
of a type can be defined as the set of the type itself, its terms, its coterms, and their reduction. The
duality transformation maps the description of an inductive type and that of a coinductive type to
each other. That is, we have the following. (1) Definition 3.7 shows that the inductive type µX.A is
mapped to the coinductive type νX.(A)◦ , the term constructed by in for the inductive type is mapped
to the coterm constructed by out for the coinductive type, and the coterm constructed by itr for the
inductive type is mapped to the term constructed by coitr for the coinductive type. (2) Proposition
3.19 shows that the cut elimination procedure of the inductive type is mapped to the cut elimination
procedure of the coinductive type. (3) the coinductive type is mapped to the inductive type in a
similar way to (1) and (2).

14

D. KIMURA AND M. TATSUTA

Remark 3.20. We cannot define our typing system by using
K : C[A/X] Γ ⊢ ∆, α : A
(µL′ )
itrαA [K, β] : µX.C Γ ⊢ ∆, β : A
instead of the typing rule (µL). If we used (µL′ ), the set of terms would not be closed under substitution, because itrαA [K, L] would not have typing rules for it and hence it would not be a term,
though it is obtained from itrαA [K, β] by substituting L for β.
4. Examples
In this section we show some examples of inductive and coinductive types in DCµν. Let X0 be a
distinguished type variable. We use the following abbreviations:
⊤ = ¬X0 ∨ X0 ,

⊥ = ¬X0 ∧ X0 ,

and

∗ = λx.x.

The type Nat of natural numbers can be represented by:
Nat = µX.(⊤ ∨ X),
0 = inNat h h∗iinl i,
succhMi = inNat h hMiinr i,
where 0 is the zero and succ is the successor. We can prove Γ ⊢ ∆ 0 : Nat. We can also
prove Γ ⊢ ∆ succhMi : Nat from Γ ⊢ ∆ M : Nat. The n-th natural number ñ is represented by succhsucch. . . succh0i . . .ii (n times of succ). We will write M[ /x]n (N) for
M[M[. . . [M[N/x]/x] . . . /x]/x] (n times of M). We define a coterm ItrB [F, N, K] of type Nat by


itrαB [y.(N • α), x.(F • (x@α))], K , where y is not free in N, the term F has type B ⊃ B, and N and
K are of type B. When the coterm ItrB [F, N, K] gets ñ as its input, it computes n-time iterations
of applying the function F to N, and passes the output to K. This reduces ñ • ItrB [λx.M, N, K] to
M[ /x]n (N) • K.
The type List(A) of lists of elements of type A is represented by:
List(A) = µX.(⊤ ∨ (A ∧ X)),
nil = inList(A) h h∗iinl i,
M :: Nl = inList(A) h h hM, Nli iinr i.
The term nil is the empty list and (::) is the list constructor. In DCµν, the judgment Γ ⊢
∆ nil : List(A) is provable. The judgment Γ ⊢ ∆ M :: Nl : List(A) is also provable from
Γ ⊢ ∆ M : A and Γ ⊢ ∆ Nl : List(A).
We note that the above examples can be considered under the call-by-value setting (section 7)
if we restrict terms in the above examples to values.
We can also define the type Stream(A) of streams of elements of type A by:
Stream(A) = νX.(A ∧ X),
h hπ1 (x), (π2 (x) • outStream(A) [α]).αi, hM, Nsi i,
conshM, Nsi = coitrA∧Stream(A)
x
hd[K] = outStream(A) [ fst[K] ],
tl[L] = outStream(A) [ snd[L] ],
where π1 (M) is the first projection of M defined by (M • fst[α]).α, and π2 (M) is the second projection of M defined by (M • snd[α]).α. The term conshM, Nsi constructs a new stream from a

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

15

given element M and a given stream Ns. The coterm hd[K] receives the first element from a given
stream and gives it to K. The coterm tl[L] removes the first element from a given stream and gives
the resulting stream to L. We can prove Γ ⊢ ∆ conshM, Nsi : Stream(A) from Γ ⊢ ∆ M : A and
Γ ⊢ ∆ Ns : Stream(A). We can also prove hd[K] : Stream(A) Γ ⊢ ∆ from K : A Γ ⊢ ∆. We can
also prove tl[L] : Stream(A) Γ ⊢ ∆ from L : Stream(A) Γ ⊢ ∆. This reduces conshM, Nsi•hd[K]
to M • K. We also reduce conshM, Nsi • tln+1 [hd[K]] to Ns • tln [hd[K]], where tln [hd[K]] is
defined by tl[tl[. . . tl[ hd[K] ] . . .]] (n times of tl). Hence the coterm tln [hd[K]] receives the
n-th element of a given stream and gives it to K. Let M be a term of type A. The stream of infinite number of M is represented by coitr⊤x hhM, xi, ∗i, where x is a fresh variable. We will write
stream(M) for coitr⊤x hhM, xi, ∗i. Indeed, the statement stream(M) • tln [hd[K]] is reduced to M
for any n. This means that any n-th element of stream(M) is M.
We note that this stream example can be considered under the call-by-name setting (section 7)
if we restrict coterms in the above example to covalues.
Proposition 4.1. Nat is dual to Stream(⊥), that is, (Nat)◦ = Stream(⊥), (0)◦ = hd[(∗)◦ ], and
(succhMi)◦ = tl[(M)◦ ] hold.
If Stream(⊥) is considered under the call-by-name setting and Nat is considered under the callby-value setting, then the duality of the above proposition can be understood as follows. The type ⊤
means the singleton set {∗}. The type ⊥ means the type of a program that returns some answer after
computation with the input ∗ since ⊥ is equivalent to ¬⊤. The type Nat means the infinite disjoint
sum ⊤ + ⊤ + ⊤ + . . .. The type Stream(⊥) means the infinite cartesian product ⊥ × ⊥ × ⊥ × . . .. Since
a term in Stream(⊥) is equivalent to a coterm in Nat, when the term gets some natural number and
is computed, it returns some answer. When the term gets the natural number ñ, since ñ is ∗ in the
n-th ⊤ in ⊤ + ⊤ + . . ., the term in the n-th ⊥ in ⊥ × ⊥ × . . . is given the input ∗ and it is computed to
give some answer.
Here we can also consider examples that include non-deterministic choices. Let M and N
be terms of same type, x be a fresh variable, α and β be fresh covariables. We define the nondeterministic choice hM | Ni by
hM | Ni = ((M • α).β • x.(N • α)).α,
where α and β are fresh covariables. This term has both (βL ) and (βR )-redexes. It is reduced to
M if the (βR )-redex is chosen, and is reduced to N if the (βL )-redex is chosen. Thus, hM | Ni
can be considered as a non-deterministic choice of either M or N. This non-deterministic choice
hM | Ni is forced to choose M under the call-by-value strategy, and is forced to choose N under the
call-by-name strategy.
An example of non-deterministic computation is the list insertion function. This function gets a
list as its input data, and non-deterministically chooses one arbitrary place in the list. Then it returns
a new list that is obtained by inserting a given element at the place.
Let M be a term of type A, and K ′ be a coterm of type List(A) ∧ List(A). Then we define
insM [K ′ ] of type List(A) by
[[L1 (α), L2 (α)], K ′ ],
insM [K ′ ] = itrList(A)∧List(A)
α
L1 (α) = x.(hM :: nil, nili • α),
L2 (α) = z.(h hπ1 (z) :: π1 π2 (z), π1 (z) :: π2 π2 (z)i | hM :: π1 (z) :: π2 π2 (z), π1 (z) :: π1 π2 (z)i i • α)
where x occurs in L1 (α) is a fresh variable of type ⊤, and z occurs in L2 (α) is a fresh variable of
type A ∧ (List(A) ∧ List(A)). Then if Nl is a list and Nl′ is a list obtained by inserting M in some
place of Nl, then the statement Nl • ins M [K ′ ] can be reduced to hNl′ , Nli • K ′ . We can show this
by induction on the length of Nl. If Nl is nil, then Nl′ is M :: nil. The statement nil • insM [K ′ ]

16

D. KIMURA AND M. TATSUTA

is reduced to hM :: nil, nili • K ′ . If Nl is N :: Nl0 , then Nl′ is either N :: Nl′0 or M :: N :: Nl0 ,
where Nl′0 is an inserted list obtained from Nl0 . The statement (N :: Nl0 ) • ins M [K ′ ] is reduced to
(hN, (Nl0 •insM [γ]).γi•L2 (α)).α•K ′ . Then this statement is reduced to (hN, hNl0 , Nl′0 ii•L2 (α)).α•
K ′ by the induction hypothesis. We have h hN :: Nl′0 , Nli | hM :: N :: Nl0 , Nli i • K ′ . Hence we can
obtain hM :: N :: Nl0 , Nli • K ′ or hM :: N :: Nl0 , Nli • K ′ .
Let K be a coterm of type List(A). Here we define
insertM [K] = insM [fst[K]].
Then the statement Nl • insertM [K] is reduced to Nl′ • K for any inserted list Nl′ obtained from
Nl.
5. The Second-Order Dual Calculus DC2
We consider the second-order extension DC2 of DC given by Tzevelekos [26]. He showed the basic
properties of DC2, such as the substitution lemma and subject reduction. Without formal discussion,
he also mentioned that his translation from DC into the symmetric λ-calculus can be extended to
the second-order case. In this section, we give a formal definition of the second-order translation
from DC2 into the second-order symmetric λ-calculus, and show the strong normalization of DC2 by
using this translation. For this purpose we will use the strong normalization result of the secondorder symmetric λ-calculus given in [21].
Definition 5.1. An expression is defined to be strongly normalizing if there does not exist any
infinite reduction sequence starting from the expression.
First, we define a second-order extension DC2 of DC.
Definition 5.2 (DC2). The types, terms, coterms, and statements of DC2 are defined by:
Types
Terms
Coterms
Statements

A F X | A ∧ A | A ∨ A | ¬A | ∀X.A | ∃X.A,
M F x | hM, Mi | hMiinl | hMiinr | [K]not | (S ).α | hMia | hMie,
K F α | [K, K] | fst[K] | snd[K] | nothMi | x.(S ) | a[K] | e[K],
S F M • K.

The typing rules and reduction rules (denoted by −→DC2 ) of DC2 are defined by extending the rules
of DC with the following rules:
K : A[B/X] Γ ⊢ ∆
Γ⊢∆ M:A
(∀R)
(∀L)
Γ ⊢ ∆ hMia : ∀Z.A
a[K] : ∀X.A Γ ⊢ ∆
Γ ⊢ ∆ M : A[B/X]
(∃R)
Γ ⊢ ∆ hMie : ∃X.A

K:A Γ⊢∆
(∃L)
e[K] : ∃Z.A Γ ⊢ ∆

(β∀) hMia • a[K] −→DC2 M • K,
(β∃) hMie • e[K] −→DC2 M • K,
where Z is not free in Γ and ∆ in (∀R) and (∃L). We write −→+DC2 to denote the transitive closure of
−→DC2 .
We have the new constructors a and e, which are trivial witnesses for the quantifiers at the
level of expressions, so that the system has subject reduction. We choose our DC2 so that it does
not contain type information in expressions, since our purpose is to show strong normalization of
the second-order dual calculus, and in general the strong normalization of the system with type
information is implied by the strong normalization of the system without type information.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

17

We sometimes use the symbol ⊢DC2 instead of the symbol ⊢ that appears in a judgment in order
to explicitly show it is a judgment of DC2. That is, we write Γ ⊢DC2 ∆ M : A for the judgment
Γ ⊢ ∆ M : A. Similarly, we write K : A Γ ⊢DC2 ∆ and Γ S ⊢DC2 ∆.
We write Γ[B/X] for x1 : C1 [B/X], . . . , xn : Cn [B/X] if Γ is x1 : C1 , . . . , xn : Cn . We also write
∆[B/X]] for α1 : D1 [B/X], . . . , αm : Dm [B/X] if ∆ is α1 : D1 , . . . , αm : Dn .
Lemma 5.3. The following claims hold.
(1) If Γ ⊢DC2 ∆ M : A, then Γ[B/X] ⊢DC2 ∆[B/X] M : A[B/X] holds.
(2) If K : A Γ ⊢DC2 ∆, then K : A Γ[B/X] ⊢DC2 ∆[B/X] holds.
(3) If Γ S ⊢DC2 ∆, then Γ[B/X] S ⊢DC2 ∆[B/X] holds.
Proof. They are shown simultaneously by induction on expressions.
The basic lemmas for DC and DCµν are also shown in DC2. We use Lemma 5.3 to show weakening lemma.
Lemma 5.4 (Weakening lemma). Let Γ ⊆ Γ′ and ∆ ⊆ ∆′ . Then the following hold in DC2.
(1) If Γ ⊢ ∆ M : A is provable, then Γ′ ⊢ ∆′ M : A holds.
(2) If K : A Γ ⊢ ∆ is provable, then K : A Γ′ ⊢ ∆′ holds.
(3) If Γ S ⊢ ∆ is provable, then Γ′ S ⊢ ∆′ holds.
Proof. They are shown simultaneously by induction on M, K, and S . We use Lemma 5.3 when we
show the cases of hMia and e[K]. We consider these cases.
The case of hMia. Assume Γ ⊆ Γ′ , ∆ ⊆ ∆′ , and Γ ⊢ ∆ hMia : A is derivable. Since the last
rule of the derivation must be (∀R), we have A is ∀X.B for some B, the variable X is not free in Γ
and ∆, and Γ ⊢ ∆ M : B is derivable. Then we have Γ ⊢ ∆ M : B[Z/X] for a fresh type variable Z
by using Lemma 5.3. By the induction hypothesis, Γ′ ⊢ ∆′ M : B[Z/X] holds. Therefore we obtain
Γ′ ⊢ ∆′ hMia : ∀Z.(B[Z/X]) by (∀R) rule, since Z is not free in Γ′ and ∆′ .
The case of e[K] is shown similar to the case of hMia.
The other cases are straightforwardly proved by the induction hypothesis.
Lemma 5.5. Let Γ′ ⊆ Γ and ∆′ ⊆ ∆. Then the following hold in DC2.
(1) If FV(M) ⊆ dom(Γ′ ) and FCV(M) ⊆ dom(∆′ ), then Γ ⊢ ∆ M : A implies Γ′ ⊢ ∆′ M : A.
(2) If FV(K) ⊆ dom(Γ′ ) and FCV(K) ⊆ dom(∆′ ), then K : A Γ ⊢ ∆ implies K : A Γ′ ⊢ ∆′ .
(3) If FV(S ) ⊆ dom(Γ′ ) and FCV(S ) ⊆ dom(∆′ ), then Γ | S ⊢ ∆ implies Γ′ | S ⊢ ∆′ .
Proof. They are shown simultaneously by induction on M, K, and S .
Lemma 5.6 (Substitution lemma). The following claims hold.
(1) Suppose Γ ⊢DC2 ∆ N : A is derivable. Then the following hold.
(1a) If Γ, x : A ⊢DC2 ∆ M : B, then Γ ⊢DC2 ∆ M[N/x] : B.
(1b) If K : B Γ, x : A ⊢DC2 ∆, then K[N/x] : B Γ ⊢DC2 ∆.
(1c) If Γ, x : A S ⊢DC2 ∆, then Γ S [N/x] ⊢DC2 ∆.
(2) Suppose L : A Γ ⊢DC2 ∆ is derivable. Then the following hold.
(2a) If Γ ⊢DC2 ∆, α : A M : B, then Γ ⊢DC2 ∆ M[L/α] : B.
(2b) If K : B Γ ⊢DC2 ∆, α : A, then K[L/α] : B Γ ⊢DC2 ∆.
(2c) If Γ S ⊢DC2 ∆, α : A, then Γ S [L/α] ⊢DC2 ∆.
Proof. The claims (1a),(1b), and (1c) are shown simultaneously by induction on M, K, and S . The
claims (2a),(2b), and (2c) are also shown simultaneously by induction on M, K, and S .

18

D. KIMURA AND M. TATSUTA

This system has subject reduction.
Proposition 5.7 (Subject reduction of DC2). The following claims hold.
(1) If Γ ⊢DC2 ∆ M : A and M −→DC2 N, then Γ ⊢DC2 ∆ N : A holds.
(2) If K : A Γ ⊢DC2 ∆ and K −→DC2 L, then L : A Γ ⊢DC2 ∆ holds.
(3) If Γ S ⊢DC2 ∆ and S −→DC2 T , then Γ T ⊢DC2 ∆ holds.
Proof. They are shown simultaneously by induction on the generation of −→DC2 using Lemma 5.3,
5.4, 5.5, and 5.6. We show the cases of (β∀) and (β∃).
The case of (β∀). Suppose Γ hMia • a[K] ⊢ ∆ is derivable. Then Γ ⊢ ∆ hMia : C and
a[K] : C Γ ⊢ ∆ are derivable for some type C. Since the last rules of these derivation must be (∀R)
and (∀L), we have C is ∀X.A for some A, X is not free in both Γ and ∆, and Γ ⊢ ∆ M : A and
K : A[B/X] Γ ⊢ ∆ are derivable for some B. Then we can obtain Γ ⊢ ∆ M : A[B/X] by Lemma 5.3.
Therefore Γ M • K ⊢ ∆ can be derived by (Cut) rule.
The case of (β∃) is shown similar to the case of (β∀).
The other cases are straightforwardly proved by the induction hypothesis.
Remark 5.8. The trivial witnesses a and e are necessary for the subject reduction. If we did not
have these constructors, the subject reduction would fail. If we chose the following (∀R′ ) and (∀L′ )
instead of (∀R) and (∀L),
K : A[B/X] Γ ⊢ ∆
Γ⊢∆ M:A
(∀R′ )
(∀L′ )
Γ ⊢ ∆ M : ∀Z.A
K : ∀X.A Γ ⊢ ∆
then the following would be a counter-example: we would have Γ (x • fst[α]).α • β ⊢ ∆ where Γ
is x : X ∧ Y, the sequence ∆ is β : ∀Z.X, and Z , X, Y, but would not have Γ x • fst[β] ⊢ ∆, though
(x • fst[α]).α • β is reduced to x • fst[β].
In λ-calculus the constructor a is not necessary for subject reduction while the constructor e is
necessary for it [25]. In our system, since ∀ and ∃ are dual, the constructor a is also needed.
The duality transformation can be extended from DC to DC2.
Definition 5.9 (Duality Transformation). The duality transformation for types, expressions, and
inference rule names of DC2 is defined by those of DC and the following equations:
(∀X.A)◦ = ∃X.(A)◦ ,
(∃X.A)◦ = ∀X.(A)◦ ,
(hMia)◦ = e[(M)◦ ],
(e[K])◦ = h(K)◦ ia,
◦
◦
(hMie) = a[(M) ],
(a[K])◦ = h(K)◦ ie,
◦
◦
(∀R) = (∃L),
(∃L) = (∀R),
(∀L)◦ = (∃R),

(∃R)◦ = (∀L).

This duality transformation preserves substitution of types, terms, and coterms.
Lemma 5.10. Let A and B be types, D be an expression, M be a term, and K be a coterm of DC2.
Then the following hold.
(1) (A[B/X])◦ = (A)◦ [(B)◦ /X].
(2) (D[M/x])◦ = (D)◦ [(M)◦ /x′ ].
(3) (D[K/α])◦ = (D)◦ [(K)◦ /α′ ].
Proof. The claim (1) is shown by induction on A. The claims (2) and (3) are shown by induction on
D.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

19

The extended duality transformation preserves typing and reduction. It is an involution in DC2.
Proposition 5.11 (Duality of DC2). The following claims hold.
(1) If J is derived from J1 , . . . , Jn (n = 1 or 2) by an inference rule R, then (J)◦ is derived from
(Jn )◦ , . . . , (J1 )◦ by the inference rule (R)◦ .
(2) D −→DC2 E implies (D)◦ −→DC2 (E)◦ .
(3) ((A)◦ )◦ = A, ((D)◦ )◦ = D, and ((J)◦ )◦ = J hold.
Proof. The claim (1) is proved by case analysis of the inference rules of DC2. The claim (2) is
proved by induction of the generation of −→DC2 using Lemma 5.10. The claim (3) is proved by
induction on types and expressions.
Next we give a definition of the second-order symmetric λ-calculus Sλ2. The symmetric λcalculus is introduced by Barbanera and Berardi [2] as a classical extension of the λ-calculus. The
strong normalization of its second-order extension Sλ2 is proved by Parigot [21] using the reducibility method. The particular system we consider here is an extension of Parigot’s system with two
additional rules (ηr and ηl ). As discussed in ibid., Parigot’s proof works with this variant without
problem.
Definition 5.12 (Sλ2). We define the second-order symmetric λ-calculus Sλ2. The types of Sλ2 are
either the special type ⊥ or m-types (denoted by τ, σ, . . .) given by:
τ F X | X ⊥ | τ × τ | τ + τ | ∀X.τ | ∃X.τ
where X, Y, . . . range over type variables. The types ∀X.τ and ∃X.τ bind X in τ. The negation (τ)⊥
of τ is defined by:
(X)⊥ = X ⊥ ,
(X ⊥ )⊥ = X,
⊥
⊥
⊥
(τ × σ) = (τ) + (σ) , (τ + σ)⊥ = (τ)⊥ × (σ)⊥ ,
(∀X.τ)⊥ = ∃X.(τ)⊥ ,
(∃X.τ)⊥ = ∀X.(τ)⊥ .
The symbols x, y, . . ., α, β, . . . range over variables. The terms of Sλ2, denoted by t, u, . . ., are defined
by
t F x | inj1 (t) | inj2 (t) | ht, ti | t ∗ t | λx.t | a(t) | e(t).
The one-step reduction relation −→Sλ2 of Sλ2 is defined as the compatible closure of the following rules:
(βr )
(λx.t) ∗ u −→Sλ2 t[u/x],
(β×+ 1) ht1 , t2 i ∗ inj1 (u) −→Sλ2 t1 ∗ u,
(β×+ 2) ht1 , t2 i ∗ inj2 (u) −→Sλ2 t2 ∗ u,
(β∀∃ )
a(t) ∗ e(u) −→Sλ2 t ∗ u,
(ηr )
λy.(y ∗ t) −→Sλ2 t,
where y is not free in t in (ηl ) and (ηr ).

(βl )
u ∗ (λx.t) −→Sλ2
(β+× 1) inj1 (u) ∗ ht1 , t2 i −→Sλ2
(β+× 2) inj2 (u) ∗ ht1 , t2 i −→Sλ2
(β∃∀ )
e(u) ∗ a(t) −→Sλ2
(ηl )
λy.(t ∗ y) −→Sλ2

t[u/x],
u ∗ t1 ,
u ∗ t2 ,
u ∗ t,
t,

20

D. KIMURA AND M. TATSUTA

A typing context (denoted by Γ, ∆) is a finite set and of the form x1 : τ1 , . . . , xn : τn . A judgment
of Sλ2 takes either the form Γ ⊢ t : τ or Γ ⊢ t : ⊥. The typing rules of Sλ2 are defined as follows:
Γ, x : τ ⊢ t : ⊥
Γ ⊢ t : (τ)⊥ Γ ⊢ u : τ
(abs)
(app)
(Ax)
Γ, x : τ ⊢ x : τ
Γ ⊢ λx.t : (τ)⊥
Γ⊢t∗u:⊥
Γ ⊢ t : τi
(+ )
Γ ⊢ inji (t) : τ1 + τ2 i (i = 1, 2)
Γ⊢t:τ
(∀)
Γ ⊢ a(t) : ∀X.τ

Γ ⊢ t : τ Γ ⊢ u : σ (×)
Γ ⊢ ht, ui : τ × σ

(X is not free in Γ)

Γ ⊢ t : τ[σ/X]
(∃)
Γ ⊢ e(t) : ∃X.τ

Theorem 5.13 (Strong normalization of Sλ2 [21]). Every typable term is strongly normalizing in
Sλ2.
We will give a reduction-preserving and type-preserving translation from DC2 into Sλ2. Our
translation is a second-order extension of the translation from DC into the symmetric λ-calculus
given by Tzevelekos [26].
Definition 5.14. Let A be a type of DC2. The type (A)† of Sλ2 is defined as follows:
(X)† = X,
(A ∧ B)† = (A)† × (B)† , (A ∨ B)† = (A)† + (B)† ,
(¬A)† = ((A)† )⊥ , (∀X.A)† = ∀X.(A)† ,
(∃X.A)† = ∃X.(A)† .
Let D be an expression of DC2. The term (D)† of Sλ2 is defined by:
(x)† = x,
((S ).α)† = λα.(S )† ,
(hMia)† = a((M)† ),
(e[K])† = a((K)† ),
(hMiinl)† = inj1 ((M)† ),
(hMiinr)† = inj2 ((M)† ),
(hM, Ni)† = h(M)† , (N)† i,
([K]not)† = λx.(x ∗ (K)† ),
(M • K)† = (M)† ∗ (K)† .

(α)† = α,
(x.(S ))† = λx.(S )† ,
(hMie)† = e((M)† ),
(a[K])† = e((K)† ),
(fst[K])† = inj1 ((K)† ),
(snd[K])† = inj2 ((K)† ),
([K, L])† = h(K)† , (L)† i,
(nothMi)† = (M)† ,

We define the translation of [K]not by using η-expansion, so that all reductions in DC2 are strictly
simulated in Sλ2.
(Γ)† and ((∆)† )⊥ are defined as x1 : (A1 )† , . . . , xn : (An )† and α1 : ((B1 )† )⊥ , . . . , αm : ((Bm )† )⊥
respectively if Γ is x1 : A1 , . . . , xn : An , and ∆ is α1 : B1 , . . . , αm : Bm . For a judgment J of DC2,
the judgment (J)† of Sλ2 is defined as follows: The judgment (Γ ⊢ ∆ M : A)† is defined
as (Γ)† , ((∆)† )⊥ ⊢ (M)† : (A)† . The judgment (K : A Γ ⊢ ∆)† is defined as (Γ)† , ((∆)† )⊥ ⊢
(K)† : ((A)† )⊥ . The judgment (Γ S ⊢ ∆)† is defined as (Γ)† , ((∆)† )⊥ ⊢ (S )† : ⊥.
This translation preserves provability and one-step reductions.
Proposition 5.15. The following claims hold.
(1) If J is provable in DC2, then (J)† is provable in Sλ2.
(2) D −→DC2 E implies (D)† −→Sλ2 (E)† .
Proof. The claim (1) is shown by induction on the proof of J. The claim (2) is shown by induction
on the definition of −→DC2 .

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

21

We can obtain strong normalization of DC2 from the above proposition.
Theorem 5.16 (Strong normalization of DC2). Every typable expression is strongly normalizing in
DC2.
Proof. Assume there is an infinite reduction sequence
D = D0 −→DC2 D1 −→DC2 . . .
starting from D. From Proposition 5.15, the expression (D)† is typable in Sλ2, and
(D)† −→Sλ2 (D1 )† −→Sλ2 . . .
is an infinite reduction sequence. This contradicts Theorem 5.13.
Remark 5.17. Tzevelekos [26] also gave a back translation (−) p from the symmetric λ-calculus
into DC. As noted in his paper (Section 3, Note 3.5), this translation cannot extend to the secondorder case since it does not preserve typing judgments for existential quantification. This is because
the translation (−) p does not preserve type substitution: (A[B/X]) p , (A) p [(B) p /X]. The same
argument applies to ours.

6. Strong Normalization of DCµν
In this section, we prove strong normalization in DCµν. We will give a translation from DCµν into
DC2 that is based on the second-order encoding of inductive and coinductive types. Our proof of
strong normalization will be done by showing the fact that one-step reduction in DCµν is translated
to one or more steps reduction in DC2.
We use the following degree of expressions in DCµν for defining the second-order coding of
inductive and coinductive types.
When we try to prove some properties of expressions by induction on expressions, that induction sometimes does not work, since the expression contains monoX,C
A,B,x.M {N} that is defined by using
induction on ||C||X . In order for solving this, we will introduce the pair of the summation of ||C||X
and the size of an expression as a measure.
Definition 6.1. Let D be an expression in DCµν. The number ||D|| is defined by:
||x|| = ||α|| = 0,
||hM, Ni|| = ||coitrAx hM, Ni|| = max(||M||, ||N||),
||M • K|| = max(||M||, ||K||),
||[K, L]|| = ||itrαA [K, L]|| = max(||K||, ||L||),
||(S ).α|| = ||x.(S )|| = ||S ||,
||hMiinl|| = ||hMiinr|| = ||nothMi|| = ||M||,
||inµX.AhMi|| = ||M|| + ||A||X + 1,
||fst[K]|| = ||snd[K]|| = ||[K]not|| = ||K||,
||outνX.A [K]|| = ||K|| + ||A||X + 1.

22

D. KIMURA AND M. TATSUTA

The number |D| is defined by:
|x| = |α| = 0,
|hM, Ni| = |coitrAx hM, Ni| = |M| + |N| + 1,
|M • K| = |M| + |K| + 1,
|[K, L]| = |itrαA [K, L]| = |K| + |L| + 1,
|(S ).α| = |x.(S )| = |S | + 1,
|hMiinl| = |hMiinr| = |nothMi| = |inµX.AhMi| = |M| + 1,
|fst[K]| = |snd[K]| = |[K]not| = |outνX.A[K]| = |K| + 1.
The degree deg(D) of the expression D is defined as the pair (||D||, |D|). We also define the order of
the degrees by the lexicographic order.
The number |D| is the number of constructors in the expression D. The number ||D|| is the
maximum summation of (||A||X + 1) for inµX.AhMi and outνX.A[K] in paths in D. For example,
deg(inµX.¬X∨X h(h[x.(hxiinr • γ)]notiinl • γ).γi) = (4, 7). We have ||E|| ≤ ||D|| and |E| < |D| when
the expression E is a proper subexpression of D. The degree satisfies the following properties.
Lemma 6.2. The following claims hold.
(1) ||D|| = ||(D)◦ || and |D| = |(D)◦ | hold.
(2) || monoX.A
B,C,x {M, N} || ≤ ||M|| + ||N|| + ||A||X holds.
X.A
(3) deg(inµX.AhMi) > deg( monoµX.A,Y,α
{ x.(y • (x@α)), β }) holds.

Proof. The claims of (1) are shown by induction on D. The claim (2) is shown by induction on
||A||X . The claim (3) is proved by using (2).
We present the second-order encoding for DCµν. We will write λ(x, α).S for λx.((S ).α). Then
(λ(x, α).S ) • (N@K) is reduced to S [N/x][K/α].
Definition 6.3 (Translation (−) from DCµν into DC2). Let A be a type of DCµν. The type A of DC2 is
defined as follows:
X = X,

A ∧ B = A ∧ B,

µX.A = ∀X.((A ⊃ X) ⊃ X),

¬A = ¬A,

A ∨ B = A ∨ B,

νX.A = ∃X.(¬(¬A ∧ X) ∧ X),

where ⊃ is defined in Definition 2.9. For an expression D of DCµν, the expression D of DC2 is defined
by induction on deg(D) as follows. For the expressions D of the same degree, we first define D for
D such that D is not of the form outνX.A[K] or coitrAx hM, Ni, and we next define D for D such that
D is of the form outνX.A[K] or coitrAx hM, Ni.
x = x,
(S ).α = (S ).α,
hM, Ni = hM, Ni,
hMiinl = hMiinl,
hMiinr = hMiinr,
[K]not = [K]not,

α = α,
x.(S ) = x.(S ),
[K, L] = [K, L],
fst[K] = fst[K],
snd[K] = snd[K],
nothMi = nothMi,

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

23

M • K = M • K,
itrαA [K, L] = a[ ( λ(x, α).(x • K) )@L ],
◦

outνX.A[K] = (inµX.(A) h(K)◦ i)◦ ,
inµX.AhMi = h λ(y, β).(y • ( (QY [X.A] • R M {y, γ}).γ@β )) ia,
◦

◦
◦ ◦
coitrAx hM, Ni = (itr(A)
x′ [(M) , (N) ]) ,
X.A
{ x.(y • (x@α)), β } ), and R M {N, K} is defined
where QY [X.A] is defined as λy.λ(z, β).( z•monoµX.A,Y,α

as ( λ(x, α).(x • a[N@α]) )@(M@K).
We also define the translation of judgments. The context Γ is defined as x1 : A1 , . . . , xn : An if Γ
is x1 : A1 , . . . , xn : An . The cocontext ∆ is defined as α1 : B1 , . . . , αm : Bm if ∆ is α1 : B1 , . . . , αm : Bm .
The judgment Γ ⊢ ∆ M : A is defined as Γ ⊢ ∆ M : A. The judgment K : A Γ ⊢ ∆ is defined as
K : A Γ ⊢ ∆. The judgment Γ S ⊢ ∆ is defined as Γ S ⊢ ∆.
The next lemma shows that this translation commutes with (−)◦ .
Lemma 6.4. ( A )◦ = (A)◦ , ( D )◦ = (D)◦ , and ( J )◦ = (J)◦ hold.
Proof. The claim for A is proved by induction on A.
The claim for D is proved by induction on D. The cases of inµX.AhMi, outνX.A[K], itrαA [K, L],
and coitrAx hM, Ni are shown by the definition of the translation and the dualities of DCµν and
◦ ◦

DC2. The case of inµX.AhMi is shown as follows: (inµX.AhMi)◦ = (inµX.((A) ) h((M)◦ )◦ i)◦ =
outνX.(A)◦ [(M)◦ ] = (inµX.AhMi)◦ . We can show the cases outνX.A[K], itrαA [K, L], and
coitrAx hM, Ni similarly. The other cases are straightforwardly proved by the induction hypothesis.
The claim for J is proved by using the claims for A and D.
The translation (−) preserves substitution.
Lemma 6.5. A[B/X] = A[B/X], D[N/x] = D[N/x], and D[L/α] = D[L/α] hold.
Proof. The first claim is shown by induction on A. The second and the third claims are shown
simultaneously by induction on deg(D). For the expressions D of the same degree, we first show
the claims for D such that D is not of the form outνX.A [K] or coitrAx hM, Ni, and we next show the
claims for D such that D is of the form outνX.A[K] or coitrAx hM, Ni.
We consider the cases of inµX.A hMi, itrαA [K, L], outνX.A [K] and coitrAx hM, Ni. The other
cases are straightforwardly proved by the induction hypothesis.
The second claim of the case inµX.AhMi is shown in the following way. By the induction
X.A
X.A
hypothesis, we have monoµX.A,Y,α
{ x.(y • (x@α)), β }[N/x] = monoµX.A,Y,α
{ x.(y • (x@α)), β }[N/x]
µX.A
X.A
since deg( monoµX.A,Y,α{ x.(y • (x@α)), β }) < deg(in
hMi) by Lemma 6.2 (3).
By
X.A
X.A
{ x.(y • (x@α)), β }[N/x] = monoµX.A,Y,α
{ x.(y • (x@α)), β }. Hence
Lemma 3.13 (2a), monoµX.A,Y,α

we have (QY [X.A])[N/x] = QY [X.A]. By the induction hypothesis, we have R M {y, γ}[N/x] =
R M[N/x] {y, γ} since deg(M) < deg(inµX.AhMi). Therefore, inµX.AhMi[N/x] is equal to h λ(y, β).(y •
( ((QY [X.A])[N/x] • (R M {y, γ})[N/x]).γ@β )) ia. Then it is equal to h λ(y, β).(y • ( (QY [X.A] •
R M[N/x] {y, γ}.γ@β )) ia. The last term is equal to (inµX.AhMi)[N/x] by the definition of (−).

24

D. KIMURA AND M. TATSUTA

The second claim of the case itrαA [K, L] is shown in the following way. The coterm
itrαA [K, L][N/x] is equal to a[ ( λ(y, α).(y • K[N/x]) )@L[N/x] ]. By the induction hypothesis,
it is equal to a[ ( λ(y, α).(y • K[N/x]) )@L[N/x] ]. Hence it is equal to (itrαA [K, L])[N/x] by the
definition of (−).
The second claim of the case outνX.A[K] is shown in the following way. Since ||K|| = ||(K)◦ ||
◦
and |K| = |(K)◦ | by Lemma 6.2 (1), we have deg(outνX.A[K]) = deg(inµX.(A) h(K)◦ i). Hence
◦
◦
inµX.(A) h(K[N/x])◦ i = inµX.(A) h(K)◦ i[(N)◦ /x′ ] holds by Lemma 3.10, since the third claim for
◦
inµX.(A) h(K)◦ i is already shown before this case. Then we can obtain the claim of this case as
follows:
◦
◦
(outνX.A [K])[N/x]
=
( inµX.(A) h(K[N/x])◦ i )◦
=
( inµX.(A) h(K)◦ i[(N)◦ /x′ ] )◦
=
µX.(A)◦
◦
◦
◦
◦
◦
◦
νX.A
νX.A
( in
h(K) i ) [((N) ) /x] = out [K][((N) ) /x] = out [K][N/x].
The third claim of this case is shown similarly.
The second and third claims of the case coitrAx hM, Ni is shown in the similar way to the case
of outνX.A[K].
Note that the second and third claims of the above lemma cannot be proved straightforwardly
by induction on D. For example, for proving the case of inµX.AhMi in the second claim, we need
X.A
induction hypothesis for monoµX.A,Y,α
{ x.(y • (x@α)), β } but it is not a subterm of inµX.AhMi.
The next proposition says the translation (−) preserves provability.
Proposition 6.6. If J is provable in DCµν, then J is provable in DC2.
Proof. This is shown by induction on the degree of the principal expression in J. We show the cases
of inµX.AhMi, outνX.A [K], itrαA [K, L], and coitrAx hM, Ni.
The case of itrαA [K, L] is shown by the induction hypothesis and Lemma 6.5. The cases of
coitrAx hM, Ni and outνX.A[K] are shown by the induction hypothesis and the dualities of DCµν and
DC2.
We prove the case of inµ hMi. We write µ, A[B], and A[C] as abbreviations of µX.A,
A[B/X], and A[C/X] respectively. This case is shown by the following three steps: (a) we show
R M {y, γ} : (µ ⊃ Y) ⊃ A[µ] ⊃ A[Y] Γ, y : A[Y] ⊃ Y ⊢ ∆, γ : A[Y] is derivable, where R M {y, γ} is
(λ(x, α).(x • a[y@α]) )@(M@γ). Next, (b) we show ⊢
QY [X.A] : (µ ⊃ Y) ⊃ A[µ] ⊃ A[Y]
X.A
is derivable, where QY [X.A] is λy.λ(z, β).( z • monoµX.A,Y,α{ x.(y • (x@α)), β } ). Finally, (c) we can
easily show Γ ⊢ ∆ inµ hMi : µ from (a) and (b).
The claim (a) is shown in the following way. Suppose Γ ⊢ ∆ inµ hMi : µ is derivable. Then
we have the derivation of Γ ⊢ ∆ M : A[µ]. By the induction hypothesis and Lemma 6.5, we obtain
Γ ⊢ ∆ M : A[µ]. Then we have a derivation of M@γ : A[µ] ⊃ A[Y] Γ ⊢ ∆, γ : A[Y] by (⊃ L) rule.
On the other hand, we can show y : A[Y] ⊃ Y ⊢ λ(x, α).(x • a[y@α]) : µ ⊃ Y. Then we have
R M {y, γ} : (µ ⊃ Y) ⊃ A[µ] ⊃ A[Y] Γ, y : A[Y] ⊃ Y ⊢ ∆, γ : A[Y].
X.A { x.(y • (x@α)), β } : A[µ] y : µ ⊃
The claim (b) is shown as follows. We can show monoµ,Y,α
Y ⊢ β : A[Y] in DCµν by using Lemma 3.14, the judgment x.(y • (x@α)) : µ y : µ ⊃ Y ⊢
α : Y, β : A[Y], and β : A[µ] y : µ ⊃ Y ⊢ β : A[Y]. By Lemma 6.2 (3), we have deg(inµX.AhMi) >
X.A { x.(y • (x@α)), β }). Hence monoX.A { x.(y • (x@α)), β } : A[µ] y : µ ⊃ Y ⊢ β : A[Y] is
deg(monoµ,Y,α
µ,Y,α
derivable by induction hypothesis and Lemma 6.5. Therefore we obtain ⊢ QY [X.A] : (µ ⊃ Y) ⊃
A[µ] ⊃ A[Y].
The other cases are straightforwardly proved by the induction hypothesis.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

25

The translation (−) maps one-step reduction to one or more steps of reduction.
Proposition 6.7. For expressions D and E of DCµν, the relation D −→DCµν E implies D −→+DC2 E.
Proof. First we show the claim without (βµ) nor (βν) by induction on −→DCµν with Lemma 6.5.
Next, by using this and Lemma 6.5, we show the claim of this proposition by induction on −→DCµν .
We consider cases according to the reduction rule.
The case of (βµ) is shown as follows: Suppose we have inµX.AhMi • itrαB [K, L]. This is
equal to hλ(y, β).(y • ((QY [X.A] • R M {y, γ}).γ@β))ia • a[(λ(x.α).(x • K))@L]. It is reduced to
(λ(y, β).(y • ((QY [X.A] • R M {y, γ}).γ@β))) • ((λ(x.α).(x • K))@L), and then we have (λ(x.α).(x •
K)) • ((QY [X.A] • R M {λ(x.α).(x • K), γ}).γ@L) by more than one step reduction. Since λ(x.α).(x • K)
equals λx.((x • K).α), we have ((QY [X.A] • R M {λ(x.α).(x • K), γ}).γ • K).α • L by (β ⊃). This is
reduced to ((QY [X.A] • R M {λ(x.α).(x • K), K}).α • L by (βR). Here R M {λ(x.α).(x • K), K} is equal to
(λ(y, β).(y • itrαB [K, β])@(M@K)). Hence we can reduce QY [X.A] • R M {λ(x.α).(x • K), K} to M •
X.A {itrB [K, β], K} by using Lemma 6.5 and the first claim. Therefore the previously obtained
monoµ,Y,α
α
X.A
expression ((QY [X.A]•R M {λ(x.α).(x•K), K}).α•L is reduced to (M•monoµX.A,Y,α
{itrαB [K, β], K}).α•
X.A
L. This is equal to (M • monoµX.A,Y,β
{itrαB [K, β], K}).α • L.
The case of (βν) is shown by using the duality of (βν) and (βµ), the duality of DC2, and
Lemma 6.4.
Other cases are shown straightforwardly.

Finally, we complete a proof of strong normalization of DCµν.
Theorem 6.8 (Strong normalization of DCµν). Every typable expression of DCµν is strongly normalizing.
Proof. Assume that D is typable in DCµν and there is an infinite reduction sequence
D −→DCµν D1 −→DCµν . . .
starting from D. Then D is typable in DC2 by Proposition 6.6 and
D −→+DC2 D1 −→+DC2 . . .
is an infinite reduction sequence starting from D by Proposition 6.7. This contradicts Theorem 5.16.

7. The call-by-value and call-by-name DCµν
The motivation for introducing the dual calculus in [27] was to show the duality between callby-value and call-by-name. In this section, we follow this motivation. That is, we will extend
the duality to inductive and coinductive types by introducing the call-by-value and call-by-name
variants of DCµν. These variants also satisfy the important properties such as strong normalization
and the Church-Rosser property.
We recall the definition of the call-by-value and call-by-name DC. The call-by-value and callby-name dual calculus use the notion of values and covalues. They are defined as follows.

26

D. KIMURA AND M. TATSUTA

Definition 7.1 (Values and covalues of DC [27]). The values (denoted by V, W, . . .) and covalues
(denoted by P, Q, . . .) of DC are defined by the following grammar:
V ::= x | hV, Vi | hViinl | hViinr | [K]not,
P ::= α | [P, P] | fst[P] | snd[P] | nothMi,
where M is a term and K is a coterm of DC.
The types, expressions, and typing rules of the call-by-value and call-by-name DC are the same
as them of DC. The call-by-value reduction relation of DC is defined as follows.
Definition 7.2 (Call-by-value reduction rules of DC). The call-by-value reduction relation −→vDC of
DC is defined from the following rules.
(β∧1 )v
(β∧2 )v
(β∨1 )v
(β∨2 )v
(β¬)v
(βR)v
(βL)v
(ς∧1 )v
(ς∧2 )v
(ς∨1 )v
(ς∨2 )v
(ηR)+v
(ηL)+v

hV, Wi • fst[K] −→vDC V • K,
hV, Wi • snd[K] −→vDC W • K,
hViinl • [K, L] −→vDC V • K,
hWiinr • [K, L] −→vDC W • L,
[K]not • nothMi −→vDC M • K,
(S ).α • K −→vDC S [K/α],
V • x.(S ) −→vDC S [V/x],
hM, Ni −→vDC (M • x.(hx, Ni • α)).α,
hV, Mi −→vDC (M • x.(hV, xi • α)).α,
hMiinl −→vDC (M • x.(hxiinl • α)).α,
hMiinr −→vDC (M • x.(hxiinr • α)).α,
M −→vDC (M • α).α, and
K −→vDC x.(x • K),

where M is not a value, and x and α in (ς∧1 )v , (ς∧2 )v , (ς∨1 )v , (ς∨2 )v , (ηL)+v and (ηR)+v are fresh.
An example of use of ς-rules is
h(S ).αiinl −→vDC ((S ).α • x.(hxiinl • β)).β −→vDC (S [x.(hxiinl • β)/α]).β.
This system is obtained from the call-by-value dual calculus given in [27] by removing the implication.
We note that the original system in [27] includes implication types, values for implication, and
a call-by-value β-rule for implication. However, as mentioned in [27], an implication A ⊃ B can be
defined as ¬(A ∧ ¬B) under call-by-value. Hence each value for implication can be replaced a value
in terms of other connectives, and the reduction rule for implication can be simulated by the other
β-rules.
The rules (ς∧1 )v , (ς∧2 )v , (ς∨1 )v , and (ς∨2 )v are the separated forms of the rule (ς) given in
[27], and our rules are equivalent to his rule. However, we prefer this separated form since this form
is easy to add ς-rules for inductive and coinductive types later.
The symbol + used in (ηL)+v and (ηR)+v means η-expansion rules. When we extend call-byvalue and call-by-name calculi with inductive and coinductive types later in this section, we will
use the reduction (ηR) and (ηL) instead of the above expansion (ηR)+v and (ηL)+v for the following
reasons. In [27], η-rules requires side conditions to avoid infinite reduction sequence: “expansions
(ηL) and (ηR) should be applied only to a term M or coterm K that is not the immediate subject
of a cut”. However, two problems still remain about η-expansion rules. One problem is that a
value becomes non-value by the η-expansion: For example, a value x is expanded to a non-value
(x • α).α by (ηR)+v -rule. The second problem is that infinite reduction sequences occur with ς-rule:
For example, hxiinl • β is reduced to h(x • α).αiinl • β by (ηR)+v . Since (x • α).α is not a value,

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

27

it can be reduced to ((x • α).α • y.(hyiinl • γ)).γ • β by (ς∨1 )v . Then, we have hxiinl • β again
by (βL)v and (βR)v -rules. Tzevelekos [26] assumed additional conditions on η-expansion rules, and
showed strong normalization and the Church-Rosser properties of the call-by-value and call-byname DC under his conditions. However, his approach does not solve the first problem. One simple
solution for the both problems is to replace η-expansion by η-reduction. For this reason, we will
adopt η-reduction in our call-by-value and call-by-name systems.
The dual calculus considered in [28] has η-rules for conjunction, disjunction, and negation.
These rules could be defined naturally because the system in [28] was based on equations. However,
we cannot define these η-rules naively in the call-by-value and call-by-name reduction systems of
DC since these rules break the Church-Rosser property: The call-by-value (η∨)-rule defined in [28]
is [x.(hxiinl • K), y.(hyiinr • K)] = K, where K has type A ∨ B. Suppose that we add (η∨)reduction rule [x1 .(hx1 iinl•K), x2 .(hx2 iinr•K)] →vDC K to the call-by-value DC. Then the statement
[x1 .(hx1 iinl • y.(z • α)), x2 .(hx2 iinr • y.(z • α))] has two normal forms [x1 .(z • α), x2 .(z • α)] and
y.(z • α). Suppose that we add (η∨)-expansion rule K →vDC [x1 .(hx1 iinl • K), x2 .(hx2 iinr • K)] to
the call-by-value DC. The statement x • y.(z • α) (the variable z and the covariable α have type X,
and the variables x and y have type A ∨ B) is reduced to z • α by (βL )-rule. The statement x • y.(z • α)
is also expanded to x • [x1 .(hx1 iinl • y.(z • α)), x2 .(hx2 iinr • y.(z • α))] by (η∨)-rule, and then it
is reduced to x • [x1 .(z • α), x2 .(z • α)] by (βL )v -rule. These two results are never confluent since
the first one z • α cannot produce a coterm of the form [K, L], and the bracket [..] in the second one
x • [x1 .(z • α), x2 .(z • α)] cannot be eliminated.
The call-by-name reduction relation of DC is defined as follows.
Definition 7.3 (Call-by-name reduction rules of DC). The call-by-name reduction relation −→nDC of
DC is defined from the following rules.
(β∧1 )n
(β∧2 )n
(β∨1 )n
(β∨2 )n
(β¬)n
(βR)n
(βL)n
(ς∧1 )n
(ς∧2 )n
(ς∨1 )n
(ς∨2 )n
(ηR)+n
(ηL)+n

hM, Ni • fst[P] −→nDC M • P,
hM, Ni • snd[P] −→nDC N • P,
hMiinl • [P, Q] −→nDC M • P,
hMiinr • [P, Q] −→nDC M • Q,
[K]not • nothMi −→nDC M • K,
(S ).α • P −→nDC S [P/α],
M • x.(S ) −→nDC S [M/x],
fst[K] −→nDC x.((x • fst[α]).α • K),
snd[K] −→nDC x.((x • snd[α]).α • K),
[K, L] −→nDC x.((x • [α, L]).α • K),
[P, K] −→nDC x.((x • [P, α]).α • K),
M −→nDC (M • α).α, and
K −→nDC x.(x • K),

where K is not a covalue, and x and α in (ς∧1 )n , (ς∧2 )n , (ς∨1 )n , (ς∨2 )n , (ηL)+n and (ηR)+n are fresh.
This system is obtained from the call-by-name dual calculus given in [27] by removing the
implication.
As mentioned in [27], an implication A ⊃ B can be defined as ¬A ∨ B under call-by-name.
Hence, covalues for implication, and a call-by-name reduction rules for implication given in the
original system can be replaced in terms of other connectives.
The call-by-value reduction and the call-by-name reduction are dual strategies in DC.

28

D. KIMURA AND M. TATSUTA

Proposition 7.4 (Duality between call-by-value and call-by-name in DC [27]). Let D and E be
expressions of DC. Then, D −→vDC E iff (D)◦ −→nDC (E)◦ , where (−)◦ is the duality transformation
defined in the section 2.
Now we will introduce the call-by-value and call-by-name variants of DCµν. We first consider
a call-by-value restriction of DCµν (called weak call-by-value DCµν) which is given by simply restricting the reduction rules of DCµν. This restricted system satisfies both strong normalization and
the Church-Rosser properties. However, this system is rather weak since it lacks the ς-rules. The
call-by-value DCµν (denoted by CBV DCµν) is obtained by adding the ς-rules to the weak call-byvalue DCµν. The weak call-by-name DCµν and the call-by-name DCµν (denoted by CBN DCµν) are
also considered. The call-by-name DCµν is the dual system of the call-by-value DCµν.
We first define the notion of values and covalues in DCµν.
Definition 7.5 (Values and covalues of DCµν). The values (denoted by V, W, . . .) and the covalues
(denoted by P, Q, . . .) of DCµν are defined by the following grammar:
V ::= x | hV, Vi | hViinl | hViinr | [K]not | inµX.AhVi | coitrAx hM, Vi,
P ::= α | [P, P] | fst[P] | snd[P] | nothMi | outνX.A[P] | itrαA [K, P],
where M is a term and K is a coterm of DCµν.
The set of values of DCµν is a subset of terms of DCµν. The set of covalues of DCµν is a subset
of coterms of DCµν. Note that the above definition is a straightforward extension of the definition of
values and covalues in DC.
The set of values and covalues are closed under substitution of values and covalues, respectively.
Lemma 7.6. Let V and W be values, and P and Q be covalues of DCµν. The following claims hold.
(1) V[W/x] is a value of DCµν.
(2) P[Q/α] is a covalue of DCµν.
Proof. They are straightforwardly proved by induction on V and P.
The types, expressions, and typing rules of the weak call-by-value and the weak call-by-name
DCµν are the same as them of DCµν. The reduction relation of the weak call-by-value DCµν is given
as follows.
Definition 7.7 (Reduction rules of the weak call-by-value DCµν). The reduction relation −→wCBV
of the weak call-by-value DCµν is defined as the compatible closure of the reduction rules (β∧1 )v ,
(β∧2 )v , (β∨1 )v , (β∨2 )v , (β¬)v , (βR)v , (βL)v , and the following reduction rules:
X.C
(βµ)v inµX.C hVi • itrαA [K, L] −→wCBV (V • monoµX.C,A,β
{ itrαA [K, β], K }).α • L,
A
(βν)v coitrAx hM, Vi • outνX.C [K] −→wCBV V • x.(monoX.C
A,νX.C,z{ coitr x hM, zi, M } • K),
(ηR)v (M • α).α −→wCBV M,
(ηL)v x.(x • K) −→wCBV K,

where x and α are fresh in (ηL)v and (ηR)v , respectively.
The reduction relation of the weak call-by-name DCµν is given as follows.
Definition 7.8 (Reduction rules of the weak call-by-name DCµν). The reduction relation −→wCBN
of the weak call-by-name DCµν is defined as the compatible closure of the reduction rules (β∧1 )n ,
(β∧2 )n , (β∨1 )n , (β∨2 )n , (β¬)n , (βR)n , (βL)n , and the following reduction rules:

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

29

X.C
(βµ)n inµX.C hMi • itrαA [K, P] −→wCBN (M • monoµX.C,A,β
{ itrαA [K, β], K }).α • P,
A
(βν)n coitrAx hM, Ni • outνX.C [P] −→wCBN M • x.(monoX.C
A,νX.C,z{ coitr x hM, zi, M } • P),
(ηR)n (M • α).α −→wCBN M,
(ηL)n x.(x • K) −→wCBN K,

where x and α are fresh in (ηL)n and (ηR)n , respectively.
The weak call-by-value reduction and the weak call-by-name reduction are dual strategies.
Proposition 7.9 (Duality between weak call-by-value and weak call-by-name in DCµν). Let D and
E be expressions of DCµν. Then, D −→wCBV E iff (D)◦ −→wCBN (E)◦ , where (−)◦ is the duality
transformation of DCµν defined in the section 3.
The rules (β¬)v , (βR)v , (ηL)v , and (ηR)v are the same as (β¬), (βR), (ηL), and (ηR)-rules of DCµν,
respectively. The rules (β∧1 )v , (β∧2 )v , (β∨1 )v , (β∨2 )v , (βL)v , (βµ)v , and (βν)v are just restrictions
of the rules (β∧1 ), (β∧2 ), (β∨1 ), (β∨2 ), (βL), (βµ), and (βν), respectively. The situation of the
call-by-name case is similar to the call-by-value case. Hence, we can easily obtain the following
proposition.
Proposition 7.10. Let D and E be expressions in DCµν. Then the following claims hold.
(1) If D −→wCBV E, then D −→DCµν E.
(2) If D −→wCBN E, then D −→DCµν E.
From the above proposition and the strong normalization result of DCµν (Theorem 6.8), we have
the strong normalization of the weak call-by-value and the weak call-by-name reduction relations.
Proposition 7.11 (Strong normalization of the weak CBV and CBN DCµν). We have the following.
(1) Every typable expression is strongly normalizing in the weak call-by-value DCµν.
(2) Every typable expression is strongly normalizing in the weak call-by-name DCµν.
The reduction relations −→wCBV and −→wCBN of DCµν satisfy the Church-Rosser property. We
first recall the definition of the Church-Rosser property.
Definition 7.12 (Church-Rosser property). Let A be a set and → be a reduction relation on A. We
write b ← a → c if both a → b and a → c hold. We also write b → a ← c if both b → a and c → a
hold.
(1) The reduction relation → satisfies the diamond property if, for all a, b, c ∈ A, the relation
b ← a → c implies that there exists d ∈ A such that b → d ← c.
(2) The reduction relation → satisfies the Church-Rosser property if →∗ satisfies the diamond property, where →∗ is the reflexive transitive closure of →.
From now on, we concentrate to show the Church-Rosser property of −→wCBV . The ChurchRosser property of −→wCBN can be obtained from the result of −→wCBV and the duality (Proposition 7.9). In order to show the Church-Rosser property of −→wCBV , we will use the parallel reduction
technique. The definition of the parallel reduction relation is given as follows.
Definition 7.13 (Parallel reduction of the weak call-by-value DCµν). The parallel reduction relation
(denoted by ⇒) of the weak call-by-value DCµν is defined inductively from the following rules.
x ⇒ x and α ⇒ α for any variable x and covariable α.
hM, Ni ⇒ hM ′ , N ′ i if M ⇒ M ′ and N ⇒ N ′ .
[K, L] ⇒ [K ′ , L′ ] if K ⇒ K ′ and L ⇒ L′ .
hMiinl ⇒ hM ′ iinl, hMiinr ⇒ hM ′ iinr, and nothMi ⇒ nothM ′ i if M ⇒ M ′ .

30

D. KIMURA AND M. TATSUTA

fst[K] ⇒ fst[K ′ ], snd[K] ⇒ snd[K ′ ], and [K]not ⇒ [K ′ ]not if K ⇒ K ′ .
inµX.A hMi ⇒ inµX.AhM ′ i if M ⇒ M ′ .
outνX.A[K] ⇒ outνX.A[K ′ ] if K ⇒ K ′ .
coitrAx hM, Ni ⇒ coitrAx hM ′ , N ′ i if M ⇒ M ′ and N ⇒ N ′ .
itrαA [K, L] ⇒ itrαA [K ′ , L′ ] if K ⇒ K ′ and L ⇒ L′ .
M • K ⇒ M ′ • K ′ if M ⇒ M ′ and K ⇒ K ′ .
(S ).α ⇒ (S ′ ).α and x.(S ) ⇒ x.(S ′ ) if S ⇒ S ′ .
M • x.(S ) ⇒ S ′ [V/x] if M ⇒ V and S ⇒ S ′ .
(S ).α • K ⇒ S ′ [K ′ /α] if K ⇒ K ′ and S ⇒ S ′ .
hM, Ni • fst[K] ⇒ V • K ′ if M ⇒ V, N ⇒ W, and K ⇒ K ′ .
hM, Ni • snd[K] ⇒ W • K ′ if M ⇒ V, N ⇒ W, and K ⇒ K ′ .
hMiinl • [K, L] ⇒ V • K ′ if M ⇒ V, K ⇒ K ′ .
hMiinl • [K, L] ⇒ V • L′ if M ⇒ V, L ⇒ L′ .
[K]not • nothMi ⇒ M ′ • K ′ if M ⇒ M ′ and K ⇒ K ′ .
X.C
inµX.C hMi • itrαA [K, L] ⇒ (V • monoµX.C,A,β
{ itrαA [K ′ , β], K ′ }).α • L′ if M ⇒ V, K ⇒ K ′ ,
and L ⇒ L′ .
A
′
′
′
′
coitrAx hM, Ni • outνX.C [K] ⇒ V • x.(monoX.C
A,νX.C,z{ coitr x hM , zi, M } • K ) if M ⇒ M ,
N ⇒ V, and K ⇒ K ′ .
(M • α).α ⇒ M ′ if M ⇒ M ′ and α is not free in M.
x.(x • K) ⇒ K ′ if K ⇒ K ′ and x is not free in K.
The parallel reduction of the weak call-by-value DCµν satisfies the following basic properties.
Lemma 7.14. Let M be a term, V and V ′ be values, K and K ′ be coterms, and D and D′ be
expressions of DCµν. Then the following hold.
(1) Suppose D ⇒ E. If D is a term, then E is also a term. If D is a coterm, then E is also a coterm.
If D is a statement, then E is also a statement. If D is a value, then E is also a value.
(2) D ⇒ D.
(3) If M ⇒ V and D ⇒ D′ , then D[M/x] ⇒ D′ [V/x].
(4) If K ⇒ K ′ and D ⇒ D′ , then D[K/α] ⇒ D′ [K ′ /α].
Proof. The claim (1) is shown by induction on the definition of ⇒. The claim (2) is shown by
induction on D.
The claim (3) is shown by induction on D ⇒ D′ with Lemma 7.6. We show the case that
N0 • y.(T 0 ) ⇒ T 1 [W/y] is derived from N0 ⇒ W and T 0 ⇒ T 1 . By the induction hypothesis, we
have N0 [M/x] ⇒ W[V/x] and T 0 [M/x] ⇒ T 1 [V/x]. By Lemma 7.6, W[V/x] is a value. Hence we
have (N0 • y.(T 0 ))[M/x] = (N0 [M/x]) • y.(T 0 [M/x]) ⇒ T 1 [V/x][W[V/x]/y] = T 1 [W/y][V/x]. The
other cases are straightforwardly proved by the induction hypothesis.
The claim (4) is shown by induction on D ⇒ D′ .
Lemma 7.15. Let D and D′ be expressions of DCµν. Then the following claims hold.
(1) If D −→wCBV E, then D ⇒ E.
(2) If D ⇒ E, then D −→∗wCBV E.
(3) The parallel reduction relation ⇒ satisfies the diamond property, that is, if the relation D1 ⇐
D ⇒ D2 holds, then there exists E such that D1 ⇒ E ⇐ D2 .
Proof. The claim (1) is shown by induction on the definition of −→wCBV . The claim (2) is shown by
induction on the definition of ⇒.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

31

The claim (3) is shown by induction on D. We show the case that D is the shape of (S ).α• x.(T ),
D1 is S ′ [L/α], and D2 is T ′ [V/x] with the conditions S ⇒ S ′ , T ⇒ T ′ , x.T ⇒ L, and (S ).α ⇒ V.
Recall that a critical pair in DCµν occurs in this shape. This case is most important to see that this
critical pair is avoided in the weak call-by-value DCµν .
From the definition of the parallel reduction and (S ).α ⇒ V, we have S = M • α, M ⇒ V, and
α is not free in M. Then, from M • α = S ⇒ S ′ , we have the following two cases: (i) S ′ = M ′ • α
and M ⇒ M ′ for some M ′ , or (ii) M = (S 0 ).β, S ′ = S 0 ′ [α/β], and S 0 ⇒ S 0 ′ for some S 0 and S 0 ′ .
From the condition x.(T ) ⇒ L, we also have the following two cases: (a) T = x • K, x is not free
in K, and K ⇒ L for some K and L, or (b) L = x.(T ′′ ) and T ⇒ T ′′ for some T ′′ .
The case of (i). We have D1 = (S ′ )[L/α] = (M ′ •α)[L/α] = M ′ •L. By the induction hypothesis
and V ⇐ M ⇒ M ′ , there exists a term W such that V ⇒ W ⇐ M ′ . From Lemma 7.14 (1), W is a
value. We then consider the subcases (a) and (b).
The subcase of (a). From the condition K ⇒ L and T = x • K, we have (x • L) ⇐ T ⇒ T ′ . By
the induction hypothesis, there exists a statement T̃ such that (x • L) ⇒ T̃ ⇐ T ′ . Hence we have
D1 = (x • L)[M ′ /x] ⇒ T̃ [W/x] ⇐ T ′ [V/x] = D2 from M ′ ⇒ W ⇐ V and Lemma 7.14 (3).
The subcase of (b). By the induction hypothesis and T ′ ⇐ T ⇒ T ′′ , there exists T̃ such
that T ′ ⇒ T̃ ⇐ T ′′ . Hence we have D2 = T ′ [V/x] ⇒ T̃ [W/x] by Lemma 7.14 (3) and V ⇒ W.
We also have D1 = M ′ • L = M ′ • x.(T ′′ ) ⇒ T̃ [W/x] from M ′ ⇒ W and T ′′ ⇒ T̃ . Therefore
D1 ⇒ T̃ [W/x] ⇐ D2 holds.
The case of (ii). We first claim that, for any S and V, if (S ).α ⇒ V, then there is some M such
that S = M • α, M ⇒ V, and α is not free in M. This claim is easily obtained from the definition
of the parallel reduction. In this case, we have V ⇐ M = (S 0 ).β ⇒ (S 0 ′ ).β. By the induction
hypothesis and Lemma 7.14 (1), there is a value W such that V ⇒ W ⇐ (S 0 ′ ).β. Then, there exists
a N such that S 0 ′ = N • β, N ⇒ W, and β is not free in N from the above claim. Hence we have
D1 = S ′ [L/α] = S 0 ′ [α/β][L/α] = S 0 ′ [L/β] = (N • β)[L/β] = N • L. We then consider the subcases
(a) and (b).
The subcase of (a). By the induction hypothesis, there exists a statement T̃ such that (x • L) ⇒
T̃ ⇐ T ′ . Hence we have D1 = (x • L)[N/x] ⇒ T̃ [W/x] ⇐ T ′ [V/x] = D2 from N ⇒ W ⇐ V and
Lemma 7.14 (3).
The subcase of (b). By the induction hypothesis and T ′ ⇐ T ⇒ T ′′ , there exists T̃ such
that T ′ ⇒ T̃ ⇐ T ′′ . Hence we have D2 = T ′ [V/x] ⇒ T̃ [W/x] by Lemma 7.14 (3) and V ⇒ W.
We also have D1 = N • L = N • x.(T ′′ ) ⇒ T̃ [W/x] from N ⇒ W and T ′′ ⇒ T̃ . Therefore
D1 ⇒ T̃ [W/x] ⇐ D2 holds.
The other cases are also proved by the induction hypothesis.
From Lemma 7.15, we can obtain the Church-Rosser property of the weak call-by-value DCµν.
Proposition 7.16. The reduction relations −→wCBV and −→wCBN of DCµνcbv satisfy the Church-Rosser
property.
Proof. We first show the Church-Rosser property of −→wCBV . Suppose that D −→∗wCBV D′ and
D −→∗wCBV D′′ hold. We will show that there exists some E such that D′ −→∗wCBV E and D′′ −→∗wCBV
E. We have D = D00 −→wCBV D01 −→wCBV . . . −→wCBV D0n = D′ and D −→wCBV D10 −→wCBV
. . . −→wCBV D1m = D′′ for some n, m ≥ 0. By Lemma 7.15 (1), D ⇒ D01 ⇒ . . . ⇒ D0n = D′ and
′′
′′
D ⇒ D′′
10 ⇒ . . . ⇒ D1m = D hold. By the diamond property of ⇒, there exists D(i+1)( j+1) such
that Di( j+1) ⇒ D(i+1)( j+1) ⇐ D(i+1) j for each 0 ≤ i ≤ n − 1 and 0 ≤ j ≤ m − 1. Hence we have
D′ = D0n ⇒ D1n ⇒ . . . ⇒ Dmn and D′′ = Dm0 ⇒ Dm1 ⇒ . . . ⇒ Dmn . By Lemma 7.15 (2), we can
replace ⇒ by −→∗wCBV . Therefore, we have D′ −→∗wCBV Dmn and D′′ −→∗wCBV Dmn .

32

D. KIMURA AND M. TATSUTA

The Church-Rosser property of −→wCBN is shown by the former result and the duality between
−→wCBV and −→wCBN (Proposition 7.9).
We will next define the call-by-value and the call-by-name DCµν, which we call CBV DCµν and
CBN DCµν. The types, expressions, and typing rules of CBV DCµν and CBN DCµν are the same as them
of DCµν.
The reduction relation of CBV DCµν is obtained by adding ς-rules to the weak call-by-value
DCµν.
Definition 7.17 (Reduction relation of CBV DCµν). The reduction relation −→CBV of CBV DCµν is
defined by the compatible closure of the reduction rules of the weak call-by-value DCµν and (ς∧1 )v ,
(ς∧2 )v , (ς∨1 )v , (ς∨2 )v , and the following reduction rules:
(ςµ)v inµX.C hMi −→CBV (M • x.(inµX.C hxi • α)).α,
(ςν)v coitryA hM, Mi −→CBV (M • x.(coitryA hM, xi • α)).α,
where M is not a value of DCµν, and the variable x and the covariable α in (ςµ)v , (ςν)v are fresh.
We sometimes write (β)v to mean (β∧1 )v , (β∧2 )v , (β∨1 )v , (β∨2 )v , (β¬)v , (βµ)v , (βν)v , (βL)v , or
(βR)v -rule. We write (η)v to mean (ηL)v or (ηL)v -rule. We also write (ς)v to mean (ς∧1 )v , (ς∧2 )v ,
(ς∨1 )v , (ς∨2 )v , (ςµ)v , or (ςν)v -rule.
The reduction relation of CBN DCµν is obtained by adding ς-rules to the weak call-by-name
DCµν.
Definition 7.18 (Reduction relation of CBN DCµν). The reduction relation −→CBN of CBN DCµν is
defined by the compatible closure of the reduction rules of the weak call-by-name DCµν and (ς∧1 )n ,
(ς∧2 )n , (ς∨1 )n , (ς∨2 )n , and the following reduction rules:
(ςµ)n itrβA [K, K] −→CBN x.((x • itrβA [K, α]).α • K),
(ςν)n outνX.C [K] −→CBN x.((x • outνX.C [α]).α • K),
where K is not a covalue of DCµν, and the variable x and the covariable α in (ςµ)n , (ςν)n are fresh.
From the above definitions, CBV DCµν includes the weak call-by-value DCµν, and CBN DCµν
includes the weak call-by-name DCµν. That is, the following lemma holds.
Lemma 7.19. Let D and E be expressions of DCµν. Then, the following claims hold.
(1) If D −→wCBV E, then D −→CBV E.
(2) If D −→wCBN E, then D −→CBN E.
The call-by-value DCµν is dual to the call-by-name DCµν.
Proposition 7.20 (Duality between call-by-value and call-by-name in DCµν). Let D and E be expressions of DCµν. Then, D −→CBV E iff (D)◦ −→CBN (E)◦ , where (−)◦ is the duality transformation
of DCµν defined in the section 3.
The call-by-value and call-by-name DCµν satisfy both the Church-Rosser and strong normalization properties. We will concentrate to show these properties of CBV DCµν. The proof will be
performed by giving a transformation from CBV DCµν into the weak call-by-value DCµν. The transformation (−)⊛ given as follows.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

33

Definition 7.21. Let D be a expression of DCµν. The expression (D)⊛ of DCµν is defined inductively
as follows.
(x)⊛ = x,
(hV, Wi)⊛ = h(V)⊛ , (W)⊛ i,
(hV, Ni)⊛ = ((N)⊛ • y.(h(V)⊛ , yi • α)).α,
⊛ • x.(hx, (W)⊛ i • α)).α,
(hM, Wi)⊛ = ((M)


⊛
(hM, Ni) = (M)⊛ • x. ((N)⊛ • y.(hx, yi • β)).β • α .α,
(hViinl)⊛ = h(V)⊛ iinl,
(hMiinl)⊛ = ((M)⊛ • x.(hxiinl • α)).α,
(hViinr)⊛ = h(V)⊛ iinr,
(hMiinr)⊛ = ((M)⊛ • x.(hxiinr • α)).α,
([K]not)⊛ = [(K)⊛ ]not,
(inµX.AhMi)⊛ = ((M)⊛ • x.(inµX.Ahxi • α)).α,
(inµX.AhVi)⊛ = inµX.Ah(V)⊛ i,
(coitrzA hM, Vi)⊛ = coitrzA h(M)⊛ , (V)⊛ i,
(coitrzA hM, Ni)⊛ = ((N)⊛ • y.(coitrzA h(M)⊛ , yi • α)).α,
((S ).α)⊛ = ((S )⊛ ).α,
(α)⊛ = α,
([K, L])⊛ = [(K)⊛ , (L)⊛ ],
(fst[K])⊛ = fst[(K)⊛ ],
(snd[K])⊛ = snd[(K)⊛ ],
(nothMi)⊛ = noth(M)⊛ i,
(outνX.A[K])⊛ = outνX.A[(K)⊛ ],
(itrγA [K, L])⊛ = itrγA [(K)⊛ , (L)⊛ ],
(x.(S ))⊛ = x.((S )⊛ ), and
(M • K)⊛ = (M)⊛ • (K)⊛ ,
where V and W are values, M and N are not values, and x, y, α, β are fresh.
We need the redundant definition of (hM, Ni)⊛ for a technical reason, and it is necessary in
order to show Proposition 7.25.
The transformation (−)⊛ preserves typing.
Proposition 7.22. Let M be a term, K be a coterm, and S be a statement of DCµν. The following
claims hold.
(1) If Γ ⊢DCµν ∆ | M : A is provable, then Γ ⊢DCµν ∆ | (M)⊛ : A holds.
(2) If K : A | Γ ⊢DCµν ∆ is provable, then (K)⊛ : A | Γ ⊢DCµν ∆ holds.
(3) If Γ | S ⊢DCµν ∆ is provable, then Γ | (S )⊛ ⊢DCµν ∆ holds.
Proof. They are shown simultaneously by induction on M, K, and S .
The transformation (−)⊛ satisfies the following basic properties.
Lemma 7.23. Let V be a value, M and N be terms, D be an expression of DCµν. Then the following
claims hold.
(1) M is a value iff (M)⊛ is a value.
(2a) h(M)⊛ , (N)⊛ i −→∗wCBV (hM, Ni)⊛ .
(2b) h(M)⊛ iinl −→∗wCBV (hMiinl)⊛ , and h(M)⊛ iinr −→∗wCBV (hMiinr)⊛ .
(2c) inµX.Ah(M)⊛ i −→∗wCBV (inµX.AhMi)⊛ .

34

D. KIMURA AND M. TATSUTA

(2d) coitrzA h(M)⊛ , (N)⊛ i −→wCBV (coitrzA hM, Ni)⊛ .
⊛
⊛
∗
X.A
⊛
(3a) monoX.A
B,C,x {(M) , (N) } −→wCBV (monoB,C,x {M, N}) .
X.A
⊛
X.A {(K)⊛ , (L)⊛ } −→∗
(3b) monoB,C,α
wCBV (mono B,C,α {K, L}) .
(4) D −→∗CBV (D)⊛ .

Proof. The claim (1) is shown by the definition of (−)⊛ . The claims (2a), (2b), (2c), and (2d) are
shown by (1) and ς-rules. The claims (3a) and (3b) are shown by induction on ||C||X using (2a),
(2b), (2c), and (2d). The claim (4) is shown by induction on D.
The transformation (−)⊛ preserves substitution of a value for a variable, and of a coterm for a
covariable.
Lemma 7.24. (D[V/x])⊛ = (D)⊛ [(V)⊛ /x] and (D[K/α])⊛ = (D)⊛ [(K)⊛ /α].
Proof. The former claim is shown by induction on D using Lemma 7.23 (1). The latter one is shown
by induction on D.
The transformation (−)⊛ translates one step reduction of −→CBV into zero or more steps reduction of −→wCBV .
Proposition 7.25. D −→CBV E implies (D)⊛ −→∗wCBV (E)⊛ . In particular, if D −→CBV E by (β)v or
(η)v , then (D)⊛ −→+wCBV (E)⊛ holds.
Proof. The claim is shown by induction on the definition of −→CBV . We show the cases of (βL)v ,
(βµ)v , and (ς∧1 )v .
The case of (βL)v is proved by Lemma 7.24. We have (V • x.(S ))⊛ = (V)⊛ • x.((S )⊛ ) −→wCBV
⊛
(S ) [(V)⊛ /x]. By Lemma 7.24, the last statement is (S [V/x])⊛ .
The case of (βµ)v is proved by Lemma 7.23 (3b). We have (inµX.C hVi • itrαA [K, L])⊛ =
µX.C
X.C
in
h(V)⊛ i • itrαA [(K)⊛ , (L)⊛ ] −→wCBV ((V)⊛ • monoµX.C,A,β
{ itrαA [(K)⊛ , β], (K)⊛ }).α • (L)⊛ =
X.C
((V)⊛ • monoµX.C,A,β
{ (itrαA [K, β])⊛ , (K)⊛ }).α • (L)⊛ . By Lemma 7.23 (3b), the last statement is
X.C
reduced to ((V)⊛ • (monoµX.C,A,β
{ itrαA [K, β], K })⊛ ).α • (L)⊛ by −→∗wCBV . Therefore this statement is
X.C
((V • monoµX.C,A,β
{ itrαA [K, β], K }).α • L)⊛ .
The case of (ς∧1 )v is proved by the definition of (−)⊛ . We consider the subcase of
hM,
Ni −→CBV (M • x.(hx, Ni • α)).α,where M and N are not values. Hence we have (hM, Ni)⊛ =



 
(M)⊛ • x. ((N)⊛ • y.(hx, yi • β)).β • α .α = (M)⊛ • x. (hx, Ni)⊛ • α .α = M • x. hx, Ni • α .α ⊛ .
The other subcase of (ς∧1 )v for hN, Vi with a non-value N is shown in the similar way.
The other cases are also shown by the induction hypothesis.
Then we can show the Church-Rosser property of −→CBV and −→CBN .
Theorem 7.26. The reduction relations −→CBV of CBV DCµν and −→CBN of CBN DCµν satisfy the
Church-Rosser property.
Proof. We first show the Church-Rosser property of −→CBV .
Assume that D −→∗CBV D′ and D −→∗CBV D′′ hold. By Proposition 7.25, we have (D)⊛ −→∗wCBV
′
⊛
(D ) and (D)⊛ −→∗wCBV (D′′ )⊛ . By the Church-Rosser property of −→wCBV , there exists E such that
(D′ )⊛ −→∗wCBV E and (D′′ )⊛ −→∗wCBV E. Therefore, by Lemma 7.19 (1) and Lemma 7.23 (4), we
have D′ −→∗CBV (D′ )⊛ −→∗CBV E and D′′ −→∗CBV (D′′ )⊛ −→∗CBV E.
The Church-Rosser property of −→CBN is shown by the former result and the duality between
−→CBV and −→CBN (Prop 7.20).

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

35

We will prove strong normalization of CBV DCµν and CBN DCµν. This property is shown by
using the strong normalization result of the weak call-by-value and the weak call-by-name DCµν
(Proposition 7.11).
We define the following rank of expressions in DCµν. This rank is used to show that there is no
infinite sequence of ς-rules.
Definition 7.27. Let D be an expression in DCµν. The rank r(D) of D is defined by:
r(x) = r(α) = 0,
r([K]not) = r(fst[K]) = r(snd[K]) = r(outνX.A[K]) = r(K),
r([K, L]) = r(itrαA [K, L]) = r(K) + r(L),
r(nothMi) = r(M),
r(hM, Ni) = r(M) + r(N) + 2,
r(hM, Vi) = r(hV, Mi) = r(M) + r(V) + 1,
r(hV, Wi) = r(V) + r(W),
r(hMiinl) = r(hMiinr) = r(inµX.AhMi) = r(M) + 1,
r(hViinl) = r(hViinr) = r(inµX.AhVi) = r(V),
r(coitrAx hM, Ni) = r(M) + r(N) + 1,
r(coitrAx hM, Vi) = r(M) + r(V),
r(x.(S )) = r((S ).α) = r(S ), and
r(M • K) = r(M) + r(K),
where V and W are values, and M and N are not values.
The rank r(D) counts the number of redexes of (ς∧1 )v , (ς∧2 )v , (ς∨1 )v , (ς∨2 )v , (ςµ)v , and (ςν)v rules. We write D −→ςv E when D is reduced to E by one step (ς)v -reduction.
Lemma 7.28. Let D and E be expressions of DCµν. Then, the following claims hold.
(1) If D −→ςv E, then r(D) > r(E).
(2) There is no infinite sequence of (ς)v -reduction.
Proof. The claim (1) is shown by induction on D. The claim (2) is shown by (1).
We then show strong normalization of CBV DCµν and CBN DCµν.
Theorem 7.29 (Strong normalization of CBV DCµν and CBN DCµν). The following claims hold.
(1) Every typable expression is strongly normalizing in CBV DCµν.
(2) Every typable expression is strongly normalizing in CBN DCµν.
Proof. We first show the call-by-value case. Assume that D is typable in DCµν and there is an infinite
reduction sequence
D −→CBV D1 −→CBV . . .
starting from D. Then (D)⊛ is typable by Proposition 7.22, and we have
(D)⊛ −→∗wCBV (D1 )⊛ −→∗wCBV . . .
by Proposition 7.25. From the strong normalization result of the weak call-by-value DCµν (Proposition 7.11), there is some Dk such that
(Dk )⊛ = (Dk+1 )⊛ = . . . .
By the latter part of Proposition 7.25, we have the following infinite sequence of (ς)v -reduction:
Dk −→ςv Dk+1 −→ςv . . . .

36

D. KIMURA AND M. TATSUTA

This contradicts Lemma 7.28 (2).
The call-by-name case is proved by strong normalization of CBV DCµν and the duality between
CBV DCµν and CBN DCµν (Proposition 7.20).
8. Conclusion
We have introduced the non-deterministic system DCµν by extending the dual calculus given in [27]
with inductive types and coinductive types. Besides the same duality of the original dual calculus,
we have shown the duality of inductive and coinductive types, by giving the involution that maps
terms and coterms for inductive types to coterms and terms of coinductive types respectively and
vice versa, and maps their reduction rules to each other. We have proved its strong normalization
by translating it into the second-order dual calculus DC2.
The second-order dual calculus DC2 also have been introduced. Its strong normalization have
been shown by translating it into the second-order symmetric lambda calculus.
We have finally introduced the call-by-value system CBV DCµν and the call-by-name system
CBN DCµν of the dual calculus with inductive and coinductive types. We have shown the duality of
call-by-value and call-by-name with inductive and coinductive types, their Church-Rosser property,
and their strong normalization. Their strong normalization have been shown by translating them
into DCµν.
The first author introduced the call-by-value and call-by-name dual calculi with recursive
types [11, section 4.2]. In these systems, a recursive type rec X.A can be defined for any type
A. If we assume that rec X.A can be defined only if every X positively occurs in A, then we can
define two provability-preserving transformations from the dual calculi with recursive types into
DCµν. The one translates a recursive type to an inductive type, and the other translates a recursive
type to a coinductive type. We could not straightforwardly show that these transformations preserve
reductions (or equations) since some additional rules such as η-rules for connectives seem to be
required. This problem would be future work.
The duality of call-by-value and call-by-name in λµ-calculus is shown by using the dual calculi
in [28]. Since our systems CBV DCµν and CBN DCµν are extensions of his dual calculi, we could
show the duality of call-by-value and call-by-name in λµ-calculus with inductive and coinductive
definitions, by using our systems CBV DCµν and CBN DCµν. It would be future work.
A reduction-based duality between call-by-value and call-by-name in the λµ-calculi was presented in [12], by refining Wadler’s result [28]. Extending the result given in [12] with inductive
and coinductive types would be future work.
Our systems use the iteration for inductive types. An extension of the iteration to primitive
recursion would be future work.
A CPS translation from the dual calculus to λ-calculus was given in [27]. Extending this CPS
translation to the systems with inductive and coinductive types would be future work.
Acknowledgment
We would like to thank Professor Philip Wadler for discussions and suggestions. We would also
like to thank Dr. Alwen Tiu, and Professor Dieter Spreen for discussions. We would also like to
thank anonymous referees for valuable comments.

CALL-BY-VALUE AND CALL-BY-NAME DUAL CALCULI WITH INDUCTIVE AND COINDUCTIVE TYPES

37

References
[1] D. Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic, 13 (1): Article
2, 2012.
[2] F. Barbanera and S. Berardi. A symmetric lambda calculus for classical program extraction. Information and Computation, 125 (2): 103–117, 1996.
[3] W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg. Iterated inductive definitions and subsystems of analysis:
Recent proof-theoretical studies. Lecture Notes in Mathematics, 897, Springer, 1981.
[4] P.-L. Curien and H. Herbelin. The duality of computation. In Proceedings of the 5th ACM SIGPLAN International
Conference on Functional Programming (ICFP), 233–243, 2000.
[5] A. Filinski. Declarative continuations and categorical duality. Master’s thesis, Computer Science Department, University of Copenhagen, DIKU Report 89/11, 1989.
[6] H. Geuvers. Inductive and coinductive types with iteration and recursion. In Proceedings of the 1992 workshop on
Types for Proofs and Programs (TYPES), 183–207, 1992.
[7] J-Y. Girard. Proof theory and logical complexity, Bibliopolis, 1987.
[8] T.G. Griffin. A formulae-as-types notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 47–58, 1990.
[9] H. Herbelin. C’est maintenant qu’on calcule au cœur de la dualité Hablitiation à deriger les recherches, L’Universitê
Paris 11, 2005.
[10] Y. Kakutani. Duality between call-by-name recursion and call-by-value iteration. In Proceedings of the 16th International Workshop on Computer Science Logic, CSL, Lecture Notes in Computer Science 2471: 506–521, 2002.
[11] D. Kimura. Call-by-value is dual to call-by-name, extended. In Proceedings of Programming Languages and Systems, 5th Asian Symposium (APLAS), Lecture Notes in Computer Science, 4807: 415–430, 2007.
[12] D. Kimura. Duality between call-by-value reductions and call-by-name reductions. IPSJ Journal, 48(4): 1721–1757,
2007.
[13] D. Kimura and M. Tatsuta. Dual calculus with inductive and coinductive types. In Proceedings of 20th International
Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, 5595: 224–238,
2009.
[14] R. McDowell and D. Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232 (1-2): 91–119, 2000.
[15] N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied
Logic, 51 (1-2): 159–172, 1991.
[16] A. Momigliano and A. Tiu. Induction and co-induction in sequent calculus. Types for Proofs and Programs International Workshop (TYPES), Revised Selected Papers, Lecture Notes in Computer Science, 3085: 293–308, 2004.
[17] A. Tiu and Momigliano. Cut elimination for a logic with induction and co-induction. manuscript, available at
arxiv.org, 2010.
[18] Nordström, B., Petersson, K. and Smith, J.M. Programming in Martin-Löf’s type theory. Oxford University Press,
1990.
[19] M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural deduction. In Proceedings of International
Conference on Logic Programming and Automated Deduction (LPAR), Lecture Notes in Computer Science, 624:
190–201, 1992.
[20] M. Parigot. Strong normalization for second order classical natural deduction. In Journal of Symbolic Logic, 62(4):
1461–1479, 1997.
[21] M. Parigot. Strong normalization of second order symmetric lambda-calculus. In Proceedings of Foundations of
Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, 1974: 442–453,
2000.
[22] C. Paulin-Mohring. Inductive definitions in the system Coq — Rules and properties. In Proceedings of Typed
Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science, 664: 328–345, 1993.
[23] P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical
Structures in Computer Science, 207–260, 2001.
[24] M. Tatsuta. Realizability interpretation of coinductive definitions and program synthesis with streams. Theoretical
Computer Science, 122(1–2): 119–136, 1994.

38

D. KIMURA AND M. TATSUTA

[25] M. Tatsuta. Simple saturated sets for disjunction and second-order existential quantification. In Proceedings of 8th
International Conference on Typed Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science,
4583: 366–380, 2007.
[26] N. Tzevelekos. Investigations on the dual calculus. Theoretical Computer Science, 360: 289–326, 2006.
[27] P. Wadler. Call-by-value is dual to call-by-name. In Proceedings of International Conference on Functional Programming (ICFP), 189–201, 2003.
[28] P. Wadler. Call-by-value is dual to call-by-name, reloaded, In Proceedings of Rewriting Techniques and Applications
(RTA), Lecture Notes in Computer Science, 3467: 185–203, 2005.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy
of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a letter to
Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher
Strasse 2, 10777 Berlin, Germany

