<ol>
<li><p>Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): <a href="https://tel.archives-ouvertes.fr/tel-00007884/en/" rel="noreferrer">Olivier Laurent, <em>Étude de la polarisation en logique</em> (2002)</a>. A good explanation of what is going on from a categorical perspective is given in <a href="https://www.sciencedirect.com/science/article/pii/S0168007209001602" rel="noreferrer">Melliès and Tabareau, <em>Resource modalities in tensor logic</em> (2010)</a>. A detailed description of the correspondence between LLP and CPS along the lines of your question appears in <a href="https://tel.archives-ouvertes.fr/tel-00918642/en/" rel="noreferrer">my PhD thesis (2013)</a> (Chapter III, pp.91-95,153-199). (There are a lot of other references in this area; the bibliographies should provide you with a good starting point.)</p>
</li>
<li><p>The two rules (J) and (B) you wrote are derived as follows (in the notations of Laurent's PhD thesis):</p>
<p><span class="math-container">\begin{array}{c}
\dfrac{\dfrac{\vdash\mathcal{N},!(P_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P_{n}^{\bot})\qquad\dfrac{\dfrac{\vdash\mathcal{N},P_{1}\quad\cdots\quad\vdash\mathcal{N},P_{n}}{\vdash\mathcal{N},\dots,\mathcal{N},P_{1}\otimes\cdots\otimes P_{n}}}{\vdash\mathcal{N},\dots,\mathcal{N},?(P_{1}\otimes\cdots\otimes P_{n})}}{\vdash\mathcal{N},\mathcal{N},\dots,\mathcal{N}}}{\vdash\mathcal{N}}\\
\dfrac{\dfrac{\vdash\mathcal{N},?(P_{1}\otimes\dots\otimes P_{n})\qquad\dfrac{\dfrac{\vdash\mathcal{N},P_{1}^{\bot},\dots,P_{n}^{\bot}}{\vdash\mathcal{N},P_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P_{n}^{\bot}}}{\vdash\mathcal{N},!(P_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P_{n}^{\bot})}}{\vdash\mathcal{N},\mathcal{N}}}{\vdash\mathcal{N}}
\end{array}</span></p>
<p>LLP is a sequent calculus and as such is finer-grained: it makes explicit structural rules and (what corresponds to) left-introduction of negation.</p>
<p>Visible above, it also internalizes duality (all formulae on the right-hand side, like in linear logic). While Laurent does not cite Thielecke's works, Thielecke's PhD thesis previously suggested that having a “duality functor” could be useful to clarify the duality aspects of CPS.</p>
<p>Laurent's graphical syntax will let you interpret linear substitution, but one would have to look at the details to see if it is exactly the same as the one you mention.</p>
</li>
</ol>

CC BY-SA 4.0
2022-04-25T14:05:15.457Z
Thank you very much for the information. It took me some time to verify the cut-elimination rules and to check how they compare to performing a jump. As you pointed out, they are pretty fine-grained, but they do allow to derive it; a difference between LLP and the CPS-calculus it seems is that the former doesn't require us to name every value. I did read the bibliography you suggested, but I wonder if anyone has pointed out the similarities between LLP and an actual IR already!
paulotorrens
CC BY-SA 4.0
2022-01-13T19:44:31.397Z
2022-01-13T19:44:31.397Z
gadmm
<p>For me, what is going on is reasonably standard:</p>
<ul>
<li>You have <span class="math-container">$c$</span> with free variables <span class="math-container">$(x_i : \tau_i)_i$</span>, and you replace it with <span class="math-container">$c[t_i/x_i]$</span> with the <span class="math-container">$(t_i)_i$</span> at types <span class="math-container">$(\tau_i)_i$</span>; this is a standard cut/substitution.</li>
<li>The replacement is done along a variable <span class="math-container">$k$</span> that is defined somewhere and used elsewhere; this sort of &quot;action at a distance&quot; is not the standard way to define cut-elimination in a sequent calculus (where we rather work by pushing definition inside terms until they meet their uses; you could define a different operational semantics to match this more small-step approach), but has been proposed for explicit substitutions for example.</li>
</ul>

CC BY-SA 4.0
2022-01-12T17:18:25.693Z
Though I did read about explicit substitution calculi, it hadn't occurred to me to look for their Curry-Howard correspondents in logic. Would you have any good references for that?
paulotorrens
CC BY-SA 4.0
2022-01-12T11:40:27.967Z
2022-01-12T11:40:27.967Z
gasche
<ol>
<li><p>You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has &quot;coexponentials.&quot; Unfortunately you can't combine &quot;coimplication&quot; and &quot;implication&quot; constructively. You need to weaken something somewhere which gets into complicated substructural logics. Its kind of like law of excluded middle or adding exceptions to a programming language. &quot;You can observe details of the evaluation&quot; breaking logical identities we rely on.</p>
</li>
<li><p>If you look at A-normal form which is closely related to CPS and use the more &quot;mathy&quot; monadic effects or call by push value (like monads but based on adjunctions) a jump with arguments ought to correspond to the counit of an adjunction <span class="math-container">$\eta: U(F(a)) \rightarrow a$</span>. I think of this as like forcing a thunk. I'm not really sure how to translate this into the language of CPS though. Call by push value can also be seen in terms of linear logic and especially so in the categorical formulation based on an asymmetric tensor and powering. Basically you have an asymmetric tensor for &quot;pushing values to a stack&quot; <span class="math-container">$\otimes : C \times D \rightarrow D$</span> and a power for &quot;popping from the stack&quot; <span class="math-container">$\pitchfork : C^{\text{op}} \times D \rightarrow D$</span>. Basically <span class="math-container">$C$</span> is like a category of values and <span class="math-container">$D$</span> is like a category of effects. Jumping into a thunk becomes the obvious evaluation map <span class="math-container">$a \otimes \pitchfork(a, b) \rightarrow b$</span>. Other people have already given linear logic explanations of this stuff though. Just wanted to say you can mostly think of some of this CPS stuff in terms of monads and adjunctions as well.</p>
</li>
</ol>

CC BY-SA 4.0
2022-01-13T21:47:09.480Z
2022-01-13T21:53:10.933Z
2022-01-13T21:53:10.933Z
Ms. Molly Stewart-Gallus
<p>It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target language of a CPS translation is the same as the source language, sometimes it's a specialized language which only allows terms in CPS form (i.e., there are no direct style functions anymore). See, e.g., <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf" rel="nofollow noreferrer">this</a> or <a href="https://www.cs.princeton.edu/%7Edpw/papers/tal-toplas.pdf" rel="nofollow noreferrer">this</a>.</p>
<p>As an example, consider Thielecke's <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.7371&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">CPS-calculus</a>, where commands are defined as either jumps or bindings:</p>
<p><span class="math-container">$$b ::=  x\langle\vec{x}\rangle\ |\ b\ \{\ x\langle\vec{x}\rangle = b\ \}$$</span></p>
<p>And one-hole contexts (commands with holes) are defined as follow:</p>
<p><span class="math-container">$$C ::= [-]\ |\ C \ \{\ x\langle\vec{x}\rangle = b\ \}\ |\ b\ \{\ x\langle\vec{x}\rangle = C\ \}$$</span></p>
<p>If we try to see these languages under the Curry-Howard isomorphism, we don't have implication anymore, but rather we use negations and products alone. The typing rules for such languages demonstrate we're trying to derive a contradiction:</p>
<p><span class="math-container">$$\frac{\color{orange}{\Gamma\vdash} k{:}\ \color{orange}{\neg\vec{\tau}}\quad\quad\color{orange}{\Gamma\vdash}\vec{x}{:}\ \color{orange}{\vec{\tau}}}{\color{orange}{\Gamma\vdash} k\langle\vec{x}\rangle}(J)$$</span></p>
<p><span class="math-container">$$\frac{\color{orange}{\Gamma,}k{:}\ \color{orange}{\neg\vec{\tau}\vdash} b\quad\quad\color{orange}{\Gamma,}\vec{x}{:}\ \color{orange}{\vec{\tau}\vdash} c}{\color{orange}{\Gamma\vdash} b\ \{\ k\langle\vec{x}\rangle=c\ \}}(B)$$</span></p>
<p>(Note that these look similar to the (AXIOM) and (CUT) rules from linear logic, though on the other side of the sequent: we have a conjunction rather than a disjunction.)</p>
<p>Reduction rules in intermediate languages such as the ones above allow jumps to be performed to bound continuations, immediately replacing arguments (hence the name &quot;jump with arguments&quot; sometimes employed). For the CPS-calculus, this can be represented by the following reduction rule:</p>
<p><span class="math-container">$$\frac{}{C[\color{blue}{k\langle \vec{x}\rangle}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \} \longrightarrow C[\color{red}{c[\color{blue}{\vec{x}}/\vec{y}]}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \}}$$</span></p>
<p><span class="math-container">$$\frac{a\longrightarrow b}{C[a]\longrightarrow C[b]}$$</span></p>
<p>...though similar languages have similar notions of jump. I'm not totally sure, but I believe that the reduction rule would corresponde to a cut inference rule similar to the following (quickly sketched):</p>
<p><a href="https://i.sstatic.net/iXClW.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/iXClW.png" alt="Cut rule" /></a></p>
<p>...where we're allowed to copy a bound proof tree and replace the jump subtree with it (in the example above, replacing subtree a with a copy of subtree b, though with a different context).</p>
<p>I'm interested on how such an intermediate language could be seen by the Curry-Howard isomorphism. So, my actual question is twofold:</p>
<ol>
<li>Has a similar implication-free subset of some logic (e.g., propositional logic) been studied somewhere? I mean, has a &quot;logic without implication&quot; been proposed?</li>
<li>What is the equivalent of a jump with arguments in logic? Assuming the cut rule I sketched above is correct (and it corresponds to the reduction rule), has something similar to it appeared elsewhere?</li>
</ol>

CC BY-SA 4.0
2022-01-12T17:22:58.487Z
The paper [Substitution, jumps, and algebraic effects](http://www.cs.ox.ac.uk/people/samuel.staton/papers/lics2014-substitution.pdf) by Fiore–Staton may be of interest to you.
varkor
<lo.logic><type-theory><pl.programming-languages><curry-howard><continuations>
What's the logical counterpart to jumps with arguments on CPS terms?
paulotorrens
# What's the logical counterpart to jumps with arguments on CPS terms?

(Asked by: username_0 on 2022-01-12)

It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target language of a CPS translation is the same as the source language, sometimes it's a specialized language which only allows terms in CPS form (i.e., there are no direct style functions anymore). See, e.g., [this](https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf) or [this](https://www.cs.princeton.edu/%7Edpw/papers/tal-toplas.pdf).

As an example, consider Thielecke's [CPS-calculus](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.7371&rep=rep1&type=pdf), where commands are defined as either jumps or bindings:

$$b ::= x\langle\vec{x}\rangle\ |\ b\ \{\ x\langle\vec{x}\rangle = b\ \}$$

And one-hole contexts (commands with holes) are defined as follow:

$$C ::= [-]\ |\ C \ \{\ x\langle\vec{x}\rangle = b\ \}\ |\ b\ \{\ x\langle\vec{x}\rangle = C\ \}$$

If we try to see these languages under the Curry-Howard isomorphism, we don't have implication anymore, but rather we use negations and products alone. The typing rules for such languages demonstrate we're trying to derive a contradiction:

$$\frac{\color{orange}{\Gamma\vdash} k{:}\ \color{orange}{\neg\vec{\tau}}\quad\quad\color{orange}{\Gamma\vdash}\vec{x}{:}\ \color{orange}{\vec{\tau}}}{\color{orange}{\Gamma\vdash} k\langle\vec{x}\rangle}(J)$$

$$\frac{\color{orange}{\Gamma,}k{:}\ \color{orange}{\neg\vec{\tau}\vdash} b\quad\quad\color{orange}{\Gamma,}\vec{x}{:}\ \color{orange}{\vec{\tau}\vdash} c}{\color{orange}{\Gamma\vdash} b\ \{\ k\langle\vec{x}\rangle=c\ \}}(B)$$

(Note that these look similar to the (AXIOM) and (CUT) rules from linear logic, though on the other side of the sequent: we have a conjunction rather than a disjunction.)

Reduction rules in intermediate languages such as the ones above allow jumps to be performed to bound continuations, immediately replacing arguments (hence the name "jump with arguments" sometimes employed). For the CPS-calculus, this can be represented by the following reduction rule:

$$\frac{}{C[\color{blue}{k\langle \vec{x}\rangle}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \} \longrightarrow C[\color{red}{c[\color{blue}{\vec{x}}/\vec{y}]}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \}}$$

$$\frac{a\longrightarrow b}{C[a]\longrightarrow C[b]}$$

...though similar languages have similar notions of jump. I'm not totally sure, but I believe that the reduction rule would corresponde to a cut inference rule similar to the following (quickly sketched):

[![Cut rule](https://i.sstatic.net/iXClW.png)](https://i.sstatic.net/iXClW.png)

...where we're allowed to copy a bound proof tree and replace the jump subtree with it (in the example above, replacing subtree a with a copy of subtree b, though with a different context).

I'm interested on how such an intermediate language could be seen by the Curry-Howard isomorphism. So, my actual question is twofold:

1. Has a similar implication-free subset of some logic (e.g., propositional logic) been studied somewhere? I mean, has a "logic without implication" been proposed?
2. What is the equivalent of a jump with arguments in logic? Assuming the cut rule I sketched above is correct (and it corresponds to the reduction rule), has something similar to it appeared elsewhere?

**Tags:** lo.logic, type-theory, pl.programming-languages, curry-howard, continuations

> **Comments:**
> **username_1**: The paper [Substitution, jumps, and algebraic effects](http://www.cs.ox.ac.uk/people/samuel.staton/papers/lics2014-substitution.pdf) by Fiore–Staton may be of interest to you.  

---

## 3 answers

### Answer by username_2 on 2022-01-13. Score: 5 | Accepted answer

1. Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): [Olivier Laurent, *Étude de la polarisation en logique* (2002)](https://tel.archives-ouvertes.fr/tel-00007884/en/). A good explanation of what is going on from a categorical perspective is given in [Melliès and Tabareau, *Resource modalities in tensor logic* (2010)](https://www.sciencedirect.com/science/article/pii/S0168007209001602). A detailed description of the correspondence between LLP and CPS along the lines of your question appears in [my PhD thesis (2013)](https://tel.archives-ouvertes.fr/tel-00918642/en/) (Chapter III, pp.91-95,153-199). (There are a lot of other references in this area; the bibliographies should provide you with a good starting point.)
2. The two rules (J) and (B) you wrote are derived as follows (in the notations of Laurent's PhD thesis):

   \begin{array}{c}
   \dfrac{\dfrac{\vdash\mathcal{N},!(P\_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P\_{n}^{\bot})\qquad\dfrac{\dfrac{\vdash\mathcal{N},P\_{1}\quad\cdots\quad\vdash\mathcal{N},P\_{n}}{\vdash\mathcal{N},\dots,\mathcal{N},P\_{1}\otimes\cdots\otimes P\_{n}}}{\vdash\mathcal{N},\dots,\mathcal{N},?(P\_{1}\otimes\cdots\otimes P\_{n})}}{\vdash\mathcal{N},\mathcal{N},\dots,\mathcal{N}}}{\vdash\mathcal{N}}\\
   \dfrac{\dfrac{\vdash\mathcal{N},?(P\_{1}\otimes\dots\otimes P\_{n})\qquad\dfrac{\dfrac{\vdash\mathcal{N},P\_{1}^{\bot},\dots,P\_{n}^{\bot}}{\vdash\mathcal{N},P\_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P\_{n}^{\bot}}}{\vdash\mathcal{N},!(P\_{1}^{\bot}\mathbin{⅋}\cdots\mathbin{⅋}P\_{n}^{\bot})}}{\vdash\mathcal{N},\mathcal{N}}}{\vdash\mathcal{N}}
   \end{array}

   LLP is a sequent calculus and as such is finer-grained: it makes explicit structural rules and (what corresponds to) left-introduction of negation.

   Visible above, it also internalizes duality (all formulae on the right-hand side, like in linear logic). While Laurent does not cite Thielecke's works, Thielecke's PhD thesis previously suggested that having a “duality functor” could be useful to clarify the duality aspects of CPS.

   Laurent's graphical syntax will let you interpret linear substitution, but one would have to look at the details to see if it is exactly the same as the one you mention.

> **Comments:**
> **username_0**: Thank you very much for the information. It took me some time to verify the cut-elimination rules and to check how they compare to performing a jump. As you pointed out, they are pretty fine-grained, but they do allow to derive it; a difference between LLP and the CPS-calculus it seems is that the former doesn't require us to name every value. I did read the bibliography you suggested, but I wonder if anyone has pointed out the similarities between LLP and an actual IR already!  

---

### Answer by username_3 on 2022-01-12. Score: 3

For me, what is going on is reasonably standard:

* You have $c$ with free variables $(x\_i : \tau\_i)\_i$, and you replace it with $c[t\_i/x\_i]$ with the $(t\_i)\_i$ at types $(\tau\_i)\_i$; this is a standard cut/substitution.
* The replacement is done along a variable $k$ that is defined somewhere and used elsewhere; this sort of "action at a distance" is not the standard way to define cut-elimination in a sequent calculus (where we rather work by pushing definition inside terms until they meet their uses; you could define a different operational semantics to match this more small-step approach), but has been proposed for explicit substitutions for example.

> **Comments:**
> **username_0**: Though I did read about explicit substitution calculi, it hadn't occurred to me to look for their Curry-Howard correspondents in logic. Would you have any good references for that?  

---

### Answer by username_4 on 2022-01-13. Score: 1

1. You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "coexponentials." Unfortunately you can't combine "coimplication" and "implication" constructively. You need to weaken something somewhere which gets into complicated substructural logics. Its kind of like law of excluded middle or adding exceptions to a programming language. "You can observe details of the evaluation" breaking logical identities we rely on.
2. If you look at A-normal form which is closely related to CPS and use the more "mathy" monadic effects or call by push value (like monads but based on adjunctions) a jump with arguments ought to correspond to the counit of an adjunction $\eta: U(F(a)) \rightarrow a$. I think of this as like forcing a thunk. I'm not really sure how to translate this into the language of CPS though. Call by push value can also be seen in terms of linear logic and especially so in the categorical formulation based on an asymmetric tensor and powering. Basically you have an asymmetric tensor for "pushing values to a stack" $\otimes : C \times D \rightarrow D$ and a power for "popping from the stack" $\pitchfork : C^{\text{op}} \times D \rightarrow D$. Basically $C$ is like a category of values and $D$ is like a category of effects. Jumping into a thunk becomes the obvious evaluation map $a \otimes \pitchfork(a, b) \rightarrow b$. Other people have already given linear logic explanations of this stuff though. Just wanted to say you can mostly think of some of this CPS stuff in terms of monads and adjunctions as well.


---

