[TYPES] [tag] Re: Declarative vs imperative

[Uday S Reddy]

Tadeusz Litak writes:

>  >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.

Dear Tadeusz, thanks for your input.  When I visited your new home page this
morning, I was greeted with a quote from Richard Feynman to the effect: 

  "a scientist speaking about a non-scientific subject is just as dumb as
   the next guy."

which was a good warning to me.  So, I won't stray too far into the
philosophy of logic.

I am happy to labelled a logical pluralist.  If anything, my position is
probably even broader than the pluralists.  As Beall and Restall clarify in
Section 7 of their article:

  http://homepages.uconn.edu/~jcb02005/papers/defplur.pdf 

their pluralism is the "one-many answer", which I already find too
restrictive.  My view is that logic is a piece of "technology" that we
employ for specific purposes.  Thare are many purposes.  So there will be
many pieces of technology.  There is no "one true logic".

As I said in my earlier response to Mark Janssen, I take logic to be the
study of "information content" of statements.  Since we do not yet have a
good idea of what that means precisely, I take logical consequence to be a
working definition, but I also believe it will need to be supplanted
eventually with a definition based on "information content".  Pholosophy of
information has been taking large leaps in recent years.  See this handbook
for example:

  http://www.amazon.com/Philosophy-Information-Handbook-Science/dp/044451726X

Computer scientists are very much part of this enterprise because logic is
but our sister discipline in studying "information".

---

Let me steer the discussion in a different direction.  While we are paying a
tribute to John Reynolds's life long work on "logical foundations of
programming", we should take a look at Reynolds's Specification Logic [1,2].
This is a typed "first-order intuitionistic theory" in Tennent's
description, where the intuitionistic part goes to account for the dynamic
nature of Algol programs.  As and when you allocate new variables, you
extend the "world", and intuitionistic logic is quite comfortable dealing
with such dynamics.

At the same time, Specification Logic has a base type called "assert" for
state assertions.  Hoare-triple specifications

      {P} C {Q}

are atomic formulas in specification logic.  Write them as Spec(P, C, Q) if
you wish, with the typing Spec : assert x comm x assert -> o.  Now, the
assertions are formulas in a subsidiary logic, which is *classical*.  Since
individual states do not have any dynamics, classical logic works fine for
those.

While this setting of an outer logic in one formalism (intuitionistic logic)
and an inner logic in a second formalism (classical logic) seems very
natural to those of studying Algol-like languages, most others find their
heads reeling with such a structure.  To make them feel a bit more
comfortable, I tell them that they should think of it as really being a
"higher-order" logic.  But, it is not a true higher-order logic, where there
would be functions of type o -> o, say, which act on propositions in the
outer logic.  Instead, we have here a second type of propositions, 'assert',
which has a different meaning, and a different notion of consequence.

Now, my question is, are there other logics of this kind anywhere?  

Cheers,
Uday


[1] Reynolds, J. C., Idealized Algol and its Specification Logic, in D. Neel
(ed) Tools and Notions of Program Construction, p. 121-161, Cambridge
U. Press, 1982.  Also in P.W. O'Hearn and R.D. Tennent (eds) Algol-like
Languages, Vol. 1, p. 125-156, Birkhauser, 1997.

[2] Tennent, R. D., Denotational semantics, in S. Abramsky, D.M. Gabbay,
T.S.E. Maibaum (eds) Handbook of Logic in Computer Science Vol. 3,
p. 169-322, Oxford University Press, 1994.