On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Abstract

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

1. Introduction

The Curry-Howard isomorphism [1,2] states that formulas and proofs in mathematical logic correspond to types and programs in programming languages. For example, propositions and proofs in intuitionistic propositional logic (IPL) correspond to types and terms in the simply typed $\lambda$-calculus (${\lambda }^{\to }$). A similar correspondence also exists between classical propositional logic (CPL) and the simply typed $\lambda$-calculus with control operators such as $\mathsf{callcc}$ (call-with-current continuation) and $\mathsf{throw}$ (${\lambda }^{\mathsf{cont}}$) [3,4].

Classical logic differs from intuitionistic logic, also known as constructive logic, in that it includes the law of excluded middle (EM), $A\vee \neg A$, as a theorem, which states that for any proposition A, either A is true or its negation $\neg A$ is true (i.e., A is false). Classical logic also includes Peirce’s law, $((A\supset B)\supset A)\supset A$, and double negation elimination (DNE), $\neg \neg A\supset A$. Any of these three theorems can be added as an axiom to proof systems for intuitionistic logic in order to obtain a sound and complete proof system for classical logic. Taking Peirce’s law and DNE as axioms corresponds to the control operators such as $\mathsf{callcc}$ and Felleisen et al.’s $\mathcal{C}$ operator, which allow a nonlocal transfer of program control, respectively [3,4,5].

A double negation translation (DNT), also known as a negative translation, translates a classically valid formula into an intuitionistically valid one [6,7,8,9,10,11], for example, by placing a double negation $\neg \neg$ in front of every subformula of the given formula [9]. More precisely, while intuitionistic logic admits double negation introduction, $A\supset \neg \neg A$, it only rejects double negation elimination, $\neg \neg A\supset A$. In other words, $\neg \neg A$ is weaker than A in intuitionistic logic, but they are equivalent in classical logic. Hence, in general, an instance of A in a classical proof derivation only corresponds to a weaker proposition $\neg \neg A$ in an intuitionistic proof derivation. In this regard, DNTs can be thought of as a proof transformation which eliminates every instance of DNE (or equivalently, EM or Peirce’s law) used in a classical derivation of A, yielding an intuitionistic proof of $\neg \neg A^{*}$, where $A^{*}$ is the formula obtained by placing $\neg \neg$ in front of every proper subformula of A. One important consequence of DNTs is the equivalence between the consistency of classical Peano arithmetic and the consistency of intuitionistic Heyting arithmetic.

The programming language counterpart of DNTs is continuation passing style (CPS) transformations [4,12,13], which are often used in compiler optimization [14,15]. Operationally, a continuation of type $A\mathsf{cont}$ is a reification of an evaluation context, i.e., the rest of the program, that expects the result of the current expression of type A. Hence, a continuation type $A\mathsf{cont}$ can be understood as a function type $A\to \mathit{Ans}$, where $\mathit{Ans}$ stands for the type of final results. If we interpret $\mathit{Ans}$ as ⊥ and define $\neg A$ as a syntactic abbreviation of $A\to \perp$ as usual, then DNTs correspond to CPS transformations, which translate an expression M of type A into a CPS function of type $(A^{*}\to \perp )\to \perp$ that explicitly takes a continuation k as an argument and applies it to the result of M in its body. Here, the continuation k expects a value of type $A^{*}$ because, as in DNTs, CPS transformations also recursively translate every subexpression of the given expression into CPS expressions. The CPS transformations from ${\lambda }^{\mathsf{cont}}$ into ${\lambda }^{\to }$ [3,4], which eliminate control operators, correspond to a DNT from CPL with Peirce’s law or DNE into IPL.

In this paper, we study the logical meaning of a selective CPS transformation [16] and present a selective DNT for CPL via the Curry-Howard isomorphism. The usual CPS transformations translate into CPS functions not only “nontrivial” expressions (possibly) with control operators (computational effects) but also “trivial” expressions, which lack them, yielding unnecessarily large expressions. In contrast, the selective CPS transformation only translates nontrivial expressions into CPS functions and keeps trivial expressions intact. To do so, it uses a type and effect system to keep track of the uses of control operators. Similarly, when viewed as a proof transformation, the usual DNTs also yield unnecessarily large proofs because they translate even intuitionistically valid proof derivations. Our selective DNT uses an annotated proof system to keep track of the uses of only classical axioms, which is similar to the type and effect system in [16], and only selectively translates the part of the given proof that exploits such axioms.

The main contributions of our paper are summarized as follows:

• We review the Curry-Howard isomorphism between the standard call-by-value (CBV) CPS transformation with control operators and the corresponding DNT from CPL into IPL.
• We review a CBV selective CPS transformation based on a type and effect system [16] and propose a corresponding selective DNT based on an annotated proof system, with its correctness proof showing that provability is preserved under the translation.
• Our work can serve as a reference point for the close correspondence between the selective CPS transformation and the selective DNT and further research on this topic.

The remainder of the paper is organized as follows. Section 2 reviews the standard CBV CPS transformation from ${\lambda }^{\mathsf{cont}}$ with control operators into ${\lambda }^{\to }$ without these operators [3]. In Section 3, we present the corresponding DNT from CPL with Peirce’s law into IPL. Section 4 reviews a CBV selective CPS transformation based on a type and effect system. In Section 5, we present an annotated proof system and propose a selective DNT corresponding to the selective CPS transformation via the Curry-Howard isomorphism. We also prove the correctness of the translation by showing that provability is preserved under the translation. Finally, Section 6 discusses related work and concludes.

2. A Call-by-Value CPS Transformation

In this section, we review the standard CBV CPS transformation [3] which translates a program in the source language ${\lambda }^{\mathsf{cont}}$ with control operators $\mathsf{callcc}$ and $\mathsf{throw}$ into an operationally equivalent program in the target language ${\lambda }^{\to }$ without control operators.

2.1. Simply Typed $\lambda$-Calculus with Control Operators

The source language ${\lambda }^{\mathsf{cont}}$ is the simply typed $\lambda$-calculus with two control operators: $\mathsf{callcc}$ and $\mathsf{throw}$ [3]. Its abstract syntax is defined as follows.

Definition 1

(Abstract syntax of ${\lambda }^{\mathsf{cont}}$).

$$\begin{array}{cccc}\hfill \mathit{expressions}& \hfill M,N& ::=& p\mid x\mid \lambda x.M\mid MN\mid \mathsf{callcc}x.M\mid \mathsf{throw}MN\hfill \\ \hfill \mathit{types}& \hfill A,B,C& ::=& P\mid A\to B\mid A\mathsf{cont}\hfill \end{array}$$

An expression M is either a constant p, a variable x, a lambda abstraction (anonymous function) $\lambda x.M$, a lambda application (function application) $MN$, or a control operator to be explained below. As for types, P ranges over an arbitrary but fixed set of primitive types, $A\to B$ denotes the type of functions from domain A to range B, and $A\mathsf{cont}$ denotes the type of continuations that expect a value of type A.

We consider a left-to-right CBV operational semantics for ${\lambda }^{\mathsf{cont}}$ using evaluation contexts, where a well-typed expression evaluates to a value.

Definition 2

(Operational semantics of ${\lambda }^{\mathsf{cont}}$).

