数理解析研究所講究録
1533 巻 2007 年 64-85

64

CPS-translation as adjoint-extended abstractKen-etsu Fujita (藤田憲悦)
Gunma University (群馬大学)$\mathrm{f}\mathrm{u}\mathrm{j}$it$\mathrm{a}\emptyset \mathrm{c}\mathrm{s}$.gunma-u.

$\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{p}$Abstract
We show that there exist translations between polymorphic A-calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic A-calculus into the existential type systemis the so-called call-by-name CPS-translation that can be expounded as an adjoint
from the neat connection. The duality appears not only in the reduction relations but
also in the proof structures such as paths between the source and the target calculi.
From a programming point of view, this result means that abstract data types caninterpret polymorphic functions under the CPS-translation. We may regard abstract
data types as a dual notion of polymorphic functions.

1

Introduction

Galois connections arise, even if we do not aware of, in many parts of computer science [8,12]. For instance, examples
logics are demonstrated in Backhouse [1], where provability
or implication relation is a partial order on the set of formulae. Other kinds of examples
come from reduction systems, whcih are shown by Danvy-Lawall [2] and Sabry-Wadler [16],where reduction relation forms a preorder over terms.
On the other hand, the term CPS-translation, in general, denotes a program translation
method into continuation passing style that is the meaning of the program as a function taking the rest of the computation. The method has been studied for program transformation,
definitional interpreter and denotational semantics [13].
We prove that there exist translations between polymorphic -calculus A2 (GirardReynolds) and a subsystem of minimal logic
with existential types, which form a Galois
connection and moreover a Galois insertion (embedding). The translation from A2 intois the so-called call-by-name CPS-translation $[10, 15]$ that can be expounded as the adjointof the inverse translation. Rom a programming point of view, this result also means that
abstract data types [7] can interpret polymorphic functions under the CPS-translation. We
may regard the notion of abstract data types as a dual notion of polymorphic functions.
Our main interest is a neat connection and proof duality between polymorphic types(2nd order universally quantified formulae) and existential types (2nd order existentially$\mathrm{h}\mathrm{o}\mathrm{m}$$\lambda$$\lambda^{\exists}$$\lambda^{\exists}$

65
quantified formulae). It is logically quite natural like de Morgan’s duality, and computationally still interesting, since dual of polymorphic functions with universal type can be
regarded as abstract data types with existential type [7]. Although one can guess the existence of such a duality from the work of Selinger [14], instead of classical systems like
[9, 14, 17], even intuitionistic systems can enjoy that polymorphic types can be interpretedby existential types. That is, computationally polymorphic function with universal typecan be interpreted by abstract data types with existential type, such that the parametric polymorphic function
for $X$ can be viewed, under the CPS-translation , as$X$an abstract data type
for , which is waiting for an implementation with type. This interpretation also contains proof duality, such that the universal
formulae introduction rule is interpreted by the use of the existential formulae elimination
rule, and the universal elimination by the existential introduction. Moreover, with respect
to reduction relations, we evtablished not only a Galois connection but also a Galois insertion (embedding) from polymorphic A-calculus (Girard-Reynolds) into the calculus withexistential types. From the neat connection between the calculi, the fundamental properties$\forall X.A$$*$$\lambda X.M$$(\lambda X.M)^{*}$$\exists X.A^{*}=(\forall X.A)^{*}$

such as normalization and Church-Rosser are related each other.
The paper is organized as follows: Section 2 provides our source and target calculi,
respectively denoted by A2 and . Section 3 is devoted to theA2into . Here we demonstrate that the CPS-translation can be expounded as a lower adjointof the inverse translation. Then the translations constitute a Galois insertion (embedding)from A2 into . Section 4 gives typing relation correspondence between the calculi andproof duality between sequences of formulae called paths.
$\lambda^{\exists}$$\mathrm{C}\mathrm{P}\mathrm{S}- \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}*\mathrm{h}\mathrm{o}\mathrm{m}$$\lambda^{\exists}$$\lambda^{\exists}$2

Source and target calculi

2.1

Source calculus: A2

We introduce our source calculus of 2nd order A-calculus (Girard-Reynolds), denoted by
A2. For simplicity, we first adopt its domain-free style, and next the Church-style when we
discuss proof terms.

Definition 1 (Types)$A::=X|A\Rightarrow A|\forall X.A$

Deflnition 2 ($(\mathrm{P}\mathrm{s}\mathrm{e}\mathrm{u}\mathrm{d}\mathrm{o})\lambda 2$-terms)$\Lambda 2\ni M::=x|$Ax.M Ax.M MM AX.M MA

Deflnition 3 (Reduction rules)$(\eta)\lambda x.Mxarrow M$, if $x\not\in FV(M)$$(\beta_{t})(\lambda X.M)Aarrow M[X:=A]$$(\eta_{t})\lambda X.MXarrow M$, if $X\not\in FV(M)$

$|$

$|$

$|$

$|$

$(\beta)(\lambda x.M_{1})M_{2}arrow M_{1}[x:=M_{2}]$66$FV(M)$ denotes a set of free variables in $M$ .
.

for the compatible relation obtained from the reflexivie and transitiveWe
for that from the transitive closure.
closure of the one step reduction relation, and’denotes the subrelation
In particular,
restricted to the reduction rules. We may write simply for either or , and for either or ,if clear from the context. We employ the notation
indicate the syntactic identity underrenaming of bound variables.
$\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}arrow\lambda 2$$arrow\lambda 2+$$R\subseteq$$\mathrm{o}\mathrm{f}arrow$$arrow R$$(\beta)$$\{\beta, \eta, \beta_{t}, \eta_{t}\}$$(\beta)$$(\eta)$$(\eta)$$(\beta_{t})$$(\eta_{t})$$\equiv \mathrm{t}\mathrm{o}$2.2Target calculus:$\lambda^{\exists}$

We next define our target calculus denoted by , which is logically a subsystem of minimal, negation, conjunction and 2nd order existential quantificalogic consisting of$A^{\exists}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{t}\perp$

tionl.

Deflnition 4 (Types)$A::=\perp|X|\neg A|A\wedge A|\exists X.A$

Definition 5 (-terms)$(\mathrm{P}\mathrm{s}\mathrm{e}\mathrm{u}\mathrm{d}\mathrm{o})\lambda^{\exists}$$\Lambda^{\exists}\ni M$

$::=$

$x|$

Ax.M MM
let X,$|\langle A, M\rangle|$

Definition 6 (Reduction rules)$(\eta)\lambda x.Mxarrow M_{f}$$|\langle M, M\rangle|$$|$$\langle$

let $\langle x, x\rangle=M$ in $M$$=M$ in $M$$x\rangle$$(\beta)(Ax.M_{1})M_{2}arrow M_{1}[x:=M_{2}]$if $x\not\in FV(M)$$(1\mathrm{e}\mathrm{t}_{\wedge})$let$\langle x_{1},x_{2}\rangle=\langle M_{1}, M_{2}\rangle$$(1\mathrm{e}\mathrm{t}_{\bigwedge_{\eta}})$let$\langle x_{1}, x_{2}\rangle=M_{1}$in $Marrow M[x_{1}:=M_{1}, x_{2}:=M_{2}]$in $M[z:=\langle x_{1}, x_{2}\rangle]arrow M[z:=M_{1}]$ ,if$(1\mathrm{e}\mathrm{t}_{\exists})$$(1\mathrm{e}\mathrm{t}_{\exists_{n}})$let X,$\langle$

let X,$\langle$$x\rangle$$=\langle A, M_{1}\rangle$$x\rangle$$=M_{1}$$x_{1},$$x_{2}\not\in FV(M)$in $Marrow M[X:=A, x:=M_{1}]$in $M[z:=\langle X, x\rangle]arrow M_{2}[z:=M_{1}]$ ,We also write simply (let) for eitherorSimilarly we
as done for A2.
$(1\mathrm{e}\mathrm{t}_{\wedge})$$(1\mathrm{e}\mathrm{t}_{\exists})$

, and

if
$(1\mathrm{e}\mathrm{t}_{\eta})$for$X,$ $x\not\in FV(M_{2})$$(1\mathrm{e}\mathrm{t}_{\bigwedge_{\eta}})$or$(1\mathrm{e}\mathrm{t}_{\exists_{0}})$.

$\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}arrow\lambda^{\exists}\mathrm{a}\mathrm{n}\mathrm{d}-arrow \mathrm{b}^{+}\lambda^{\exists}$

1For further introduction of the CPS target calculus

version [4] of this paper.

$\lambda^{\exists}$

with let-expressions, see also the previous

67

3CPS-translation and Galois connection
3.1

A2 into$\mathrm{C}\mathrm{P}\mathrm{S}-\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}*\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}$$\Lambda^{\exists}$

We define a translation, so-called modified CPS-translation *from pseudo -terms into
pseudo -terms, which preserves not only reduction relations but also typing relations
introduced later. In each case, a fresh and free variable is introduced, which is called acontinuation variable.
$\lambda 2$$A^{\exists}$$a$Deflnition 72.

1. $x^{*}=xa$$(Ax.M)*=\mathrm{l}\mathrm{e}\mathrm{t}\langle x, a\rangle=a$

