What's the logical counterpart to jumps with arguments on CPS terms?

Question

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 or this.

As an example, consider Thielecke's CPS-calculus, 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):

...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?

Answer 1

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). 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). A detailed description of the correspondence between LLP and CPS along the lines of your question appears in my PhD thesis (2013) (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.

Answer 2

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.

Answer 3

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.