$$\begin{array}{cccc}\hfill \mathit{extended}\mathit{expressions}& \hfill M,N& ::=& \cdots \mid \langle E\rangle \hfill \\ \hfill \mathit{evaluation}\mathit{contexts}& \hfill E& ::=& \left[\right]\mid EN\mid VE\mid \mathsf{throw}EN\mid \mathsf{throw}VE\hfill \\ \hfill \mathit{values}& \hfill V& ::=& p\mid \lambda x.M\mid \langle E\rangle \hfill \end{array}$$

$$\begin{array}{ccc}\hfill E\left[(\lambda x.M)V\right]& \mapsto & E\left[M[V/x]\right]\hfill \\ \hfill E\left[\mathsf{callcc}x.M\right]& \mapsto & E\left[M[\langle E\rangle /x]\right]\hfill \\ \hfill E\left[\mathsf{throw}\langle E_1\rangle V\right]& \mapsto & E_1\left[V\right]\hfill \end{array}$$

An evaluation context E is an expression with a hole $\left[\right]$. Every expression M can be decomposed into a unique context E and a unique reducible expression (redex) N, i.e., $M=E\left[N\right]$, where $E\left[N\right]$ denotes the expression obtained by filling the hole in E with N. An evaluation context can be considered a pending computation which expects the result of another computation. Hence, we represent a continuation as a captured evaluation context of the form $\langle E\rangle$. A value V is then either a constant, a lambda abstraction, or a continuation.

We use a reduction judgment $M\mapsto M^{\prime }$ to denote one-step reduction of M to $M^{\prime }$. Given any program, the redex to be reduced is implicitly determined by the left-to-right CBV definition of evaluation contexts. There are three kinds of redexes. First, a lambda application of the form $(\lambda x.M)V$ reduces to $M[V/x]$ ($\beta$-reduction), where $M[V/x]$ denotes the standard capture-avoiding substitution which replaces every occurrence of x in M with V. Since we use a CBV semantics, $\beta$-reduction always substitutes a value for the formal parameter. Second, $\mathsf{callcc}x.M$ captures the current context E, stores a continuation $\langle E\rangle$ in x, and proceeds to reduce M. Finally, $\mathsf{throw}\langle E_1\rangle V$ throws a value V to a continuation $\langle E_1\rangle$ and discards the current evaluation context, thus allowing a nonlocal transfer of control.

We evaluate only well-typed closed expressions [3]. To type expressions, we use a typing judgment $\Gamma ⊢M:A$ which means that expression M is of type A under typing context $\Gamma$. Here, a typing context $\Gamma$ is a set of type bindings of the form $x:A$, and we use · to denote an empty context. We assume that each variable is associated with at most one type, for example, by means of $\alpha$-conversion.

$$\begin{array}{cccc}\hfill \mathrm{typing}\mathrm{contexts}& \Gamma \hfill & ::=& ·\mid \Gamma ,x:A\hfill \end{array}$$

A closed expression M is well-typed with respect to a type A if $·⊢M:A$ is provable using the typing rules in Definition 3.

Definition 3

(Typing rules for ${\lambda }^{\mathsf{cont}}$).

$$\begin{array}{ccc}\frac{}{\Gamma ,x:A⊢x:A}\mathsf{Tvar}& \frac{\mathtt{CONST}-\mathtt{TYPE}\left(p\right)=P}{\Gamma ⊢p:P}\mathsf{Tconst}& \frac{\Gamma ,x:A⊢M:B}{\Gamma ⊢\lambda x.M:A\to B}\mathsf{Tlam}\end{array}$$

$$\begin{array}{cc}\frac{\Gamma ⊢M:A\to B\Gamma ⊢N:A}{\Gamma ⊢MN:B}\mathsf{Tapp}& \frac{\Gamma ,x:A\mathsf{cont}⊢M:A}{\Gamma ⊢\mathsf{callcc}x.M:A}\mathsf{Tcallcc}\end{array}$$

$$\frac{\Gamma ⊢M:A\mathsf{cont}\Gamma ⊢N:A}{\Gamma ⊢\mathsf{throw}MN:C}\mathsf{Tthrow}$$

The above typing rules are standard [3]. In the rule $\mathsf{Tconst}$, $\mathtt{CONST}\text{-}\mathtt{TYPE}$ is a predefined mapping from constants to primitive types. In the rule $\mathsf{Tcallcc}$, $\mathsf{callcc}x.M$ is of type A if M is also of type A assuming $x:A\mathsf{cont}$. Please note that x will at runtime be bound to a continuation that expects the result of M. Therefore, $\mathsf{callcc}$ itself can be given a type $(A\mathsf{cont}\to A)\to A$ for any type A, which corresponds to Peirce’s law. In the rule $\mathsf{Tthrow}$, if M and N are of type $A\mathsf{cont}$ and A, respectively, then $\mathsf{throw}MN$ can be assigned an arbitrary type C because its reduction never returns to the current evaluation context. Therefore, the rule $\mathsf{Tthrow}$ corresponds to the law of non-contradiction (followed by false elimination).

The type system given in Definition 3 is sound with respect to the operational semantics given in Definition 2 in that well-typed expressions never go wrong, i.e., cannot cause type errors during evaluation [17].

2.2. A Call-by-Value CPS Transformation

The CBV CPS transformation [3] translates the source language ${\lambda }^{\mathsf{cont}}$ into the target language ${\lambda }^{\to }$ without $\mathsf{callcc}$ and $\mathsf{throw}$. The abstract syntax of ${\lambda }^{\to }$ is defined as follows.

Definition 4

(Abstract syntax of ${\lambda }^{\to }$).

$$\begin{array}{cccc}\hfill \mathit{expressions}& \hfill M,N& ::=& p\mid x\mid \lambda x.M\mid MN\hfill \\ \hfill \mathit{types}& \hfill A,B,C& ::=& P\mid A\to B\mid \perp \hfill \\ \hfill \mathit{values}& \hfill V& ::=& p\mid \lambda x.M\hfill \end{array}$$

The main idea of the transformation is twofold. First, it interprets a continuation of type $A\mathsf{cont}$ as a function of type $A\to \perp$, where we use ⊥ to denote the type of final answers. Second, it translates every expression M into a CPS function that explicitly takes as argument a continuation k expecting the result of M and applies k to the result in its body. Formally, the CBV CPS transformation associates each type A with $A^{*}$, which is the type of values of type A after the CPS transformation and defined in Definition 5. Based on this, it translates each expression M of type A into a CPS expression $\mathcal{C}〚M〛$ of type $(A^{*}\to \perp )\to \perp$, which is defined in Definition 6.

Definition 5

(CBV type translation).

$$\begin{array}{ccc}\hfill P^{*}& =& P\hfill \\ \hfill {(A\to B)}^{*}& =& A^{*}\to ((B^{*}\to \perp )\to \perp )\hfill \\ \hfill {\left(A\mathsf{cont}\right)}^{*}& =& A^{*}\to \perp \hfill \end{array}$$

Definition 6

(CBV CPS transformation).