3. $(M_{1}M_{2})^{*}=\{$

4.

in$M^{*}$

for$M_{1}^{*}[a:=\langle x, a\rangle]$otherwise$M_{1}^{*}[a:=\langle Aa.M_{2}^{*}, a\rangle]$$(\lambda X.M)^{*}=\mathrm{l}\mathrm{e}\mathrm{t}\langle X, a\rangle=a$in$M_{2}\equiv x$$M^{*}$

5. $(MA)^{*}=M^{*}[a:=\langle A^{*}, a\rangle]$
6. $X^{*}=X_{j}$;$(A_{1}\Rightarrow A_{2})^{*}=\urcorner A_{1}^{*}\wedge A_{2}^{*}$$(\forall X.A)^{*}=\exists X.A^{*}$

contains exactly one free occurrence of a continuation variable , andhas neither -redex nor -redex. Let. Then, under the translation,
have typethe parametric polymorphic function
with respect to $X$ becomes an abstract data
type
togetherfor $X$ , which is waiting for an implementation with typewith an interface (a signature) with type , i.e., (AX.M)’ isRemarked that

$M^{*}$$a$$\beta$$\lambda X.M$$\eta$$M^{*}$$\forall X.A$$\lambda X.M$$(\lambda X.M)^{*}$$\exists X.A^{*}$$a$$A^{*}$

abstype $X$ with $a:A^{*}$ is

$a$

in

$M^{*}$

in a familiar notation.

1. We have
Lemma 1.
In particular, $M_{1}^{*}[x:=Aa.M_{2}^{*}]arrow\beta(M_{1}[x:=M_{2}])^{*}$ provided that$M_{1}^{*}[x:=\lambda a.M_{2}^{*}]arrow\beta\eta(M_{1}[x:=M_{2}])^{*}$

2. If$M_{1}arrow_{\beta}M_{2}$, then3. If$M_{1}arrow_{\eta}M_{2}$, then$M_{1\beta\eta \mathrm{l}\mathrm{e}\mathrm{t}}^{*+}arrow M_{2}^{*}$$M_{2}$

is not a variable.

.

$M_{1}^{*}arrow_{\eta 1\cdot \mathrm{t}_{\eta}}^{+}M_{2}^{*}$

Proof. By straightforward inductions.
Proposition 1 If we have$M_{1}arrow_{\lambda 2}M_{2}$, thenProof. By induction on the derivation.

$\square$$M_{1\lambda}^{*+}arrow M_{2}^{*}\exists$.
$\square$68
3.2

CPS-translation as adjoint

The main problem is how to define or expound an inverse translation. Sabry and Felleisen[15] have defined the universe of CPS terms, to say, $cps(\Lambda)=$ { $P|M^{*}arrow P$ for some},for mapping canonical CPS terms back to the original ones. In our terminology, for$P\in cps(\Lambda)$ , the downset, andis a subset of. Rom the definition, for each $P\in cps(\Lambda)$ there exists someifsuch that$M^{*}arrow P$ . If we have
, then the inverse of , denoted by , can be defined as $M$,
fortunately. Otherwise, we would take an approximation
to such that, and this process. Then there also exists
A such that
where 1
could be continued. In order to make the plan workable, we should have such a downclosed, and moreover an inverse ofshould be obtained by
set asfor some $M\in$ A. Here we must guarantee thatthe inverse imageisprincipal, i.e.,
is generated by a single. That is,such that$M\in$$P\in
cps(\Lambda)$
A suchthere uniquely exists.
for any
monotonic if $M_{1}arrow M_{2}$ implies
We say that the translation. It is$P\in
cps(\Lambda)$
for some
observed that there may not exists
unlessmonotonic. For
instance, assume thatbutfor some , and no other reductions
are possible. Then cannot be defined along the above. Moreover, for every normal form
there should be uniquely exists $M$ with.
In order to give an inverse translation following the plan above, first we provide themutual inductive definitions, respectively for denotations Univ and continuations , asfollows:$M\in\Lambda$$\downarrow P\mathrm{d}\mathrm{e}\mathrm{f}=\{Q|Parrow Q\}$$cps(\Lambda)$$\downarrow P_{2}\subseteq\downarrow P_{1}$$M\in\Lambda$$P_{1}arrow P_{2}$$M^{*}\equiv P$

$P\#$

$P$

$P_{1}\in\downarrow P$$M_{1}\in$$P_{1}\subseteq\downarrow P$$P$$Parrow P_{1}$$M_{1}^{*}arrow P_{1}$$P\#\equiv M\mathrm{h}\mathrm{o}\mathrm{m}$$P\in\varphi s(\Lambda)$$cps(\Lambda)$$[\downarrow P]^{-*}=\downarrow M$$[\downarrow P]^{-*}$$M\in\Lambda$$[\downarrow P]^{-*}$$[\downarrow P]^{-*}=\downarrow M$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\downarrow M=[\downarrow P]^{-*}$$*\mathrm{i}\mathrm{s}$$M_{1}^{*}arrow M_{2}^{l}$$P\#$$M_{1}arrow M_{2}$$*\mathrm{i}\mathrm{s}$$P$$M_{1}^{*}arrow Parrow M_{2}^{*}$$P\#$$P_{nf}\equiv M^{*}$$P_{nf}$$C$$\frac{C\in C}{xC\in U\mathrm{n}\mathrm{i}v}$$\frac{C\in CP\in Uni\mathrm{v}}{(\lambda a.P)C\in U\mathrm{n}\mathrm{i}v}$$\frac{C\in CP\in Univ}{1\mathrm{e}\mathrm{t}\langle X,a\rangle=C\mathrm{i}\mathrm{n}P\in Uni\mathrm{v}}$$\frac{C\in CP\in Uni\mathrm{v}}{1\mathrm{e}\mathrm{t}\langle x,a\rangle=C\mathrm{i}\mathrm{n}P\in Un\mathrm{i}\mathrm{v}}$$\frac{C\in C}{\langle x,C\rangle\in C}$$a$$\in C$$\frac{C\in CP\in Univ}{\langle\lambda a.P,C\rangle\in C}$$\frac{C\in C}{\langle A^{*},C\rangle\in C}$

forwith $n>1$ , andWe writeforwith $n=1$ .
$C\in C$ is in the form of, orwhere $R_{i}(1\leq i\leq n)$ iswith $n\geq 0$ .
We explicitly mention that $C\in C$ has exactly one occurence of free variable such thatwith $n\geq 0$ . $P\in Univ$ also has exactly one occurence of hee variableainsuchC asaproper subterm of P.
$\langle R_{1}, R_{2}, \ldots, R_{n}\rangle$$\langle R_{1}, \langle R_{2}, \ldots, R_{n}\rangle\rangle$$\langle R_{1}\rangle$$\langle R_{1}, \ldots, R_{n}, a\rangle$$x,$$\lambda a.P$

$R_{1}$$A^{*}$$a$$C\equiv\langle R_{1}, \ldots, R_{n}, a\rangle$

Lemma 2
2. If

1. If $P_{1}\in Univ$ and$C_{1}\in C$

and$C_{1}arrow_{\lambda^{\exists}}C_{2}$$P_{1}arrow_{\lambda}{}_{\exists}P_{2}$, then$C_{2}\in C$.

, then$P_{2}\in$

Univ.

69
Proof. Let

and$P,$ $P_{1}\in Univ$$C,$ $C_{1}\in C$. Then $P[a:=C_{1}],$$P[x:=\lambda a.P_{1}],$

Univ, and $C[a:=C_{1}],$ $C[x:=\lambda a.P_{1}],$ $C[X:=A^{*}]\in C$ .

$P[X:=A^{*}]\in\square$is defined over , theHence, both Univ and are closed
is well-defined over Univ and as well.
binarydefined by $Parrow Q$ , the reflexive and transitive
We employ a preorder. Then an inverse of $P\in$ Univ, denoted by $u(P)$ is defined as anof one step
upper adjoint (left adjoint) of , as follows:$\Lambda^{\exists}$$C$$\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{r}arrow\lambda^{\exists}\cdot \mathrm{A}\mathrm{l}\mathrm{t}\mathrm{h}\mathrm{o}\mathrm{u}\mathrm{g}\mathrm{h}arrow\lambda^{\exists}$$C$$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow\lambda^{\exists}$$\mathrm{c}\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{u}\mathrm{r}\mathrm{e}arrow$$Q\subseteq P$$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow$$*$$u(P)^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}} \sup\{M\in\Lambda 2|M^{*}\subseteq P\}$a preorder here rather than a partial order
The existence of $\sup$ is not trivial,in complete lattices [8, 1, 12]. In fact, this definition works well, which can be verified bycase analysis on $P\in$ Univ, in the following way:$\mathrm{s}\mathrm{i}\mathrm{n}\mathrm{c}\mathrm{e}\subseteq \mathrm{i}\mathrm{s}$$\bullet$Case
Rom the definition of
where$P\equiv xC\equiv x\langle R_{1}, \ldots, R_{n}, a\rangle$

-If

-If
-If
$\bullet$$R_{i}\equiv x_{i}$$*,$$u(P)$

with $n\geq 0$

is in the form of$xN_{1}\ldots N_{n}$from the definition of .
, then similarly find the maximum, then we take.

, then$N_{i}$,$*$$N_{i}\equiv x_{i}$$N_{i}$$R_{i}\equiv\lambda a.P_{i}$$R_{\dot{\tau}}\equiv A_{i}^{*}$

for some term or typesuch that$N_{:}^{*}\subseteq P_{i}$.

$N_{i}\equiv A_{i}$Case $P\equiv(\lambda a.P’)C$
We have no $M$ such that $M^{*}\equiv(Aa.P’)C$ . Then we should find the greatest $M’$ suchthat $M^{J*}\subseteq P’[a:=C]\subseteq(\lambda a.P’)C$ , where is a linear variable.
$a$$\bullet$Case$P\equiv 1\mathrm{e}\mathrm{t}\langle x, a\rangle=C$

is in the form ofgreatest $M$ such that$u(P)$

-If

-If
-If
$\bullet$Case$R_{i}\equiv x_{i}$in $P’$ with $C=\langle R_{1}, \ldots, R_{n}, a\rangle(n\geq 0)$$(\lambda x.M)N_{1}\ldots N_{n}$$M^{*}\subseteq P’$$N_{i}$, where we should find the, and:.
then
then find the greatest.
then$N_{i}\equiv x_{i}$$R_{i}\equiv\lambda a.P_{i}$$R_{i}\equiv A_{i}^{*}$

for some $M$ and$N_{i}$

such that$N_{i}^{*}\subseteq P_{i}$.

$N_{i}\equiv A_{i}$$P\equiv 1\mathrm{e}\mathrm{t}\langle X, a\rangle=C$

in $P’$ is handled simiarly.

