The Devil of the Excluded Middle

• February 14, 2022

The tale of the “Devil of the Excluded Middle” appears in [Wadl03] as a humorous sketch depicting the execution of a program typed by the law of the excluded middle. With apologies to Wadler, I reproduce it here:

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? “No”, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

It seems obvious that the devil, being the spirit of evil, has cheated the man. We can interpret the devil’s choice of (b) as a change in the nature of his offer. Accordingly, the man acts on the belief that the offer is transactional, i.e., in exchange for a billion dollars, the devil would grant him anything he desired. It’s almost as though the devil merely created an illusion at the beginning by presenting two possibilities.

A more amenable (and more confusing) version of this tale (by Peter Selinger) appears as exercise (6.19) in [SøUr06]. In it, an evil king gives a shepherd the following orders:

“You must bring me the philosopher’s stone, or you have to find a way to turn the philosopher’s stone into gold. If you don’t, your head will be taken off tomorrow!”

[SøUr06] presents the following solution to the shepherd’s quandary:

The next day the poor shepherd brings to the king’s palace a huge machine. The machine has two openings. One is marked “Put the philosopher’s stone here!” and on the other it reads “The gold will fall out from here”. That will perfectly work as long as the king cannot put the philosopher’s stone into the machine. But what if, somehow, the king comes into the possession of the philosopher’s stone? Then the shepherd’s brother, hidden inside the machine, will grab the stone, and hand it discretely to the shepherd. The shepherd now can say: “Oops, Your Majesty, I’ve been mistaken. Here is the philosopher’s stone!”

Again, this seems wrong. The shepherd’s machine cannot produce gold from the philosopher’s stone, and it isn’t the philosopher’s stone (by virtue of not being a stone). The machine seems only capable of producing the philosopher’s stone from itself.

An infuriating (and therefore fascinating?) aspect of the computational interpretation of classical logic is that both these stories mirror the behaviour of a program of type \(\alpha \lor \lnot \alpha\) somewhat accurately. (To be pedantic, the type here is \(\alpha \lor (\alpha \to \beta)\), a classical tautology that behaves nearly identically to \(\alpha \lor \lnot \alpha\)). Studying this interpretation can add important details to these tales, such as the wonderful hint hidden in Martens’ presentation.

The contents of this post assumes some knowledge of typed \(\lambda\) calculus, natural deduction style proofs, and a basic understanding of the Curry-Howard Isomorphism. Some knowledge of the Call-by-Value evaluation strategy is helpful (look here for a readable explanation). To keep this post short, I won’t be presenting the proofs for the claims made in [Grif89], but I believe I’ve provided enough details in the next section to explain the devil’s behaviour.

Preliminaries

It’s well known that the Law of the Excluded Middle (LEM) is not accepted as truth in constructive logics. This is unfortunate, as simply typed \(\lambda\) terms correspond to proofs over (the propositional fragment of) these logics and not their classical counterparts. This means that, in order to understand the devil, we need a new set of computational rules that can be typed with LEM.

In [Grif89], Griffin shows how control operators can be typed with the Double Negation Elimination (DNE) rule. These operators are based on the call/cc subroutine in the programming language Scheme. [FFKD87] presents a syntax and a set of rewrite rules for Idealized Scheme, a language that captures this control operator. Griffin types terms in this language with DNE.

The syntax of Idealized Scheme is: \[ M \Coloneqq x \mid M M \mid \lambda x. M \mid \mathcal{C}(M) \mid \mathcal{A}(M) \] The elements \(\mathcal{C}\) and \(\mathcal{A}\) are the control operators.

The operational semantics of Idealized Scheme uses a Call-By-Value (CBV) style evaluation strategy. The principle of CBV is to fully reduce all parameters of a function before beginning its evaluation. It’s also deterministic; the first valid reducible expression (redex) encountered in a left-to-right sweep of the term (i.e., the leftmost-outermost one) is the one to get reduced. Felleisen et. al. use the notion of Evaluation Contexts (or simply contexts) to capture this strategy. Its syntax is: \[ E \Coloneqq [\;] \mid VE \mid EM \] Here, the hole \([\;]\) is meant to contain a redex. \(V\) is a value: i.e., it contains no valid redexes. Notably, in a CBV execution, functions who’s bodies contain redexes are considered values; this is because those redexes are considered invalid. As a consequence, badly written functions remain badly written until absolutely required. In terms of execution contexts, this means \(E \not\Coloneqq \lambda x. E\).