$$\begin{array}{ccc}\hfill \mathcal{C}〚p〛& =& \lambda k.kp\hfill \\ \hfill \mathcal{C}〚x〛& =& \lambda k.kx\hfill \\ \hfill \mathcal{C}〚\lambda x.M〛& =& \lambda k.k(\lambda x.\mathcal{C}〚M〛)\hfill \\ \hfill \mathcal{C}〚MN〛& =& \lambda k.\mathcal{C}〚M〛(\lambda f.\mathcal{C}〚N〛(\lambda v.fvk))\hfill \\ \hfill \mathcal{C}〚\mathsf{callcc}x.M〛& =& \lambda k.\left(\mathcal{C}〚M〛\right[k/x\left]\right)k\hfill \\ \hfill \mathcal{C}〚\mathsf{throw}MN〛& =& \lambda k.\mathcal{C}〚M〛(\lambda k^{\prime }.\mathcal{C}〚N〛k^{\prime })\hfill \end{array}$$

The transformation simply translates values and variables into the CPS form. Please note that in the translation of a lambda abstraction, the body is also translated into a CPS expression. For a lambda application $MN$, let us first analyze the type structure of the transformed expression:

In the transformed expression $\lambda k:B^{*}\to \perp .\mathcal{C}〚M〛(\lambda f:{(A\to B)}^{*}.\mathcal{C}〚N〛(\lambda v:A^{*}.fvk))$,

$\mathcal{C}〚M〛$ will bind the CPS-transformed evaluation result of M to f and $\mathcal{C}〚N〛$ will bind that of N to v. Then the function f is called with the argument v and the initial continuation k as $fvk$, which returns an answer of type ⊥. In the translation of $\mathsf{callcc}x.M$, $\mathcal{C}〚M〛$ of type $(A^{*}\to \perp )\to \perp$ will apply the initial continuation k of type $A^{*}\to \perp$ to the CPS-transformed evaluation result of M, which is of type $A^{*}$. Moreover, the continuation variable x of type $A\mathsf{cont}$ is substituted with the explicit continuation k in $\mathcal{C}〚M〛$. Finally, in the translation of $\mathsf{throw}MN$, $\mathcal{C}〚M〛$ will bind the continuation evaluated from M to $k^{\prime }$, and then $\mathcal{C}〚N〛$ will apply $k^{\prime }$ to the CPS-transformed evaluation result of N. Please note that the initial continuation k is not used.

The above transformation preserves the operational meaning of the source program of primitive type: when applied to an initial continuation (an identity function), the translated program terminates if and only if the source program does, and in that case they evaluate to the same value of primitive type [3,16].

Theorem 1.

If M is a closed expression of type P, then

$$M{\mapsto }^{*}V\iff \mathcal{C}〚M〛(\lambda x.x){\mapsto }^{*}V$$

where ${\mapsto }^{*}$ is the reflexive and transitive closure of one-step reduction ↦.

The transformation also preserves typing [3], i.e., provability, as stated below, where ${\Gamma }^{*}$ is the typing context such that $x:A^{*}\in {\Gamma }^{*}$ if and only if $x:A\in \Gamma$.

Theorem 2.

If $\Gamma ⊢M:A$, then ${\Gamma }^{*}⊢\mathcal{C}〚M〛:(A^{*}\to \perp )\to \perp .$

Proof. 

By induction on the structure of M. □

3. A Double Negation Translation

By the Curry-Howard isomorphism, types and expressions in ${\lambda }^{\mathsf{cont}}$ correspond to formulas and proofs in classical implicational propositional logic (CPL) [4]. The formulas of CPL are defined as follows.

Definition 7

(CPL formulas).

$$\begin{array}{cccc}\hfill \mathit{formulas}& A,B,C& ::=& P\mid A\supset B\mid \neg A\hfill \end{array}$$

P ranges over atomic propositions. We choose only implication ⊃ and negation ¬ as primitive connectives to clearly show the connection between ${\lambda }^{\mathsf{cont}}$ and CPL. Other connectives $A\vee B$ and $A\wedge B$ can be notionally defined as $\neg A\supset B$ and $\neg (A\supset \neg B)$, respectively. A continuation type $A\mathsf{cont}$ in ${\lambda }^{\mathsf{cont}}$ is interpreted as a negated formula $\neg A$ in CPL.

The type system for ${\lambda }^{\mathsf{cont}}$ given in Definition 3 can be interpreted as the proof system for CPL given in Definition 8. We use a hypothetical judgment $\Gamma {⊢}_{\mathsf{K}}A$ to mean that a proposition A is true under a set $\Gamma$ of hypotheses (where the subscript $\mathsf{K}$ stands for Klassical). Below, by removing the terms in each typing rule in Definition 3, we obtain the corresponding inference rule for CPL. (For simplicity, we omit the rule corresponding to $\mathsf{Tconst}$ because it is not necessary for studying the Curry-Howard isomorphism between CPL and IPL. However, it is needed for proving the observational soundness for the CPS transformation, stated in Theorem 1).

Definition 8

(Proof system for CPL).

$$\begin{array}{c}\frac{}{\Gamma ,A{⊢}_{\mathsf{K}}A}\mathsf{Hyp}\end{array}\frac{\Gamma ,A{⊢}_{\mathsf{K}}B}{\Gamma {⊢}_{\mathsf{K}}A\supset B}\supset \mathsf{I}\frac{\Gamma {⊢}_{\mathsf{K}}A\supset B\Gamma {⊢}_{\mathsf{K}}A}{\Gamma {⊢}_{\mathsf{K}}B}\supset \mathsf{E}$$

$$\begin{array}{c}\frac{\Gamma ,\neg A{⊢}_{\mathsf{K}}A}{\Gamma {⊢}_{\mathsf{K}}A}\mathsf{Peirce}\end{array}\frac{\Gamma {⊢}_{\mathsf{K}}\neg A\Gamma {⊢}_{\mathsf{K}}A}{\Gamma {⊢}_{\mathsf{K}}C}\mathsf{Contra}$$

The typing rules $\mathsf{Tcallcc}$ and $\mathsf{Tthrow}$ for control operators correspond to the rules $\mathsf{Peirce}$ and $\mathsf{Contra}$ which internalize Peirce’s law and the law of non-contradiction, respectively. Using them, we can derive the following rules for double negation elimination and the law of excluded middle.

$$\frac{}{\Gamma {⊢}_{\mathsf{K}}\neg \neg A\supset A}\mathsf{DNE}\frac{}{\Gamma {⊢}_{\mathsf{K}}A\vee \neg A}\mathsf{EM}$$

The DNT corresponding to the CBV CPS transformation translates CPL into intuitionistic implicational propositional logic (IPL) which corresponds to ${\lambda }^{\to }$ in Definition 4. The formulas of IPL are defined as follows.

Definition 9

(IPL formulas).

$$\begin{array}{cccc}\hfill \mathit{formulas}& A,B,C& ::=& P\mid A\supset B\mid \perp \hfill \end{array}$$

A natural deduction system for IPL is defined below. We use a judgment $\Gamma {⊢}_{\mathsf{I}}A$ to mean that a proposition A is true in IPL under a set $\Gamma$ of hypotheses (where the subscript $\mathsf{I}$ stands for Intuitionistic).

Definition 10

(Proof system for IPL).

