<p>Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for <em>any</em> formula <span class="math-container">$X$</span>, the subset of formulae <span class="math-container">$\overline{A} = A → X$</span> is a reverse-mapping of the logic (i.e. if <span class="math-container">$A ⊢ B$</span> then <span class="math-container">$\overline{B} ⊢ \overline{A}$</span>) and forms a <em>Boolean</em> sub-logic, associated with a Boolean sub-lattice of the Heyting lattice. The <span class="math-container">$\overline{∧}$</span> of the sub-logic corresponds to the <span class="math-container">$∨$</span> of the original logic since you have the equivalence
<span class="math-container">$$\overline{A}\overline{∧}\overline{B} = (A → X)∧(B → X) ⊣⊢ A∨B ⊃ X = \overline{A∨B}.$$</span>
But the <span class="math-container">$\overline{∨}$</span> need not correspond to <span class="math-container">$∧$</span> of the original logic, since you only have
<span class="math-container">$$\overline{A}\overline{∨}\overline{B} = (A → X)∨(B → X) ⊢ A∧B ⊃ X = \overline{A∧B}.$$</span>
Nevertheless, the <span class="math-container">$\overline{A}$</span> form a Boolean sub-logic. Negation corresponds to <span class="math-container">$\overline{¬}\overline{A} = \overline{A} → X$</span>, and the double negative rule applies, since you have the equivalence
<span class="math-container">$$\overline{A} = A → X ⊣⊢ ((A → X) → X) → X = \overline{¬}\overline{¬}\overline{A}.$$</span>
The <span class="math-container">$⊢$</span> direction is a special case of the inference
<span class="math-container">$$b ⊢ (b → c) → c,$$</span>
while the <span class="math-container">$⊣$</span> direction is a special case of the inference
<span class="math-container">$$b → d ⊣ ((b → c) → c) → d.$$</span></p>
<p>So, continuations can refer broadly to any <span class="math-container">$X$</span>, not just to <span class="math-container">$⊥$</span>. The mapping <span class="math-container">$A$</span> into <span class="math-container">$\overline{\overline{A}}$</span> is then a <em>forward</em> map of the original logic into a Boolean-sublogic, while the <span class="math-container">$\overline{A}$</span> map into &quot;responses&quot; for the <span class="math-container">$\overline{\overline{A}}$</span>. This is laid out in detail at the very outset of <a href="https://www.cambridge.org/core/journals/journal-of-functional-programming/article/classical-logic-continuation-semantics-and-abstract-machines/CCC69E5E233D89BE6378EB7BF50E3AB9" rel="nofollow noreferrer">Classical logic, continuation semantics and
abstract machines</a>, <em>J. Functional Programming</em> <strong>8</strong> (6): 543–572, November 1998, which is open access at the link. You can get a clearer (and more accurate) picture there, than what I laid out in my brief description here.</p>

CC BY-SA 4.0
2024-04-04T13:57:01.910Z
Can you clarify what you mean by a "sub-logic"? You use a subset of the formulae but the notion of implication is flipped and the interpretation of the connectives is different so I would not use that term myself.
Max New
CC BY-SA 4.0
2024-04-05T08:02:21.997Z
Ok. Sub-lattice should suffice, then. Double-bar to unflip. The key observation is that, though one of the connectives changes, the least upper bound and greatest lower bound property still holds amongst the subset of formulae ... and it comprises a Boolean lattice. Since $(a → e) → (c → f), (b → d) → (c → e) ⊢ (a∧b → d) → (c → f)$ is intuitionistically valid, then setting $d = e = f = X$ yields $\overline{a} → \overline{c}, \overline{b} → \overline{c} ⊢ \overline{a∧b} → \overline{c}$ even though $\overline{a∧b} ⊬ \overline{a}∨\overline{b}$. I'll add an edit on this later.
NinjaDarth
CC BY-SA 4.0
2024-04-03T23:52:43.703Z
2024-04-03T23:52:43.703Z
NinjaDarth
<p>The type of a function (lambda) is the type of its argument and the type of what it returns. Some functions do not return anything - they go into an infinite loop or in some theories raise an error, and thus their return type is empty. It's not that their return type is null (or unit type, or really they are procedures). It's that they never return anything and any potential capture of their result value will never happen.</p>