Any term \(M\) can be viewed as \(E[M']\) where \(M'\) is the leftmost-outermost valid redex inside \(M\). It’s expected that this context will change in the course of the evaluation of a term as the leftmost-outermost redex changes. The rewrite rules are specified over these contexts. They are: \[ \begin{aligned} E[(\lambda x. M)] V &\to_{\beta_v} E\left[M\left[x \coloneqq V\right]\right]\\ E[\mathcal{A}(M)] &\to_\mathcal{A} M\\ E[\mathcal{C}(M)] &\to_\mathcal{C} M\left(\lambda z. \mathcal{A}\left(E\left[z\right]\right)\right) \end{aligned} \] These rules inspire an understanding of \(\mathcal{A}\) as an aborting or an escaping operation that drops the context surrounding the term it contains. \(\mathcal{C}\) is similar to call/cc: the execution of \(\mathcal{C}(M)\) passes to \(M\) an abstraction of the continuation of \(\mathcal{C}(M)\) such that, if this continuation is invoked, the evaluating machine jumps to the subterm requiring it. The following is a representative use-case of these operators: \[ \begin{aligned} E[\mathcal{C}(M)] &\to_\mathcal{C} M(\lambda z. \mathcal{A}(E[z]))\\ &\overset{*}{\to} E'\left[ \left(\lambda x. M'\right) \left(\lambda z. \mathcal{A}(E[z])\right) \right]\\ &\to_{\beta_v} E'\left[ M'\left[ x := \lambda z. \mathcal{A}(E[z]) \right] \right]\\ &\overset{*}{\to} E''[(\lambda z. \mathcal{A}(E[z])) N]\\ &\to_{\beta_v} E''[\mathcal{A}(E[N])]\\ &\to_{\mathcal{A}} E[N] \end{aligned} \]

In [Grif89], Griffin argues for the consistency of the typing rules \[ \begin{prooftree} \AxiomC{$\Gamma \vdash M: (\varphi \to \bot) \to \bot$} \UnaryInfC{$\Gamma \vdash \mathcal{C}(M): \varphi$} \end{prooftree} \] And \[ \begin{prooftree} \AxiomC{$\Gamma \vdash M: \bot$} \UnaryInfC{$\Gamma \vdash \mathcal{A}^\varphi(M): \varphi$} \end{prooftree} \] He also imports the typing rules of Church’s simply-typed calculus for typing \(\lambda\) abstractions and applications. It’s clear that the new rules correspond to the double negation elimination and \(\bot\) elimination rules respectively.

Unfortunately, Griffin’s analysis requires the overall term \(E[\mathcal{C}(M)]\) to be typed by \(\bot\) to use the \(\to_\mathcal{C}\) rule. The typed rule now looks like: \[ E^\bot[\mathcal{C}^\varphi(M^{\lnot \lnot \varphi})] \to_{\mathcal{C}} M^{\lnot \lnot \varphi} (\lambda z^\varphi. \mathcal{A}^\bot(E^\bot[z])) \] This is a problem, as no closed term can be typed \(\bot\). Griffin gets around this by mandating a continuation variable on each typed term. Formally, transform \[ M^\alpha \Longrightarrow \mathcal{C}(\lambda k^{\lnot \alpha}. k M^\alpha) \] Where \(k\) is not free in \(M\). Griffin’s typing rules give \[ \begin{prooftree} \AxiomC{$\vdash M: \alpha$} \UnaryInfC{$k: \lnot \alpha \vdash kM: \bot$} \UnaryInfC{$\vdash \lambda k^{\lnot \alpha}. kM: \lnot \lnot \alpha$} \UnaryInfC{$\vdash \mathcal{C}(\lambda k^{\lnot \alpha}. kM): \alpha$} \end{prooftree} \] He then restricts the scope of evaluation contexts to be within the scope of this continuation variable. This allows us to use the \(\mathcal{C}\) rewrite rule, by changing it to \(\to_{t \mathcal{C}}\): \[ \mathcal{C} \left( \lambda k^{\lnot \alpha}. E^\bot \left[\mathcal{C}^\varphi(M^{\lnot \lnot \varphi}) \right] \right) \to_{t \mathcal{C}} \mathcal{C} \left(\lambda k^{\lnot \alpha}. M^{\lnot \lnot \varphi} (\lambda z^\varphi. \mathcal{A}^\bot(E^\bot[z])) \right) \] Griffin removes the \(\mathcal{C}(\lambda k. \cdots)\) for brevity. I will do the same.