Here we have a valid induction measure, since continuation variable is linear and we always
choose strictly smaller subterms to find an upper adjoint. This definition is summarized
as follows:$u$

1. $u(x)=x;u(\lambda a.P)=u(P);u(A^{*})=A$
2. $u(x\langle R_{1}, \ldots, R_{n}, a\rangle)=x(u(R_{1}))\ldots(u(R_{n}))$

3. $u((\lambda a.P)C)=u(P[a:=C])$
4.

$u$

(let

$\langle x,$$a\rangle=\langle R_{1},$$\ldots,$$R_{n},$$a\rangle$

in $P$ ) $=(\lambda x.u(P))(u(R_{1}))\ldots(u(R_{n}))$

70
5.

$u$

(let

$\langle X,$$a\rangle=\langle R_{1},$$\ldots,$$R_{n},$$a\rangle$

in $P$ ) $=(AX.u(P))(u(R_{1}))\ldots(u(R_{n}))$, and the clause 2 through 5 aresuch that
where the clause 1 is forfor $P\in$ Univ.
The discussion above essentially gives a proof to the statement that for any $P\in$ Univ,.
such that 1
there uniquely exists
On the other hand, usually the definition of inverse translation cah be inductively
given as follows $[6, 5]$ , where we write $C[]$ for $C\in C$ with a hole :$\langle R_{1}, \ldots, R_{n}, a\rangle\in C$$R_{i}$$M\in\Lambda 2$$M=[\downarrow P]^{-*}$

$\#$

$[]$

Definition 8(0) $x\#=x;(\lambda a.P)\#=P\#;(A^{*})\#=A$(1) $(xC)\#=C\#[x]\#$(2) $((Aa.P)C)\#=C\#[(\lambda a.P)\#]$(3) (let$\langle x,$$a\rangle=C$

in $P$ ) $\#=C\#[\lambda x.P\#]$(4) (let X, $a\rangle=C$ in $P$ ) $\#=C\#[AX.P\#]$$\langle$(5) $a\#=[]$(6) $\langle x, C\rangle\#=C\#[[]x\#]$(7) $\langle\lambda a.P, C\rangle\#=C\#[[](Aa.P)\#]$(8)$\langle A^{*}, C\rangle\#=c\#[[](A^{*})\#]$

Note that we have $c\#=$$[$$]R_{1}^{\#}\ldots R_{n}\#$with left associativity, if $C\in C$ is in the form of$\langle R_{1}, \ldots, R_{n}, a\rangle$.

Lemma 3

1. $(P[a:=C])\#=C\#[P\#]$

2. Let$P,$ $P_{1}\in Univ$

and $C\in C$ .

$(P[x:=\lambda a.P_{1}])\#=P\#[x:=P_{1}^{\#}]$$(C[x:=\lambda a.P_{1}])\#=C\#[x:=P_{1}^{\#}]$

Proof. By induction on the structures of$P$

and C.

Proposition 2 (Inverse translation as adjoint) For any$P\#$$\square$, we have $u(P)=$$P\in Un\mathrm{i}v$.

Proof. By induction on the structure of$P\in$

Univ.

$\square$In turn, given as above, a lower adjoint (right adjoint) of is defined as follows:
$\#$

$\#$

