Calculi for Intuitionistic Normal Modal Logic

∗

Yoshihiko Kakutani

arXiv:1606.03180v1 [cs.LO] 10 Jun 2016

Department of Information Science, University of Tokyo
kakutani@is.s.u-tokyo.ac.jp

Abstract
This paper provides a call-by-name and a call-by-value term calculus,
both of which have a Curry-Howard correspondence to the box fragment
of the intuitionistic modal logic IK. The strong normalizability and the
confluency of the calculi are shown. Moreover, we define a CPS transformation from the call-by-value calculus to the call-by-name calculus, and
show its soundness and completeness.

1

Introduction

It is well-known that the intuitionistic propositional logic exactly corresponds
to the simply typed λ-calculus: formulae as types and proofs as terms. Such a
correspondence is called a Curry-Howard correspondence after [12]. A CurryHoward correspondence enables us to study an equality on proofs of a logic
computationally. Though Curry-Howard correspondences for higher-order and
predicate logics were provided in [3], we investigate only propositional logics
in this paper. The aim of this study is to give a proper calculus that have a
Curry-Howard correspondence with a modal logic.
Modal logics have a long history and are now widely studied both theoretically and practically. Especially, studies about Kripke semantics [14] of modal
logics are quite active. Curry-Howard correspondences of modal logics are, however, less studied except for linear logics [9]. (In fact, exponentials of linear logics
are a kind of S4 modality.) Since K is known to be the simplest modal logic,
first we focus the intuitionistic modal logic IK. A difficulty of a calculus for
K is lack of acknowledged models. Because a model of the modality in call-byname S4 is acknowledged as a monoidal comonad, a model of the modality in
K should be a generalization of a monoidal comonad. This paper defines a callby-name calculus, which is called the λ2-calculus, based on a categorical model
proposed by Bellin et al. in [4]. Another difficulty is a problem about natural
deductions of modal logics pointed out in [24]. A solution of the problem in IS4
is found in [2], but it cannot be applied to IK. The formulation of [4] and this
paper is a natural deduction style, and solves this problem.
On the other hand, studies on Curry-Howard correspondences for modal
logics, especially IS4, are applied to staged computations and information flow
∗ This paper was reported at PPL 2007. The results of this paper have already been
published as DOI:10.11309/jssst.25.1 167 written in Japanese.

1