Typing and Evaluating LEM

As per Glivenko’s Theorem, \(\lnot \lnot (\alpha \lor \lnot \alpha)\) is true in constructive logics. Its proof is: \[ \begin{prooftree} \AxiomC{$\lnot (\alpha \lor \lnot \alpha) \vdash \lnot (\alpha \lor \lnot \alpha)$} \AxiomC{$\lnot (\alpha \lor \lnot \alpha), \alpha \vdash \lnot (\alpha \lor \lnot \alpha)$} \AxiomC{$\lnot (\alpha \lor \lnot \alpha), \alpha \vdash \alpha$} \UnaryInfC{$\lnot (\alpha \lor \lnot \alpha), \alpha \vdash \alpha \lor \lnot \alpha$} \BinaryInfC{$\lnot (\alpha \lor \lnot \alpha), \alpha \vdash \bot$} \UnaryInfC{$\lnot (\alpha \lor \lnot \alpha) \vdash \alpha \to \bot$} \UnaryInfC{$\lnot (\alpha \lor \lnot \alpha) \vdash \alpha \lor \lnot \alpha$} \BinaryInfC{$\lnot (\alpha \lor \lnot \alpha) \vdash \bot$} \UnaryInfC{$\vdash \lnot \lnot (\alpha \lor \lnot \alpha)$} \end{prooftree} \] This proof corresponds to the term \[ \lambda x^{\lnot (\alpha \lor \lnot \alpha)}. x\, \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. x\, \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right) \] Applying the \(\mathcal{C}\) operator gives us a term typed by LEM \[ \mathcal{C}\left(\lambda x^{\lnot (\alpha \lor \lnot \alpha)}. x\, \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. x\, \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right)\right) \] The typed execution of this term in a context \(E\) evaluated under the scope of a continuation variable \(k\) is: \[ \begin{aligned} &E\left[ \mathcal{C}\left( \lambda x^{\lnot (\alpha \lor \lnot \alpha)}. x \, \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left( \lambda y^{\alpha}. x \, \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right) \right) \right] \\ &\to_{t \mathcal{C}} \left(\lambda x^{\lnot (\alpha \lor \lnot \alpha)}. x \, \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. x \, \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right) \right) \left(\lambda z^{\alpha \lor \lnot \alpha}. \mathcal{A}^{\bot}(E[z]) \right) \\ &\to_{\beta_v} \left(\lambda z^{\alpha \lor \lnot \alpha}. \mathcal{A}^{\bot}(E[z])\right) \left(\mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. \left(\lambda z^{\alpha \lor \lnot \alpha}. \mathcal{A}^{\bot}(E[z]) \right) \left(\mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right)\right)\right) \\ &\Rightarrow_{\beta_v} \mathcal{A^\bot} \left(E \left[ \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. \mathcal{A}^\bot \left(E \left[\mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right]\right) \right) \right] \right) \\ &\to_{t \mathcal{A}} E \left[ \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left(\lambda y^{\alpha}. \mathcal{A}^\bot \left(E \left[\mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y)\right] \right) \right) \right] \end{aligned} \] As previously mentioned, I omit the \(\mathcal{C}(\lambda k^{\lnot \varphi}. \cdots)\) to avoid (even more) clutter. The resulting term produces the type \(\alpha \lor \lnot \alpha\) from the subterm \(\lambda y^{\alpha}. \mathcal{A}^\bot (\cdots)\) of type \(\lnot \alpha\). Importantly, a copy of the context \(E\) is inside the aborting \(\mathcal{A}\) operator. At both points, its hole contains a value of type \(\alpha \lor \lnot \alpha\).

