# Complete Call-by-Value Calculi of Control Operators, II: Strong termination

Ryu Hasegawa  Graduate School of Mathematical Sciences, The University of
Tokyo, Komaba 3-8-1, Meguro-ku, Tokyo 153-8914, Japan<EMAIL_ADDRESS>
###### Abstract.

We provide characterization of the strong termination property of the CCV
$\lambda\mu$-calculus introduced in the first part of the series of the paper.
The calculus is complete with respect to the standard CPS semantics. The
union-intersection type systems for the calculus is developed in the previous
paper. We characterize the strong normalizability of terms of the calculus in
terms of the CPS semantics and typeability.

###### keywords:

$\lambda\mu$-calculus, control operators, call-by-value, normalization, type
discipline

###### 1991 Mathematics Subject Classification:

F.4.1 [Mathematical Logic]: Lambda calculus and related systems, D.3.3
[Language Constructs and Features]: Control structures

## Introduction

This is the second half of a series of papers. In the first part [tsd43], we
proposed a call-by-value $\lambda\mu$-calculus, called the CCV
$\lambda\mu$-calculus, that were complete for the CPS semantics. Furthermore,
we proposed the union-intersection type discipline. Among others, we verified
the following: (1)A term $M$ terminates with respect to the call-by-value
evaluation if and only if its CPS translation $[\\![M]\\!]$ is solvable.

(2)A term $M$ is weakly normalizing if and only if its CPS translation
$[\\![M]\\!]$ is weakly normalizing.

(3)A term $M$ terminates with respect to the call-by-value evaluation if and
only if $M$ is typeable.

(4)A term $M$ is weakly normalizing if and only if $M$ is typeable where the
typing judgment of $M$ contains neither empty intersection nor empty union.

The theme of the second part is further pursuance of extension of these
results. We give characterization of the strong termination property.
Specifically we show

(5)$M$ is strongly normalizing iff its CPS translation $[\\![M]\\!]$ is
strongly normalizing.

(6)$M$ is strongly normalizing iff $M$ is typeable using empty intersection or
empty union nowhere.

After brief introduction to the CCV $\lambda\mu$-calculus and its type system
containing union and intersection, we first verify strong termination for a
fragment in §2.1 as an intermediate step. Employing this result, we verify (6)
in Thm. LABEL:rzq50 and (5) in Thm. LABEL:tml91 in §LABEL:eqw96.

An essential idea behind our calculus is in departure from the conventional
demand that terms be freely generated by syntactic grammars. An analogy is
found in arithmetic. We frequently use an expression such as $3+5+7$. When we
calculate it (or implement a calculator on computers), we forcibly interpret
the expression as either $(3+5)+7$ or $3+(5+7)$ and perform calculation.
However, there is little advantage to strictly distinguish them for humans to
understand the essence of arithmetic. We positively use the expression $3+5+7$
as an amalgamation of two ways of bracketed expressions, or even as a sum of
three numbers. This type of intended ambiguity helps us to process arithmetic
flexibly. In the same vein, we introduce ambiguity in the constructors of the
call-by-value calculus. The produced calculus is complete with respect to the
standard semantics, and yet usable.

##  1\. Preliminaries

We recall the CCV $\lambda\mu$-calculus and the union-intersection type
discipline for the calculus [tsd43]. Also we review some of the results needed
later. Details are found in that paper.

###  1.1. CCV $\lambda\mu$-calculus

The CCV $\lambda\mu$-calculus is a variant of the call-by-value
$\lambda\mu$-calculus. It employs the let-syntax as in Moggi’s
$\lambda_{c}$-calculus [dvp96]. However, we write the let-binding to the right
of its body:

$M\mathbin{\upharpoonright}x\mathbin{:=}N$ in place of ${\sf let}\ x=N\ {\sf
in}\ M$.

Note that the order of $M$ and $N$ is reversed.

Formally, the syntax of the CCV $\lambda\mu$-calculus is given as follows. We
distinguish ordinary variables and continuation variables. We also distinguish
terms $M$ and jumps $J$. They are defined mutually recursively by the
following syntax:

$M$ | ${}\ \mathrel{::=}\ x\ \ \ |\ \ \ \lambda x.\,M\ \ \ |\ \ \ MM\ \ \ |\ \ \ M\mathbin{\upharpoonright}x\mathbin{:=}M\ \ \ |\ \ \ \mu k.\,J$
---|---
$J$ | ${}\ \mathrel{::=}\ [k]M\ \ \ |\ \ \ J\mathbin{\upharpoonright}x\mathbin{:=}M$

where $x$ ranges over ordinary variables and $k$ over continuation variables.
The notion of free variable is naturally defined. The let-construct
$M\mathbin{\upharpoonright}x\mathbin{:=}N$ binds $x$ and its scope is $M$. We
use notation $z\in M$ to denote that a variable $z$ that is ordinary or
continuation occurs freely in $M$.

A key idea is that this syntax is not regarded to freely generate the
entities. We introduce syntactic equalities by two associativity axioms:

$L\mathbin{\upharpoonright}x\mathbin{:=}(M\mathbin{\upharpoonright}y\mathbin{:=}N)$ |  ${}\ =\ (L\mathbin{\upharpoonright}x\mathbin{:=}M)\mathbin{\upharpoonright}y\mathbin{:=}N$ | if $y\not\in L$
---|---|---
$[k](L\mathbin{\upharpoonright}x\mathbin{:=}M)$ |  ${}\ =\ ([k]L)\mathbin{\upharpoonright}x\mathbin{:=}M.$ |

We do not syntactically distinguish two terms (or two jumps) if they turn out
to be equal by a series of application of these rules. Mostly we omit
brackets:

$L\mathbin{\upharpoonright}x\mathbin{:=}M\mathbin{\upharpoonright}y\mathbin{:=}N$
---
$\mu k.\,J\mathbin{\upharpoonright}x\mathbin{:=}M$
$[k]L\mathbin{\upharpoonright}x\mathbin{:=}M.$

For the first, if the side condition is not satisfied (i.e., if $y\in L$), we
regard it to mean
$(L\mathbin{\upharpoonright}x\mathbin{:=}M)\mathbin{\upharpoonright}y\mathbin{:=}N$.
For the second, we read it $\mu
k.\,(J\mathbin{\upharpoonright}x\mathbin{:=}M)$.

A value is either a variable or a lambda abstraction. We have the following
ten reduction rules where $N$ is a non-value and $V$ is a value:

$({\it ad}_{1})$ | $NM$ | ${}\ \rightarrow\ zM\mathbin{\upharpoonright}z\mathbin{:=}N$ |
---|---|---|---
$({\it ad}_{2})$ | $VN$ | ${}\ \rightarrow\ Vz\mathbin{\upharpoonright}z\mathbin{:=}N$ |
$(\beta_{\lambda})$ | $(\lambda x.\,M)V$ | ${}\ \rightarrow\ M\mathbin{\upharpoonright}x\mathbin{:=}V$ |
$(\beta_{\it let})$ | $M\mathbin{\upharpoonright}x\mathbin{:=}V$ | ${}\ \rightarrow\ M\\{V/x\\}$ |
$(\beta_{\mu})$ | $M\mathbin{\upharpoonright}x\mathbin{:=}\mu k.\,J$ | ${}\ \rightarrow\ \hbox to0.0pt{$\mu k.\,J\\{[k]\square\mapsto[k]M\mathbin{\upharpoonright}x\mathbin{:=}\square\\}$\hss}$ |
$(\beta_{\it jmp})$ | $[l]\mu k.\,J$ | ${}\ \rightarrow\ J\\{l/k\\}$ |
$(\eta_{\lambda})$ | $\lambda x.\,Vx$ | ${}\ \rightarrow\ V$ | (if $x\not\in V$)
$(\eta_{\it let})$ | $x\mathbin{\upharpoonright}x\mathbin{:=}M$ | ${}\ \rightarrow\ M$ |
$(\eta_{\mu})$ | $\mu k.\,[k]M$ | ${}\ \rightarrow\ M$ | (if $k\not\in M$)
$({\it exch})$ | $(\mu k.\,J)\mathbin{\upharpoonright}x\mathbin{:=}M$ | ${}\ \rightarrow\ \mu k.\,J\mathbin{\upharpoonright}x\mathbin{:=}M$ | (if $k\not\in M$).

In the first two rules, $z$ is a fresh ordinary variable. We use curly brace
for substitution. The notation
$J\\{[k]\square\mapsto[k]M\mathbin{\upharpoonright}x\mathbin{:=}\square\\}$ is
a standard context substitution in the $\lambda\mu$-calculus. We write
$L=_{\it ccv}M$ if two terms are equivalent with respect to the smallest
equivalence relation generated from reductions.

Since we allow to alter the scope of let-binding by the equality axioms, the
continuation $M\mathbin{\upharpoonright}x\mathbin{:=}\square$ captured by rule
$\beta_{\mu}$ is changeable, depending on the choice of the scope. This
ambiguity is intended, and is crucial to verify the sharpened completeness
theorem, that is a key result in the previous paper.

######  Remark .

In the previous paper, we had the third equality axiom:

$(\mu k.\,J)\mathbin{\upharpoonright}x\mathbin{:=}M\ =\ \mu
k.\,(J\mathbin{\upharpoonright}x\mathbin{:=}M)$ if $k\not\in M$.

Namely we were able to exchange $\mu$-operator and let-operator. As we
commented in the paper, however, this equality axiom was inessential for proof
of the sharpened completeness theorem. In place, we can consider a reduction
rule. For the purpose in this paper, the latter approach gives better results
at this stage. So we adopt the rule exch above. It is open whether the same
results are obtained if the equality axiom is chosen. See Rem. LABEL:orv02.

The semantics of the CCV $\lambda\mu$-calculus is given by the call-by-value
continuation-passing style (CPS) translation. It maps each CCV term and each
jump to a lambda term. The following definition is standard.

$[\\![V]\\!]$ | ${}\ \mathrel{:=}\ \lambda k.\,kV^{*}$
---|---
$[\\![MN]\\!]$ | ${}\ \mathrel{:=}\ \lambda k.\,[\\![M]\\!](\lambda x.\,[\\![N]\\!](\lambda y.\,xyk))$
$[\\![M\mathbin{\upharpoonright}x\mathbin{:=}N]\\!]$ | ${}\ \mathrel{:=}\ \lambda k.\,[\\![N]\\!](\lambda x.\,[\\![M]\\!]k)$
$[\\![\mu k.\,J]\\!]$ | ${}\ \mathrel{:=}\ \lambda k.\,[\\![J]\\!]$
$[\\![[k]M]\\!]$ | ${}\ \mathrel{:=}\ [\\![M]\\!]k$
$[\\![J\mathbin{\upharpoonright}x\mathbin{:=}N]\\!]$ | ${}\ \mathrel{:=}\ [\\![N]\\!](\lambda x.\,[\\![J]\\!])$
$x^{*}$ | ${}\ \mathrel{:=}\ x$
$(\lambda x.\,M)^{*}$ | ${}\ \mathrel{:=}\ \lambda x.\,[\\![M]\\!].$

This is a standard call-by-value CPS translation. We write $[\\![M]\\!]_{s}$
for this type of CPS translation, however, since we largely consider the
translation induced by the colon translation given below.

The colon translation is introduced in [pag41]. We use the notation
$(\mskip-4.0mu|M|\mskip-4.0mu)[K]$ in place of $M:K$ for readability.

$(\mskip-4.0mu|V|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ KV^{*}$
---|---
$(\mskip-4.0mu|V_{1}V_{2}|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ V_{1}^{*}V_{2}^{*}K$
$(\mskip-4.0mu|VN|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|N|\mskip-4.0mu)[\lambda y.\,V^{*}yK]$
$(\mskip-4.0mu|NV|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|N|\mskip-4.0mu)[\lambda x.\,xV^{*}K]$
$(\mskip-4.0mu|N_{1}N_{2}|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|N_{1}|\mskip-4.0mu)[\lambda x.\,(\mskip-4.0mu|N_{2}|\mskip-4.0mu)[\lambda y.\,xyK]]$
$(\mskip-4.0mu|L\mathbin{\upharpoonright}x\mathbin{:=}M|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|M|\mskip-4.0mu)[\lambda x.\,(\mskip-4.0mu|L|\mskip-4.0mu)[K]]$
$(\mskip-4.0mu|\mu k.\,J|\mskip-4.0mu)[K]$ | ${}\ \mathrel{:=}\ (\lambda k.\,(\mskip-4.0mu|J|\mskip-4.0mu))K$
$(\mskip-4.0mu|[k]M|\mskip-4.0mu)$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|M|\mskip-4.0mu)[k]$
$(\mskip-4.0mu|J\mathbin{\upharpoonright}x\mathbin{:=}M|\mskip-4.0mu)$ | ${}\ \mathrel{:=}\ (\mskip-4.0mu|M|\mskip-4.0mu)[\lambda x.\,(\mskip-4.0mu|J|\mskip-4.0mu)]$
$x^{*}$ | ${}\ \mathrel{:=}\ x$
$(\lambda x.\,M)^{*}$ | ${}\ \mathrel{:=}\ \lambda xk.\,(\mskip-4.0mu|M|\mskip-4.0mu)[k]$
$[\\![M]\\!]_{c}$ | ${}\ \mathrel{:=}\ \lambda k.\,(\mskip-4.0mu|M|\mskip-4.0mu)[k]$

Here $V$ and $V_{i}$ are values; $N$ and $N_{i}$ are non-values. Two CPS
translations $[\\![M]\\!]_{s}$ and $[\\![M]\\!]_{c}$ are equal up to
$\beta\eta$-equality of the lambda calculus. We give priority to
$[\\![M]\\!]_{c}$ and write it simply $[\\![M]\\!]$.

It is better to regard the target of the CPS translation as a sorted lambda
calculus. There are four sorts. The terms of the sorted calculus are defined
as follows:

Term | $T$ | ${}\ \mathrel{::=}\ \lambda k.\,Q\ \ |\ \ WW$
---|---|---
Jump | $Q$ | ${}\ \mathrel{::=}\ KW\ \ |\ \ TK$
Value | $W$ | ${}\ \mathrel{::=}\ x\ \ |\ \ \lambda x.\,T$
Continuation | $K$ | ${}\ \mathrel{::=}\ k\ \ |\ \ \lambda x.\,Q$

The CPS translation yields the terms that are subject to this syntax.

We also have the inverse translation $(\hbox{-})^{-1}$ from the target
calculus back into the CCV $\lambda\mu$-calculus. We do not, however, need the
concrete shape of the translation for we use it only through Lem. 1 and 2
below. We refer the interested reader to [tsd43].

We list several results that are used in this paper from [tsd43]. We call a
reduction by rule $(\eta_{\mu})$ vertical, and a reduction by $({\it ad}_{1})$
or $({\it ad}_{2})$ administrative. A non-administrative reduction is called
practical.

######  Lemma 1.

Let $M$ be a term of the CCV $\lambda\mu$-calculus. There is a term
$M^{\dagger}$ of the calculus such that
$M\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle
A^{*}$}\kern-2.0pt}}}M^{\dagger}\mathrel{\mathop{\longleftarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle V^{*}$}\kern-2.0pt}}}[\\![M]\\!]^{-1}$ (notice
the direction). Here $A^{*}$ denotes a finite number of administrative
reductions and $V^{*}$ a finite number of vertical reductions.