$$\begin{array}{cccc}\frac{}{\Gamma ,A{⊢}_{\mathsf{I}}A}\mathsf{Hyp}& \frac{\Gamma ,A{⊢}_{\mathsf{I}}B}{\Gamma {⊢}_{\mathsf{I}}A\supset B}\supset \mathsf{I}& \frac{\Gamma {⊢}_{\mathsf{I}}A\supset B\Gamma {⊢}_{\mathsf{I}}A}{\Gamma {⊢}_{\mathsf{I}}B}\supset \mathsf{E}& \frac{\Gamma {⊢}_{\mathsf{I}}\perp }{\Gamma {⊢}_{\mathsf{I}}C}\perp \mathsf{E}\end{array}$$

Although we include the $\perp \mathsf{E}$ rule in Definition 10 for the completeness of the system, it is never used in the translation of CPL proof trees into IPL ones. In other words, our study is still valid without the $\perp \mathsf{E}$ rule. Please note that ⊥ is not even included in CPL (although it can be encoded, for example, as $A\wedge \neg A$). Meanwhile, we regard $\neg A$ as a syntactic abbreviation of $A\supset \perp$ in IPL. Therefore, the following rules are special cases of the ⊃ introduction and elimination rules.

$$\begin{array}{cc}\frac{\Gamma ,A{⊢}_{\mathsf{I}}\perp }{\Gamma {⊢}_{\mathsf{I}}\neg A}\neg \mathsf{I}& \frac{\Gamma {⊢}_{\mathsf{I}}\neg A\Gamma {⊢}_{\mathsf{I}}A}{\Gamma {⊢}_{\mathsf{I}}\perp }\neg \mathsf{E}\end{array}$$

We define a translation of CPL formulas into IPL formulas exactly like the CBV CPS transformation of types, as follows.

Definition 11

(DNT for formulas).

$$\begin{array}{ccc}\hfill P^{*}& =& P\hfill \\ \hfill {(A\supset B)}^{*}& =& A^{*}\supset ((B^{*}\supset \perp )\supset \perp )\hfill & \equiv & A^{*}\supset \neg \neg B^{*}\hfill \\ \hfill {(\neg A)}^{*}& =& A^{*}\supset \perp \hfill \end{array}$$

Our translation slightly differs from the double negation translations proposed by Kolmogorov [9], Gödel and Gentzen [6,8], and Kuroda [10]. Kolmogorov’s translation directly corresponds to the call-by-name CPS transformation [4,12,18] via the Curry-Howard isomorphism. In particular, in his translation, $A\to B$ is translated into $\neg \neg A^{*}\supset \neg \neg B^{*}$.

The correctness of the DNT is stated as follows, where ${\Gamma }^{*}$ applies the translation elementwise: $A^{*}\in {\Gamma }^{*}$ if and only if $A\in \Gamma$.

Theorem 3.

If $\Gamma {⊢}_{\mathsf{K}}A$ is provable, then ${\Gamma }^{*}{⊢}_{\mathsf{I}}\neg \neg A^{*}$ is also provable.

Proof. 

We define a recursive function that maps a derivation of $\Gamma {⊢}_{\mathsf{K}}A$ into a derivation of ${\Gamma }^{*}{⊢}_{\mathsf{I}}\neg \neg A^{*}$. In particular, for each case, we build a derivation tree corresponding to its counterpart CPS transformation in Definition 6 (although a smaller derivation may be constructed). □

4. A Call-by-Value Selective CPS Transformation

In this section, we review Nielsen’s CBV selective CPS transformation [16]. The main idea is to distinguish trivial expressions whose evaluation does not give rise to computational effects (i.e., evaluation of $\mathsf{callcc}$ or $\mathsf{throw}$) from nontrivial ones whose evaluation may give rise to effects. In general, it is undecidable to determine if the evaluation of an expression gives rise to effects, for example, in the presence of a recursive operator or recursive types. Since it is safe to assume that every expression might have an effect, the usual CPS transformation assumes every expression as nontrivial and translates into the CPS form.

To translate only nontrivial expressions selectively, while keeping trivial ones in the direct style, we use a type and effect system, where (definitely) trivial expressions are annotated with $\mathtt{T}$ while (possibly but not necessarily) nontrivial ones with $\mathtt{N}$. The following is the minimally annotated syntax of the source language ${\lambda }^{\mathsf{cont}}$, where we omit annotations when clear from the structure of the given expression.

Definition 12

(Annotated syntax).

$$\begin{array}{cccc}\hfill \mathit{annotations}& \hfill \mathtt{a}& ::=& \mathtt{T}\mid \mathtt{N}\mathrm{where}\mathtt{N}<\mathtt{T}\hfill \\ \hfill \mathit{expressions}& \hfill M,N& ::=& p\mid x\mid {\lambda }^{\mathtt{a}}x.M\mid {\left(M{@}^{\mathtt{a}}N\right)}^{\mathtt{a}}\mid \mathsf{callcc}x.M\mid \mathsf{throw}MN\hfill \\ \hfill \mathit{types}& \hfill A,B,C& ::=& P\mid A\stackrel{\mathtt{a}}{\to }B\mid A\mathsf{cont}\hfill \end{array}$$

We understand values and identifiers to always be implicitly annotated with $\mathtt{T}$ and control expressions with $\mathtt{N}$, and thus do not explicitly mark them in the syntax. Moreover, we denote an application by $M@N$ instead of $MN$ for specifying annotations. Still, when annotations do not matter, we use the usual notation $MN$. Special care should be taken for abstractions and applications. For an application of the form $(\lambda x.M)@V$, if the function body M is nontrivial, the evaluation of its $\beta$-reduct $M[V/x]$ gives rise to an effect. For such applications, we annotate @ with $\mathtt{N}$ as in $(\lambda x.M){@}^{\mathtt{N}}V$. An application $M@N$ is annotated with $\mathtt{N}$, i.e., ${(M@N)}^{\mathtt{N}}$, if the evaluation of M, N, or its $\beta$-reduct (obtained after both M and N are reduced to values) gives rise to an effect. Furthermore, in the presence of higher-order functions, different abstractions may be applied at the same application point (e.g., M and N in $(\lambda f.\mathsf{fst}\left(fM\right)\left(fN\right))(\lambda g.gp)$ where $\mathsf{fst}=\lambda x.\lambda y.x$ and p is a some constant), and such abstractions should be transformed into the same style. Therefore, some abstraction with a trivial body might sometimes need to be transformed into the CPS form. For such abstractions, we annotate $\lambda$ with $\mathtt{N}$ as in ${\lambda }^{\mathtt{N}}x.M$. Correspondingly, if $\lambda x.M$ is of type $A\to B$, then ${\lambda }^{\mathtt{N}}x.M$ and ${\lambda }^{\mathtt{T}}x.M$ respectively have an annotated type $A\stackrel{\mathtt{N}}{\to }B$ and $A\stackrel{\mathtt{T}}{\to }B$.

We say that annotations are consistent (with respect to the program’s behavior) if

• every expression annotated with $\mathtt{T}$ is indeed trivial,
• every abstraction annotated with $\mathtt{T}$ (resp. $\mathtt{N}$) is applied only at application points annotated with $\mathtt{T}$ (resp. $\mathtt{N}$), and
• every abstraction whose body is annotated with $\mathtt{N}$ is also annotated with $\mathtt{N}$.

