Claus Reinke writes:
[nice exposition of C-H correspondence & state threads]
> The main caveat is the insistence on constructive proofs (in the classical
> logic most of us tend to learn, there is this favourite proof technique: if
> I assume that xs don't exist, I am led to a contradiction, so xs have to
> exist, even if I haven't seen any of them yet - this is not acceptable in
> constructive logics).
>
> [haven't read the papers on a correspondence for classical logic yet, but
> I assume they exist, for otherwise I would contradict Frank Atanassow ;-]
Here's a nice example, which you alluded to. Reading | as `or' and ~ as
`not', a|~a is a theorem of classical logic but not intuitionistic logic. By
definition, ~a = a->_|_ (falsum). A proof of this proposition is given by the
term
/\ a -> \\(m::a|n::a->Void) -> [n] (\x -> [m] x) -- /\ is big-lambda
"[m] t" and "\\m::a -> t" are new term forms. They throw and catch
continuations, where a continuation accepting values of type a is something of
type a -> Void. Void is the empty type, so this means that a continuation is a
something like a function which never returns.
"[m] t" takes a term t :: a, and yields a term of type Void with a fresh free
variable m :: a->Void. You can think of [m] t as meaning, "throw value t at
continuation m". When this gets reduced, the current context is discarded and
execution proceeds from m, with t as input.
"\\" is usually written with Greek letter `mu'. In "\\m::a -> t", the term t
must be of type Void and possess a free variable m :: a->Void; the result is a
term of type a, in which m is now bound. You can think of "\\m::a -> t" as
meaning, "catch a value v thrown to continuation m and return v as the
result". Note that since t has type Void, it must always throw something and
can never return normally. (In case of conflicts, which value gets caught
depends of course on the reduction order.)
"\\(m::a|n::b) -> t" is a pattern-matching variation on the mu-binder. t is
again of type Void, but the result is of type a|b. The meaning is that it
catches values thrown to either continuation, injects it into the sum, and
then returns it. (There is also variant "[m|n] t" of the "[m] t" syntax, but
we don't need it.)
So what does our term
/\a -> \\(m::a|n::a->Void) -> [n] (\x -> [m] x)
mean? Well, when it gets reduced, it remembers its calling context and
associates it with m and n. Then it initially returns (by throwing it at n) to
that context the closure (\x->[m]x)::a->Void which gets injected into the
right summand. Execution proceeds, and if at any point this closure ever gets
applied to some value v, then the original context is magically restored, but
this time with v injected into the left summand. So this is an example of the
time-travelling effect you get with multiply-invoked continuations (because we
can consider that there is only one continuation of type a|a->Void.)
Incidentally, the reason you need a special form for continuation
"application" is that I glossed over a technical detail concerning whether to
take ~a or a->Void as primitive. At least in the lambda-mu calculus, you're
not allowed, actually, to write "f x" if f::A->Void for any A; you have to use
"[f] x". I forget the details.
--
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