######  Lemma 2.

If $P\rightarrow_{\beta\eta}Q$ in the target calculus, then
$P^{-1}\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle+$}\kern-2.0pt}}}Q^{-1}$ by one or more steps
of practical reductions with no use of rule exch.

######  Lemma 3.

If $L^{\prime}\mathrel{\mathop{\longleftarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle
V^{*}$}\kern-2.0pt}}}L\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle P^{*}$}\kern-2.0pt}}}M$ by finite steps of
vertical reductions and practical reductions, there is a term $M^{\prime}$
such that $L^{\prime}\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle
P^{*}$}\kern-2.0pt}}}M^{\prime}\mathrel{\mathop{\longleftarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle V^{*}$}\kern-2.0pt}}}M^{\prime}$. Moreover,
the arrow $L^{\prime}\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle P^{*}$}\kern-2.0pt}}}M^{\prime}$ may be an
identity only when $L\mathrel{\mathop{\longrightarrow}\limits^{\vbox
to0.0pt{\vss\hbox{$\scriptstyle P^{*}$}\kern-2.0pt}}}M$ consists solely of
$\beta_{\mu}$, $\beta_{\it jmp}$, $\eta_{\mu}$, and exch.

###  1.2. Union-intersection type discipline

Types are divided in three categories, raw types $R$, subsidiary types $S$,
and types $T$. These are defined by the following syntax:

$R$ | ${}\ \mathrel{::=}\ \alpha\ \ |\ \ S\rightarrow T$
---|---
$S$ | ${}\ \mathrel{::=}\ \bigcap R$
$T$ | ${}\ \mathrel{::=}\ \bigcup S$

where $\alpha$ ranges over atomic types. $\bigcap R$ means a nonempty finite
formal intersection $R_{1}\cap R_{2}\cap\cdots\cap R_{n}$ ($n\geq 1$).
$\bigcup S$ is similar. Intersection and union follow associativity and
commutativity.

######  Remark 4.

In the previous work [tsd43], empty intersection $\omega$ and empty union
$\mathord{\hbox{\hbox{\kern 23.9989pt\vbox{\hbox{\hbox{\kern
4.30534pt\vbox{\hbox{$\omega$} \kern 1.91902pt}\kern-6.22406pt}}
\kern-17.77393pt}\kern-6.22406pt}}}$ are allowed. In this paper, we use only
the type derivations that contain $\omega$ or $\mathord{\hbox{\hbox{\kern
23.9989pt\vbox{\hbox{\hbox{\kern 4.30534pt\vbox{\hbox{$\omega$} \kern
1.91902pt}\kern-6.22406pt}} \kern-17.77393pt}\kern-6.22406pt}}}$ nowhere. So
we omit them from the beginning.

We define subtype relation $\leq$ by the following derivation rules.

$\alpha\leq\alpha$
---
$S^{\prime}\leq S\qquad T\leq T^{\prime}$
---
$S\rightarrow T\leq S^{\prime}\rightarrow T^{\prime}$

$S\leq S^{\prime}$
---
$S\cap S^{\prime\prime}\leq S^{\prime}$

$[\ S\leq S_{i}\ ]_{i}$
---
$S\leq\bigcap_{i}S_{i}$