To check the consistency of annotations, we use a type and effect system using a judgment $\Gamma ⊢M:A,\mathtt{a}$ which means that expression M is of type A and can be annotated with $\mathtt{a}$ under typing context $\Gamma$.

Definition 13

(Type and effect system).

$$\begin{array}{cc}\frac{}{\Gamma ,x:A⊢x:A,\mathtt{T}}\mathsf{Tvar}& \frac{\mathtt{CONST}-\mathtt{TYPE}\left(p\right)=P}{\Gamma ⊢p:P,\mathtt{T}}\mathsf{Tconst}\end{array}$$

$$\frac{\Gamma ,x:A⊢M:B,{\mathtt{a}}_1\mathtt{a}\le {\mathtt{a}}_1}{\Gamma ⊢{\lambda }^{\mathtt{a}}x.M:A\stackrel{\mathtt{a}}{\to }B,\mathtt{T}}\mathsf{Tlam}$$

$$\frac{\Gamma ⊢M:A\stackrel{{\mathtt{a}}_3}{\to }B,{\mathtt{a}}_1\Gamma ⊢N:A,{\mathtt{a}}_2\mathtt{a}\le \min ({\mathtt{a}}_1,{\mathtt{a}}_2,{\mathtt{a}}_3)}{\Gamma ⊢{\left(M{@}^{{\mathtt{a}}_3}N\right)}^{\mathtt{a}}:B,\mathtt{a}}\mathsf{Tapp}$$

$$\begin{array}{cc}\frac{\Gamma ,x:A\mathsf{cont}⊢M:A,\mathtt{a}}{\Gamma ⊢\mathsf{callcc}x.M:A,\mathtt{N}}\mathsf{Tcallcc}& \frac{\Gamma ⊢M:A\mathsf{cont},{\mathtt{a}}_1\Gamma ⊢N:A,{\mathtt{a}}_2}{\Gamma ⊢\mathsf{throw}MN:C,\mathtt{N}}\mathsf{Tthrow}\end{array}$$

The relation $\mathtt{a}\le {\mathtt{a}}_1$ in the rule $\mathsf{Tlam}$ allows us to annotate an abstraction with a trivial body with $\mathtt{N}$. Similarly, in the rule $\mathsf{Tapp}$, even if ${\mathtt{a}}_1$, ${\mathtt{a}}_2$, and ${\mathtt{a}}_3$ are all $\mathtt{T}$, the application can be annotated with $\mathtt{N}$. From now on, we consider only well-annotated expressions which are allowed by the type and effect system, i.e., typable by Definition 13. The following theorem shows that the type and effect system indeed ensures the consistency of annotations. As a corollary, if a closed expression M can be annotated with $\mathtt{T}$, the evaluation of M does not give rise to an effect.

Theorem 4.

If $\Gamma ⊢M:A,\mathtt{a}$, annotations in M are consistent.

Proof. 

By induction on a derivation of $\Gamma ⊢M:A,\mathtt{a}$. □

Corollary 1.

Given a closed expression M, if $·⊢M:A,\mathtt{T}$, no effects occur during the evaluation of M.

The CBV selective CPS transformation associates each type A with $A^{\star }$ defined below. The main difference from Definition 5 is the translation of function types, where a trivial function type $A\stackrel{\mathtt{T}}{\to }B$ is kept in the direct style.

Definition 14

(Selective type translation).

$$\begin{array}{ccc}\hfill P^{\star }& =& P\hfill \\ \hfill {\left(A\stackrel{\mathtt{N}}{\to }B\right)}^{\star }& =& A^{\star }\to ((B^{\star }\to \perp )\to \perp )\hfill \\ \hfill {\left(A\stackrel{\mathtt{T}}{\to }B\right)}^{\star }& =& A^{\star }\to B^{\star }\hfill \\ \hfill A{\mathsf{cont}}^{\star }& =& A^{\star }\to \perp \hfill \end{array}$$

In order to transform expressions selectively, we use two functions: $\mathcal{S}〚-〛$ translates expressions of type A into those of type $(A^{\star }\to \perp )\to \perp$ and ${\mathcal{S}}_t〚-〛$ translates expressions of type A into those of type $A^{\star }$. Given an expression, the former translates it into a CPS expression, whereas the latter keeps it in the direct style. In particular, ${\mathcal{S}}_t〚-〛$ takes only trivial expressions.

Definition 15

(Selective CPS transformation).

$$\begin{array}{ccc}\hfill \mathcal{S}〚M^{\mathtt{T}}〛& =& \lambda k.k{\mathcal{S}}_t〚M〛\hfill \\ \hfill \mathcal{S}〚{\left(M{@}^{\mathtt{N}}N\right)}^{\mathtt{N}}〛& =& \lambda k.\mathcal{S}〚M〛(\lambda f.\mathcal{S}〚N〛(\lambda v.fvk))\hfill \\ \hfill \mathcal{S}〚{\left(M{@}^{\mathtt{T}}N\right)}^{\mathtt{N}}〛& =& \lambda k.\mathcal{S}〚M〛(\lambda f.\mathcal{S}〚N〛(\lambda v.k\left(fv\right)))\hfill \\ \hfill \mathcal{S}〚\mathsf{callcc}x.M〛& =& \lambda k.\left(\mathcal{S}〚M〛\right[k/x\left]\right)k\hfill \\ \hfill \mathcal{S}〚\mathsf{throw}MN〛& =& \lambda k.\mathcal{S}〚M〛(\lambda k^{\prime }.\mathcal{S}〚N〛k^{\prime })\hfill \\ \\ \hfill {\mathcal{S}}_t〚x〛& =& x\hfill \\ \hfill {\mathcal{S}}_t〚p〛& =& p\hfill \\ \hfill {\mathcal{S}}_t〚{\lambda }^{\mathtt{N}}x.M〛& =& \lambda x.\mathcal{S}〚M〛\hfill \\ \hfill {\mathcal{S}}_t〚{\lambda }^{\mathtt{T}}x.M〛& =& \lambda x.{\mathcal{S}}_t〚M〛\hfill \\ \hfill \mathcal{S}〚{\left(M{@}^{\mathtt{T}}N\right)}^{\mathtt{T}}〛& =& {\mathcal{S}}_t〚M〛{\mathcal{S}}_t〚N〛\hfill \end{array}$$

The main difference between Definitions 6 and 15 is the transformation of functions and applications annotated with $\mathtt{T}$. In the translation of a function ${\lambda }^{\mathtt{T}}x.M$, the body M is kept in the direct style, i.e., translated using ${\mathcal{S}}_t〚-〛$. Similarly, in the translation of an application ${\left(M{@}^{\mathtt{T}}N\right)}^{\mathtt{T}}$, both M and N are kept in the direct style. Finally, for an application ${\left(M{@}^{\mathtt{T}}N\right)}^{\mathtt{N}}$, the annotation $\mathtt{T}$ for @ indicates that M is of type $A\stackrel{\mathtt{T}}{\to }B$ for some types A and B. In other words, if M evaluates to an abstraction $\lambda x.M^{\prime }$, then $M^{\prime }$ would be trivial. Therefore, in the transformed expression, $\mathcal{S}〚M〛$ is applied to a continuation of type ${\left(A\stackrel{\mathtt{T}}{\to }B\right)}^{\star }\to \perp$. Specifically, at runtime, f will be bound to the result evaluated from M, which is of type $A^{\star }\to B^{\star }$, and $fv$ will evaluate to a value of type $B^{\star }$, which is in the direct style. Hence, we apply to $fv$ a continuation k that expects the result of $MN$.