<p>Continuations are, for all practical purposes, infinite loops. They never return anything and thus their return type is void. Waiting for them to finish will take forever.</p>

<p>Now you can modify your theory slightly. You may say that when a continuation receives a special value from the void type, it finishes and returns null, for instance.
This does not affect the definition of a continuation. The continuation will still never return, because this value from the void type does not exist. However, the type of continuation behaves as negation from now. When you feed a value from non-empty type, the continuation loops forever. When you feed it a hypothetical value from a void type, it returns null, which is non-empty.</p>

<p>You could make it a little bit less hypothetical if you introduce a special "error" value. The use of this value is forbidden, that means when you use it, an error happens (compare it to throwing an exception). Now "empty type" does not mean "looping forever" but "raising an error, failing to finish normally". You define a continuation in such a way that when they encounter an error, they quit gracefully returning a normal value.</p>

<p>Now when you feed the continuation a normal value, they would loop forever, as expected. When you feed them the "error" value, they encounter an error the moment they try to use it and exit, returning a value.</p>

<p>Again, this works as a type negation. Here "false type" does mean "a type without any non-error value". This could be a valid theory for a language featuring weak pointers (like C) where the "error" value is a null pointer. You can define some void type without any normal value but you still can make a null pointer to that type, where dereferencing always fails. (Side note: "void" in C doesn't mean a "false type" but unit type actually.)</p>

<p>The key point is that you can always extend your theory with some axiom that says: when we receive a value from the empty type, something happens. This is always compatible with the theory, as this can never happen, yet it can serve some theoretical purposes.</p>

CC BY-SA 4.0
2019-06-13T14:55:37.663Z
Okay, let me see if I understand, In Haskell, non-termination and errors are semantically equivalent; there is the one "undefined" element, ⊥. (To avoid confusion with void, I'm going to call void $0$.) So constructing a non-⊥ element of $A\to 0$ proves that $A$ has no non-⊥ elements.

Are you saying that with continuations, non-termination is different from ⊥? Because continuations are defined (they aren't semantically $\bot$), but they don't terminate? And for $x:A\to 0$ to prove $A$ has no terminating elements, $x$ needs to be not just non-⊥, but also terminating, correct?
greatBigDot
CC BY-SA 4.0
2019-06-13T14:57:42.083Z
Also, there are things like Agda and Idris and Coq where every program terminates (unless certain pragmas or compilation flags are given). Under that system an element $x : A \to 0$ really does prove that $A$ is empty; no caveats about "non-⊥" are necessary. It sounds like that kind of totality impossible if you have continuations in your language, yes?
greatBigDot
CC BY-SA 4.0
2019-06-14T08:09:43.673Z
The statement "*Continuations are [...] infinite loops*" is deeply misleading. A better way of thinking about continuations is as *return channel* or *jump* (with values). See H. Thielecke's [Continuations, functions and jumps](https://dl.acm.org/citation.cfm?id=568561), or, even better, R Milner's [https://hal.inria.fr/inria-00075405/document](https://hal.inria.fr/inria-00075405/document).
Martin Berger
CC BY-SA 4.0
2019-06-13T11:56:35.493Z
2019-06-13T11:56:35.493Z
haael
<p>When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it.</p>

<p>With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression <span class="math-container">$e : +\mathsf{int}$</span> and reduce that expression to a numeral <span class="math-container">$n$</span>. This means that the continuation <span class="math-container">$\bullet : ¬int$</span> is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually <span class="math-container">$\mathsf{int}$</span>, because we are interested in using continuation-based computations that eventually result in integers. <span class="math-container">$\bullet$</span> is something that immediately completes the computation, hence the rules:</p>

<p><span class="math-container">$$(begin)\ \ \ \  e : +int \leadsto \langle e | \bullet \rangle$$</span>
<span class="math-container">$$(end)\ \ \ \  \langle n | \bullet \rangle \leadsto n$$</span></p>

<p>I don't know what happens if you have <span class="math-container">$\bullet$</span> involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.</p>

<p>Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.</p>

<p>In that setting, <span class="math-container">$⊥$</span> is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also <span class="math-container">$0$</span>, which gets the principle of explosion (which is arguably the distinct part of the empty type<sup>1</sup>). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom <span class="math-container">$⊥$</span> is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).</p>

<p>Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.</p>

<ol>
<li>In the continuation-with-abstract-result-type setting, you can also interpret explosion, but it has sort of a different meaning. Effectively such interpretations are always 'delimited' somewhere, even if it's only the end of your program. Explosion means that if you somehow get a value of the abstract result type, you can throw away your current continuation and jump to the delimiter. So it is an 'abort' operation. Linear logic doesn't allow this; all continuations <em>must</em> be used (and used exactly once), so explosion must be justified by involving an 'impossible' situation, like having a value of an empty type.</li>
</ol>

CC BY-SA 4.0
2019-06-18T22:27:32.593Z
While the second part of the answer looks speculative, there is indeed an interpretation in the same area as the first linked paper based on linear (involutive) negation. See Girard, [A new constructive logic: classical logic](https://doi.org/10.1017/S0960129500001328) (1991). Its continuation semantics is given by attributing to continuations an entirely different role than representing negation.
gadmm
CC BY-SA 4.0
2019-06-19T00:52:09.720Z
Oh, another paper to look at is [Linear Logic for Constructive Mathematics](https://arxiv.org/abs/1805.07518), which gives an interpretation of classical linear logic in terms of intuitionistic logic that is (I think) different than what you'll find in Girard's paper. Contrary to the title, the semantics are not exactly linear, but it still has some similar distinctions.
Dan Doel
CC BY-SA 4.0
2019-06-14T01:13:18.247Z
2019-06-14T12:59:29.077Z
2019-06-14T12:59:29.077Z
Dan Doel
<p>Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the Cartesian product is logical conjunction.)</p>

<p>Negation is represented as <span class="math-container">$A \to \bot$</span>, where <span class="math-container">$\bot$</span> is the empty type. This works because if a type is inhabited, there can't be any function <span class="math-container">$A \to \bot$</span> (if you do you have such a function and the type is inhabited, feed the value into it and you get an element of the empty type, hence a contradiction), and vice versa (if <span class="math-container">$A$</span> is empty, the empty function <span class="math-container">$A \to \bot$</span> exists).</p>

<p>But once you add continuations to your language, an <span class="math-container">$A$</span>-continuation can also be given the type <span class="math-container">$A \to \bot$</span>. (see e.g. <a href="https://pdfs.semanticscholar.org/3a68/6ab25229599b4e68d45f84196cad9cdb3817.pdf" rel="noreferrer">the symmetric lambda calculus</a>). This apparently provides computational meaning to classical theorems; for example, the <span class="math-container">$\mathcal{C}$</span>-operator (a basic operator for manipulating continuations), has type <span class="math-container">$\neg\neg A \to A$</span>.</p>

<p>But can't you have continuations for non-empty types? If you add continuations, does <span class="math-container">$\neg A$</span> no longer express "<span class="math-container">$A$</span> is-empty/is-false/has-no-proofs"? It can't, right? <a href="http://pllab.is.ocha.ac.jp/~asai/papers/diku-ist11.pdf" rel="noreferrer">This formulation</a> makes an inhabitant of <span class="math-container">$\mathbb{N} \to \bot$</span> axiomatic, and <span class="math-container">$\mathbb{N}$</span> certainly isn't uninhabited. So what does "<span class="math-container">$\neg A$</span>" actually express, if not "<span class="math-container">$A$</span> is-empty/is-false/has-no-proof"? And how do you actually express "<span class="math-container">$A$</span> is-empty/is-false/has-no-proof" when continuations exist?</p>

<lo.logic><type-theory><proof-theory><continuations><curry-howard>
How do continuations represent negations (under the Curry–Howard correspondence)?
greatBigDot
# How do continuations represent negations (under the Curry–Howard correspondence)?

(Asked by: username_0 on 2019-06-12)

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the Cartesian product is logical conjunction.)

Negation is represented as $A \to \bot$, where $\bot$ is the empty type. This works because if a type is inhabited, there can't be any function $A \to \bot$ (if you do you have such a function and the type is inhabited, feed the value into it and you get an element of the empty type, hence a contradiction), and vice versa (if $A$ is empty, the empty function $A \to \bot$ exists).

But once you add continuations to your language, an $A$-continuation can also be given the type $A \to \bot$. (see e.g. [the symmetric lambda calculus](https://pdfs.semanticscholar.org/3a68/6ab25229599b4e68d45f84196cad9cdb3817.pdf)). This apparently provides computational meaning to classical theorems; for example, the $\mathcal{C}$-operator (a basic operator for manipulating continuations), has type $\neg\neg A \to A$.

But can't you have continuations for non-empty types? If you add continuations, does $\neg A$ no longer express "$A$ is-empty/is-false/has-no-proofs"? It can't, right? [This formulation](http://pllab.is.ocha.ac.jp/~asai/papers/diku-ist11.pdf) makes an inhabitant of $\mathbb{N} \to \bot$ axiomatic, and $\mathbb{N}$ certainly isn't uninhabited. So what does "$\neg A$" actually express, if not "$A$ is-empty/is-false/has-no-proof"? And how do you actually express "$A$ is-empty/is-false/has-no-proof" when continuations exist?

**Tags:** lo.logic, type-theory, proof-theory, continuations, curry-howard

---

## 3 answers

### Answer by username_5 on 2019-06-14. Score: 11 | Accepted answer

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$
$$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of the empty type1). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.

1. In the continuation-with-abstract-result-type setting, you can also interpret explosion, but it has sort of a different meaning. Effectively such interpretations are always 'delimited' somewhere, even if it's only the end of your program. Explosion means that if you somehow get a value of the abstract result type, you can throw away your current continuation and jump to the delimiter. So it is an 'abort' operation. Linear logic doesn't allow this; all continuations *must* be used (and used exactly once), so explosion must be justified by involving an 'impossible' situation, like having a value of an empty type.

> **Comments:**
> **username_6**: While the second part of the answer looks speculative, there is indeed an interpretation in the same area as the first linked paper based on linear (involutive) negation. See Girard, [A new constructive logic: classical logic](https://doi.org/10.1017/S0960129500001328) (1991). Its continuation semantics is given by attributing to continuations an entirely different role than representing negation.  
> **username_5**: Oh, another paper to look at is [Linear Logic for Constructive Mathematics](https://arxiv.org/abs/1805.07518), which gives an interpretation of classical linear logic in terms of intuitionistic logic that is (I think) different than what you'll find in Girard's paper. Contrary to the title, the semantics are not exactly linear, but it still has some similar distinctions.  

---

### Answer by username_1 on 2024-04-03. Score: 1

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for *any* formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of the logic (i.e. if $A ⊢ B$ then $\overline{B} ⊢ \overline{A}$) and forms a *Boolean* sub-logic, associated with a Boolean sub-lattice of the Heyting lattice. The $\overline{∧}$ of the sub-logic corresponds to the $∨$ of the original logic since you have the equivalence
$$\overline{A}\overline{∧}\overline{B} = (A → X)∧(B → X) ⊣⊢ A∨B ⊃ X = \overline{A∨B}.$$
But the $\overline{∨}$ need not correspond to $∧$ of the original logic, since you only have
$$\overline{A}\overline{∨}\overline{B} = (A → X)∨(B → X) ⊢ A∧B ⊃ X = \overline{A∧B}.$$
Nevertheless, the $\overline{A}$ form a Boolean sub-logic. Negation corresponds to $\overline{¬}\overline{A} = \overline{A} → X$, and the double negative rule applies, since you have the equivalence
$$\overline{A} = A → X ⊣⊢ ((A → X) → X) → X = \overline{¬}\overline{¬}\overline{A}.$$
The $⊢$ direction is a special case of the inference
$$b ⊢ (b → c) → c,$$
while the $⊣$ direction is a special case of the inference
$$b → d ⊣ ((b → c) → c) → d.$$

So, continuations can refer broadly to any $X$, not just to $⊥$. The mapping $A$ into $\overline{\overline{A}}$ is then a *forward* map of the original logic into a Boolean-sublogic, while the $\overline{A}$ map into "responses" for the $\overline{\overline{A}}$. This is laid out in detail at the very outset of [Classical logic, continuation semantics and
abstract machines](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/classical-logic-continuation-semantics-and-abstract-machines/CCC69E5E233D89BE6378EB7BF50E3AB9), *J. Functional Programming* **8** (6): 543–572, November 1998, which is open access at the link. You can get a clearer (and more accurate) picture there, than what I laid out in my brief description here.

> **Comments:**
> **username_2**: Can you clarify what you mean by a "sub-logic"? You use a subset of the formulae but the notion of implication is flipped and the interpretation of the connectives is different so I would not use that term myself.  
> **username_1**: Ok. Sub-lattice should suffice, then. Double-bar to unflip. The key observation is that, though one of the connectives changes, the least upper bound and greatest lower bound property still holds amongst the subset of formulae ... and it comprises a Boolean lattice. Since $(a → e) → (c → f), (b → d) → (c → e) ⊢ (a∧b → d) → (c → f)$ is intuitionistically valid, then setting $d = e = f = X$ yields $\overline{a} → \overline{c}, \overline{b} → \overline{c} ⊢ \overline{a∧b} → \overline{c}$ even though $\overline{a∧b} ⊬ \overline{a}∨\overline{b}$. I'll add an edit on this later.  

---

### Answer by username_3 on 2019-06-13. Score: -3

The type of a function (lambda) is the type of its argument and the type of what it returns. Some functions do not return anything - they go into an infinite loop or in some theories raise an error, and thus their return type is empty. It's not that their return type is null (or unit type, or really they are procedures). It's that they never return anything and any potential capture of their result value will never happen.

Continuations are, for all practical purposes, infinite loops. They never return anything and thus their return type is void. Waiting for them to finish will take forever.

Now you can modify your theory slightly. You may say that when a continuation receives a special value from the void type, it finishes and returns null, for instance.
This does not affect the definition of a continuation. The continuation will still never return, because this value from the void type does not exist. However, the type of continuation behaves as negation from now. When you feed a value from non-empty type, the continuation loops forever. When you feed it a hypothetical value from a void type, it returns null, which is non-empty.

You could make it a little bit less hypothetical if you introduce a special "error" value. The use of this value is forbidden, that means when you use it, an error happens (compare it to throwing an exception). Now "empty type" does not mean "looping forever" but "raising an error, failing to finish normally". You define a continuation in such a way that when they encounter an error, they quit gracefully returning a normal value.

Now when you feed the continuation a normal value, they would loop forever, as expected. When you feed them the "error" value, they encounter an error the moment they try to use it and exit, returning a value.

Again, this works as a type negation. Here "false type" does mean "a type without any non-error value". This could be a valid theory for a language featuring weak pointers (like C) where the "error" value is a null pointer. You can define some void type without any normal value but you still can make a null pointer to that type, where dereferencing always fails. (Side note: "void" in C doesn't mean a "false type" but unit type actually.)

The key point is that you can always extend your theory with some axiom that says: when we receive a value from the empty type, something happens. This is always compatible with the theory, as this can never happen, yet it can serve some theoretical purposes.

> **Comments:**
> **username_0**: Okay, let me see if I understand, In Haskell, non-termination and errors are semantically equivalent; there is the one "undefined" element, ⊥. (To avoid confusion with void, I'm going to call void $0$.) So constructing a non-⊥ element of $A\to 0$ proves that $A$ has no non-⊥ elements.  Are you saying that with continuations, non-termination is different from ⊥? Because continuations are defined (they aren't semantically $\bot$), but they don't terminate? And for $x:A\to 0$ to prove $A$ has no terminating elements, $x$ needs to be not just non-⊥, but also terminating, correct?  
> **username_0**: Also, there are things like Agda and Idris and Coq where every program terminates (unless certain pragmas or compilation flags are given). Under that system an element $x : A \to 0$ really does prove that $A$ is empty; no caveats about "non-⊥" are necessary. It sounds like that kind of totality impossible if you have continuations in your language, yes?  
> **username_4**: The statement "*Continuations are [...] infinite loops*" is deeply misleading. A better way of thinking about continuations is as *return channel* or *jump* (with values). See H. Thielecke's [Continuations, functions and jumps](https://dl.acm.org/citation.cfm?id=568561), or, even better, R Milner's [https://hal.inria.fr/inria-00075405/document](https://hal.inria.fr/inria-00075405/document).  

---