Γ ` cτ : τ
Γ, x : τ, Γ 0 ` x : τ
Γ, x : σ ` M : τ
Γ ` λxσ. M : σ ⊃ τ
Γ ` M :σ⊃τ
Γ ` N :σ
Γ ` MN : τ
x1 : σ1 , . . . , x n : σn ` M : τ
Γ ` N1 : 2σ1
···
Γ ` Nn : 2σn
σ1
σn
Γ ` box hx1 , . . . , xn i be hN1 , . . . , Nn i in M : 2τ
Figure 1: Typing rules of λ2-calculus
analysis (e.g., [6], [17]) in the field of programming languages. Since our λ2calculus can be extended easily to IT, IK4, IS4, and so on, this work is expected
to contribute such programming language matters.
This paper provides not only a call-by-name calculus but also a call-by-value
one. A call-by-value calculus is usually defined by a CPS transform, which
is originally introduced by [8] and [23]; for example, a call-by-value control
operator is defined by a CPS transform in [7]. In [25], Sabry and Felleisen
showed that the λc -calculus [19] is sound and complete for CPS semantics. We
give the call-by-value λ2-calculus as an extension of the λc -calculus. Moreover,
we define a CPS transformation from the call-by-value λ2-calculus to the callby-name λ2-calculus. The soundness and completeness for the CPS semantics
are shown along the line of [25].

2

Call-by-Name Calculus

−
→
First, we remark special notations used in this paper. We use a notation “M ”
for a sequence of meta-variables “M1 , . . . , Mn ” including the empty sequence.
−
→ →
−
−
→
→
−
Hence, an expression “M , N ” stands for the concatenation of M and N . For a
−
→
unary operator Φ(−), we write “Φ(M )” for the sequence “Φ(M1 ), . . . , Φ(Mn )”.
→
− −
We use also “ N (λ→
x . M )” as an abbreviation for “N1 (λx1 . · · · Nn (λxn . M ) · · ·)”.
A hole in a context is represented by “−” in this paper. For a context C,
“C[M ]” denotes the result of filling holes in C with M as usual.
Definition 1. Types σ and terms M of the call-by-name λ2-calculus are defined
as follows:
σ ::= p | σ ⊃ σ | 2σ,
M ::= c | x | λxσ. M | M M | box hxσ, . . . , xσi be hM, . . . , M i in M,
where p, c, and x range over type constants, constants, and variables, respec→
−
→
−
−
tively. Free variables of box h→
x i be h N i in M are free variables of N . The
typing rules are given in Figure 1. The reduction rules are given in Figure 2.
Define n as the set {β⊃ , η⊃ , id2 , β2 }.
−
−
We remark that all free variables of M are included by {→
x } if box h→
x i be
→
−
h N i in M is typable.
2

(λx. M )N −→β⊃ M {N/x}
λx. M x −→η⊃ M

x 6∈ FV(M )

box hxi be hM i in x −→id2 M
→
−
→
−
→
−
−
−
−
box h→
w , x, →
z i be h P , box h→
y i be h L i in N, Q i in M
→
− →
− →
−
−
−
−
−→β2 box h→
w,→
y ,→
z i be h P , L , Q i in M {N/x}

→
−
−
|→
w | = |P |

Figure 2: Call-by-name reductions of λ2-calculus
The λ2-calculus has essentially the same syntax as [4]. Hence, one can see
that our calculus corresponds to the intuitionistic modal logic. The calculus can
be regarded as a natural deduction by forgetting terms. Our logic is equivalent
to the ⊃2-fragment of the usual intuitionistic modal logic IK with respect to
provability. Let IK be an intuitionistic Hilbert system with the axiom 2(σ ⊃
τ ) ⊃ 2σ ⊃ 2τ and the box inference rule. The axiom is validated in our calculus
as the term
` λf. λx. box hf 0 , x0 i be hf, xi in f 0 x0 : 2(σ ⊃ τ ) ⊃ 2σ ⊃ 2τ .
The box rule is simulated as
` M :τ
` box hi be hi in M : 2τ .
Conversely, the typing rule of the λ2-calculus is simulated by IK:
σ1 , . . . , σn ` τ
` σ1 ⊃ · · · ⊃ σn ⊃ τ
` 2(σ1 ⊃ · · · ⊃ σn ⊃ τ )
Γ ` 2(σ1 ⊃ · · · ⊃ σn ⊃ τ )
Γ ` 2σ1 ⊃ 2(σ2 ⊃ · · · ⊃ σn ⊃ τ )
Γ ` 2σ1
Γ ` 2(σ2 ⊃ · · · ⊃ σn ⊃ τ )
..
.
Γ ` 2(σn ⊃ τ )
Γ ` 2σn ⊃ 2τ
Γ ` 2τ