The operational meaning of the source program of primitive type is preserved by the selective CPS transformation as stated below [16].

Theorem 5.

If M is a closed and well-annotated expression of type P, then

$$M{\mapsto }^{*}V\iff \mathcal{S}〚M〛(\lambda x.x){\mapsto }^{*}V.$$

The transformation also preserves typing, as stated below, where ${\Gamma }^{\star }$ is the typing context such that $x:A^{\star }\in {\Gamma }^{\star }$ if and only if $x:A\in \Gamma$.

Theorem 6

(Preservation of typing).

(1)

If $\Gamma ⊢M^{\mathtt{a}}:A,\mathtt{a}$, then ${\Gamma }^{\star }⊢\mathcal{S}〚M〛:(A^{\star }\to \perp )\to \perp$.

(2)

If $\Gamma ⊢M^{\mathtt{T}}:A,\mathtt{T}$, then ${\Gamma }^{\star }⊢{\mathcal{S}}_t〚M〛:A^{\star }$.

Proof. 

By simultaneous induction on derivations. □

5. A Selective Double Negation Translation

In this section, we present an annotated proof system for CPL, which corresponds to the type and effect system given in Definition 13 via the Curry-Howard isomorphism. It keeps track of the uses of the $\mathsf{Peirce}$ and $\mathsf{Contra}$ rules using annotations. Based on the annotations in the proof, our selective DNT translates only the parts of the proof which use the $\mathsf{Peirce}$ or $\mathsf{Contra}$ rules into the double negation form.

We use annotated formulas defined below, where annotations are defined as in Definition 12.

Definition 16

(Annotated CPL formulas).

$$\begin{array}{cccc}\hfill \mathit{formulas}& A,B,C& ::=& P\mid A{\supset }^{\mathtt{a}}B\mid \neg A\hfill \end{array}$$

A formula $A{\supset }^{\mathtt{N}}B$ means that assuming A is provable, B is also provable under the assumption A, (possibly) using the $\mathsf{Peirce}$ or $\mathsf{Contra}$ rules. In contrast, a formula $A{\supset }^{\mathtt{T}}B$ means that assuming A is provable, B is also provable but without using those rules.

The proof system for annotated formulas is obtained from the type and effect system by removing the terms in each typing rule. (As in Definition 8, we omit the rule corresponding to $\mathsf{Tconst}$ for simplicity.) We use a judgment $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}$ which means that A is true under a set $\Gamma$ of hypotheses, and its proof does not use the $\mathsf{Peirce}$ or $\mathsf{Contra}$ rules if $\mathtt{a}$ is $\mathtt{T}$; otherwise, the proof may use them.

Definition 17

(Annotated proof system).

$$\begin{array}{ccc}\frac{}{\Gamma ,A{⊢}_{\mathsf{K}}A,\mathtt{T}}\mathsf{Hyp}& \frac{\Gamma ,A{⊢}_{\mathsf{K}}B,{\mathtt{a}}_1\mathtt{a}\le {\mathtt{a}}_1}{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{a}}B,\mathtt{T}}\supset \mathsf{I}& \frac{\Gamma ,\neg A{⊢}_{\mathsf{K}}A,\mathtt{a}}{\Gamma {⊢}_{\mathsf{K}}A,\mathtt{N}}\mathsf{Peirce}\end{array}$$

$$\frac{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{{\mathtt{a}}_3}B,{\mathtt{a}}_1\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2\mathtt{a}\le \min ({\mathtt{a}}_1,{\mathtt{a}}_2,{\mathtt{a}}_3)}{\Gamma {⊢}_{\mathsf{K}}B,\mathtt{a}}\supset \mathsf{E}$$

$$\frac{\Gamma {⊢}_{\mathsf{K}}\neg A,{\mathtt{a}}_1\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2}{\Gamma {⊢}_{\mathsf{K}}C,\mathtt{N}}\mathsf{Contra}$$

The interpretation of the annotations in the rules $\supset \mathsf{I}$ and $\supset \mathsf{E}$ is similar to the one for the rules $\mathsf{Tlam}$ and $\mathsf{Tapp}$ in Definition 13. In the rule $\supset \mathsf{I}$, even if B is proved without using the $\mathsf{Peirce}$ or $\mathsf{Contra}$ rules, we may annotate the implication with $\mathtt{N}$ as if B is proved using them. In the rule $\supset \mathsf{E}$, if all of ${\mathtt{a}}_1$, ${\mathtt{a}}_2$, and ${\mathtt{a}}_3$ are $\mathtt{T}$, then it means that the derivation of $\Gamma {⊢}_{\mathsf{K}}B,\mathtt{a}$ does not use the $\mathsf{Peirce}$ or $\mathsf{Contra}$ rules. Nevertheless, it can be annotated with $\mathtt{N}$ as in the type and effect system. The annotated proof system is equivalent to the original proof system in the following sense.

Theorem 7

(Soundness and completeness).

1.

If $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}$ is provable, then $\mathit{erase}(\Gamma ){⊢}_{\mathsf{K}}\mathit{erase}\left(A\right)$ is also provable, where the function erase removes every annotation in the given context and formula.

2.

If $\Gamma {⊢}_{\mathsf{K}}A$ is provable, then there exists at least one annotation for A that is provable in the annotated proof system.

Proof. 

(1) By straightforward induction on a derivation of $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}$. (2) The one where every implication is marked with $\mathtt{N}$ is always provable. □

We can further extend the completeness statement such that there exists a maximal annotation with as many $\mathtt{T}$’s as possible. We now define a selective translation of annotated CPL formulas into IPL formulas as follows, which directly corresponds to the selective type translation in Definition 14.

Definition 18

(Selective DNT for formulas).

$$\begin{array}{ccc}\hfill P^{\star }& =& P\hfill \\ \hfill {\left(A{\supset }^{\mathtt{N}}B\right)}^{\star }& =& A^{\star }\supset ((B^{\star }\supset \perp )\supset \perp )\hfill & \equiv & A^{\star }\supset (\neg \neg B^{\star })\hfill \\ \hfill {\left(A{\supset }^{\mathtt{T}}B\right)}^{\star }& =& A^{\star }\supset B^{\star }\hfill \\ \hfill \neg A^{\star }& =& A^{\star }\supset \perp \hfill \end{array}$$

The correctness of our selective DNT is stated as follows, where ${\Gamma }^{\star }$ applies the translation elementwise: $A^{\star }\in {\Gamma }^{\star }$ if and only if $A\in \Gamma$.

Theorem 8

(Correctness).

1.

If $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}$ is provable, then ${\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }$ is also provable.

2.

If $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T}$ is provable, then ${\Gamma }^{\star }{⊢}_{\mathsf{I}}{A}^{\star }$ is also provable.