$T\leq T^{\prime}$
---
$T\leq T^{\prime\prime}\cup T^{\prime}$
$[\ T_{i}\leq T\ ]_{i}$
---
$\bigcup_{i}T_{i}\leq T$

.

The notation $[\>S\leq S_{i}\>]_{i}$ means a sequence of derivations where $i$
ranges over a finite index set. $[\>T_{i}\leq T\>]_{i}$ is similar.

A typing judgement has the form
$\Gamma\;\vdash\;M\mathbin{:}T\;\mathbin{|}\;\Delta$ where $\Gamma$ is a
finite sequence of $x_{i}\mathbin{:}S_{i}$, and $\Delta$ is a finite sequence
of $k_{j}\mathbin{:}T_{j}$. Note that ordinary variables have only subsidiary
types. We assume a special type $\bot\,\hbox to0.0pt{\hss$\bot$}$ for typing
jumps. The inference rules are given as follows:

$\Gamma,\>x\mathbin{:}S\ \vdash\ x\mathbin{:}S\ \mathrel{|}\ \Delta$
---

$[\ \Gamma,\>x\mathbin{:}S_{i}\ \vdash\ M\mathbin{:}T_{i}\ \mathrel{|}\
\Delta\ ]_{i}$
---
$\Gamma\ \vdash\ \lambda x.\,M\mathbin{:}\bigcap_{i}(S_{i}\rightarrow T_{i})\
\mathrel{|}\ \Delta$

$\Gamma\ \vdash\ M\mathbin{:}\bigcup_{i}\bigcap_{j}(S_{ij}\rightarrow T)\
\mathrel{|}\ \Delta\qquad[\ \Gamma\ \vdash\ N\mathbin{:}\bigcup_{j}S_{ij}\
\mathrel{|}\ \Delta\ ]_{i}$
---
$\Gamma\ \vdash\ MN\mathbin{:}T\ \mathrel{|}\ \Delta$

$[\ \Gamma,\>x\mathbin{:}S_{i}\ \vdash\ M\mathbin{:}T\ \mathrel{|}\ \Delta\
]_{i}\qquad\Gamma\ \vdash\ N\mathbin{:}\bigcup_{i}S_{i}\ \mathrel{|}\ \Delta$
---
$\Gamma\ \vdash\ M\mathbin{\upharpoonright}x\mathbin{:=}N\mathbin{:}T\
\mathrel{|}\ \Delta$

$\Gamma\ \vdash\ J\mathbin{:}\bot\,\hbox to0.0pt{\hss$\bot$}\ \mathrel{|}\
\Delta,\>k\mathbin{:}T$
---
$\Gamma\ \vdash\ \mu k.\,J\mathbin{:}T\ \mathrel{|}\ \Delta$

$\Gamma\ \vdash\ M\mathbin{:}T\ \mathrel{|}\ \Delta,\>k\mathbin{:}T$
---
$\Gamma\ \vdash\ [k]M\mathbin{:}\bot\,\hbox to0.0pt{\hss$\bot$}\ \mathrel{|}\
\Delta,\>k\mathbin{:}T$

$[\ \Gamma,\>x\mathbin{:}S_{i}\ \vdash\ J\mathbin{:}\bot\,\hbox
to0.0pt{\hss$\bot$}\ \mathrel{|}\ \Delta\ ]_{i}\qquad\Gamma\ \vdash\
N\mathbin{:}\bigcup_{i}S_{i}\ \mathrel{|}\ \Delta$
---
$\Gamma\ \vdash\
J\mathbin{\upharpoonright}x\mathbin{:=}N\mathbin{:}\bot\,\hbox
to0.0pt{\hss$\bot$}\ \mathrel{|}\ \Delta$

$\Gamma\ \vdash\ M\mathbin{:}T\ \mathrel{|}\ \Delta\qquad T\leq T^{\prime}$
---
$\Gamma\ \vdash\ M\mathbin{:}T^{\prime}\ \mathrel{|}\ \Delta$

Each index ($i$ or $j$) ranges over a finite set. The notation $[\cdots]_{i}$
denotes a finite sequence of judgements. In each rule, the same indices are
understood to range over the same set. For example, in the third rule, $i$
ranges over a finite set $I$ and $j$ over a finite set $J(i)$ depending on
$i$, and these $I$ and $J(i)$ are shared between the assumptions.

###  1.3. Type system of the target calculus

The characterization of strong termination is verified through the type theory
of the target calculus we present here. It is based on the standard
intersection type discipline. We assume a special atomic type $\bot\,\hbox
to0.0pt{\hss$\bot$}$ and write $\neg(\hbox{-})$ in place of
$(\hbox{-})\rightarrow\bot\,\hbox to0.0pt{\hss$\bot$}$. We define strict types
$\tau,\kappa,\sigma$ and types $\underline{\kappa},\underline{\sigma}$ by the
following:

$\sigma$ | ${}\ \mathrel{::=}\ \alpha\ \ |\ \ \underline{\sigma}\rightarrow\tau$ | $\underline{\sigma}$ | ${}\ \mathrel{::=}\ \bigcap\sigma$
---|---|---|---
$\kappa$ | ${}\ \mathrel{::=}\ \neg\underline{\sigma}$ | $\underline{\kappa}$ | ${}\ \mathrel{::=}\ \bigcap\kappa$
$\tau$ | ${}\ \mathrel{::=}\ \neg\underline{\kappa}$

where $\alpha$ represents atomic types. $\bigcap\kappa$ denotes finite formal
intersection $\kappa_{1}\cap\kappa_{2}\cap\cdots\cap\kappa_{n}$ with $n\geq
1$. $\bigcap\sigma$ is similar. Intersection follows associativity and
commutativity. We have subtype relation $\leq$ between types. It is defined
naturally.

A typing judgment $\Pi,\Theta\vdash_{s}M\mathbin{:}\rho$ has two environments
$\Pi$ and $\Theta$, the former a finite sequence of
$x\mathbin{:}\underline{\sigma}$ and the latter of
$k\mathbin{:}\underline{\kappa}$. Here $M$ is one of term $T$, jump $Q$, value
$W$, and continuation $K$, on which the kind of type $\rho$ depends. A term
has type $\tau$, a jump $\bot\,\hbox to0.0pt{\hss$\bot$}$, a value $\sigma$,
and a continuation $\kappa$. We note that only strict types occur in the right
hand of $\vdash_{s}$ (the subscript signifies this).

The inference rules of the intersection type discipline is standard [bkw61],
except that sorts must be respected. For instance, the derivation rule for
$W_{1}W_{2}$ is

$\Pi,\>\Theta\ \vdash_{s}\
W_{1}\mathbin{:}\underline{\sigma}\rightarrow\tau\qquad[\ \Pi,\>\Theta\
\vdash_{s}\ W_{2}\mathbin{:}\sigma_{i}\ ]_{i}$
---
$\Pi,\>\Theta\ \vdash_{s}\ W_{1}W_{2}\mathbin{:}\tau$

Moreover, we include the inheritance rule for each sort, e.g.,

$\Pi,\>\Theta\ \vdash_{s}\ T\mathbin{:}\tau\qquad\tau\leq\tau^{\prime}$
---
$\Pi,\>\Theta\ \vdash_{s}\ T\mathbin{:}\tau^{\prime}$

to deal with $\eta$-rules. We refer the reader to [tsd43] for the presentation
of the complete set.

######  Theorem 5.

Let $M$ be a term of the CCV $\lambda\mu$-calculus. If
$\Pi,\,\Theta\>\vdash_{s}\>[\\![M]\\!]\mathbin{:}\tau$ is derivable in the
target calculus, then $\Gamma\>\vdash\>M\mathbin{:}T\>|\>\Delta$ is derivable
for some $\Gamma,\Delta$, and $T$ in the CCV $\lambda\mu$-calculus.

######  Proof 1.1.

The theorem is verified in [tsd43] using the inverse translation. By
inspection of the proof therein, we see that the induced derivation of
$\Gamma\>\vdash\>M\mathbin{:}T\>|\>\Delta$ contains neither $\omega$ nor
$\mathord{\hbox{\hbox{\kern 23.9989pt\vbox{\hbox{\hbox{\kern
4.30534pt\vbox{\hbox{$\omega$} \kern 1.91902pt}\kern-6.22406pt}}
\kern-17.77393pt}\kern-6.22406pt}}}$, provided the derivation of
$\Pi,\,\Theta\>\vdash_{s}\>[\\![M]\\!]\mathbin{:}\tau$ contains $\omega$
nowhere. ∎

##  2\. Strong Normalization

The main theorems of this section are the following: (i) A CCV
$\lambda\mu$-term $M$ is strongly normalizable if and only if $[\\![M]\\!]$ is
strongly normalizable (Thm. LABEL:tml91). (ii) $M$ is strongly normalizable if
and only if $M$ is typeable (Thm. LABEL:rzq50). We note that strong
normalizability of lambda terms is not closed under $\beta\eta$-equality. It
happens that $M=_{\beta\eta}N$ and $M$ is strongly normalizable whereas $N$ is
not. Hence the main result (i) is sensitive to the choice of the CPS
translation. We mainly deal with $[\\![\,]\\!]=[\\![\,]\\!]_{c}$ based on the
colon translation given in section 1.1. The case of the standard CPS
translation is briefly discussed in LABEL:zqb05.

###  2.1. Termination of $\beta_{\mu}\beta_{jmp}\eta_{\mu}$ reduction
sequences

