[TYPES] [tag] Re: Declarative vs imperative

[Tadeusz Litak]

If I may chime in. The original point made by Uday re classical logic:

 >Coming to classical logic per se, I believe it is ill-fit for describing
computer programs or "processes"

is certainly worthy of attention. But it does not seem to imply the conclusion of that mail:

 >It is time to leave behind the classical logic.  In fact, we should have
done it a long time ago.

(even if it wasn't intended, it does indeed sound "like a total and unconditional rejection"... such things happen in 
the fervor of a discussion :-)

"Logical pluralism" is a position rather well-established in the philosophy of logic. I would think that in the context 
of Computer Science, it is even more tempting.

[incidentally and perhaps contrary to established views, even Brouwer himself could be perhaps seen as one of first 
logical pluralists. While he very strongly rejected Fregean-Russellian logicism in *foundations of mathematics*, he has 
always held the work of Boole and the whole algebraic tradition in logic in high regard... But this is an aside]

It might even happen to be Uday's own position, if I understand correctly the remark that "we can perfectly well 
circumscribe various regimens for various purposes." Most of my email will elaborate on this.


  I would simply  say that whenever one wants, needs or has to think of all propositional formulas (also those possibly 
involving implication, and also those involving fusion, "tensor product" or what have you) as *rewritable to a 
conjunctive-disjunctive normal form without loss of information*, then the underlying domain logic is essentially classical.

It is hard to imagine whole areas of Theoretical CS if rewriting formulas to CNF or proofs by 
contradiction/contraposition/excluded middle are suddenly deemed outdated and/or illegal... I mean not only and not even 
primarily logic programming, but also finite model theory, complexity theory, ontologies/description  logics or the 
whole PODS/VLDB community...

[actually, as a curious aside, the logic of database theorists, while certainly not constructive, is not fully classical 
either. They dread the top constant and unrestricted negation, preferring instead relative complement. This has to do 
with assumptions such as "closed world", "active domain" and the demand that queries are "domain independent". In short, 
their logic is rather that of Boolean rings without identity, which---funnily enough---also happen to be the setting of 
Stone's original work. It is just contemporary and ahistorical misrepresentation to say that Stone was working with 
"Boolean algebras". But this, again, is an aside...]

And even in the context of Curry-Howard correspondence, classical logic is a legitimate setting to discuss languages 
with control operators, first-class continuations, static catch/throw a la Scheme etc. There is so much stunningly 
beautiful work in that community that deserves to be better known...


But, equally obviously, not all the programming languages have such constructs. Furthermore, as linear logicians 
(already mentioned by Uday) will be happy to tell you, there are contexts when even intuitionistic notion of implication 
(so also the one of topos-theorists or proof-assistants, for example) is way too coarse-grained. Particularly when one 
wants, needs or has to be resource-aware. Also, the recent work of Wadler, Pfenning and other authors suggests that 
Curry-Howard correspondence for concurrency will have to do with linear rather than intuitionistic logic.


[And as substructural logicians will be happy to tell you, there are contexts where even linear logicians may seem 
coarse-grained, thick-skinned,   corner-cutting brutes. :-) But this, yet again, is an aside.]

But where I most likely would part ways with Uday is when he claims (if I understand correctly) that we are approaching 
or even should approach "a final answer" of any kind. To me,  searching for one logic valid in all CS-relevant contexts 
seems a rather misguided enterprise. Especially or at least when we talk about logic understood as a formal inference 
system.

What we perhaps need is more introductory logic courses---and also handbooks and monographs---for budding CS 
undergraduates and graduates (and perhaps also some postgraduates) which would make them understand the subtlety and 
complexity of the picture. And the benefits and costs of adopting specific inference rules.

Proof-assistant based courses seem to go in just the right direction. I am teaching right now one based on that 
excellent "Software Foundations" material of Benjamin Pierce et al. I think it changes and sharpens not only the 
thinking of students, but also that of the teacher himself (or herself :-).

But even this only goes so far---after all, the underlying logic is essentially intuitionistic... on the other hand, any 
weaker one could quickly become a nightmare for actually discussing things as demanding as semantics of programming 
languages (with bangs and exclamation marks in every second lemma... :-)


To conclude, a few minor points:


 > In fact, we cannot accept that we have a final answer until the entire natural language has been formalized

We'll wait for this only a little longer than for the  invention of perpetuum mobile and heat death of the universe... :-)

And which "natural language" are we talking about? Sometimes I think the only reason why, e.g., Chomsky ever came up 
with the idea of  "universal grammar" was that he did not speak too many languages in the first place (although Hebrew 
seems reasonably distant from English)...


 > (The view I take, following Quine, is that logic is a regimentation of natural language.

Same objection as above, and this is just to begin with.

[The only redeeming features of Quine were that he wrote well and had a certain logical culture. As a philosopher, in my 
opinion, he had a rather destructive influence on development of logic, particularly in philosophy departments, even if 
nowhere near as disastrous as the neopositivists or the majority of "analytic philosophers". But this is just one more 
aside...]


 > We can perfectly well circumscribe various regimens for various purposes.

As said above, I'm perfectly in agreement with this statement.



 >  I am entirely happy with the characterization of logical connectives as "information composition" operators. But we 
can only accept it as a good, but vague, intuition. We do not know what this "information" is. Neither do we know what 
the information is about. So, in order to claim that classical logic is a canonical information composition calculus, 
somebody would need to formalize those notions.


I think I can agree with every word here. Perhaps the difference then is not so big...

I guess then that "leaving classical logic behind" meant rather "stop presenting it to students as the only, final and 
 >>real<< formalism for Computer Scientists, everything else being a marginal pathology, if mentioned at all"... and if 
this was indeed intended by this remark, I would have a hard time disagreeing.

Okay... back then to popcorn and a comfortable seat in the audience...

Best,
t.