Γ ` 2σn
.

According to this encoding, it is not trivial whether an exchange rule commutes with a box operation. Hence, we distinguish two terms, box hx, yi be
hN, Li in M and box hy, xi be hL, N i in M , in the λ2-calculus, although it is
common to consider proofs up to exchanges. Commutativity with exchanges
requires another axiom, symmetricity, given in Section 6.
Remark 1. The typing rules of our calculus are the same as those of Bellin et
al.’s [4], but reductions are essentially different. In [4], they addresses natural
deduction style formulation and categorical semantics, but not a term calculus
itself, so their calculus has room for improvement. Differences between Bellin
et al.’s calculus and our λ2-calculus are the following.
3

• The first reduction of their calculus corresponds to a special case of −→β2 .
• The direction of the first reduction is opposite to −→β2 : our reduction
merges adjacent two boxes into one box, while their reduction splits a box
into two boxes.
• The second reduction of their calculus cannot be applied to any typable
term.
• Their calculus does not have a reduction corresponding to −→id2 .
Though Bellin et al.’s calculus does not have the semantic completeness, it has
syntax for a diamond property. Intuitionistic characterization of a diamond
property is not obvious, but the author has observed a diamond property in the
classical modal logic K in [13].
For a set of labels X, we write −→X as a reduction whose label is a member
of X, and =X as the reflexive transitive symmetric closure of −→X . We also
use ≡ for the α-equivalence.
We can easily check the subject reduction theorem for this calculus.
Proposition 1. If Γ ` M : τ and M −→n N hold, then Γ ` N : τ holds.
Other important properties, the strong normalizability and the confluency,
also hold.
Proposition 2. The call-by-name λ2-calculus is strongly normalizable with
respect to −→n .
Proof. Define the transformation d−e to the simply typed λ-calculus by
→
−
→
−
−
−
dbox h→
x i be h N i in M e = λk. d N e(λ→
x . kdM e).
Then, M : τ implies dM e : dτ e if we define the type transformation d−e by
d2τ e = (dτ e ⊃ p) ⊃ p. One can see that dbox hxi be hM i in xe −→+
η⊃ dM e and
→
−
→
−
→
−
−
−
−
dbox h→
w , x, →
z i be h P , box h→
y i be h L i in N, Q i in M e
→
−
→
−
→
−
−
−
−
≡ λk. d P e(λ→
w . (λh. d L e(λ→
y . hdN e))(λx. d Q e(λ→
z . kdM e)))
→
−
→
−
→
−
→
−
→
−
→
−
−→ λk. d P e(λ w . d L e(λ y . (λx. d Q e(λ z . kdM e))dN e))
β⊃

→
−
→
−
→
−
−
−
−
−→β⊃ λk. d P e(λ→
w . d L e(λ→
y . d Q e(λ→
z . kdM e{dN e/x})))
→
−
→
−
→
−
→
−
→
−
→
−
≡ λk. d P e(λ w . d L e(λ y . d Q e(λ z . kdM {N/x}e)))
→
− →
− →
−
−
−
−
≡ dbox h→
w,→
y ,→
z i be h P , L , Q i in M {N/x}e
hold. Because the simply typed λ-calculus is SN w.r.t. −→β⊃ ,η⊃ (e.g., q.v. [10]),
the call-by-name λ2-calculus is SN.
We note here that the strong normalization theorem was proved via a different calculus in [1].
Proposition 3. −→n is confluent.

4

Proof. By Newman’s lemma [20], it is sufficient to check the local confluency.
The call-by-name λ2-calculus has essentially four kinds of critical pairs other
than pairs of the λ-calculus:
→
−
→
−
/−→id2 box h y i be h L i in N
→
−
−
box hxi be hbox h→
y i be h L i in N i in x
→
−
−
−→β2 box h→
y i be h L i in N,

\

/−→id2

box hxi be hN i in M

box hxi be hbox hyi be hN i in yi in M
\

−→β2 box hyi be hN i in M {y/x},
→
−
−
−→ box hyi be hbox h→
z i be h P i in Li in M {N/x}

/

β2

→
−
−
box hxi be hbox hyi be hbox h→
z i be h P i in Li in N i in M
→
−
−
\
−→ box hxi be hbox h→
z i be h P i in N {L/y}i in M,
β2

→
−
→
−
→
−
−
box h→
y , x0 i be h L , box h y 0 i be hL0 i in N 0 i in M {N/x}
→
−
→
−
→
−
−
box hx, x0 i be hbox h→
y i be h L i in N, box h y 0 i be hL0 i in N 0 i in M
→
−
→
−
→
−
−
\
−→β2 box hx, y 0 i be hbox h→
y i be h L i in N, L0 i in M {N 0 /x0 }.
/−→β2

It is easily shown that all the pairs are joinable.
Last, we mention the subformula property of this calculus.
Theorem 4. A normal form in the call-by-name λ2-calculus has the subformula
property.
→
−
−
Proof. By induction on construction of terms. If box h→
x i be h N i in M is a
normal form, then M is a normal form and each Ni has a form yL1 · · · Lm .
Therefore, the subformula property holds in this case by the induction hypothesis. Other cases are just the same as the simply typed λ-calculus.
A characterization of the λ2-calculus by a standard translation into the
predicate logic is given by Abe in [1]. Since our motivation arises from logics
and categorical semantics, computational meaning of the calculus still remains
to be studied. We believe the following discussions are helpful.
Because the logic IK is weaker than the logic IS4, the λ2-calculus is expected to be a subcalculus of a calculus for IS4. A method for extending the
λ2-calculus to IS4 is discussed in Section 6. Through this approach, computational analyses of IS4 calculi might be applied to the λ2-calculus.
Another approach to understand computational meaning of the λ2-calculus
is to investigate a relation to monads. It is remarkable that the transformation
d−e mentioned in the proof of Proposition 2 preserves the equality. It means
that 2 in the λ2-calculus can be interpreted as a continuation monad in the
λ-calculus. In fact, such a transformation exists for any strong monad because
a strong monad is a lax monoidal endofunctor. Hence, we can conclude that
the λ2-calculus includes an abstract setting of strong monads. In [16], McBride
and Paterson have studied a structure abstracting a strong monad. It must be
strongly related to our calculus though their formulation has a tensorial strength
with respect to cartesian products.
5

V, W : value
C : simple evaluation context
E : evaluation context
(λx. x)M −→id⊃ M
v M {V /x}
(λx. M )V −→β⊃

x 6∈ FV(V )

v V
λx. V x −→η⊃

C[(λx. M )N ] −→lift (λx. C[M ])N
C[yM ] −→flat (λx. C[x])(yM )

C 6= V −

(λx. E[yx])M −→βΩ E[yM ]

x 6∈ FV(E[y])

box hxi be hM i in x −→id2 M
−
→
→
−
→
−
−
−
−
box h→
w , x, →
z i be hW , box h→
y i be h N i in V, P i in M
−
→ →
− →
−
−
−
−
−→β2v box h→
w,→
y ,→
z i be hW , N , P i in M {V /x}

−
→
−
|→
w | = |W |

Figure 3: Call-by-value reductions of λ2-calculus

3

Call-by-Value Calculus

Definition 2. Types σ, terms M , values V , simple evaluation contexts C, and
evaluation contexts E of the call-by-value λ2-calculus are defined as follows:
σ ::= p | σ ⊃ σ | 2σ,
M ::= c | x | λxσ. M | M M | box hxσ, . . . , xσi be hM, . . . , M i in M,
V ::= c | x | λxσ. M | box hxσ, . . . , xσi be hV, . . . , V i in M,
C ::= −M | V − | box hxσ, . . . , xσi be hV, . . . , V, −, M, . . . , M i in M,
E ::= − | C[E].
The typing rules are just the same as the call-by-name. The reduction rules are
v
v
v
, η⊃
, lift, flat, βΩ , id2 , β2
}.
given in Figure 3. Define v as the set {id⊃ , β⊃
Proposition 5. If Γ ` M : τ and M −→v N hold, then Γ ` N : τ holds.
Since the definition of terms and the typing rules are the same as those of
the call-by-name calculus, also the call-by-value λ2-calculus corresponds to IK.
In order to define CPS semantics, however, we restrict terms as follows:
M ::= c | x | λxσ. M | M M | box hxσ, . . . , xσi be hM, . . . , M i in V.
These terms are closed under call-by-value reductions because values are closed
under substitutions. Hence, we can say that the full call-by-value calculus is a
conservative extension of the restricted version. In the rest of this section (and
the first half of the next section), we focus on this restricted calculus.
Our call-by-value λ2-calculus is an extension of Sabry and Felleisen’s calculus in [25]. As mentioned in [25], it is equivalent to the λc -calculus [19], which
is acknowledged as a call-by-value language, with respect to equalities. We give
CPS semantics of the call-by-value λ2-calculus and show the soundness and
completeness along the line of [25].
6

p=p
σ ⊃ τ = (τ ⊃ R) ⊃ σ ⊃ R
2σ = 2σ
x=x
c=c
λx. M = λk. λx. [[M ]]k
→
−
→
−
−
−
box h→
x i be h U i in V = box h→
x i be h U i in V
[[x]] = λk. kx
[[c]] = λk. kc
[[λx. M ]] = λk. k(λx. M )
[[M N ]] = λk. [[M ]](λy. [[N ]](yk))
−
→
−
→ −
−
−
−
[[box h→
x i be hM i in V ]] = λk. [[M ]](λ→
y . k(box h→
x i be h→
y i in V ))
Figure 4: CPS transformation with 2
Definition 3. The CPS transformation [[−]] from the call-by-value λ2-calculus
to the call-by-name λ2-calculus is defined by Fig 4. We write Φ(M, K) for the
administrative normal form of [[M ]]K.
Proposition 6. If x1 : σ1 , . . . , xn : σn ` M : τ holds, x1 : σ1 , . . . , xn : σn ` [[M ]] :
(τ ⊃ R) ⊃ R holds.
Definition 4. The CPS language is defined as a subcalculus of the call-by-name
λ2-calculus:
V ::= c | x | λk. K | box hx, . . . , xi be hV, . . . , V i in V,
K ::= k | λx. A | V K,
A ::= KV | (λk. A)K.
The transformation Ψ (−) from the CPS language to the call-by-value λ2calculus is defined by Fig 5.
Proposition 7. The CPS language is closed under −→n .
The following lemma is the core of the soundness and completeness. An
outline of the proof is just the same as [25]’s.
Lemma 8.

1. M −→lift,flat N implies Φ(M, k) ≡ Φ(N, k).

+
v ,β v ,β ,id ,β v N implies Φ(M, k) −→
2. M −→id⊃ ,β⊃
n Φ(N, k).
2 2
⊃ Ω

3. M −→n N implies Ψ (M ) −→∗v Ψ (N ).
4. M −→∗lift,flat Ψ (Φ(M, k)).

7

Ψ (c) = c
Ψ (x) = x
Ψ (λk. k) = λx. x
Ψ (λk. λx. A) = λx. Ψ (A)
Ψ (λk. V K) = λx. Ψ (V Kx)
→
−
→
−
−
−
Ψ (box h→
x i be h U i in V ) = box h→
x i be hΨ ( U )i in Ψ (V )
Ψ (k) = −
Ψ (λx. A) = (λx. Ψ (A))−
Ψ (cK) = Ψ (K)[c−]
Ψ (xK) = Ψ (K)[x−]
Ψ ((λk. H)K) = Ψ (H{K/k})
Ψ (KV ) = Ψ (K)[Ψ (V )]
Ψ ((λk. A)K) = Ψ (A{K/k})
Figure 5: Inverse of CPS transformation
Theorem 9. For λ2-terms M and N , M =v N holds if and only if [[M ]] =n [[N ]]
holds.
The lemma helps us to prove the strongly normalizing property and the
confluency of the call-by-value λ2-calculus too.
Proposition 10. The call-by-value λ2-calculus is strongly normalizable with
respect to −→v .
Proof. There is no infinite sequence of −→lift and −→flat . Therefore, if there
is an infinite reduction sequence in the call-by-value λ2-calculus, there is an
infinite reduction sequence in the call-by-name calculus via Φ(−, k).
Proposition 11. −→v is confluent.
Proof. Although the confluency can be shown directly, we prove it using the
lemma and the confluency of the call-by-name λ2-calculus. Assume M −→∗v N1
and M −→∗v N2 . Since Φ(M, k) −→∗n Φ(Nj , k), there is a term L such that
Φ(Nj , k) −→∗n L. Ψ (L) is an evidence of confluence.

4

Other Formulations of Call-by-Value

Although it has been shown that the call-by-value λ2-calculus has expected
properties, we can propose another call-by-value axiomatization following [18].
Definition 5. Define the computational λ2-calculus by adding the new syntax
let x be N in M to the syntax of the call-by-value λ2-calculus. The reduction
rules of the computational λ2-calculus are given in Figure 6. Define c as the
v
v
v
v
set {idlet , βlet
, β⊃
, η⊃
, comp, let, id2 , β2
}.

8

V, W : value
A : non-value
C : simple evaluation context
let x be M in x −→idlet M
v
let x be V in M −→βlet
M {V /x}
v M {V /x}
(λx. M )V −→β⊃

x 6∈ FV(V )

v V
λx. V x −→η⊃

let x be (let y be L in N ) in M
−→comp let y be L in let x be N in M

y 6∈ FV(M )

C[A] −→let let x be A in C[x]
box hxi be hM i in x −→id2 M
−
→
→
−
→
−
−
−
−
box h→
w , x, →
z i be hW , box h→
y i be h N i in V, P i in M
−
→ →
− →
−
−
−
−
−→β2v box h→
w,→
y ,→
z i be hW , N , P i in M {V /x}

−
→
−
|→
w | = |W |

Figure 6: Computational reductions of λ2-calculus
Proposition 12. If Γ ` M : τ and M −→c N hold, then Γ ` N : τ holds.
It is easily seen that the computational λ2-calculus is equivalent to the
previous call-by-value λ2-calculus with respect to equalities.
Proposition 13. For λ2-terms M and N , M =v N holds if and only if M =c
N holds.
We can show the strong normalization theorem of the computational λ2calculus via the strong normalizability of the λc -calculus.
Proposition 14. The computational λ2-calculus is strongly normalizable with
respect to −→c .
Proof. Define b−c into the typed λc -calculus by
→
−
→
− −
−
bbox h→
x i be h V i in M c = bM c{b V c/→
x },
→
−
→
−
→
−
→
−
bbox h w , x, z i be h V , A, N i in M c
→
−
→
−
−
−
= let y be bAc in bbox h→
w , x, →
z i be h V , y, N i in M c.
One can see that bV c is a value when V is a value, remembering that boxed
−
→
−
terms are restricted to the form box h→
x ibehM i in V . Let −→let2 be the special
case of −→let :
−
→
→
−
−
−
box h→
w , x, →
z i be hW , A, P i in M
−
→ →
−
−
−
−→
let y be A in box h→
w , x, →
z i be hW , y, P i in M
let2

−
→
−
|→
w | = |W |.

It can be checked that M −→id2 ,β2v ,let2 N implies bM c −→∗c bN c, otherwise,
M −→c N implies bM c −→c bN c. Because we know the λc -calculus is SN
9

(it was proved by Hasegawa in [11]), it is sufficient to show there is no infinite
sequence that consists of −→id2 , −→β2v , and −→let2 .
We extend the transformation d−e, which is defined in the proof of Proposition 2, to the computational λ2-calculus by
dlet x be N in M e = dM e{dN e/x}.
Then, M −→id2 ,β2v N implies dM e −→+
β⊃ ,η⊃ dN e, and M −→let2 N implies
dM e ≡ dN e. Suppose the existence of an infinite sequence of −→id2 , −→β2v ,
and −→let2 . Since there is no infinite reduction sequence in the simply typed
λ-calculus, neither −→id2 nor −→β2v appears infinitely in the sequence. The
assumption contradicts the fact that there is no infinite sequence of −→let2 .
Proposition 15. −→c is confluent.
Proof. According to Newman’s lemma [20], we consider the local confluency.
Because the λc -calculus and the call-by-name λ2-calculus are confluent, the
following critical pairs are essential:
/−→let

let y be M in box hxi be hyi in x

box hxi be hM i in x
\

−→id2 M,

→
−
−
let z be (box h→
y i be h N i in V ) in box hxi be hzi in M
→
−
−
box hxi be hbox h→
y i be h N i in V i in M
/−→let

→
−
−
−→β2v box h→
y i be h N i in M {V /x}.

\

−
→
−
Confluence of the former pair is easily shown. For the latter case, let let →
w be N 0 in
−
→
→
−
−
−
box h→
y i be hW i in x be the −→let -normal form of box h→
y i be h N i in x.
→
−
−
let z be (box h→
y i be h N i in V ) in box hxi be hzi in M
−
→
−
→
−
−
−→∗let let z be (let →
w be N 0 in box h→
y i be hW i in V ) in box hxi be hzi in M
−
→
−
→
−
−
−→∗
let →
w , z be N 0 , (box h→
y i be hW i in V ) in box hxi be hzi in M
comp

−
→
−
→
−
−
v
−→βlet
let →
w be N 0 in box hxi be hbox h→
y i be hW i in V i in M
−
→
−
→
−
−
−→β2v let →
w be N 0 in box h→
y i be hW i in M {V /x}.
On the other hand, the lower term goes to the same term by −→∗let .
We have restricted forms of terms in the call-by-value calculi for CPS completeness. Leaving completeness on one side, now we can present another CPS
transformation on full terms:
2σ 0 = 2((σ 0 ⊃ R) ⊃ R),
→
−
−
[[box h→
x i be h N i in M ]]0
→
−
−
−
−
−
−
= λk. [[ N ]]0 (λ→
y . k(box h→
z i be h→
y i in λh. →
z (λ→
x . [[M ]]0 h))),
where a non-overridden part of the definition is just the same as Figure 4. We
remark that the definition of [[−]]0 does not require a value transformation like
−. Also this transformation preserves the equality.
10

Theorem 16. For λ2-terms M and N , M =v N implies [[M ]]0 =n [[N ]]0 .
Unfortunately, it can be seen that this modified CPS transformation does
not reflect the equality. For example,
[[box hxi be hbox hyi be hLi in N i in M ]]0
=n [[box hyi be hLi in (λx. M )N ]]0 ,
but box hxibehbox hyi be hLi in N i in M 6=v box hyibehLi in (λx. M )N unless
N is a value. It is still open to find an axiomatization complete for [[−]]0 .

5

Semantics

Since Kripke semantics [14] concern only provability, they are not suitable for our
study. It is proposed by Bellin et al. in [4] that a model of IK is a cartesian closed
category with a lax monoidal endofunctor with respect to cartesian products.
(Fundamental properties of monoidal functors are found in [15].) Indeed, it is
shown in [13] that the call-by-name λ2-calculus with conjunctions is sound and
complete for the class of such models. The completeness without conjunctions is
expected to be proved in a way similar to the case of the simply typed λ-calculus.
Bellin et al.’s calculus has the same syntax as ours, but it is not complete for
the semantics.
Semantics for the call-by-value calculus is more complex than the call-byname semantics. We show construction of a call-by-value model as follows.
Let a cartesian closed category C have a strong monad hT, η, µi and a
monoidal endofunctor h2, m1 , mi. We focus on the Kleisli category CT , which
is a model of the λc -calculus. For a morphism f ∈ C(B, A), there exists a
morphism η ◦ 2f ∈ CT (2B, 2A). This fact explains a construction
x:σ ` V :τ
y : 2σ ` box hxi be hyi in V : 2τ
which is functorial:
box hxi be hM i in x =v M,
box hxi be hbox hyi be hM i in W i in V =v box hyi be hM i in V {W/x}.
The natural transformation {mA,B ∈ C(2A × 2B, 2(A × B))} induces a typeindexed family {η ◦ mA,B ∈ CT (2A × 2B, 2(A × B))}. This family is not a
natural transformation but natural in values. It explains an equation
box hx, zi be hbox hyi be hN i in V, P i in M =v box hy, zi be hN, P i in M {V /x}.
X

If a monad T is a continuation monad, that is, T X = RR , the categorical
semantics coincides with the CPS semantics.

6

Extensions

In this section, we show an extension of the call-by-name calculus to IS4. A
call-by-value axiomatization still remains future work.
11

We introduce type-indexed families of constants {εσ : 2σ ⊃ σ} and {δσ :
2σ ⊃ 22σ} with the following axioms:
→
−
→
− −
−
ε(box h→
x i be h N i in M ) =natε M {ε N /→
x },
→
−
→
−
−
−
−
−
δ(box h→
x i be h N i in M ) =natδ box h→
y i be hδ N i in box h→
x i be h→
y i in M ,
δ(δM ) =mon box hxi be hδM i in δx,
ε(δM ) =mon box hxi be hδM i in εx =mon M.
(It is trivial that this calculus corresponds to IS4.) We only consider equalities
because it is not obvious in some equations which side is a result of a computation. Naturally, it is possible to give calculi for IT and IK4 as fragments of
this IS4 calculus.
Bierman and de Paiva introduced the λS4 -calculus in [5]. We show our
calculus can emulate the 2-fragment of their calculus. Let
→
−
→
−
−
−
box M with N for →
x ≡ box h→
x i be hδ N i in M,
unbox M ≡ εM.
The following equation holds in our calculus:
→
−
→
− −
−
unbox (box M with N for →
x ) = M { N /→
x }.
On the other hand, Bierman and de Paiva’s calculus does not emulate our
calculus because ours is complete for the class of cartesian closed categories
with monoidal comonads but theirs is not.
It is also possible to compare our calculus to a dual context version of IS4
like Barber and Plotkin’s DILL [2]. A dual context calculus for IS4 is proposed
by Pfenning and Davies in [22]. (Their calculus has a diamond modality too,
but we just ignore it here.) The dual context calculus requires new syntax 2M
→
−
−
and let 2x be N in M instead of box h→
x i be h N i in M . The typing rules
consist of
∆, a : τ, ∆0 | Γ ` a : τ
∆ | ` M :τ
∆ | Γ ` 2M : 2τ
∆, a : σ | Γ ` M : τ
∆ | Γ ` N : 2σ
σ
∆ | Γ ` let 2a be N in M : τ
and the usual rule of the simply typed λ-calculus with respect to right-hand
contexts. We use a, b, . . . for variables of left-hand contexts to distinguish them
from those of right-hand contexts. The equality is defined by
C : context,
let 2a be 2N in M = M {N/a},
let 2a be M in 2a = M,
C[let 2a be N in M ] = let 2a be N in C[M ]
12

a 6∈ FV(C),

where C is a context such that its hole does not appear under a box.
In the λ2-calculus, we call the following equality the strongness condition:
→
−
→
−
−
−
box h→
w , x, →
z i be h P , N, Q i in M
→
− →
−
−
−
= box h→
w,→
z i be h P , Q i in M

→
−
−
|→
w | = | P |,

→
−
→
−
−
−
box h→
w , x, y, →
z i be h P , N, N, Q i in M
→
−
→
−
−
−
= box h→
w , x, →
z i be h P , N, Q i in M {x/y}

→
−
−
|→
w | = | P |.

st

st

The following equality is called the symmetricity.
→
−
→
−
−
−
box h→
w , x, y, →
z i be h P , N, L, Q i in M
→
−
→
−
−
−
=
box h→
w , y, x, →
z i be h P , L, N, Q i in M

→
−
−
|→
w | = | P |.

sym

The terms “strong” and “symmetric” follow the terms “strong monoidal functor” and “symmetric monoidal functor” in the category theory. We show that
the dual context calculus is equivalent to the λ2-calculus with the symmetricity and the strongness condition. Define the transformation h|−|i from the dual
context calculus into the λ2-calculus by
h|a|i = εa,
→
−
→
−
h|2M |i = box h b i be hδ b i in h|M |i

→
−
where { b } = FV(M ),

h| let 2a be N in M |i = (λa. h|M |i)h|N |i.
For a derivable judgment a1 : ρ1 , . . . | x1 : σ1 , . . . ` M : τ , the judgment
a1 : 2ρ1 , . . . , x1 : σ1 , . . . ` h|M |i : τ
is derivable in the λ2-calculus, and M = N implies h|M |i = h|N |i under the
strongness condition and the symmetricity. Its inverse (|−|) can be defined by
(|ε|) = λy. let 2a be y in a,
(|δ|) = λy. let 2a be y in 22a,
→
−
→
−
−
−
−
−
(| box h→
x i be h N i in M |) = let 2→
a be (| N |) in 2((|M |){→
a /→
x }).
One can see that M = N implies (|M |) = (|N |). While h|(|−|)|i is the identity
up to the equality, (|h|−|i|) is not the identity itself. The reason is that the dual
context calculus is redundant in some sense: for example, two judgments,
| x : 2σ ` x : 2σ,
a : σ | ` 2a : 2σ,
have the same semantics.
Another possible extension of our calculus is a calculus corresponding to
the classical modal logic K. In [21], Parigot has extended the simply typed
λ-calculus to the λµ-calculus, which corresponds to the classical logic. We can
extend the call-by-name λ2-calculus with µ-operator in a straightforward way.
A call-by-value version and analyses of the relation between call-by-name and
call-by-value are found in [13].
13

Acknowledgments
I am grateful to Tatsuya Abe. This work has developed over discussions with
him. I also thank PPL referees for valuable comments.

References
[1] T. Abe. Completeness of modal proofs in first-order predicate logic. Computer Software, JSSST Journal, 24:165–177, 2007.
[2] A. Barber. Dual intuitionistic linear logic. Technical report, LFCS, University of Edinburgh, 1996.
[3] H. P. Barendregt. Lambda calculi with types. In S. Abramski, D. M.
Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer
Science, volume 2, pages 117–309. Oxford University Press, 1992.
[4] G. Bellin, V. C. V. de Paiva, and E. Ritter. Extended Curry-Howard
correspondence for a basic constructive modal logic. In Proceedings of
Methods for Modalities, 2001.
[5] G. M. Bierman and V. C. V. de Paiva. On an intuitionistic modal logic.
Studia Logica, 65:383–416, 2000.
[6] R. Davies and F. Pfenning. A modal analysis of staged computation. Journal of ACM, 48:555–604, 2001.
[7] M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. F. Duba. A syntactic
theory of sequential control. Theoretical Computer Science, 52:205–237,
1987.
[8] M. Fischer. Lambda calculus schemata. In Proving Assertions about Programs, pages 104–109. ACM Press, 1972.
[9] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
[10] J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge
University Press, 1989.
[11] M. Hasegawa. Simply typed computational lambda calculus is strongly
normalizing. Personal communication, 2003.
[12] W. A. Howard. The formulae-as-types notion of construction. In Essays
on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490.
Academic Press, 1980.
[13] Y. Kakutani. Call-by-name and call-by-value in normal modal logic. In
Asian Symposium on Programming Languages and Systems, volume 4807
of LNCS, pages 399–414. Springer-Verlag, 2007.
[14] S. Kripke. Semantic analysis of modal logic I, normal propositional logic.
Zeitschrift für Mathemathische Logik und Grundlagen der Mathematik,
9:67–96, 1963.

14

[15] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag,
2nd edition, 1997.
[16] C. McBride and R. Paterson. Applicative programming with effects. Journal of Functional Programming, 18:1–13, 2008.
[17] K. Miyamoto and A. Igarashi. A modal foundation for secure information
flow. In Proceedings of Foundations of Computer Security, 2004.
[18] E. Moggi. Computational lambda-calculus and monads. Technical report,
LFCS, University of Edinburgh, 1988.
[19] E. Moggi. Computational lambda-calculus and monads. In Logic in Computer Science, pages 14–23. IEEE Computer Society, 1989.
[20] M. H. A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43:223–243, 1942.
[21] M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural
deduction. In Logic Programming and Automated Reasoning, volume 624
of LNCS, pages 190–201. Springer-Verlag, 1992.
[22] F. Pfenning and R. Davies. A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science, 11:511–540, 2001.
[23] G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.
[24] D. Prawitz. Natural Deduction: a proof-theoretic study. Almqvist and
Wiksell, 1965.
[25] A. Sabry and M. Felleisen. Reasoning about programs in continuationpassing style. LISP and Symbolic Computation, 6:289–360, 1993.

15

