A topology of cut-elimination

One of the central ideas of Ludics is an orthogonality relationship between proofs and refutations, which says, essentially, that they can be "successfully" cut against each other. Recall that Gentzen's cut rule is a method of composing derivations:

Γ ⊢ Δ, 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:

 ⊢ A      A ⊢
——————————————
⊢ 

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_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₂ = {t, f}. We can describe any boolean continuation as essentially fitting one of the following four recipes:

[t|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 Ω₂ is simply the discrete topology. In general, though, the topology Ω_A will be more complicated.

Fact: Ω_A is T₀.

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₀ says that syntactic inequality implies contextual inequivalence.

Fact: Ω_A is not always T₁.
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)]

[]

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
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...