 Theoretical Computer Science

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

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? ## Solution

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