[TYPES] Declarative vs imperative

[Uday S Reddy]

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