3
$\begingroup$

In Wikipedia's Double-negation translation article, I found that any formula in classical logic has its double negation as its intuitionist equivalent:

It is also possible to define φN by prefixing ¬¬ before every subformula of φ, as done by Kolmogorov. Such a translation is the logical counterpart to the call-by-name continuation-passing style translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.

Could anyone explain how prefixing ¬¬ before every sub formula of a proposition is the logical counter part to call-by-name continuation-passing style? If possible, could you use Python, since I'm not familiar with Scheme and Haskell.

I've done some research into CPS, but I'm not seeing the relationship, apart from the fact that a function $P \to \bot$ doesn't have a return value.

$\endgroup$
  • $\begingroup$ You might be interested in this answer to What are the most interesting equivalences arising from the Curry-Howard Isomorphism?. $\endgroup$ – Joshua Taylor Aug 25 '14 at 19:58
  • 1
    $\begingroup$ Some slides of mine tackle this question. They start with a general introduction to the difference between classical and constructive mathematics and end with specific Haskell code. $\endgroup$ – Ingo Blechschmidt Jan 12 '16 at 20:33
  • $\begingroup$ @IngoBlechschmidt I don't understand the part on interpreting classical logics as defending a proposition with jumping back the time allowed. Could you please elaborate? I understand by Curry-Howard correspondence, simply typed $\lambda\mu$-calculus corresponds to classical logic, and roughly speaking, $\mu$ is equivalent to call/cc, something related to jumping back, but I don't understand how this could be understood as defending with jumping backs... $\endgroup$ – Yai0Phah Jun 30 '19 at 14:18
  • $\begingroup$ @IngoBlechschmidt (continued) especially, if we consider intuitionistic logic constructive, how can we consider classical logic constructive with jumping back the time allowed? $\endgroup$ – Yai0Phah Jun 30 '19 at 14:19
  • $\begingroup$ @Yai0Phah: The double negation translation of the law of excluded middle $\varphi\vee\neg\varphi$ stores the current continuation before proceeding to give the bluffed answer $\neg\varphi$ (i.e. $\varphi\Rightarrow\bot$). In case the bluff is called (if evidence for $\varphi$ is presented), the previously-stored continuation is taken and the new answer $\varphi$ is given in place of the old one. This can be regarded as a form of time travel. In this sense we defend the claim $\varphi \vee \neg\varphi$ by means of time travel. Does that make sense? Feel free to ask for further clarification! $\endgroup$ – Ingo Blechschmidt Jul 1 '19 at 15:14
1
$\begingroup$

Turns out that my question is answered in great detail here: http://www.ps.uni-saarland.de/~duchier/python/continuations.html

$\endgroup$
  • 1
    $\begingroup$ Can you add some commentary? I don't see any mention in that article about the correspondence between double negation and call-by-name CPS. $\endgroup$ – Joshua Taylor Aug 25 '14 at 19:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.