We verify the termination of all reduction sequences consisting exclusively of
$\beta_{\mu}$, $\beta_{\it jmp}$, and $\eta_{\mu}$. The reasons we prove it
independently are the following: (a) It is used later in Prop. LABEL:ntw00.
(b) It holds irrelevant of types. (c) In proof, we introduce the notion of
places that are used in the sequel. (d) It explains why we regard the exchange
of $\mu$-operator and let-operator as a reduction rule rather than an equality
rule in the previous work.

Since we have equality axioms between terms, the notion of subterms is
obscure. As a replacing concept, we introduce the notion of places.

Suppose that a CCV $\lambda\mu$-term $M_{0}$ is given. A term $M$ occurs at
place $p$ if $p\mathbin{\hbox{\tt@}}M$ is derived by the following recursive
process. Let $p_{0}$ be an arbitrary fresh symbol. We start with
$p_{0}\mathbin{\hbox{\tt@}}M_{0}$, and apply the following operations
recursively until we reach variables:

  1. (1)

If either $p\mathbin{\hbox{\tt@}}(MN)$ or
$p\mathbin{\hbox{\tt@}}(M\mathbin{\upharpoonright}x\mathbin{:=}N)$, then
$p\mathbin{\hbox{\tt@}}M$ and $q\mathbin{\hbox{\tt@}}N$ concurrently where $q$
is a fresh place symbol.

  2. (2)

If either $p\mathbin{\hbox{\tt@}}(\lambda x.\,M)$ or
$p\mathbin{\hbox{\tt@}}(\mu k.\,[l]M)$, then $q\mathbin{\hbox{\tt@}}M$ where
$q$ is a fresh place symbol.

We say that a place $q$ occurs in $M$ whenever $q\mathbin{\hbox{\tt@}}N$ is
derived for some $N$ during the process from $p\mathbin{\hbox{\tt@}}M$ (case
$p=q$ is inclusive).

Here we assume to read $[k](L\mathbin{\upharpoonright}x\mathbin{:=}M)$ for
$[k]L\mathbin{\upharpoonright}x\mathbin{:=}M$. For associativity of let-
construct, either bracketing yields the same set of places up to renaming of
place symbols. For instance, the following term has five places:

| $(\mu k.\,[l]$ |  | $(\lambda z.\,$ |  | $x)$ |  | $y)\mathbin{\upharpoonright}y\mathbin{:=}\,$ |  | $x.$
---|---|---|---|---|---|---|---|---|---
$\uparrow$ $p_{0}$ |  |  $\uparrow$ $p_{1}$ |  |  $\uparrow$ $p_{2}$ |  |  $\uparrow$ $p_{3}$ |  |  $\uparrow$ $p_{4}$

Namely a place marks the location from which a term starts. Note that one
place may mark several terms. For example, place $p_{0}$ marks the whole term,
as well as $\mu k.\,[l](\lambda z.\,x)y$. Likewise place $p_{1}$ marks
$(\lambda z.\,x)y$ and $\lambda z.\,x$.

Let $p$ be a place occurring in a given term $M_{0}$. The vision $V(p)$ is the
set of places in $M_{0}$ recursively defined as follows:

  1. (1)

If $p\mathbin{\hbox{\tt@}}M$ occurs as the let-argument of
$p_{1}\mathbin{\hbox{\tt@}}L\mathbin{\upharpoonright}x\mathbin{:=}M$, then
$V(p)$ is defined by $\bigcup_{q}(\\{q\\}\cup V(q))$ where $q$ ranges over the
set of all places in $L$ ($p_{1}$ inclusive).

  2. (2)

If $p\mathbin{\hbox{\tt@}}M$ is preceded by a jumper as in
$p_{1}\mathbin{\hbox{\tt@}}\mu k.\cdots[k]M\cdots$, then $V(p)$ is defined by
$V(p_{1})$. Intuitively, place $p$ is superposed over $p_{1}$ and the
intermediate places between $\mu k$ and the jumper $[k]$ are invisible. If $k$
is not bound, we deal with $V(p)$ by the following third rule (thus
$V(p)=\emptyset$).

  3. (3)

For all other cases, we set $V(p)=\emptyset$.

######  Remark 6.

  1. (1)

The places in $V(p)$ occur physically to the left of $p$. Hence $V(p)$ is
defined by induction from left to right.

  2. (2)

By definition, visions are transitive. That is, if $r\in V(q)$ and $q\in
V(p)$, then $r\in V(p)$.

  3. (3)

Definition of visions is irrelevant of the bracketing for associativity of the
let-construct. Namely, if $p\mathbin{\hbox{\tt@}}N$ occurs in
$L\mathbin{\upharpoonright}x\mathbin{:=}M\mathbin{\upharpoonright}y\mathbin{:=}N$
with $y\not\in L$, then either bracketing yields the same set $V(p)$ up to the
renaming of place symbols.

  4. (4)