The evaluation must now proceed through a different redex. Suppose the only way this term can appear in a redex is in a \(\mathsf{case}\) expression. Let’s fast-forward to this point, and abstract away the new context to \(E'\): \[ \begin{aligned} &E \left[ \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left( \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right) \right]\\ &\overset{*}{\to} E' \left[ \mathsf{case}\left( \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left( \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right), [x_\alpha]F_\alpha, [x_{\lnot \alpha}]F_{\lnot \alpha} \right) \right] \end{aligned} \] Semantically, \(\mathsf{case}(N^{\alpha \lor \beta}, [x_\alpha]F_\alpha, [x_\beta]F_\beta)\) is understood as passing the contents of \(N\) to the variable \(x_\alpha\) in \(F_\alpha\) or \(x_\beta\) in \(F_\beta\) based on its inner type. Hence, \[ \begin{aligned} &E' \left[ \mathsf{case}\left( \mathsf{inj}_2^{\alpha \lor \lnot \alpha} \left( \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right), [x_\alpha]F_\alpha, [x_{\lnot \alpha}]F_{\lnot \alpha} \right) \right] \\ &\to_{case} E'\left[ F_{\lnot \alpha}\left[ x_{\lnot \alpha} := \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right] \right] \end{aligned} \] Evaluation now proceeds at a different redex. Again, for our term to appear in one, it will need a value (say \(V^\alpha\)) of type \(\alpha\). Let’s suppose this happens under the context \(E_{F_{\lnot \alpha}}\). This causes the following cascade: \[ \begin{aligned} &E'\left[ F_{\lnot \alpha}\left[ x_{\lnot \alpha} := \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right] \right]\\ &\overset{*}{\to} E_{F_{\lnot \alpha}}\left[ \left( \lambda y^{\alpha}. \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(y) \right] \right) \right) V^\alpha \right]\\ &\to_{\beta_v} E_{F_{\lnot \alpha}}\left[ \mathcal{A}^\bot \left( E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(V^\alpha) \right] \right) \right]\\ &\to_{t \mathcal{A}} E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(V^\alpha) \right] \end{aligned} \] Remarkably, this final context jump transports us back to the original context \(E\) with one key difference: its hole is constructed from a value of type \(\alpha\)! Remember, this value was generated after the initial evaluation of the \(\mathsf{case}\) expression. The context \(E\) had proceeded under the assumption that it had a term that could produce \(\bot\) from \(\alpha\) and generated \(V^\alpha\) accordingly. This is akin to the bag containing a billion dollars that the man earns (steals?) for the devil. After receiving the value, the execution jumps to the copy of the initial context \(E\) surrounding an abstraction of this value. This jump indicates that the Devil, now a billion dollars richer, “turns back the clock” to the point where his offer was made. This is the detail Martens adds to the tale.

All this causes a different behaviour at the (eventual) \(\mathsf{case}\) expression: \[ \begin{aligned} &E \left[ \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(V^\alpha) \right]\\ &\overset{*}{\to} E' \left[ \mathsf{case}\left( \mathsf{inj}_1^{\alpha \lor \lnot \alpha}(V^\alpha), [x_\alpha]F_\alpha, [x_{\lnot \alpha}]F_{\lnot \alpha} \right) \right] \\ &\to_{case} E'[F_\alpha[x_\alpha := V^\alpha]] \end{aligned} \] This produces what very well might be the final term.

Issues

The earlier section assumes that a \(\mathsf{case}\) expression is the only way to interact with a value of type \(\alpha \lor \beta\). However, [Grif89] doesn’t provide a separate syntax for disjunctive types. Instead, they’re coded into the language using implication and negation: \[ \alpha \lor \beta \triangleq \lnot \alpha \to \lnot \lnot \beta \] To simulate \(\lor\)-elimination in this encoding, a \(\mathcal{C}\) expression is required. This is because the encoding is only classically correct; \(\alpha \vdash \gamma\) and \(\beta \vdash \gamma\) does not constructively imply \(\lnot \alpha \to \lnot \lnot \beta \vdash \gamma\).

The \(\mathsf{case}\) expression corresponds to this \(\lor\)-elimination. For the Call-by-Name variant, it’s defined as: \[ \mathsf{case}^\delta (M, F_1, F_2) \triangleq \mathcal{C}(\lambda j^\delta. M (\lambda x. j(F_1 x)) (\lambda x. j(F_2 x))) \] The expression simulating \(\mathsf{case}\) in Call-by-Value is more complicated, and its presentation isn’t necessary.

All this gives the impression that a \(\mathsf{case}\) expression isn’t the only way to use a term of a disjunctive type. One could supply a value of type \(\lnot \alpha\) to it and get a value of type \(\lnot \lnot \beta\) in return.

Unfortunately, I can’t counter this objection with a technical argument. One possible approach would involve extending the syntax of Idealized Scheme with separate injection, pairing and case categories that play nice with the existing encoding schemes. Perhaps the Dual Calculus detailed in [Wadl03] achieves this.

I’ll only say this: \(\lnot \alpha \to \lnot \lnot \beta\) is provably not a disjunctive type without the applicability of the \(\mathsf{case}\) expression. In a sense, it’s the application of a \(\mathsf{case}\) that makes it a disjunctive type. Without it, the conclusions we can arrive at wouldn’t necessarily only hold for these types.

Explaining the tales

The devil’s actions were mostly explained in the previous section. To repeat, the devil, being (probably) omnipotent, has the ability to alter the state of the world at will. Martens gives the devil the simple power to turn back time. To faithfully simulate \(\mathcal{C}\) and \(\mathcal{A}\), I grant the devil these greater powers. The devil remembers the state of the world when he makes his offer to the man. Once the man gives him the billion dollars, he reverts the state of the world to the remembered state, and makes his offer again. This time, he chooses (a). Whether the man remembers his misdeeds is up-to the devil.

The shepherd’s tale is less satisfying. His only way out is the approach suggested in [SøUr06]. To pull off this sleight-of-hand, he needs to acquire the philosopher’s stone from the king. Being the crafty man he is, he produces a list of instructions to be followed by the King’s trusted knights. He then informs the king that those instructions would provide the king with what he wants when augmented with the entire sequence of actions the king wishes to perform on what he wants. When the king hesitates, he points out that the instructions would be carried out by his trusted knights: men incapable of disloyalty.

Now convinced, the king begins preparing his instructions. Naturally, he must account for both possibilities: the shepherd creating a machine, or producing the stone. Therefore, his instructions would be something like:

private KING_STONE;

switch (shepherd_output.type) {
    case STONE:
        printf("It's the stone!");
        return shepherd_output.stone;

    case MACHINE:
        printf("It's a machine. Inputting stone...\n");
        if (shepherd_output.run(KING_STONE) != GOLD) {
            kill_shepherd();
        }
}

After receiving the augmented set of instructions, the knights begin their work. First, they duplicate the king’s instructions and embed the copy inside the shepherd’s list of instructions. Next, the shepherd requires the knights to execute the king’s instructions as though he had produced a machine that would convert the philosopher’s stone to gold. To do this, they retrieve the philosopher’s stone from the king’s quarters. The next step requires them to embed the stone into the list of instructions.

At this point, the knights encounter the copy of the king’s instructions. They are told to forget everything they’ve done so far and execute the king’s instructions with the stone they find (which they placed!) inside. If outputs could be logged in medieval Europe, they would say:

It's a machine. Inputting stone...
It's the stone!

Thus, the knights return to the king with the philosopher’s stone. The king, now satisfied, spares the shepherd.

References