[TYPES] [tag] Re: Declarative vs imperative

[Guillaume Munch-Maccagnoni]

Kalani Thielen wrote :
> But I'm not sure that I've got a straight story on this interpretation
> of negation, quite.  I think that it's suggesting that the size of the
> set of continuations A->_|_ is |_|_|^|A|, or 0^|A|, which should be 0,
> right?  So there are 0 continuations -- they're impossible to
> construct?

Dear Kalani,


The cardinal of A->empty is 0 only in the case |A| is non-empty.
Otherwise, there is exactly 1 function. Therefore, by interpreting
continuations as you do with sets, you do obtain an interpretation of
classical logic, however with boolean truth values, and no structure of
proofs.

Continuations are not interpreted as arrows A->_|_ but as A->R for some
chosen R. To witness the difference, let me take a proof of a Sigma^0_1
formula P (roughly speaking, a datatype containing no arrow type).

Through the appropriate translation, this gives an intuitionistic proof
of (P->R)->R with R not appearing in P. Now I may choose R=P and deduce
an intuitionistic proof of P by applying to \x.x.

>From the computational perspective, this corresponds to the fact that
the reduction of a program containing control operators is only defined
with respect to an initial context (here the empty context corresponding
to \x.x).

(Your question is relevant. There have been many arguments against the
possibility of a model of classical logic that discriminates proofs, and
they can be reduced to a generalization of your remark: there is at most
one arrow A->_|_ in any model of intuitionistic logic that has an
initial object (a bottom). However, this only indicates that in
intuitionistic logic, negation and falsity are not obvious to define.)


With this explanation in mind I wish to go back to the following
message:

Uday S Reddy wrote :
> Coming to classical logic per se, I believe it is ill-fit for describing
> computer programs or "processes" as you call them.  First of all, classical
> logic doesn't have any well-developed notion of time or dynamics, and it has
> a nasty existential quantifier which assumes that all things exist once and
> for all.  In computer systems, new things come into being all the time, well
> beyond the time of the original development or deployment.  We know how to
> write computer programs that deal with that.  Classical logic doesn't.  (LEJ
> Brouwer made this criticism a long time ago in the context of mathematics.
> There it might have been just a philosophical problem.  But in Computer
> Science, it is a *practical* problem.)
> 
> <ranting about logicians elided>
> 
> - Girard has formulated Linear Logic, which broadens our idea of what kind
> of "things" a logic can talk about.  David Pym and Peter O'Hearn invented
> Bunched Implication Logic, extending Linear Logic with a beautiful
> model-theoretic basis.  These logics applied to imperative programming
> (which go by the name of "Separation Logic") are revolutionizing the
> development of technology for imperative programs.
> 
> It is time to leave behind the classical logic.  In fact, we should have
> done it a long time ago.

Yet Girard, which Uday mention, and others, have theorized how classical
logic can be given a nice notion of "dynamics", all the while being as
strong as intuitionistic logic in terms of constructiveness over certain
formulae.

In the example above, a classical proof of P yields an intuitionistic
one. There are restrictions on the shape of P (a datatype containing no
arrow), but not on the theorems used to prove P. So we may argue that
the constructive contents were already in the classical proofs involved.

Constructiveness is of course relaxed compared to intuitionistic logic.
We may use a direct analogy with programming languages that are not
purely functional, but allow effects. Functional types are opaque,
because it makes no sense to retrieve the source code of a function
created at runtime, in the presence of call/cc, storage, I/O, etc. This
does not make such programming languages non-constructive or lacking
dynamics: the thing still computes values.

This makes a nice refinement (along with other examples Uday mentions)
of the intuitionist's take on constructiveness, which showed, more than
twenty years ago already, that a computational interpretation of logic
may give up referential transparency in favor of interactivity with the
context/opponent.

(On a side note, I know "logicians of philosophical inclination" that
are very well aware of such developments regarding the issue of
constructiveness.)


Sergei SOLOVIEV wrote :
> 
> To add a bit in support to Uday's remark about "presumption of 
> supremacy" of classical logic:
> 
> In fact, it is well known that classical logic can be embedded in 
> intuitionistic logic
> using, for example, negative interpretation (classical "exists" becomes 
> \not\forall\not etc.)
>  From the point of view of provability, the interpretation of a 
> classical theorem is provable
> intuitionistically if and only if the original theorem was provable 
> classically.
> So, what is bad rationally, if instead of respectable "exists" we shall 
> say "it is
> not true that for all x does not exist..."? It is clear, that it is a 
> "bad publicity",
> a less "convincing" way to say - bad for "supremacy", but it has nothing 
> to do
> with scientific rationality itself. (Constructive mathematics is just 
> more subtle
> concerning existence.)
> 

I do not exactly understand the claim here. However, the particular
translation used in my example is already "more subtle concerning
existence" than the one sketched by Serguei. Moreover, negative
interpretation does not reduce the problem of understanding the
constructive contents of classical logic to the one of understanding
intuitionistic logic, because problems are converted modulo some
translation which is not compositional on proofs. Thus the issue becomes
to understand the translations as much as it is to understand
intuitionistic logic.

Serguei's remark is against "presumption of supremacy" of classical
logic, but it should not be seen as the other extreme: redundancy of
classical logic with respect to intuitionistic logic. (It seemed to me
that so far, the discussion were indeed in favour of plurality in
logic.)


Best regards,
-- 
Guillaume Munch-Maccagnoni <Guillaume.Munch at pps.univ-paris-diderot.fr>