In contrast, the interchange law of $\mu$ and let is annoying. If we returned
to the identification of $(\mu k.\,J)\mathbin{\upharpoonright}x\mathbin{:=}M$
and $\mu k.\,(J\mathbin{\upharpoonright}x\mathbin{:=}M)$ where $k\not\in M$ as
commented in Rem. 1.1, then we would have the following double vision problem.
Suppose $p$ is the place of $M$ in $p_{1}\mathbin{\hbox{\tt@}}\mu
k.\,[l]L\mathbin{\upharpoonright}x\mathbin{:=}M$ where $k\not\in M$. If we
understand it to be $p_{1}\mathbin{\hbox{\tt@}}(\mu
k.\,[l]L)\mathbin{\upharpoonright}x\mathbin{:=}M$, place $p_{1}$ is visible
from $p$. On the other hand, if we regard it as $p_{1}\mathbin{\hbox{\tt@}}\mu
k.\,[l](L\mathbin{\upharpoonright}x\mathbin{:=}M)$, the vision of $p$ skips
place $p_{1}$ jumping from $[l]$. Namely the vision is affected by bracketing.

Let us write $q\prec p$ if $q$ is an immediately visible from $p$. Namely
$q\in V(p)$ holds while $q\in V(r)$ and $r\in V(p)$ hold for no $r$.

######  Remark 7.

The relation $q\prec p$ holds if and only if either of the following two cases
happens: (i) $p\mathbin{\hbox{\tt@}}N$ is the place of the let-argument of
$L\mathbin{\upharpoonright}x\mathbin{:=}N$, and $q$ occurs in $L$.
Furthermore, if $q$ occurs in a let-expression
$P\mathbin{\upharpoonright}y\mathbin{:=}Q$ inside $L$, $q$ lies in the
argument side $Q$. (ii) $p\mathbin{\hbox{\tt@}}N$ is the place preceded by a
jumper as in $p_{1}\mathbin{\hbox{\tt@}}(\mu l.\,\cdots[l]N\cdots)$ with
$q\prec p_{1}$.

The breadth $|p|$ of a place $p$ is defined by induction on physical locations
from left to right. We define $|p|$ as the smallest natural number $n$
satisfying $|q|<n$ for all places $q\in V(p)$. In particular, $|p|=0$ if
$V(p)=\emptyset$.

In other words, $|p|$ is the height of the tree of all sequences of places
$q\prec q^{\prime}\prec\cdots\prec p$ having $p$ as its root.

Let us observe how the breadth $|p|$ changes before and after one-step
$\beta_{\mu}$-reduction. For distinction, we write bars over the places after
reduction. Let us set places symbols as follows:

| $M\mathbin{\upharpoonright}x\mathbin{:=}\,$ |  | $\mu k.\,\cdots[k]$ |  | $Q\cdots$ | $\qquad\longrightarrow\qquad$ |  | $\mu k.\,\cdots[k]$ |  | $M\mathbin{\upharpoonright}x\mathbin{:=}\,$ |  | $Q\cdots$
---|---|---|---|---|---|---|---|---|---|---|---|---
$\uparrow$ $s$ |  |  $\uparrow$ $r_{0}$ |  |  $\uparrow$ $r_{i}$ |  |  |  $\uparrow$ $\bar{r}_{0}$ |  |  $\uparrow$ $\bar{s}_{i}$ |  |  $\uparrow$ $\bar{r}_{i}$

where the displayed jumper denotes the $i$-th occurrence of $[k]$ under an
appropriate enumeration $i=1,2,\ldots,n$. For each place $\bar{p}$ in $M$
after reduction, there is a unique corresponding place $p$ in $M$ before
reduction. For each $p$ in $M$, there are $n$ places $\bar{p}=\bar{p}_{i}$
($i=1,2,\ldots,n$), one in each copy. Namely we have an $n$-to-one
correspondence if we look from the term after reduction. For all other places
$\bar{p}$, there is a one-to-one correspondence to the places $p$ before
reduction.

######  Lemma 8.

Let us consider $\beta_{\mu}$ reduction
$C[M\mathbin{\upharpoonright}x\mathbin{:=}\mu k.\,J]\rightarrow C[\mu
k.\,J^{\prime}]$ where
$J^{\prime}=J\\{[k]\square\mapsto[k]M\mathbin{\upharpoonright}x\mathbin{:=}\square\\}$.
We set place symbols as above.

  1. (1)

Strict inequality $|\bar{r}_{0}|<|r_{0}|$ holds.

  2. (2)

$|\bar{p}|\leq|p|$ holds for every place $\bar{p}$ occurring in $C[\mu
k.\,J^{\prime}]$.