Proof. 

We define two mutually recursive functions f and g which translate derivations of $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}$ and $\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T}$ into derivations of ${\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }$ and ${\Gamma }^{\star }{⊢}_{\mathsf{I}}{A}^{\star }$, respectively. Their definitions directly correspond to the selective CPS transformation $\mathcal{S}〚-〛$ and ${\mathcal{S}}_t〚-〛$ in Definition 15. In the translations below, whenever necessary, we implicitly apply weakening on the induction hypothesis, i.e., the result of a recursive call.

1.

$f\left(\begin{array}{c}\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T}\end{array}\right)=\begin{array}{c}\frac{\frac{}{{\Gamma }^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\neg A^{\star }}\mathsf{Hyp}g(\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T})}{\frac{{\Gamma }^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\perp }{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }}\supset \mathsf{I}}\supset \mathsf{E}\end{array}$

2.

$\begin{array}{c}f\left(\begin{array}{c}\frac{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{T}}B,{\mathtt{a}}_1\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2}{\Gamma {⊢}_{\mathsf{K}}B,\mathtt{N}}\supset \mathsf{E}\end{array}\right)=\\ \mathtt{let}\left\{\begin{array}{c}{\Gamma }_1^{\star }={\Gamma }^{\star },\neg B^{\star }\hfill \\ {\Gamma }_2^{\star }={\Gamma }_1^{\star },A^{\star }\supset B^{\star }\hfill \\ {\Gamma }_3^{\star }={\Gamma }_2^{\star },A^{\star }\hfill \end{array}\right.\\ \mathtt{and}\mathcal{D}=\left\{\begin{array}{c}\frac{\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}\neg B^{\star }}\mathsf{Hyp}\frac{\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}{A}^{\star }\supset B^{\star }}\mathsf{Hyp}\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}{A}^{\star }}\mathsf{Hyp}}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}{B}^{\star }}\supset \mathsf{E}}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}\end{array}\right.\\ \mathtt{in}\end{array}$

$\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{T}}B,{\mathtt{a}}_1)\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2)\frac{\mathcal{D}}{{\Gamma }_2^{\star }{⊢}_{\mathsf{I}}\neg A^{\star }}\supset \mathsf{I}}{{\Gamma }_2^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }_1^{\star }{⊢}_{\mathsf{I}}\neg (A^{\star }\supset B^{\star })}\supset \mathsf{I}}{{\Gamma }_1^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg B^{\star }}\supset \mathsf{I}$

3.

$\begin{array}{c}f\left(\begin{array}{c}\frac{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{N}}B,{\mathtt{a}}_1\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2}{\Gamma {⊢}_{\mathsf{K}}B,\mathtt{N}}\supset \mathsf{E}\end{array}\right)=\\ \mathtt{let}\left\{\begin{array}{c}{\Gamma }_1^{\star }={\Gamma }^{\star },\neg B^{\star }\hfill \\ {\Gamma }_2^{\star }={\Gamma }_1^{\star },A^{\star }\supset \neg \neg B^{\star }\hfill \\ {\Gamma }_3^{\star }={\Gamma }_2^{\star },A^{\star }\hfill \end{array}\right.\\ \mathtt{and}\mathcal{E}=\left\{\begin{array}{c}\frac{\frac{\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}{A}^{\star }\supset \neg \neg B^{\star }}\mathsf{Hyp}\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}{A}^{\star }}\mathsf{Hyp}}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}\neg \neg B^{\star }}\supset \mathsf{E}\frac{}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}\neg B^{\star }}\mathsf{Hyp}}{{\Gamma }_3^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}\end{array}\right.\\ \mathtt{in}\end{array}$

$\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{N}}B,{\mathtt{a}}_1)\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2)\frac{\mathcal{E}}{{\Gamma }_2^{\star }{⊢}_{\mathsf{I}}\neg A^{\star }}\supset \mathsf{I}}{{\Gamma }_2^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }_1^{\star }{⊢}_{\mathsf{I}}\neg (A^{\star }\supset \neg \neg B^{\star })}\supset \mathsf{I}}{{\Gamma }_1^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg B^{\star }}\supset \mathsf{I}$

4.

$f\left(\begin{array}{c}\frac{\Gamma ,\neg A{⊢}_{\mathsf{K}}A,\mathtt{a}}{\Gamma {⊢}_{\mathsf{K}}A,\mathtt{N}}\mathsf{Peirce}\end{array}\right)=\begin{array}{c}\frac{\frac{f(\Gamma ,\neg A{⊢}_{\mathsf{K}}A,\mathtt{a})\frac{}{{\Gamma }^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\neg A^{\star }}\mathsf{Hyp}}{{\Gamma }^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }}\supset \mathsf{I}\end{array}$

5.

$\begin{array}{c}f\left(\begin{array}{c}\frac{\Gamma {⊢}_{\mathsf{K}}\neg A,{\mathtt{a}}_1\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2}{\Gamma {⊢}_{\mathsf{K}}C,\mathtt{N}}\mathsf{Contra}\end{array}\right)=\\ \begin{array}{c}\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}\neg A,{\mathtt{a}}_1)\frac{\frac{f(\Gamma {⊢}_{\mathsf{K}}A,{\mathtt{a}}_2)\frac{}{{\Gamma }^{\star },\neg C^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\neg A^{\star }}\mathsf{Hyp}}{{\Gamma }^{\star },\neg C^{\star },\neg A^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }^{\star },\neg C^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }}\supset \mathsf{I}}{{\Gamma }^{\star },\neg C^{\star }{⊢}_{\mathsf{I}}\perp }\supset \mathsf{E}}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg C^{\star }}\supset \mathsf{I}\end{array}\end{array}$

(6)

$g\left(\begin{array}{c}\frac{}{\Gamma ,A{⊢}_{\mathsf{K}}A,\mathtt{T}}\mathsf{Hyp}\end{array}\right)=\begin{array}{c}\frac{}{{\Gamma }^{\star },A^{\star }{⊢}_{\mathsf{I}}{A}^{\star }}\mathsf{Hyp}\end{array}$

(7)

$g\left(\begin{array}{c}\frac{\Gamma ,A{⊢}_{\mathsf{K}}B,\mathtt{T}}{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{T}}B,\mathtt{T}}\supset \mathsf{I}\end{array}\right)=\begin{array}{c}\frac{g(\Gamma ,A{⊢}_{\mathsf{K}}B,\mathtt{T})}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}{A}^{\star }\supset B^{\star }}\supset \mathsf{I}\end{array}$

(8)

$g\left(\begin{array}{c}\frac{\Gamma ,A{⊢}_{\mathsf{K}}B,\mathtt{a}}{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{N}}B,\mathtt{T}}\supset \mathsf{I}\end{array}\right)=\begin{array}{c}\frac{f(\Gamma ,A{⊢}_{\mathsf{K}}B,\mathtt{a})}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}{A}^{\star }\supset \neg \neg B^{\star }}\supset \mathsf{I}\end{array}$

(9)

