Γ ⊢ Δ, A Γ, A ⊢ Δ

———————————————————————

Γ ⊢ Δ

The rule gives a derivation of Γ ⊢ Δ from derivations of weaker sequents, using A as an intermediary. Gentzen proved that the cut rule is unnecessary, i.e. that it is always possible to obtain a direct derivation of Γ ⊢ Δ without going through the middle-man. However it turned out that this process of cut-elimination was of extreme interest.

In "Locus Solum", Girard tells us to focus our attention on the following instance of cut:

In words: "From a proof of A and a refutation of A, derive contradiction." But isn't that a vacuous instance of cut? Logic is supposed to be consistent, so how could we ever have both a proof and a refutation of the same proposition? Well, Girard's solution is to add a single rule, the daimon, that can conclude anything from no premises:

Since the logic becomes inconsistent, it is now entirely possible to have both a proof and a refutation of the same proposition. But isn't that...crazy? Perhaps Girard inhaled a bit too much mustard before coming up with this stuff?

But actually, if we think of cut-elimination in terms of the Curry-Howard correspondence, the daimon makes a good deal of sense. A proof of A corresponds to a value of type A (in the ordinary programming languages sense), while a refutation of A corresponds to a continuation accepting type A. (Strictly speaking, in Ludics proofs don't correspond to values in the ordinary sense, but for now we can ignore the difference.) Now, what can a continuation K do with a value V:A? Well, V might itself contain suspended continuations, and K could call any of those with some values. But another possibility is that K simply terminates the computation. And that's when it calls the daimon. In other words, daimon is just French for "done". Thus when Girard defines a proof and a refutation to be orthogonal when their cut normalizes to the daimon, this is another way of saying that we can throw a value to a continuation and get a terminating result (notation: V⊥K).

So what does this have to do with topology? For any type A, let's collect all of its values into a set X

Let's try to see how this works for the type of booleans, with set of values X

The top recipe ([t|f ↦ done]) describes a continuation which, given either t or f, simply returns. The next recipe on the left ([t ↦ done]) describes a continuation which returns on t, but whose behavior is unspecified (and thus possibly non-terminating) on f. Similarly with [f ↦ done]. Finally, [] is the boolean continuation with totally unspecified behavior. It is easy to see the basic open set corresponding to each continuation:

In "Locus Solum", Girard tells us to focus our attention on the following instance of cut:

⊢ A A ⊢

——————————————

⊢

——————

Γ ⊢ Δ

But actually, if we think of cut-elimination in terms of the Curry-Howard correspondence, the daimon makes a good deal of sense. A proof of A corresponds to a value of type A (in the ordinary programming languages sense), while a refutation of A corresponds to a continuation accepting type A. (Strictly speaking, in Ludics proofs don't correspond to values in the ordinary sense, but for now we can ignore the difference.) Now, what can a continuation K do with a value V:A? Well, V might itself contain suspended continuations, and K could call any of those with some values. But another possibility is that K simply terminates the computation. And that's when it calls the daimon. In other words, daimon is just French for "done". Thus when Girard defines a proof and a refutation to be orthogonal when their cut normalizes to the daimon, this is another way of saying that we can throw a value to a continuation and get a terminating result (notation: V⊥K).

So what does this have to do with topology? For any type A, let's collect all of its values into a set X

_{A}= {V | V:A}. Now, let K be any A-accepting continuation. We can use K to pick out a subset of X_{A}, namely the set of values on which K terminates. That is, we build the set K^{⊥}= {V:A | V⊥K}. And then we define a topology Ω_{A }on X_{A}, generated by all of the basic open sets K^{⊥}.Let's try to see how this works for the type of booleans, with set of values X

_{2}= {t, f}. We can describe any boolean continuation as essentially fitting one of the following four recipes:[t|f ↦ done]

[t ↦ done] [f ↦ done]

[]

[t ↦ done] [f ↦ done]

[]

The top recipe ([t|f ↦ done]) describes a continuation which, given either t or f, simply returns. The next recipe on the left ([t ↦ done]) describes a continuation which returns on t, but whose behavior is unspecified (and thus possibly non-terminating) on f. Similarly with [f ↦ done]. Finally, [] is the boolean continuation with totally unspecified behavior. It is easy to see the basic open set corresponding to each continuation:

{t,f}

{t} {f}

{}

And so Ω

Fact: Ω

Expanding the definition of Ω

Fact: Ω

Counter-example: Consider Ω

The top continuation simply ignores its argument and returns. The next two call k with a single boolean, either t or f. The continuation on the third line calls k with both t and f. And finally, the behavior of the continuation [] is, again, unspecified. Now let us use the shorthand {t,f}, {t}, {f}, {}, to refer to the four previously-defined boolean continuations in the evident way. Then the above ¬2-continuations generate the following basic open sets:

con([t|f ↦ done]) is also acceptable; the former supplies a continuation guaranteed to terminate only on t, the latter one that that will terminate on any boolean. It might also be worth noting that the two values con([t ↦ done])and con([f ↦ done]) are separable, but not by open neighborhoods.

Okay! Hopefully that's a reasonable sketch of the basics of the topological interpretation in Ludics. Stay tuned for more...

{t} {f}

{}

And so Ω

_{2}is simply the discrete topology. In general, though, the topology Ω

_{A}will be more complicated.

Fact: Ω

_{A}is T

_{0}.

Expanding the definition of Ω

_{A}and of the separation axiom, this means that for any two "syntactically distinct" values of type A (omitting the precise definition), there is some continuation which terminates on one but not the other. Or in programming language terminology, T

_{0}says that syntactic inequality implies contextual inequivalence.

Fact: Ω

_{A}is not always T

_{1}.

Counter-example: Consider Ω

_{¬2}, the topology on boolean continuations treated as values. We treat a continuation as a value by wrapping it in con, so for example con([t ↦ done]) is a value of type ¬2. Now, we can again summarize the behavior of any ¬2-continuation, this time with five possibilities:

[con(k) ↦ done]

[con(k) ↦ k(t)] [con(k) ↦ k(f)]

[con(k) ↦ k(t)∥k(f)]

[]

[con(k) ↦ k(t)] [con(k) ↦ k(f)]

[con(k) ↦ k(t)∥k(f)]

[]

The top continuation simply ignores its argument and returns. The next two call k with a single boolean, either t or f. The continuation on the third line calls k with both t and f. And finally, the behavior of the continuation [] is, again, unspecified. Now let us use the shorthand {t,f}, {t}, {f}, {}, to refer to the four previously-defined boolean continuations in the evident way. Then the above ¬2-continuations generate the following basic open sets:

{{t,f},{t},{f},{}}

{{t,f},{t}} {{t,f},{f}}

{{t,f}}

{}

Then, for example, {t} and {t,f} cannot be separated, since the latter is in every open set containing the former. Another way of putting this is that any context in which the value con([t ↦ done]) is acceptable, the value{{t,f},{t}} {{t,f},{f}}

{{t,f}}

{}

con([t|f ↦ done]) is also acceptable; the former supplies a continuation guaranteed to terminate only on t, the latter one that that will terminate on any boolean. It might also be worth noting that the two values con([t ↦ done])and con([f ↦ done]) are separable, but not by open neighborhoods.

Okay! Hopefully that's a reasonable sketch of the basics of the topological interpretation in Ludics. Stay tuned for more...

_{ }_{ }_{ }