$l(M)^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}} \inf\{P\in U\mathrm{n}\mathrm{i}\mathrm{v}|M\subseteq P\#\}$

Then the recursive procedure to find $l(M)$ is provided by case analysis on $M$ .
$\bullet$Case $M$ of :We have $l(x)=xa\in$ Univ, since $x\subseteq x=(xa)\#$ .
$x$

71

$\bullet$Case $M$ of Ax.M’:(letbom Ax.M’. Thensuch thatin $P$ ) , we should find the minimal $P\in Univ$$l(\lambda x.M’)$ is in the form of let
in $P$ .

$\subseteq\lambda x.P\#=$$M’\subseteq P\#$$\bullet$Case $M$ of$M_{1}M_{2}$$\#$$\langle x,$$a\rangle=a$$\langle x, a\rangle=a$:-Case $M\equiv xM_{2}$ :We have$xM_{2}\subseteq xR\#=(x\langle R, a\rangle)\#$. Here$R$

is either

$x’$

or

$\lambda a.P$.
, then $l(xx’)=x\langle x’, a\rangle$ from, find the least $P\in Univ$ such that.
the form offor some $P\in$ Univ.

$x^{\prime\#}=x’$$*\mathrm{I}\mathrm{f}M_{2}\equiv x’$$M_{2}\subseteq P\#$$*\mathrm{O}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{w}\mathrm{i}\mathrm{s}\mathrm{e}$. Then$l(xM_{2})$is in$x\langle P, a\rangle$:-Casein ) , we should find theFrom. As in the previous
least and , respectively such that
and$P’\in$is in thecase, is either or
Univ. Thenfor some.
inform of letin or let-Case $M\equiv M_{4}M_{3}M_{2}$ :$M\equiv(\lambda x.M_{3})M_{2}$$P$$(\lambda x.M_{3})M_{2}\subseteq(\lambda x.P\#)R\#=(1\mathrm{e}\mathrm{t}\langle x, a\rangle=\langle R, a)$

$P$

$R$

$M_{2}\subseteq R\#$

$M_{3}\subseteq P^{t}$

$x’$

$R$

$\#$

$l((\lambda x.M_{3})M_{2})$$\lambda a.P’$$P$$\langle x, a\rangle=\langle x‘, a\rangle$$P$$\langle x, a\rangle=\langle P’, a\rangle$$R_{2},\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}1\mathrm{y},\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{h}\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}M_{4}\subseteq p\#,M_{2}\subseteq R_{3}\mathrm{R}\mathrm{o}\mathrm{m}M_{4}M_{3}M_{2}\subseteq P\# R_{3}^{\#}R_{2}^{\#}=(P[a:=\langle R_{3},R_{2},a\rangle])\#=((\lambda a.P)\langle R_{3},R_{2}, a\rangle \mathit{1}_{\mathrm{a}\mathrm{n}\mathrm{d}}^{\#},’ \mathrm{w}\mathrm{e}$$\mathrm{S}\mathrm{h}\mathrm{o}\mathrm{u}1\mathrm{d}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{S}\mathrm{t}P,R_{3},$$M_{2}\subseteq R_{2}^{\#}$

either$\bullet$$x_{\dot{\iota}}’$Case $M$ of
Rom AX.M’such that. Thenor$\lambda a.P_{i}’$$\lambda X.M$

Case $M$ of$M_{i}\subseteq P_{i}^{\prime\#}$, wherefor $i=2,3$ .

$R_{i}’$

isin $P$ ) , we should find the least $P\in Univ$. Then $l(\lambda X.M’)$ is in the form of let X, $=a$ in $P$ .

$\subseteq\lambda X.P\#=$$M_{1}A$$P[a:=\langle R_{3}’, R_{2}’, a\rangle]$:$M’\subseteq P\#$$\bullet$is in the form of$P_{1}’\in
Univ$together withfor$l(M_{4}M_{3}M_{2})$(let$\langle X,$$\#$$a\rangle=a$$a\rangle$$\langle$:-Case $M\equiv xA$ :, we have
Since-Other cases can be confirmed similarly.
$xA\subseteq xA=(x\langle A^{*}, a\rangle)\#$$l(x\langle A^{*}, a\rangle)=xA$.

That is, the procedure is summarized in the following, where we write $N$ for either a term
or a type:$l$

1. $l(x)=xa$2.

$l(\lambda x.M)=1\mathrm{e}\mathrm{t}\langle x, a\rangle=a$3.

$l(\lambda X.M)=1\mathrm{e}\mathrm{t}\langle X, a\rangle=a$

in $l(M)$in $l(M)$

4. $l(MN_{1}\ldots N_{n})=l(M)[a:=\langle l’(N_{1}), \ldots, l’(N_{n}), a\rangle]$
where $l’(x)=x;l’(A)=A^{*};l’(M)=\lambda a.l(M)$ otherwise.
The CPS-trtslation$*\mathrm{i}\mathrm{s}$of course the lower adjoint of from the definitions.
$\#$

Proposition 3 (CPS-translation as adjoint) For any$M\in\Lambda 2$, we have $l(M)=M^{*}$ .

72
Galois insertion (embedding)

3.3

As expected from the previous propositions, the translations form the so-called Galois.
andconnection between$Uni\mathrm{v}$$\lambda \mathit{2}$Lemma 4 Let$P_{2}\in Un\mathrm{i}v$$P_{1},$.

, then$P_{1}^{\#}\equiv P_{2}^{\#}$, then$P_{1}^{\#}\equiv P_{2}^{\#}$

1. If$P_{1}{}_{arrow\beta}P_{2}$

2. If$P_{1}arrow_{\eta}P_{2}$

S. If$P_{1}{}_{arrow 1\mathrm{Q}\mathrm{t}}P_{2}$

4. If$P_{1}arrow_{1\mathrm{e}\mathrm{t}_{\eta}}P_{2}$, then.
.
.

$P_{1}^{\#}{}_{arrow\beta}P_{2}^{\#}$, then$P_{1}^{\#}arrow_{\eta}P_{2}^{\#}$.

Proof. By induction on the derivations.
Lemma 5 Let$M\in\Lambda 2$

1. $M^{*\#}\equiv M$ andand $P\in$ Univ.

$Parrow_{\beta\eta}P\#*$

2. If $M$ is in -normal, thenIf is in -normal, then$\lambda 2$$P$$\square$$A^{\exists}$$M^{*}$

is in$\lambda^{\exists}$-normal.

is in A2-normal.

$P\#$

Proof. By induction on the structures of$M\in\Lambda \mathit{2}$and $P\in$ Univ.

$\square$

Theorem 1 (Galois insertion) A2, Univ,
forms a Galois connection, in particular$M^{*\#}\equiv M.$
andThat is, let $M,$
Galois insertion (embedding) such thatproperties:
following
theUniv. Then we have$*,$$\langle$$\#\rangle$$M_{1},$ $M_{2}\in\Lambda \mathit{2}$$P,$ $P_{1},$ $P_{2}\in$

1. If$M_{1}arrow_{\lambda 2}M_{2}$

2. If$P_{1}arrow_{\lambda}\exists P_{2}$

3. If

then

then

$M^{*\#}arrow_{\lambda 2}M$

$M_{1}^{*}arrow\lambda^{\exists}M_{2}^{*}$$P_{1}^{\#}{}_{arrow\lambda 2}P_{2}^{\#}$

and

.

.

$Parrow\lambda^{\exists}P\#*$.

In other words:$P^{\#}arrow_{\lambda 2}M$

if and only if$Parrow_{\lambda^{\exists}}M^{*}$

Proof. From Lemmata 4 and 5.

$\square$We summarize results induced from the discussion above.
Corollary 1

2.

$\lambda 2$

1. Strong normalization of Univ implies that of.

is weakly normalizing iff Univ is weakly normalizing.

3. There exzsts$a$one-to-one correspondence between

foms.

4.

$A2$

is Church-Rosser iff Univ is Church-Rosser.
We remark thatitself is not Church-Rosser.

$\lambda 2$$\Lambda^{\exists}$$\lambda 2$-normal forms and Univ-normal

73
5. Given the $translation*$ . Then an inverse translation which satisfies the properties ofLemma 4 and Lemma 5 (1) above is unique under renaming of bound variables.
6.

is principal,
Univ. Then an inverse image
that is generated by ais equal
in the sense that the inverse image.
single$Let\downarrow P$

be$\{Q|Parrow\exists\lambda Q\}$

for$P\in$$of\downarrow P$$to\downarrow(P\#)$$of\downarrow P$$P\#\in\Lambda 2$

7.

$Let\downarrow\lambda^{\exists}$[A2]’ be {$Parrow\rho_{\eta}M^{*}for$

Then weWe remark$P|M^{*}arrow\lambda^{\exists}P$

some$M\in\Lambda 2$}.

$have\downarrow_{\lambda}\mathrm{a}[\Lambda 2]^{*}\subseteq Univ$$(\lambda a.xa)a\in$for some$=\uparrow\beta\eta[\Lambda \mathit{2}]^{*}$$that\subseteq is$strict, for instance,

Univ, but$(\lambda a.xa)a\not\in\downarrow\lambda^{\exists}[\Lambda 2]^{*}$$M\in\Lambda \mathit{2}$}.

$Let\uparrow\beta\eta[\Lambda 2]^{*}$

be $\{P\in Univ$

$|$

.

.

4

Proof duality

4.1

Typing relation correspondence

Fkom now on, we consider proof terms in the Church-style, and so are terms in Univ or .
for pairs in . We
, andIn particular, we write $Aa:A^{*}.P$ for -terms in,
respectively,asfollows.
give type assignment rules forand$Un\mathrm{i}v$$\lambda$$C$$\lambda^{\exists}$$\lambda 2$$\lambda 2$.

$\langle A_{1}^{*}, C\rangle_{\exists X.A}$$C$:$\frac{x:A\in\Gamma}{\Gamma\vdash x:A}$$\frac{\Gamma\vdash M_{1}:A_{1}\Rightarrow A_{2}\Gamma\vdash M_{2}:A_{1}}{\Gamma\vdash M_{1}M_{2}:A_{2}}(\Rightarrow E)$$\frac{\Gamma,x:A_{1}\vdash M:A_{2}}{\Gamma\vdash\lambda x:A_{1}.M:A_{1}\Rightarrow A_{2}}(\Rightarrow I)$$\frac{\Gamma\vdash M:A}{\Gamma\vdash AX.M:\forall X.A}(\forall I)^{\star}$

where$A^{\exists}$$(\forall I)^{\star}$$\frac{\Gamma\vdash M:\forall X.A}{\Gamma\vdash MA_{1}:A[X:=A_{1}]}(\forall E)$

denotes the eigenvariable condition $X\not\in FV(\Gamma)$ .

:$\frac{x:A\in\Gamma}{\Gamma\vdash x:A}$$\frac{\Gamma,x:A\vdash M:\perp}{\Gamma\vdash\lambda x:A.M:\neg A}(\neg I)$$\frac{\Gamma\vdash M_{1}:A_{1}\Gamma\vdash M_{2}:A_{2}}{\Gamma\vdash\langle M_{1},M_{2}\rangle:A_{1}\wedge A_{2}}(\wedge I)$$\frac{\Gamma\vdash M_{1}:\neg A\Gamma\vdash M_{2}:A}{\Gamma\vdash M_{1}M_{2}:\perp}(\neg E)$$\frac{\Gamma\vdash M_{1}:A_{1}\wedge A_{2}\Gamma,x_{1}:A_{1},x_{2}:A_{2}\vdash M:A}{\Gamma\vdash 1\mathrm{e}\mathrm{t}\langle x_{1},x_{2}\rangle=M_{1}i\mathrm{n}M:A}(\wedge E)$

74$\frac{\Gamma\vdash M:A[X:=A_{1}]}{\Gamma\vdash\langle A_{1},M\rangle_{\exists X.A}:\exists X.A}(\exists I)$$\frac{\Gamma\vdash M:\exists X.A\Gamma,x:A\vdash M_{1}:A_{1}}{\Gamma\vdash 1\mathrm{e}\mathrm{t}\langle X,x\rangle=Mi\mathrm{n}M_{1}:A_{1}}(\exists E)^{\star}$denotes the eigenvariable condition $X\not\in FV(\Gamma, A_{1})$ .
where
The typability problem foris decidable, i.e., given and $M$ , we can find
. We give a certain typability for terms \‘a la Church in Univ or .
$(\exists E)^{\star}$$\lambda^{\exists}$$\Gamma$$A$

such that$C$$\Gamma\vdash_{\lambda}\exists M:A$

Lemma 6 For $P\in Univ$ and1. if we have

2. if we have

$C\in C_{f}$“,$a:A^{*}\vdash_{\lambda^{\ni}}P:B_{1}$then$B_{1}\equiv\perp_{i}$and$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda^{\ni}}C:B_{2}$then$B_{2}\equiv A_{1}^{*}$

for some$\neg\Gamma$$A_{1}$.

This lemma means that if the unique variable has some type in the form ofand other
$P\in
Univ$
free variables in or , denoted by , have typefor some , thenhas type
has typefor some .
$A^{*}$

$a$

$P$

$C$

$\perp \mathrm{t}\mathrm{d}C\in C$$x$$A_{1}$$\neg A_{1}^{*}$$A_{2}$$A_{2}^{*}$

Proof. By simultaneous induction on the structures of
1. Case of$B\equiv\perp,$

2. Case of$\neg\Gamma^{*},$, and$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda}\mathrm{a}C:A^{\prime*}$3. Case of$\neg\Gamma^{*},$$\neg\Gamma^{*},a:A^{*}\vdash_{\lambda^{\exists}}\lambda d.P:\neg B’$$\neg\Gamma$

“,

$C$

.

for some $A’$ .

$a:A^{*}\vdash_{\lambda^{\exists}}(\lambda a’.P)C:B$, and
By the second induction hypothesis, we have

$B\equiv 1,$

and$a:A^{*}\vdash_{\lambda^{\exists}}xC:B$$x:\neg A^{\prime*}\in\neg\Gamma^{*}$$\neg\Gamma^{*},$$P$$a:A^{*}\vdash_{\lambda^{\exists}}$$a:A^{*}\vdash_{\lambda^{\exists}}C$:let$A_{1}\wedge A_{2}$$\neg\Gamma^{*},$$\langle x, a’\rangle=C$$a:A^{*}\vdash_{\lambda^{\exists}}C:B’$$B’\equiv A^{\prime*}$for some $B’$ .

for some$A’$.

in $P:B$, andfor some.
, and from the second induction
From the first induction hypothesis, we have$A’$
hypothesis, we haveA
for some . From the definition,andfor some.
$\neg\Gamma^{*},$$a:A^{*},$ $x:A_{1},$ $a’$:$A_{2}\vdash_{\lambda}\exists P:B$

$A_{1},$ $A_{2}$$B\equiv\perp$$A_{1}$$\neg\Gamma^{*},$$A_{1}\equiv\neg A_{3}^{*}$$A_{3},$ $A_{4}$$A_{2}\equiv A_{4}^{*}$

4. Case of$A_{2}\equiv A^{\prime*}$$a:A^{*}\vdash_{\lambda^{\exists}}$

let X,$\langle$$a’\rangle$$=C$ in $P:B$, andfor some$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda^{\exists}}C:\exists X.A_{1}$$\neg\Gamma^{*},$$a:A^{*},x:A_{1}\vdash_{\lambda^{\exists}}P:B$$A_{1}$.

From the first induction hypothesis, we have
, and from the second induction
hypothesis, we havefor some . Rom the definition,
for some$B\equiv\perp$$\exists X.A_{1}\equiv A_{2}^{*}$$A_{3}$.

5. Case of
We have $B\equiv A$“.
$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda}\exists a:B$

$A_{2}$$A_{1}\equiv A_{3}^{*}$

75
6. Case of$\neg\Gamma^{*},$$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda^{\exists}}\langle x, C\rangle$$a:A^{*}\vdash_{\lambda^{\exists}}x:B_{1}$$B_{1}\equiv\neg A_{1}^{*}\in\neg\Gamma^{*}$

7. Case of$\neg\Gamma^{*},$, andfor some:$B$$\neg\Gamma^{*},$$A_{1}$$a:A^{*}\vdash_{\lambda}\exists\langle\lambda a’ :$a:A^{*}\vdash_{\lambda^{\exists}}C:B_{2}$, and$B_{2}\equiv A_{2}^{*}$:A^{\prime*}.P, C\rangle$:, andsecond induction hypothesis, we have$\neg\Gamma^{*},$$a:A”\vdash_{\lambda}\exists\lambda a’$

8. Case of
We have$\neg\Gamma^{*},$$A^{\prime*}.P:\neg A^{;*}$:$\neg\Gamma^{*},$$B_{1},$ $B_{2}$.

by the second induction hypothesis.

$B$$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda^{\exists}}\langle A_{1}^{*}, C\rangle_{\exists X.A_{\dot{2}}}$for some$a:A”\vdash_{\lambda}\exists C:B_{2}$$B_{2}\equiv B_{3}^{*}$

for some

for some$B_{3}$$B_{1},$ $B_{2}$.

. From the$B$$a:A^{*}\vdash_{\lambda}\exists C:A_{2}^{*}[X:=A_{1}^{*}]$, and$B\equiv\exists X.A_{2}^{*}$.

Fbom the above, the following set of typing rules, denoted byand :$\lambda_{U}^{\exists}$, is enough for Univ

$C$$\frac{x:\neg A_{1}^{*}\in\neg\Gamma^{*}\neg\Gamma^{*},a:A^{*}\vdash C:A_{1}^{*}}{\neg\Gamma^{*},a:A^{*}\vdash xC:\perp}$$\frac{\neg\Gamma^{*},a:A^{*}\vdash C:\neg A_{1}^{*}\wedge A_{2}^{*}\neg\Gamma^{*},x:\neg A_{1}^{*},a:A_{2}^{*}\vdash P:\perp}{\neg\Gamma^{*},a:A^{*}\vdash 1\mathrm{e}\mathrm{t}\langle x,a\rangle=Ci\mathrm{n}P:\perp}(\wedge E)$$\frac{\neg\Gamma^{*},a:A^{*}\vdash C:\exists X.A_{1}^{*}\neg\Gamma^{*},a:A_{1}^{*}\vdash P:\perp}{\neg\Gamma^{*},a:A^{*}\vdash 1\mathrm{e}\mathrm{t}\langle X,a\rangle=Ci\mathrm{n}P:\perp}(\exists E)^{\star}$$\frac{\neg\Gamma^{*},a:A^{*}\vdash C:A_{1}^{*}\neg\Gamma^{*},a:A_{1}^{*}\vdash P:\perp}{\neg\Gamma^{*},a:A^{*}\vdash(\lambda a:A_{1}^{*}.P)C:\perp}(\neg IE)$$\neg\Gamma^{*},a:A^{*}\vdash a:A^{*}$$” \frac{x:\neg A_{1}^{*}\in\neg\Gamma^{*}\neg\Gamma^{*},a:A^{*}\vdash C:A_{2}^{*}}{\neg\Gamma,a:A^{*}\vdash\langle x,C\rangle:\neg A_{1}^{*}\wedge A_{2}^{*}}(\wedge I_{vat})$$\frac{\neg\Gamma^{*},a:A_{1}^{*}\vdash P:\perp\neg\Gamma^{*},a:A^{*}\vdash C:A_{2}^{*}}{\neg\Gamma^{*},a:A^{*}\vdash\langle\lambda a:A_{1}^{*}.P,C\rangle:\neg A_{1}^{*}\wedge A_{2}^{*}}(\wedge I_{\lambda})$$\frac{\neg\Gamma^{*},a:A^{*}\vdash C:A_{1}^{*}[X:=A_{2}^{*}]}{\neg\Gamma^{*},a:A^{*}\vdash\langle A_{2}^{*},C\rangle_{\exists X.A}\mathrm{i}:\exists X.A_{1}^{*}}(\exists I)$

where$(\exists E)^{\star}$

Lemma 72.

$\neg\Gamma^{l},$denotes the eigenvariable condition1.

$\urcorner\Gamma^{*},$$a:A^{*}\vdash_{\lambda}{}_{\exists}P:\perp if$$a:A^{*}\vdash_{\lambda^{\ni}}C:A_{1}^{*}$$X\not\in FV(\Gamma, A_{1})$and only if

if and only if$\neg\Gamma$“,$\neg\Gamma^{*},$.

$a:A^{*}\vdash_{\lambda_{U}}{}_{\exists}P:\perp$$a:A^{*}\vdash_{\lambda_{U}^{\exists}}C:A_{1}^{*}$

Proof. If-part is clear. Only-if-part is by induction on the structures of

$P$

and

$C$

.

76
Proposition 41. If we have

2. If we have$\neg\Gamma^{*},$$\neg\Gamma^{*},$$a:A^{*}\vdash_{\lambda_{U}^{\exists}}C:A_{1}^{*}$$a:A^{*}\vdash_{\lambda_{U}^{\exists}}P:\perp then$

then$\Gamma\vdash_{\lambda 2}P\#:A$$x:A_{1}\vdash_{\lambda 2}(xC)\#:A$$\Gamma,$.

.

Proof. By simultaneous induction on the derivations.
1. Case of $xC:\perp$
By the induction hypothesis, we have $\Gamma,y:A_{1}\vdash C\#[y]:A$ . Hence, we have$(xC)\#:$
.
from
$A$

$\Gamma,$$x:A_{1}\vdash$$x:A_{1}\in\Gamma$

2. Case of let
in $P:\perp$
By the induction hypotheses, we have
. Hence, we have: .
$\langle x, a\rangle=C$$\Gamma\vdash C\#[\lambda x.P\#]$$A_{2}$

3. Case of let X, $=C$ in $P:\perp$
By the induction hypotheses, we have
. Hence, we have
$X\not\in FV(\Gamma, A_{1})$$y:\forall X.A_{1}\vdash C\#[y]:$ $A$$\Gamma,$$\Gamma\vdash C\#[\lambda X.P\#]$

4. Case of $(\lambda a.P)C:\perp$
By the induction hypotheses, we have
we have $\Gamma\vdash C\#[P\#]:A$ .
$a$

:

$A$

and

$\Gamma,$

:

$A$

.
:

$y:A_{1}\vdash c\#[y]$

$A$

and

and

$\Gamma\vdash P\#:A_{1}$$\Gamma\vdash P\#$:

$A_{1}$:$A$$x,$ $C\rangle$$\neg A_{1}^{*}$$A_{2}^{*}$$\Gamma,$$A_{2}\vdash C\#[zx]$$A$$\langle\lambda a.P, C\rangle$$A$$z:A_{1}\Rightarrow A_{2}\vdash C\#[zP\#]$:
By the induction hypothesis, we have
$z:\forall X.A_{1}\vdash C\#[zA_{2}]:A$ , where$\langle A_{2}^{*}, C\rangle_{\exists X.A}\mathrm{i}$:$A_{1}$

and$\Gamma,$$y:A_{1}[X:=A_{2}]\vdash C\#[y]$$(z\langle A_{2}^{*}, C\rangle)\#=C\#[zA_{2}]$$\Gamma\vdash_{\lambda 2}M:$$A$$\Gamma,y:A_{2}\vdash C\#[y]$:$A$. Hence,$(z\langle Aa.P, C\rangle)\#=\langle Aa.P, C\rangle\#[z]=C\#[zP^{\mathfrak{p}}]$if and only if$\Gamma\vdash_{\lambda 2}M$:$A$$\neg\Gamma^{*},a:A^{*}\vdash_{\lambda}\exists M^{*}:$, then$\neg\Gamma$“,$\neg\Gamma^{*},$.

.

$a:A^{*}\vdash_{\lambda^{\exists}}M^{*}$$:\perp$:$A$. Hence, we have$\perp$induction on the, then we also havewhere $(M^{*})\#\equiv M$ .

$a:A^{*}\vdash_{\lambda}\exists M^{*}$

derivation. In turn, if we have
. Hence, from Proposition 4 above, we have$M^{*}:$$z:A_{1}\Rightarrow$$\exists X.A_{1}^{*}$$\Gamma,$

Proof. If we have$\Gamma,$$\neg A_{1}^{*}\wedge A_{2}^{*}$$\Gamma\vdash P\#$$\perp$$A$$y:A_{2}\vdash \mathit{0}\#[y]$$x:A_{1}\in\Gamma$:
7. Case of
By the induction hypotheses, we have
we have: , where

Theorem 2. Hence,, where $(xa)\#=x$ .

:6. Case of (A
By the induction hypothesis, we have
: . Hence, we have$(z\langle
x,C\rangle)\#=C\#[zx]$, where: from
.

8. Case ofwhere$A^{*}$$x:A\vdash(xa)^{\mathfrak{p}}$$\Gamma,$:$x:A_{1}\vdash P\#$$\Gamma,$$a\rangle$$\langle$

5. Case of :We have$y:A_{1}\Rightarrow A_{2}\vdash c\#[y]$$\Gamma,$$A$$\Gamma\vdash_{\lambda 2}(M^{*})\#:$$:\perp \mathrm{b}\mathrm{y}$$\neg\Gamma^{*},$$A$$a:A^{*}\vdash_{\lambda_{U}^{\exists}}$

77
4.2

Duality on formulae, proofs and paths

Well-known duality like de Morgan’s appears on the sets of formulae Form with provability
which forms a partial order. Such a duality is characlogical. In Gentzen’s sequent calculus ,terised as translations between the tuples Form,
gives
one example under the translaswitching formulae between antecident and succedent$(A\veeB)^{d}=A^{d}\wedgeB^{d},$,
tion $d:X^{d}=X;(\neg A)^{d}=\neg A^{d};(A\wedge B)^{d}=A^{d}\vee B^{d},$.
iff. Then for Form, and Form, , we have.
and Form,
Along this line, another translation is negation between Form,.
iff
Then we have
Yet another example of translations known as sectioning (Curry version of binary operators) are given in Backhouse [1], as follows:$\vdash \mathrm{o}\mathrm{r}$$\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\Rightarrow \mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{L}\mathrm{K}$$\Rightarrow\rangle$$\langle$$(\forall x.A)^{d}=\exists x.A^{d}$$\Gamma\dashv\Delta^{d}$$\Gamma^{d}\vdash\Delta$$(\exists x.A)^{d}=\forall x.A^{d}$$\vdash\rangle$$\langle$$\dashv\rangle$$\langle$$\neg$$\neg A\Rightarrow B$$\Rightarrow\rangle$$\langle$$\langle$$\Leftarrow\rangle$$A\Leftarrow\neg B$$(A\wedge)$$\mathrm{d}\mathrm{e}\mathrm{f}=Xrightarrow A\wedge X$$(A\Rightarrow)\mathrm{d}\mathrm{e}\mathrm{f}=X\vdasharrow A\Rightarrow X$, and commutativity with
Then we haveiffis
, where $X\not\in FV(A)$ . Moreover, Form,
, and
iff
iff
a poset, and the supremum can be regarded as existential quantification. We may write ais thought of as thepartial. The supremum of the translation$\sup(A\wedge)$is given by the following
supremum of the range of the translation. Then, in fact,$X$ :$B^{(A\wedge)}\Rightarrow C$$\exists X.B^{(A\wedge)}$$B\Rightarrow C^{(A\Rightarrow)}$$(\forall X.B)^{(A\Rightarrow)}$$\mathrm{q}\mathrm{u}\mathrm{a}\mathrm{n}\mathrm{t}\mathrm{i}\mathrm{f}\mathrm{i}\mathrm{e}\mathrm{r}\mathrm{s}^{2}:(\exists X.B)^{(A\wedge)}$$\forall X.B^{(A\Rightarrow)}$$(A\wedge)$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\subseteq \mathrm{i}\mathrm{n}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{a}\mathrm{d}\mathrm{o}\mathrm{f}\Rightarrow$

1. For any $B\in Form,$$B^{(A\wedge)}\subseteq X$

2. For arbitrary $C\in Form$ , if$\Rightarrow\rangle$$\langle$.

$B^{(A\wedge)}\subseteq C$

for any $B\in Form$ , then$X\subseteq C$.

and commutes with
, whereThat is, we have $\sup(A\wedge)=\exists X.A$ A$\inf(A\Rightarrow)=\forall
X.A\Rightarrow X=$
the translationfrom the commutativity. Similarly, we have, as the following $X$ :$X=\mathrm{T}^{(A\wedge)}$$\mathrm{T}\equiv\exists X.X$$\exists$$(A\wedge)$$\perp(A\Rightarrow)\mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\perp\equiv\forall X.X$

1. For any $B\in Form,$$X\subseteq B^{(A\Rightarrow)}$

2. For arbitrary $C\in Form$ , if.

$C\subseteq B^{(A\Rightarrow)}$

for any $B\in Form$ , then$C\subseteq X$.

Not only with provalibity but also with proof terms, Wadler [17] has introduced the dual
calculus for classical propositional logic. The previous simple example
might be involved in the dual calculus. An involutive duality on -calculus is revealed on
the dual calculus via translations.
The control and -control categories by Selinger [14] elegantly reveals, as internal languages, duality between call-by-value and call-by-name Ap-calculi with conjunctions anddisjunctions.
Here we demonstrate another duality on a sequence of formulae from the viewpoint of
proof structures. Following Prawitz [11], we define the notion of paths together with namesof inference rules $(R)$ . In particular, introduction rules are denoted by (I), and eliminations
are by $(E)$ .
$\Gamma^{d}\vdash\Delta\Leftrightarrow\Gamma\dashv\Delta^{d}$$\lambda\mu$$\mathrm{c}$$\overline{2\mathrm{W}\mathrm{e}}$refomulate his di\S cussion[l]in the second order intuitionistic logic.

78
Definition 9 (Path) A sequence consisting of formulaeand inference rules$A_{i}$$(R_{i})$$A_{1}(R_{1})A_{2}(R_{2})\ldots A_{n-1}(R_{n-1})A_{n}$is defined as a path in the deduction(i)$A_{1}$

is a top-formula in

$\Pi$

$\Pi$

of

$\lambda 2$

or$\lambda^{\exists}$, as follows:, which is not discharged by an application of(ii) $A_{1}(i<n)$ is not the minor premiss of an application of$(\Rightarrow E)$or$(\wedge E)$$(\neg E)$

oris the formula occu

is the major premiss of an application; andassumption discharged byor$(\wedge E)$$(\exists E)$$A_{i+1}$;, and either, andis not the major premiss ofor, orby an application of
immediately below$(a)A_{i}$$(\exists E)$$7\mathrm{V}\mathrm{t}nce$$(R_{i})$$A_{i}$$(b)A_{i}$$(R_{i})$of$(\wedge E)$$(\exists E)$, and$A_{i+1}$

is an$(R_{i})$(iii)$A_{n}$

is either a minor premiss of$(\Rightarrow E)$or$(\neg E)$, or the end-formula of .
$\Pi$

We call a path a main path if the path ends with the end-formula of the deduction. We
assign an order to each path , denoted by $ord(\pi)$ . A main path has the order . A paththat ends with a minor premiss of an applicationor
has order $n+1$ if thecorresponding major premiss of this application belongs to a path with order . A lengthof the path $\pi\equiv A_{1}(R_{1})A_{2}(R_{2})\ldots A_{n-1}(R-1)A_{n}$ is defined as , denoted by $len(\pi)$ .
Let be either or $X$ . We simply write let
in
for
$0$

$\pi$

$(\neg E)$$(\Rightarrow E)$

$n$

$n$

$\langle\chi_{1}, \chi_{2}, x_{3}\rangle=M_{1}$$x$$\chi$

let$\langle\chi_{1},y\rangle=M_{1}$in let$\langle\chi_{2}, x_{3}\rangle=y$$M_{2}$

in $M$, and so on.
is a hesh variable. Similarly, we write letinbe a normal form of 2-terms with $m\geq 0$ andiseither a term or a type. Then,

where
Let

$M_{2}$$\langle\chi_{1}, \ldots \dagger \chi_{n}, x\rangle=M_{1}$

$y$

$A$

$M_{nf}\equiv\lambda\chi_{1}\ldots.\lambda\chi_{n}.xN_{1}\ldots N_{m}$$M_{nf}^{*}\equiv \mathrm{l}\mathrm{e}\mathrm{t}\langle\chi_{1}, \ldots,\chi_{n}, a\rangle=a$in$N_{i}$$n,$$x\langle N_{1}^{*}, \ldots, N_{m}^{*}, a\rangle$

is also normal in . We analyze the proof structure of
in terms of paths. We
define the following inference rules correspondence between
and :
, and
.
$\Lambda^{\exists}$$M_{nf}^{*}$$\Lambda^{\exists}$$\Lambda \mathit{2}$$(\Rightarrow I)^{*}=(\wedge E),$$(\Rightarrow E)^{*}=(\wedge I),$

Theorem 3 (Proof duality) Let
the no rmal deduction of$\neg\Gamma^{*},$$(\forall I)^{*}=(\exists E)$$\Pi$$(\forall E)^{*}=(\exists I)$

be the normal deduction of: , and. We have a path of , to say:$\Gamma\vdash_{\lambda 2}M$

$a:A^{*}\vdash_{\lambda}\exists M^{*}$$:\perp$

$\pi$

$A$

$\Pi^{*}$

be

$\Pi$

$A_{1}(E_{1})A_{2}(E_{2})\ldots A_{m}(E_{m})A_{m+1}(I_{m+1})\ldots A_{m+n-1}(I_{m+n})A_{m+n+1}$

with the proviso that $len(\pi)>1$ if $ord(\pi)>0$ ,if, and only if we have a pathof with the same length and $ord(\pi)+1$ order, suchthat$\pi^{*}$$\Pi^{*}$$A_{m+n+1}^{*}(I_{m+n})^{*}A_{m+n-1}^{*}\ldots(I_{m+1})^{*}A_{m+1}^{*}(E_{m})^{*}A_{m}^{*}\ldots(E_{2})^{*}A_{2}^{*}(E_{1})^{*}A_{1}^{*}$.

For a path beginning with a top-formulaand ending with a conclusion , we have
beginning with a top-formula
the corresponding path. The
and ending withside condition concerns a technical matter. Since the definition says that $(Mx)^{*}=M^{*}[a$ $:=$
$A$

$A_{1}$

$\pi$

$\pi$

$A^{*}$$A_{1}^{*}$

79, we have no corresponding path to the type of . Although the definition of the CPStranslation can be simplified as $(Mx)”=M^{*}[a:=\langle\lambda a.xa, a\rangle]$ for removing the condition,
this simplification might involve an extra -redex. The path consisting of the type of suchis not a main path, i.e., the order is greater than and the length is 1.
$x$$\langle x, a\rangle]$$\eta$$0$$x$

Proof. If-part is by induction on the derivation.
1. Case of $M\equiv x$ where $ord(\pi)=0$ and $len(\pi)=1$ :$\frac{x:\neg A^{*}a:A^{*}}{xa:\perp}(\neg E)$

Then$\pi^{*}=A^{*}$

with $ord(\pi^{*})=1=ord(\pi)+1$ and $len(\pi^{*})=1=len(\pi)$ .

2. Case of $M\equiv M_{1}M_{2}$ :$\frac{M_{1}:A^{1}\Rightarrow BM_{2}A\Pi\prod_{:}2}{M_{1}M_{2}:B}(\Rightarrow E)$

where$\pi=\pi_{1}(A\Rightarrow B)(\Rightarrow E)B$

with $ord(\pi)=n+1$ . Then we have$. \frac{\frac{M_{2^{*}}:\perp[a.A^{*}]\Sigma 2}{\lambda a.M_{2}^{*}:\neg A^{*}\langle Aa.M_{2}^{*},a\rangle}(\neg I)a:B^{*}}{\Sigma_{1}:\neg A^{*}\wedge B^{*}}(\wedge I)$$M^{*}[a:=\langle\lambda a.M_{2}^{*}, a\rangle]$“
where path
hypothesis $ord(\pi_{1}^{*})=ord(\pi_{1})+1$ .
$\pi^{*}=B^{*}(\Rightarrow E)$

3. Case of$M\equiv\lambda x$: A.

$M_{1}$$(A\Rightarrow B)^{*}\pi_{1}^{*}$

with$:\perp$$ord(\pi^{*})=ord(\pi)+1\mathrm{h}\mathrm{o}\mathrm{m}$the induction:$[x:A]$$\frac{M_{1}B\prod_{:}1}{\lambda x:A.M_{1}:A\Rightarrow B}(\Rightarrow I)$

where$\pi=\pi_{1}B(\Rightarrow I)(A\Rightarrow B)$. Then we have$[x : \neg A^{*}][a :B^{*}]\Sigma_{1}$$\frac{a:\neg A^{*}\wedge B^{*}M_{1}^{*}:\perp}{1\mathrm{e}\mathrm{t}\langle x,a\rangle=ai\mathrm{n}M^{*}:\perp}(\wedge E)$

wherehypothesis.

$\pi^{*}=(A\Rightarrow B)^{*}(\Rightarrow I)^{*}B^{*}\pi_{1}^{*}$

with $ord(\pi^{*})=ord(\pi)+1$ from the induction

80
4. Case of $M\equiv M_{1}B$ :$\frac{M_{1}\prod_{:\forall^{1}x.A}}{M_{1}B:\mathrm{A}[X:=B]}(\forall E)$

where $\pi=\pi_{1}(\forall X.A)(\forall E)(A[X:=B])$ . Then we have$\frac{a:A^{*}[X:=B^{*}]}{\langle B^{*},a\rangle:\exists X.A^{*},\Sigma_{1}}(\exists I)$$M_{1}^{*}[a:=\langle B^{*}, a\rangle]$$:\perp$where $\pi^{*}=(A[X:=B])^{*}(\forall E)^{*}(\exists X.A^{*})\pi_{1}^{*}$ with order $(\pi^{*})=order(\pi)+1$ .

5. Case of$M\equiv\lambda X.M_{1}$:$\frac{M_{1}A\prod_{:}1}{\lambda X.M_{1}:\forall X.A}(\forall I)$

where$\pi=\pi_{1}A(\forall I)(\forall X.A)$. Then we have$\frac{a:\exists X.A^{*}M_{1^{*}}:\perp[a:A^{*}]\Sigma 1}{1\mathrm{e}\mathrm{t}\langle X,a\rangle=a\mathrm{i}\mathrm{n}M_{1}^{*}:\perp}(\exists E)$

where$\pi^{*}=(\forall X.A)^{*}(\forall I)^{*}A^{*}\pi_{1}^{*}$

with $ord(\pi^{*})=ord(\pi)+1$ .

Only-if-part:Case of $len(\pi^{*})=1$ where $\pi^{*}=A$ “.
In this case, we have $M_{nf}^{*}=xa$ , and hence $M_{nf}=x$ and $\pi=A$ with $ord(\pi)=0$ and$len(\pi)=1$.

Case of $len(\pi^{*})>1$ .
We letandis either a term or a type.

$\pi^{*}=A_{m+n+1}^{*}(I_{m+n})^{*}A_{m+n-1}^{*}\ldots(I_{m+1})^{*}A_{m+1}^{*}(E_{\mathrm{m}})^{*}A_{m}^{*}\ldots(E_{2})^{*}A_{2}^{*}(E_{1})^{*}A_{1}^{*}$

let$\langle\chi_{1}, \ldots, \chi_{n}, a\rangle=a$

From$\pi^{*}\mathrm{t}\mathrm{d}M_{nf}^{*}$

in$x\langle N_{1}^{*}, \ldots, N_{m}^{*}, a\rangle$, where$N_{i}$$M_{nf}^{*}\equiv$, we have the following structure as a part of the normal proof of81$A_{U}^{\exists}$:$\frac{N_{m}^{*}:\neg B_{m+1}^{*}[a:A_{m+1}^{*}]}{\langle N_{m}^{*},a\rangle:A_{m}^{*},:}(E_{m})^{*}$:$\frac{[a:A_{m+2}^{*}];}{\perp,:}\frac{N_{1}^{*}.\neg B_{2}^{*}\langle N_{2}^{*},\ldots,N_{m}^{*},a\rangle:A_{2}^{*}}{\frac{x:\neg A_{1}^{*}}{x}(\neg E)}(E_{1})^{*}$$\frac{a:A_{m+n+1}^{*}}{M}\frac{[a:A_{m+n}^{*}]\perp:}{nf*:\perp\perp(I_{m+n})^{*}}(I_{m+n-1})^{*}$. Here, we haveor
, andis eitheris eitheror$B_{i+1}(1\leq
i\leq
m)$
.
is a term, and thenif
for some:
is to be deleted from the, and then
Otherwise
is a type to say
for some $A_{\+1}’.(1\leq i\leq m)$ .
figure andwhere: $A_{m+n+1}$
position 4, we have the desired derivation of
Following the proof of
follows:
from that ofwhere$N_{1}^{*}:$$(\wedge E)$$(I_{1})^{*}$$(\wedge I)$$(E_{j})^{*}$$(\exists E)$$(\forall I)$$A_{i}^{*}\equiv\neg B_{i+1}^{*}\wedge A_{i+1}^{*}$$N_{i}$$\neg B_{i+1}^{*}$$N_{i}$$N_{i}^{*}$$A_{i^{*}}’$$\neg B_{i+1}^{*}$$A_{i+1}^{*}\equiv A_{i^{*}+1}’[X:=A_{i}^{\prime*}]$$A_{i}^{*}\equiv\exists X.A_{i+1}^{\prime*}$$M_{nf}$$\mathrm{P}\mathrm{r}o$$M_{nf}^{*}$$:\perp \mathrm{a}8$(a) Case of I-part ($\mathrm{i}$. Subcase of
Htom the$A_{i}$

with $1\leq i\leq m+1$ )::deduction where$N_{m}^{*}\equiv x_{m}$$\lambda_{U}^{\exists}$$A_{m}^{*}\equiv(\neg B_{m+1}^{*}\wedge A_{m+1}^{*})$$\frac{x_{m}:\neg B_{m+1}^{*}a:A_{m+1}^{*}}{\langle x_{m},a\rangle:A_{m}^{*}}(\wedge I_{va\mathrm{r}})$we have the$A2$deduction with $(B_{m+1}\Rightarrow A_{m+1})\equiv A_{m}$$\frac{z_{m}:B_{m+1}\Rightarrow A_{m+1}x_{m}:B_{m+1}}{z_{m}x_{m}:A_{m+1}}(\Rightarrow E)$$\mathrm{i}\mathrm{i}$. Subcase of
Rom the:deduction where$N_{m}^{*}\equiv\lambda a.P_{m}$$\lambda_{U}^{\exists}$$A_{m}^{*}\equiv$($\neg B_{m+1}^{*}$

A$A_{m+1}^{*}$):$a:B_{m+1}^{*}:$$\frac{P_{m}:\perp a:A_{m+1}^{*}}{\langle\lambda a.P_{m},a\rangle:A_{m}^{*}}(\wedge I_{\lambda})$we have the$\lambda \mathit{2}$deduction with$(B_{m+1}\Rightarrow A_{m+1})\equiv A_{m}$$\frac{z_{m}:B_{m+1}\Rightarrow A_{m+1}P_{m}\#:B_{m+1}}{z_{m}P_{m}\#:A_{m+1}}(\Rightarrow E)$

82$\mathrm{i}\mathrm{i}\mathrm{i}$. Subcase of
Rom the$N_{m}^{*}\equiv A_{m}^{\prime*}:$$\lambda_{U}^{\exists}$

deduction where$A_{m+1}^{*}\equiv A_{m+1}^{l*}[X:=A_{m}^{\prime*}]$and$A_{m}^{*}\equiv\exists X.\mathrm{A}_{m+1}^{\prime*}$$\frac{a:A_{m+1}^{*}}{\langle A_{m}^{\prime*},a\rangle:\exists X.A_{m+1}^{\prime*}}(\exists I)$

we have the$\lambda 2$

deduction with$\forall X.A_{m+1}’\equiv A_{m}$and $A_{m+1}’[X:=A_{m}’]\equiv A_{m+1}$$\frac{z_{m}:\forall X.A_{m+1}’}{z_{m}A_{m}’:A_{m+1}[X:=A_{m}’]},(\forall E)$$\mathrm{i}\mathrm{v}$. Subcase of
Rom the$N_{1}^{*}\equiv x_{1}$$\lambda_{U}^{\exists}$:

deduction where$A_{1}^{*}\equiv(\neg B_{2}^{*}\wedge A_{2}^{*})$:$a:A_{m+1}^{*}:$$\frac{x_{1}:\neg B_{2}^{*}\langle N_{2}^{*},\ldots,N_{m}^{*},a\rangle:A_{2}^{*}}{\langle x_{1},N_{2}^{*},\ldots,N_{m}^{*},a\rangle:A_{1}^{*}}(\wedge I_{va\mathrm{r}})$we have the$\lambda 2$

deduction with$(B_{2}\Rightarrow A_{2})\equiv A_{1}$$z_{2}$$\frac{z_{1}:B_{2}\Rightarrow A_{2}x_{1}:B_{2}}{z_{1}x_{1}:A_{2}}(\Rightarrow E)$

and

:

: :
$A_{2}$$A_{m+1}:$$z_{2}N_{2}\ldots N_{m}$and hence,$\frac{z_{1}:B_{2}\Rightarrow A_{2}x_{1}:B_{2}}{z_{1}x_{1}:A_{2},::}(\Rightarrow E)$: $A_{m+1}$$(z_{1}x_{1})N_{2}\ldots N_{m}$$\mathrm{v}$. Subcase of
From the:deduction where$N_{1}^{*}\equiv Aa.P_{1}$$A_{U}^{\exists}$$A_{1}^{*}\equiv(\neg B_{2}^{*}\wedge A_{2}^{*})$$a:B_{2}^{*}$::$a:A_{m+1}^{*}$::$\frac{P_{1}:\perp(N_{2}^{*},,N_{m}^{*},a\rangle:A_{2}^{*}}{\langle\lambda a.P_{1},N_{2}^{*},.N_{m}^{*},a\rangle:A_{1}^{*}}::;(\wedge I_{\lambda})$we have the$\lambda 2$

deduction with$(B_{2}\Rightarrow A_{2})\equiv A_{1}$$z_{2}$$\frac{z_{1}:B_{2}\Rightarrow A_{2}P_{1}^{\#}:B_{2}}{z_{1}P_{1}^{\#}:A_{m+1}}(\Rightarrow E)$

and$\frac{z_{1}:B_{2}\Rightarrow A_{2}P_{1}^{\#}:B_{2}}{z_{1}P_{1}^{\#}:A_{2},::}(\Rightarrow E)$: $A_{m+1}$:$A_{2}$$A_{m+1}:$$z_{2}N_{2}\ldots N_{m}$and hence,$(z_{1}P_{1}^{\#})N_{2}\ldots N_{m}$

:

:

83

$\mathrm{v}\mathrm{i}$. Subcase of
From the$N_{1}^{*}\equiv A_{1^{*}}’:$

deduction where$\lambda_{U}^{\exists}$$A_{2}^{*}\equiv A_{2^{*}}’[X:=A_{1}^{\prime*}]$we have thea\rangle:A_{2^{*}}’[X:=.A_{1^{*}}’]:}{\langle A_{1}^{\prime*},N_{2}^{*},..,N_{m}^{*},a\rangle:\exists XA_{2^{*}}},(\exists I)$

deduction with

$A2$

$A_{1}^{*}\equiv\exists X.A_{2}^{J*}$“: $A_{m+1}$:$a$$\frac{\langle N_{2}^{*},\ldots,N_{m}^{*}.’

and$\forall X.A_{2}’\equiv A_{1}$and $A_{2}’[X:=A_{1}’]\equiv A_{2}$:$z_{2}N_{2}\ldots N_{m}:A_{m+1}z_{2}:A_{2}:$$\frac{z_{1}:\forall X.A_{2}’}{z_{1}A_{1}’.A_{2}},(\forall E)$andand hence,$\frac{z_{1}:\forall X.A_{2}’}{z_{1}A_{1}’:A_{2}[X:=A_{1}’],::},(\forall E)$$(z_{1}A_{1}’)N_{2}\ldots N_{m}$: $A_{m+1}$(b) Case of minimum segment:
From thededuction$\lambda_{U}^{\exists}$$a:A_{m+1}^{*}$::$\frac{x:\neg A_{1}^{*}\langle N_{1’)}^{*}N_{m}^{*}.a\rangle:A_{1}^{*}}{x\langle N_{1}^{*},\ldots,N_{m}^{*},a\rangle\cdot\perp}\ldots,(\neg E)$

we have the$A2$deduction$x:A_{1}$:$A_{m+1}:$$xN_{1}\ldots N_{m}$:(c) Case of E–part ( with $m+2\leq j\leq m+n+1$ ):In this case, we have eitheror.
deduction of$A_{j}$$A_{j}^{*}\equiv\neg B_{j-1}^{*}\wedge A_{j-1}^{*}$$M_{nf}^{*}$$\mathrm{i}$. Case of$A_{m+2}^{*}\equiv\neg B_{m+1}^{*}$

From the$\lambda_{U}^{\exists}$$A_{j}^{*}\equiv\exists X.A_{j-1}^{*}$$:\perp$A$A_{m+1}^{*}$:

deduction$a:A_{m+1}^{*}$::$\frac{a:A_{m+2}^{*}x\langle N_{1},\ldots,N_{m}^{*},a\rangle:\perp}{1\mathrm{e}\mathrm{t}\langle x_{n},a\rangle=ai\mathrm{n}x\langle N_{1}^{*},\ldots,N_{m}^{*},a\rangle:\perp}"(\wedge E)$

we have the$\lambda 2$

deduction with

$B_{m+1}\Rightarrow A_{m+1}\equiv A_{m+2}$$\frac{xN_{1}.\cdot.\cdot.\cdot N_{m}:A_{m+1}}{\lambda x_{n}:B_{n}.xN_{1}N_{m}:B_{m+1}\Rightarrow A_{m+1}}(\Rightarrow I)$

from the84$\mathrm{i}\mathrm{i}$.

:$\mathrm{F}\mathrm{r}\mathrm{o}\mathrm{m}\mathrm{t}\mathrm{h}\mathrm{e}\lambda_{U}^{\xi^{2}}\mathrm{d}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{C}\mathrm{a}\mathrm{s}\mathrm{e}\mathrm{o}\mathrm{f}A_{m}^{*}\equiv\exists X_{n}.A_{m+1}^{*}$$a:A_{m+1}^{*}$::$\frac{a:A_{m+2}^{*}x\langle N_{1}^{*},\ldots N_{m}^{*},a\rangle:\perp}{1\mathrm{e}\mathrm{t}\langle X_{n},a\rangle=a\mathrm{i}\mathrm{n}x\langle N_{1}^{*}’,\ldots,N_{m}^{*},a\rangle:\perp}(\exists E)$

we have the$\lambda 2$

deduction with$\forall X_{n}.A_{m+1}\equiv A_{m+2}$$\frac{xN_{1}N_{m}:A_{m+1}}{\lambda X_{n}.xN_{1}N_{m}:\forall X_{n}.A_{m+1}}:::(\forall I)$$\mathrm{i}\mathrm{i}\mathrm{i}$. Other cases are confirmed similarly. Finally, we have the stated property
for the deduction of:.
$M_{nf}\equiv\lambda\chi_{1}\ldots.\lambda\chi_{n}.xN_{1}\ldots N_{m}$5$A_{m+n+1}$

Concluding Remarks

The target calculus can be regarded as a subsystem of , in the sense of the impredica, A and . Along the line of Theorem 2, we have a correspondence such
tive encodingthatfor some
if and only iffor $P\in$ Univ, whichitself does not imply the undecidability of the inhabitation of . We conjecture that the
inhabitation problem of is decidable, which remains open.
In the previous conference version [4], we have provided yet another call-by-name CPStranslation. For the theorem (proof duality), we have introduced the notion of dual paths,
where dual paths form a duality with respect to the so-called paths. On the other hand,
this paper introduced much simpler CPS-translation for the extensional -calculus, andderived a natural form of proof duality. The simple hamework can serve as an
is foroperators,recursions,extensions with control
and so on. For instance, this frameworkhas been applied for analyzing parametricity in the classical system -calculus [9]plus control operators) in [6]. This CPS-translation is sound and complete with respect
to the equational -theory of the -calculus, whose syntactic analysis will appear in aforthcoming paper with Masahito Hasegawa.
$A2$$\lambda^{\exists}$$\mathrm{o}\mathrm{f}\perp$$\Gamma\vdash_{\lambda 2}M:$$\exists$$A$$M\in\Lambda 2$$\urcorner\Gamma,$$a:A^{*}\vdash_{\lambda^{\exists}}P:\perp$$A^{\exists}$$A^{\exists}$$\lambda 2$$\mathrm{b}\mathrm{a}s$$A\mu$$\beta\eta$$(\lambda 2$$A\mu$

References[1] R. Backhouse: Galois Connections and Fixed Point Calculus, Lecture Notes in Computer Science 2297 (2002) 89-150.
[2] O. Danvy and J. L. Lawall: Back to Direct Style II: First-Class Continuations, Proc.
of the ACM Conference on Lisp and Functional Programming (1992) 299-310.

[3] K. Fujita: A sound and complete CSP-translation for
Computer Science 2701 (2003) 120-134.

$A\mu$-Calculus, Lecture Notes in[4] K. FUjita: Galois embedding from polymorphic types into existential types, Lecture
Notes in Computer Science 3461 (2005) 194-208.

85[5] K. Fujita: Galois embedding from universal types into existential types -extended
abstract-, Kyoto University RIMS Kokyuroku 1503 (2006) 121-128.
[6] M. Hassegawa: Relational parametricity and control (extended abstract), Proc. Logicin Computer Science (2005) 72-81.

[7] J. C. Mitchell and G. D. Plotkin: Abstract types have existential type, Proc. the 12th
Annual ACM Symposium on Principles of Programming Languages (1985) 37-51.
[8] A. Melton, D. A. Schmidt, G. E. Strecker: Galois Connections and Computer Science
Applications, Lecture Notes in Computer Science 240 (1986) 299-312.
[9] M. Parigot:-Calculus: An Algorithmic Interpretation of Classical Natural Deduction,
Lecture Notes in Computer Science 624 (1992) 190-201.
$\lambda\mu$[10] G. Plotkin:
Science 1 (1975) 125-159.

$\mathrm{C}\mathrm{a}\mathrm{l}\mathrm{l}- \mathrm{b}\mathrm{y}rightarrow \mathrm{N}\mathrm{a}\mathrm{m}\mathrm{e},$Call-by-Value and the -Calculus, Theoretical Computer[11] D. Prawitz:
NATURAL DEDUCTION,ALMQVIST&WIKSELL, Stockholm, 1965.

$\lambda$

A

Proof Theoretical

Study,[12] H. A. Priestley: Ordered Sets and Complete Lattices, A Primer for Computer Science,
Lecture Notes in Computer Science 2297 (2002) 21-78.
[13] J. C. Reynolds: The discoveries of continuation, Lisp and Symbolic Computation 6(1993) 233-247.

[14] P. Selinger: Control Categories and Duality: on the Categorical Semantics of theLambda-Mu Calculus, Math. Stretct. in Compu. Science 11 (2001) 207-260.
[15] A. Sabry and M. Felleisen: Reasoning about Programs in Continuation-Passing Style,
LISP AND SYMBOLIC COMPUTATION: An Intemational Journal 6 (1993) 289-360.

[16] A. Sabry and Ph. Wadler: A Reflection on Call-by-Value, ACM Transactions on
Programming Languages and Systems 19-6 (1997) 916-941.
[17] Ph. Wadler: Call-by-value is dual to call-by-name, International Conference ontional Programming, August 25-29, Uppsala, 2003.

$\mathbb{R}nc-$