$g\left(\begin{array}{c}\frac{\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{T}}B,\mathtt{T}\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T}}{\Gamma {⊢}_{\mathsf{K}}B,\mathtt{T}}\supset \mathsf{E}\end{array}\right)=\begin{array}{c}\frac{g(\Gamma {⊢}_{\mathsf{K}}A{\supset }^{\mathtt{T}}B,\mathtt{T})g(\Gamma {⊢}_{\mathsf{K}}A,\mathtt{T})}{{\Gamma }^{\star }{⊢}_{\mathsf{I}}{B}^{\star }}\supset \mathsf{E}\end{array}$

In the above translations, whereas f eliminates the instances of the rules $\mathsf{Peirce}$ and $\mathsf{Contra}$ used in the given derivation by double-negating the goal formula, g keeps the given derivation as it is since it is also valid in IPL. □

The following diagram summarizes the relationship between the selective CPS transformation and the selective DNT. We note that the selective CPS transformation can be derived from the selective DNT by assigning proof terms to each inference rule.

$$\begin{array}{ccc}\left\{\begin{array}{c}\Gamma ⊢M:A,\mathtt{a}\hfill \\ \Gamma ⊢M:A,\mathtt{T}\hfill \end{array}\right.\hfill & \iff & \left\{\begin{array}{c}\Gamma {⊢}_{\mathsf{K}}A,\mathtt{a}\hfill \\ \Gamma {⊢}_{\mathsf{K}}A,\mathtt{T}\hfill \end{array}\mathrm{in}\mathrm{CPL}\right.\hfill \\ \downarrow \begin{array}{c}\hfill \mathrm{Selective}\mathrm{GPS}\\ \mathrm{transformation}\hfill \end{array}\hfill & \begin{array}{c}\hfill \mathrm{Curry}-\mathrm{Howard}\hfill \\ \hfill \mathrm{isomorphic}\hfill \end{array}& \downarrow \begin{array}{c}\hfill \mathrm{Selective}\mathrm{DNT}\end{array}\hfill \\ \left\{\begin{array}{c}{\Gamma }^{\star }⊢\mathcal{S}〚M〛:(A^{\star }\to \perp )\to \perp \hfill \\ {\Gamma }^{\star }⊢{\mathcal{S}}_t〚M〛:A^{\star }\hfill \end{array}\right.\hfill & \iff & \left\{\begin{array}{c}{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg A^{\star }\hfill \\ {\Gamma }^{\star }{⊢}_{\mathsf{I}}{A}^{\star }\hfill \end{array}\right.\hfill \end{array}$$

6. Discussion and Conclusions

In this paper, we studied the logical meaning of a selective CPS transformation [16]. Although we considered only a CBV semantics, our analysis can also be applied to a call-by-name (CBN) CPS transformation [4,12,18]. In a CBN semantics, a lambda application $(\lambda x.M)N$ reduces to $M[N/x]$ regardless of whether N is a value or not. Therefore, under the CBN CPS transformation, a translated function is passed an argument in the CPS form, and thus a function type $A\to B$ is translated into $((A^{*}\to \perp )\to \perp )\to (B^{*}\to \perp )\to \perp$. The corresponding DNT, such as Kolmogorov’s translation [9], translates $A\supset B$ into $\neg \neg A^{*}\supset \neg \neg B^{*}$, and we can exploit our annotated proof system, presented in Section 5, to derive a CBN selective DNT.

While our selective DNT is a direct logical interpretation of Nielsen’s selective CPS transformation [16], there is still room for further improvement. First, unlike the rule $\mathsf{Peirce}$, the rule $\mathsf{Contra}$ is valid not only in classical logic but also in intuitionistic logic, and therefore we may not need to translate the instances of $\mathsf{Contra}$ into the double negation form. We choose to translate them in order to keep the direct correspondence between the CPS transformation and the DNT. Second, by further analyzing annotations, we can produce a smaller proof. For example, the following derivation

$$\frac{\Gamma {⊢}_{\mathsf{K}}\stackrel{ \mathcal{D}}{A}{\supset }^{\mathtt{T}}B,\mathtt{T}\Gamma \stackrel{ \mathcal{E}}{{⊢}_{\mathsf{K}}}A,\mathtt{T}}{\Gamma {⊢}_{\mathsf{K}}B,\mathtt{N}}\supset \mathsf{E}$$

can be translated into

$$\frac{\frac{}{{\Gamma }^{\star },\neg B^{\star }{⊢}_{\mathsf{I}}\neg B^{\star }}\mathsf{Hyp}\frac{g\left(\begin{array}{c}\Gamma {⊢}_{\mathsf{K}}\stackrel{ \mathcal{D}}{A}{\supset }^{\mathtt{T}}B,\mathtt{T}\end{array}\right)g\left(\begin{array}{c}\Gamma \stackrel{ \mathcal{E}}{{⊢}_{\mathsf{K}}}A,\mathtt{T}\end{array}\right)}{{\Gamma }^{\star },\neg B^{\star }{⊢}_{\mathsf{I}}{B}^{\star }}\supset \mathsf{E}}{\frac{{\Gamma }^{\star },\neg B^{\star }{⊢}_{\mathsf{I}}\perp }{{\Gamma }^{\star }{⊢}_{\mathsf{I}}\neg \neg B^{\star }}\supset \mathsf{I}}\supset \mathsf{E}$$

which is much smaller than the result of the selective DNT given in the proof of Theorem 8. The corresponding case of the selective CPS transformation given in Definition 15 can also be improved as follows.

$$\begin{array}{ccc}\hfill \mathcal{S}〚{\left(M^{\mathtt{T}}{@}^{\mathtt{T}}{N}^{\mathtt{T}}\right)}^{\mathtt{N}}〛& =& \lambda k.k\left({\mathcal{S}}_t〚M〛{\mathcal{S}}_t〚N〛\right)\hfill \end{array}$$

We leave as future work a further investigation into whether or not this finer analysis of annotations still preserves the operational meaning of the source program in the sense of Theorem 5. Moreover, in this paper, we considered only control operators $\mathsf{callcc}$ and $\mathsf{throw}$ and the corresponding selective CPS transformation. Since there are other control structures (e.g., delimited continuations [19,20,21] and exceptions [22]) and corresponding selective CPS transformations, it will also be interesting to investigate their logical interpretation by parameterizing our analysis over such control operators. For further details on various control structures and CPS transformations, the reader may refer to [23].

Another interesting direction for future work is to include other connectives such as conjunction and disjunction which respectively correspond to product and sum types in programming languages. In addition, since we consider only propositional logic, one natural extension is to consider first-order predicate logic, which corresponds to dependently typed $\lambda$-calculus. However, it is challenging to define a computationally sound double negation proof translation for classical predicate logic, namely a CPS transformation for a dependently typed language. For example, the standard CPS transformation based on double negation is not type preserving for a dependently typed language with $\Sigma$ types (strong dependent pairs which correspond to universal quantifiers) [24]. Moreover, unrestricted uses of $\mathsf{callcc}$ and $\mathsf{throw}$ together with $\Sigma$ types and equality even leads to an inconsistent system [25]. Recently, Bowman et al. [26] developed type-preserving CBN and CBV CPS transformations for a dependently typed language with $\Sigma$ and $\Pi$ types based on answer type polymorphism [27]. It would be interesting to investigate the logical meaning of such translations, which we leave as future work.