1
$\begingroup$

I am puzzled by a point in this paper by Phil Wadler.

Figure 6 shows a proof of the law of the excluded middle, $A ∨ ¬A$. The computational interpretation of this proof exploits the ability of classisal [sic] control operators to return multiple times from a single term. The term of type $A ∨ ¬A$ first returns an injection into the right of the sum, a continuation that expects a value of type $A$. If the continuation is ever passed such a value, then the original term of type $A ∨ ¬A$ now returns an injection into the left of the sum, containing the value passed to the continuation.

The article includes a sort of parable about the devil, which I don't understand. The parable is also featured on Chris Marten's website, in interactive form, but I don't quite understand that either.

So, my question is, what is this "ability of classical control operators to return multiple times from a single term"?

I think I understand the following:

  • $¬A$ is equivalent to $A → ⊥$, which, in the computational interpretation, is a function which takes an A and never returns.
  • $A ∨ ¬A$ is equivalent to $¬A → A$ (but also, by commutativity, to $A → ¬A$?) [Correction: it is equivalent to $A → A$ and $¬A → ¬A$]

What I am clearly a bit shaky on is the relationship between a negated term and a term which "takes" a value. I assume that this has something to do with the idea of "negative position", but I am struggling to learn more.

$\endgroup$
2
  • $\begingroup$ Do you understand continuations? $\endgroup$ Commented Dec 14, 2023 at 18:23
  • $\begingroup$ To some extent. I understand that A → ⊥ is a continuation but I'm not sure I'm interpreting it correctly. I don't understand why "The term of type A ∨ ¬A first returns an injection into the right of the sum". Why the right and not the left? One possible interpretation I have is that, having accepted a value of type A, the continuation evaluates to false, causing the whole term to return the value on the other side of the disjunction. I am sure there is some gap in my knowledge here. $\endgroup$
    – Theo H
    Commented Dec 14, 2023 at 19:19

2 Answers 2

2
$\begingroup$

The control operators in question allow you to capture continuations such that calling the continuation is in some sense equivalent to "returning from" the expression. so, for instance, in (using Haskell syntax):

callCC (\k -> ...)

There are two ways for the expression to "return" to its context:

  1. The ... can produce some value, and that value is returned
  2. Something can call k with a value, and that value is effectively 'returned' to the same place

But, the kicker is that 2 does not require the call to k to happen according to the stack discipline that you might be used to thinking about. So, for instance, something as simple as:

callCC (\k -> k)

results in a continuation value being returned, and if that continuation value is subsequently called, control effectively jumps back and "returns again" with whatever value the continuation was called with, even though you are no longer "within" the lexical scope of the expression.

So, the callCC ... expression can effectively "return" as many times as we can arrange for a smuggled copy of the continuation to be called, because calling the continuation works just like returning from the expression. The expression I gave above is not easy to give a type to, but excluded middle is, and we can implement it like:

callCC (\k -> Right (\x -> k (Left x)))

So, initially, we return the normal way, with an $A → ⊥$ value in the right-hand case. This is our only choice, because we don't have an $A$ value yet to return. This $¬A$ value has a smuggled copy of the continuation, though. And if it ever gets called with an $A$ value, it calls the continuation to jump back and produce a left-hand case instead (because at that point, we do have an $A$ value).

Obviously, all this is not accomplished with actual "time travel" or whatever. It is implemented by saving, discarding, and restoring implicit control flow information. The result is largely the same as if you were jumping back in the program's execution history, though, except that other side effects are generally not undone.

Incidentally, $A ∨ ¬A$ is classically equivalent to $A → A$ and $¬A → ¬A$, not the two implications you gave.

$\endgroup$
3
  • $\begingroup$ Thanks. So the "classical control operators" that Wadler refers to are call/cc and similar? He only uses the term once in the paper, so I just wasn't clear what exactly he was referring to. $\endgroup$
    – Theo H
    Commented Dec 15, 2023 at 21:20
  • $\begingroup$ I'm afraid I find the paper very hard to follow and am trying to read these lecture notes instead: cs.cmu.edu/~fp/courses/15317-s23/lectures/12-cont.pdf $\endgroup$
    – Theo H
    Commented Dec 15, 2023 at 21:37
  • $\begingroup$ I have written a complementary answer which covers the other aspects of the question (what I thought they were when I asked it, anyway) $\endgroup$
    – Theo H
    Commented Dec 18, 2023 at 22:20
0
$\begingroup$

Dan Doel's answer is helpful, but I want to include some more introductory info I've uncovered, about what "classical control operators" refers to.

First of all, "classical" doesn't refer here to classical logic. It refers to a range of control operators derived in the 80s and 90s, all of which provide the facility of reifying a continuation (i.e. storing a continuation as a variable). In some cases they offer the more powerful abstraction of delimited continuations.

Wadler's paper refers to Sussman and Steel's call/cc and Felleisen et al.'s $C$ operator. There are many other control operators from this era. They are discussed in (for example) in section 9.4.1 Classical Control Operators of the PLT Scheme manual.

Wikipedia has a different list, focusing exclusively on operators which support delimited continuations:

Delimited continuations were first introduced by Felleisen in 1988 with an operator called $\mathcal {F}$ first introduced in a tech report in 1987, along with a prompt construct $\#$. The operator was designed to be a generalization of control operators that had been described in the literature such as call/cc from Scheme, ISWIM's J operator, John C. Reynolds' escape operator, and others. Subsequently, many competing delimited control operators were invented by the programming languages research community such as prompt and control,4 shift and reset, cupto, fcontrol, and others.

via https://en.wikipedia.org/wiki/Delimited_continuation#History

call/cc has a type which corresponds to Peirce's Law, while the type of Felleisen's $C$ operator corresponds to double-negation elimination. Each of these theorems is not derivable in intuitionistic logic, but adding either of them to intuitionistic logic gives classical logic. In other words, they are equivalent to the law of the excluded middle.

It's tempting to surmise that the types of any of the classical control operators must add up to some theorems that, when added to intuitionistic logic, give classical logic, but I can't find any articles which confirm this. If this were true, it would imply that the word "classical" in "classical control operators" has a double meaning. The closest thing I've found is these lecture slides by Xavier Leroy: You’ve got to decide one way or the other! Classical logic, continuations, and control operators.

More generally, the term "extract" seems to occur in the literature when referring to the computational interpretations of logical proofs. I was not aware of of this, and it seems to make clear that using the Curry-Howard isomorphism to turn the law of the excluded middle into "code" is a bit of an extrapolation. Frank Pfenning's lecture notes refer to this particular case as evidence that "the whole enterprise of a computational interpretation of classical logic [is] brittle and ultimately unsatisfactory".

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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