[TYPES] [tag] Re: Declarative vs imperative

Fri May 3 09:09:13 EDT 2013

On 04/26/2013 11:44 PM, Uday S Reddy wrote:
> Marc Denecker writes:
> 
>> There is no inherent form of inference to such a logic. Therefore,
>> theories in such a logic are not representations of problems.
>>
>> However, the information in a theory can be used to solve
>> computational problems or perform tasks, by applying suitable forms of
>> inference. ...<snip>
>>
>> It also means that C, C++, Java programs,... decaratively describe
>> something: namely these computer processes. In this respect, these
>> languages can be seen as process logics. So, for me  C is indeed a
>> declarative logic.
>>
>> However, it is obviously a very different logic than say classical
>> logic. One aspect is related to "universality": C++ can only describe a
>> very restricted class of (computer executable) processes. Classical
>> logic can be used (although not so conveniently)
>> to describe such processes as well (e.g., using some
>> methodology for temperal knowledge representation such as situation or
>> event calculus).
>>
>> Another difference is that C++, seen as a declarative process logic,
>> is (currently) associated with a unique form of inference:  "execution
>> inference" of the computer process.
> 
> Thank you for your long and thoughtful post.  I am in agreement with much of
> what you say.  But some key points of difference remain.
> 
> First of all, there is no law that says that declarative languages need to
> be executable.  However there is a law to the effect that programming
> languages need to have a declarative reading.  That is so that we can reason
> about the programs written in them.  ("Declarative" and "procedural" were
> the terms coined in the logic programming community.  The corresponding
> terms in programming language community are "denotational semantics" and
> "operational semantics".)
> 
> The attractiveness of logic programming, when it was first launched, was that
> it had a ready-made declarative reading, which was expected to make a big
> difference for programming.  Unfortunately, Prolog also had a bad procedural
> reading that people struggled with.  So, in practice, Prolog programmers
> spent almost all of their effort on the procedural meaning, and the
> declarative meaning went out of the window.  In the end, Prolog was a good
> dream, but a bad reality.
> 
> 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.)
> 
> I believe logicians of philosophical inclination are prone to be enamored
> with what they have and lose sight of what they don't have.  For a good part
> of two millennia, they kept debating Aristotilean syllogisms, without
> realizing that classical logic was yet to be discovered.  Finally, it was
> left to the mathematicians to formulate classical logic.  The logicians of
> today are similarly enamored with classical logic without much of an
> understanding of what it lacks.  We would be ill-advised to listen to them.
> Or, we would be stuck for another two millennia, God forbid.
> 
> [By the way, the Wikipedia page on Classical Logic is in a pitiful state.  I
> hope somebody will pay attention to it.]
> 
> Brilliant new things are happening in Logic.  
> 
> - Mathematicians have formulated Toposes (a generalization of Kripke
> models), which give us a great new variety of models for intuitionistic
> logic.  There are deep mathematical facts buried in them and continue to be
> discovered.  Toposes and intuitionistic logic are appropriate for modeling
> computer programs, which live in a growing dynamic world rather than a
> static one.
> 
> - 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.
> 
> Cheers,
> Uday
> 

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

To me, that sounds like a total and unconditional rejection.

You mention "(classical logic) is ill-fit for describing computer
programs or processes" and your references to scientific progress are
all in the context of  modelling (the executions of) computer programs
("processes").  I am not an expert in logics for modelling programs and
processes, and it was not my intention with my previous email nor with
this one  to defend classical logic for this purpose.

But there are plenty of applications of logic outside modelling computer
programs.

I certainly have reservations about FO. I would agree that FO's syntax
need to be improved, that FO is not expressive enough and  needs to be
extended.  For example, I think you have a good point that classical
logic's existential quantifier is not well suited for expressing
"dynamic creation" of objects, and that such an operator might somehow
be added.

However, I would not throw away the standard
existential quantifier; in many applications it is
exactly the one that we need. In my opinion, that is the case with all
the connectives and quantifiers of FO (\land,\lor,\neg,\forall,\exists):
they are all fundamentally important information composition operators
and their semantics in FO is essentially correct.

If your rejection is as total as it sounded, you will disagree with
that. Let me give you a potential argument for your case, which would
really pull me over to your side.

Consider the following  information.

A	if in a semester no student registered for a course, then
	this course does not take place in that semester.

In class we represent it in FO as:

B	! c ! s : Semester(s) & Course(c) & ~ ? st: Registered(st,c,s)
		   => ~ TakesPlace(x,s)

or as

B'	! c ! s : Semester(s) & Course(c) & TakesPlace(x,s)
		   =>  ? st: Registered(st,c,s)

(! is shorthand for forall, ? for exists, ~ for not)

I point my students to the precision of B and B' as representations of
A, and to the correctness of B's FO connectives and quantifiers  to
capture exactly the information that was to be expressed. The example is
one of a dime a dozen. I argue to them that standard conjunction,
disjunction, (objective) negation, universal
and existential quantifiers are fundamentally important information
composition operators and their FO model semantics is the
right one. We see computational applications of such sentences using our
KBS system as a didactic tool, for querying in the context of a
database,  for searching course plannings in the context of scheduling,
and for some other sorts of applications. Note that the sentence
contains the existential quantifier. But I think it is a clear case
where the standard FO existential quantifier is appropriate, and not
your "dynamic creation" one.

If my strong claims above are
right, then  I would argue that FO is indeed a base language (in the
sense that \land, \lor, \neg, \forall, \exists are base composition
operators, and FO's semantics for them is correct!).

On the other hand,  here is a very convincing way to show me that I am
wrong: it suffices to show me ONE database in which the informal
proposition A is true and the formal sentence B is false or vice versa.

Best wishes,

Marc

-- 

   Marc Denecker (prof)
   KU Leuven   			
   Departement Computerwetenschappen    tel: ++32 (0)16/32.75.57
   Celestijnenlaan 200A Room A02.145    fax: ++32 (0)16/32.79.96
   B-3001 Heverlee, Belgium
   email: Marc.Denecker at cs.kuleuven.be
   http://people.cs.kuleuven.be/~marc.denecker/
 ........................................................................

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm