gmane.comp.science.types

Re: [TYPES] [tag] Re: Declarative vs imperative

Marc Denecker — 2013-05-13T10:35:33

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


On 05/03/2013 11:22 PM, Uday S Reddy wrote:
fact, we
language

We then agree on this point. This view goes back to Frege and
even to  Leibniz, right?

But do we agree that the standard logical connectives of FO correctly
implement an important set of  basic information composition operators.
That is, conjunction, disjunction, negation, the quantifiers?

If that is the case  then FO's connectives
will have to be in other languages as well?  We agree that these
operators are not enough but  the  more universal languages that the
scientific community should strive for in your and my opinion,  will
have to contain FO's information composition operators (modulo syntactic
sugar) and hence be extensions of classical logic?

I'm confused about your position in this right now. On the one hand, you
do not (unconditionally) reject FO ; on the other hand, in your reaction
on my first email. you seemed to react against the fact that  I propose
FO as a base language. If you agree that FO's connectives correctly
implement a set of  basic information composition operators, then you
should agree with me on that claim. But if you think FO's connectives
are not correct or not basic, then please consider the challenge in my
previous email (or see below)



I'm sure Tarski would disagree with you. I think this would be his answer.

The notion of "information" that you claim is vague, is actually
formalized in model semantics in a very precise way, albeit slightly
implicitly.

The information content of a logic expression/theory T is formalized by
the class of its models (i.e., the structures in which T is true).
Models are formal representations of possible states of affairs,
non-models are formal representations of impossible states of affairs.
This set is characteristic for the information expressed in T.

This is obvious e.g., when we look at the notion of logical equivalence:
two expressions T, T' are equivalent iff the classes of their models are
identical.

The logical connectives and quantifiers correspond to
operators on these classes of models. Their definition is implicit
in the definition of the satisfaction relation.   E.g., the
characteristic function of a conjunction is the intersection of the
classes of models of the  conjuncts.

From this formal concept (the class of models), we can derive concepts
like formal concepts of entailment, validity, equivalence.  All this is
mathematical and precise.

This formal notion of "information" needs to be connected to the
informal notion of "information" which is the interpretation that we,
human experts, give to a logical expression.

Logic does not know and is not supposed to know  what the informal
information (in a logic sentence) is about because  this
depends on the meaning that we, human
experts, give to the uninterpreted non-logical symbols.
But once a precise intended interpretation is given,
then I would say that the informal information content of a logic
sentence is precise as well.

For example, if we interpret the nonlogical symbols Semester/1,
Course/1, Registered/3, TakesPlace/2 in the way the names suggest, then
the intuitive information content of


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

is perfectly clear and is given by the equally precise informal sentence


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


If anything is vague or inprecise, then I guess it should be easy to
come up with e.g., an example of a database representing a situation
where B and A disagree or at least where it is not clear whether A or B
is true or not. This was the challenge in my previous email.

I think informal language sentence A is precise, at least in any context
where the underlying relations semester, course, are precise,
and I dont think one can find a database where A and B would disagree.

I would love to see a counterexample.




One can only view a logic theory as a program if one associates an
inherent  form of inference to the logic. As I argued in my first email,
this is the first step in messing up the difference between declarative
logic and programming languages.

It is the association of a unique
inherent form of inference to a logic  that blurs the distinction
between declarative theories and procedural programs



Cheers,

Marc


 For

Re: [TYPES] [tag] Re: Declarative vs imperative

Martin Escardo — 2013-05-05T22:31:44

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

In real analysis, it may be contentious what 0^0 ought to be, if 
anything at all.

In set theory (classical or constructive), X^0 is always 1, even when 
X=0. And so it is in type theory

This is because there is only one function 0->X (that with empty graph, 
or vacuously defined by zero cases).

So if you imagine 1=unit type="true" (and more generally any inhabited 
set/type X=true) and 0=_|_=false (the type with no inhabitants), then 
the "classical truth table" agrees with the constructive meaning of 
(X->Y) = Y^X. The constructive meaning gives you more, in that you are 
not restricted to 0 and 1 for the possibilities of what X and Y can be.

Of course, one should carefully distinguish the meanings of the notation 
_|_ invoked in the discussions in this list. It clearly has different 
meanings in e.g. domain theory and logic. In domain theory, it is not a 
type, but an element of any domain.

I hope this explains the confusion.

M.

On 05/05/13 22:04, Kalani Thielen wrote:

Re: [TYPES] [tag] Re: Declarative vs imperative

Guillaume Munch-Maccagnoni — 2013-05-05T22:10:45

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Kalani Thielen wrote :

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 :

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 :

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,

Re: [TYPES] [tag] Re: Declarative vs imperative

Kalani Thielen — 2013-05-05T21:04:24

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Thanks for the response.  Maybe I should have stated my question at the start instead of at the end, because I think that I might have been a bit unclear.  Let me try again.

If |A->B| = |B|^|A| and ~A = A->_|_ then e.g. |~Bool| (a continuation on a Bool) = |Bool->_|_| = 0^2 = 0.  This seems to imply that there are 0 continuations on Bool values (or any other non-empty set, though there's still the identity function _|_->_|_ = 0^0 = 1).

I'm sure that my interpretation or expectation is wrong somewhere (I'm just an uneducated country programmer, like I said) and I'd appreciate somebody setting me straight.

I don't think that we need to worry about induction/coinduction, as there's no reference to recursive types here.  The considerations about CBV/CBN and Turing-completeness forcing _|_ into all types can be set aside too, I believe, by just considering the translation of classical logic (as described in e.g. Timothy Griffin's "A Formulae-as-Types Notion of Control") in the simply-typed lambda calculus.  Consider just CPS-transformed boolean functions then, where the only source of "non-termination" is in your expectation that invoking a continuation produces 0 values (i.e.: it never returns).

Are there 0 continuations, or am I miscounting them somehow (or should counting not apply here)?  I'm just very curious to develop intuition about "classical types" a bit more, since I've found them to be very useful and reasonable in other respects (and as I said, I'm sure that it's just my intuition that's wrong or confused here).

Thanks.



On May 4, 2013, at 6:19 PM, Moez AbdelGawad <moezadel-1ViLX0X+lBJBDgjK7y7TUQ< at >public.gmane.org> wrote:

Re: [TYPES] [tag] Re: Declarative vs imperative

Sergei SOLOVIEV — 2013-05-05T11:23:03

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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

Best regards

Sergei Soloviev

Uday S Reddy wrote:

Re: [TYPES] [tag] Re: Declarative vs imperative

Uday S Reddy — 2013-05-05T09:37:16

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Tadeusz Litak writes:


Having thought about why it sounds like a "total and unconditional
rejection", I believe the difference is in the perspective of what logic is
about.

Logic consists of the principles of "reasoned discourse", as per Aristotle.
Our reasoned discourse happens in natural language, which is a humongous
ocean.  We may never be able to understand fully all the principles of logic
that are there.  But it is clear that the logic that we do understand (all
the known logics put together) represents only a miniscule proprotion of the
vast ocean of "logic" that is employed in reasoned discourse.  So, it seems
to me that a great deal of humility is warranted in talking about "logic" in
general.

In contrast, people that vax about classical logic seem to have the
presumption that classical logic has it all cased.  They seem to think that
it represents the sum total of all reasonable principles of reasoned
discourse (even if they are willing to admit modal logics of one kind or
another as being reasonable *extensions* of classical logic).  Hence,
anybody that talks about alternative logics is seen to be mounting an attack
on the classical logic, denying the supreme position of classical logic as
the one true logic.

We, the non-believers, of course deny that classical logic is supreme in any
sense.  However, that is not an attack on classical logic itself.  It is
just an attack on the *presumption* that classical logic is supreme.

All that we can say about classical logic is that it seems to be the
canonical logic for the present-day mathematics.  Given that mathematics is
a very conservative discipline, with the bar of entry for new ideas set very
high, it has an abundance of depth but not so much in breadth.  Thus, a
canonical logic for mathematics in no way represents a canonical logic for
all of human thought.

In particular, in a young and dynamic discipline like Computer Science,
which has none of the mathematical conservatism, we should be free to
explore all possible logics and invent new ones.  In fact, devising logics
is our very main business.  We should be very wary of any presumptions about
"the canonical logic" of any kind.

Cheers,
Uday

Re: [TYPES] [tag] Re: Declarative vs imperative

Moez AbdelGawad — 2013-05-04T22:19:12

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Kalani,

Here are my two cents.

_|_  (bottom/divergence) is a member of every type, including the "empty" type.  The cardinality of the empty type is thus 1, not 0.  Also, for the same reason, the cardinality of the Bool type is 3, not 2.

-> is the constructor of (lazy/call-by-name) continuous functions (ie, not of all possible mathematical functions). 'Continuous' here is in a domain-theoretic sense, sometimes also called 'Scott-continuity'. The cardinality |A->B| is thus not necessarily |B|^|A|. Noting that A and B contain _|_ as noted above, |A->B| is |B|^|A| in case A and B are 'flat' domains/types. Without much ado, Bool and the empty type are flat.  Also, note that -o-> usually denotes the strict/eager/call-by-value version of ->. If, again, A and B are flat, |A-o->B| = |B|^(|A|-1), where |A|-1 is the cardinality of non-bottom elements in A, because -o-> can map _|_ in A only to _|_ in B, not to other elements of B.

As such, if I assume you meant eager functions over booleans, |Bool-o->Bool| = 3^2 = 9, not 4  (I believe you can easily figure out these nine functions if you note that a function, in addition to returning true or false, may also diverge/"return" _|_).  Similarly, we have |A->_|_| = 1.

Regards,


-Moez

Re: [TYPES] [tag] Re: Declarative vs imperative

Uday S Reddy — 2013-05-04T18:17:08

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Tadeusz Litak writes:


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.

Re: [TYPES] [tag] Re: Declarative vs imperative

Lukasz Stafiniak — 2013-05-04T16:10:28

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Sat, May 4, 2013 at 5:49 PM, Kalani Thielen <kthielen-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org> wrote:



My wild guess is that a continuation type ~A is a co-inductive type, and
the correspondence with cardinality of sets works only for inductive types.
Inductive types are the smallest sets built according to the specification,
while co-inductive types are the largest sets meeting some constraints.
Therefore the latter have infinite cardinality.

Re: [TYPES] [tag] Re: Declarative vs imperative

Uday S Reddy — 2013-05-04T16:08:55

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Mark Janssen writes:


Oh, no!  Wherever you have learnt logic from, I am afraid they didn't do a
very good of explaining what logic is about (which is not unusual).

As Marc Denecker alluded to, logic is essentially a study of the information
content of statements.  The "information content" idea is formalized in
terms of consequence: which statement is a consequence of which other
statements.  If B is a consequence of A, i.e., if B necessarily happens to be
true in all situations where A is true, we understand that the information
contained in B is already contained in A.

Programming languages are also regimentations of natural language, albeit a
different part of natural language than the one classical logic has
traditionally concerned itself with.  When I was taught programming in the
70's, I was encouraged to use natural language for writing algorithms
because it helps you to think better.  (However, using natural language
correctly, i.e., precisely and unambiguously, requires quite a bit of
mathematical training, which is becoming increasingly rare in recent times.)

Programming logic is the logic used for reasoning about programs.  There, we
are interested not only in the consequences of statements, but also the
consequences of commands (or functions, operations or whatever).

We use natural language to communicate (and to think in) every day.  It is
obviously not meant for just the philosophers!

Cheers,
Uday

Re: [TYPES] [tag] Re: Declarative vs imperative

Kalani Thielen — 2013-05-04T15:49:48

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


I am not an academic or qualified in any way to speak on this, I'm just an uneducated, small town, country programmer, but on this point you've raised I wonder if the list could clear up a bit of confusion that I have.

I'm familiar with thinking of types as sets and logical connectives (type constructors) as operations on sets.  So the type A*B has size |A|*|B|, the product of the sizes of two sets.  A->B has size |B|^|A| and this works out well (e.g.: Bool->Bool has size 2^2 = 4: not, id, const True, const False).

So like you say, type negation corresponds to a continuation on that type (where a continuation doesn't return any value at all, satisfying the empty type).  So ~A=A->_|_.  That interpretation works out really well too, because identities like A+B=~A->B can be read as compilation techniques for variants (with the obvious construction and destruction approaches).

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?

I appreciate any explanations y'all can offer on this point.

Regards.



On May 3, 2013, at 8:23 PM, Tadeusz Litak <tadeusz.litak-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org> wrote:

Re: [TYPES] [tag] Re: Declarative vs imperative

Luis Caires — 2013-05-04T11:37:59

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Fri, May 3, 2013 at 11:28 PM, Mark Janssen <dreamingforward-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org> wrote:

Hi, about this point: perhaps it is helpful to recall some very basic
stuff, put in very simple terms, even if it may sound quite
elementary...

While what (I think) you call boolean logic may be useful for explaining
(basic) computing operations, and provide an adequate foundation for
(basic) hardware design, it just does not scale up to higher levels of
abstraction, as needed to talk and reason about complex computing
systems.

It really takes quite a bit to build up from bit-level operations as
actually performed by the hardware up to concepts such as "ADTs",
"algorithms", "objects", "functions", "modules", "types", "abstract
machines" - ideas such as "code as data", "atomicity", "fairness",
"levels of interpretation" - and all the great stuff that belong to
the world of (both practical and theoretical) computer science. To be
able to talk about all this we need much more than basic "binary
artihmetic and boolean algebra".

For our purposes, it is perhaps more convenient to think of "symbolic
logic" as just a the convenient language to describe properties and
formally reason about objects in some domain.

Currently, one single unified logic is not yet available, we need
several logics;
different logics describe different kinds of properties of CS objects,
useful for different purposes, all based, we hope, on a common trunk
of deep principles.

For example, I guess every programmer appreciate the usefulness of
types in programming languages. But a type system is nothing more than
a certain kind of a symbolic logic. It does not calculate with
concrete data values or bits, but instead uses logic to deduce and
reason about the type of things around, allowing the compiler to
prove, at compile time, without executing the generated code, that a
program satisfies a set of properties. Namely that, when actually
executed, it will not suffer from basic runtime errors, such as
invalid operations on data, etc.

This is just an example. Each particular logic provides reasoning
rules, allowing us to know how properties expressible in the logic
relate, and how the objects the logic talks about satisfies a property
or not. In some cases, algorithms can be provided to check whether an
object satisfy a given property (automated verification).

These basic concepts are essential for computer science, as no
artifact (processors, algorithms, programming languages, compilers,
etc) can be precisely and fully understood without reference to the
various properties it should satisfy. If you want to check that a
given code piece really returns a sorted vector, you cannot do this
conveniently just with (what I think you call) boolean logic (even if some
simple verification problems can be "compiled" down to boolean
logic). As another example, some of us may teach (separation) logic to
students to empower them with solid techniques for checking the
absence of races in concurrent java programs. As yet another example,
we (with colleagues) have recently discovered how to use (linear)
logic to reason about the safety of session protocols in distributed
systems.

So there is this idea that (symbolic) logic is actually the "calculus
of computer science" (see
e.g. http://www.cs.rice.edu/~vardi/logic/). While symbolic logic has
roots in philosophy, I guess it is fair to recognize that it is being
now developed mostly in conection with (theoretical) computer science
and math, often driven by the deep relation between logic and
computation. So I would really encourage you to look into all this.

Logical concepts may be also perhaps useful to discuss other issues in
this thread such as "specs versus programs", and "declarative versus
imperative". Let me copy some remarks by Hoare (ACM, 2009):

"So I believe there is now a better scope than ever for pure research
in computer science. The research must be motivated by curiosity about
the fundamental principles of computer programming, and the desire to
answer the basic questions common to all branches of science: what
does this program do; how does it work; why does it work; and what is
the evidence for believing the answers to all these questions? We know
in principle how to answer them. It is the specifications that
describes what a program does; it is assertions and other internal
interface contracts between component modules that explain how it
works; it is programming language semantics that explains why it
works; and it is mathematical and logical proof, nowadays constructed
and checked by computer, that ensures mutual consistency of
specifications, interfaces, programs, and their implementations."

So I guess this view of logic actually belongs to the CSD ...

Thanks,

Luis

Re: [TYPES] [tag] Re: Declarative vs imperative

Tadeusz Litak — 2013-05-04T00:23:49

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.

Re: [TYPES] [tag] Re: Declarative vs imperative

Philippa Cowderoy — 2013-05-04T00:02:57

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 05/03/13 23:28, Mark Janssen wrote:

We must do no such thing! Booleans are not especially fundamental to 
computing, however much they are part of our hardware implementations. 
To talk about how things map onto binary arithmetic and boolean algebra, 
we must talk about the things we are mapping onto them: this means 
accepting that some logics talk about other objects of study.

Re: [TYPES] [tag] Re: Declarative vs imperative

Mark Janssen — 2013-05-03T22:28:01

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


But if we're going to be in the Computer Science department, can we
get away from the idea of "logic as a regimentation of natural
language" (which is fine for the Philosophy department) and move to
the idea of logic as equations of Binary Artihmetic and Boolean
Algebra?

Re: [TYPES] [tag] Re: Declarative vs imperative

Uday S Reddy — 2013-05-03T21:22:28

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Marc Denecker writes:


No, what I meant is that the classical logic represents a stage in the
development of logic.  It cannot be taken as the final answer.  In fact, we
cannot accept that we have a final answer until the entire natural language
has been formalized, which might take a very very long time indeed!  (The
view I take, following Quine, is that logic is a regimentation of natural
language.  We can perfectly well circumscribe various regimens for various
purposes.)

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.

Even though Vladimir has omitted the word "programming" in titling this
subthread, the discussion has been about "declarative" and "imperative" as
paradigms of programming.  So, I would rather not divorce myself from
programming concerns in discussing these issues.

Cheers,
Uday

PS. I will try to respond to your more detailed points a little later.  For
now, I just wanted to set the record straight about what you called my
"total and unconditional rejection" of classical logic, which it wasn't.

Re: [TYPES] [tag] Re: Declarative vs imperative

Marc Denecker — 2013-05-03T13:09:13

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 04/26/2013 11:44 PM, Uday S Reddy wrote:


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

Aif 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

Re: [TYPES] Future of TLCA

Dan Licata — 2013-05-01T14:22:18

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

In case anyone else would like to follow this discussion using a
non-gmail address, you can subscribe an email address to the group 
by sending an email to

tlca-list+subscribe< at >googlegroups.com

It just took me a few minutes to figure out how to do this,
so I thought I'd share.

-Dan


On May01, Paweł Urzyczyn wrote:

[TYPES] Future of TLCA

Paweł Urzyczyn — 2013-05-01T12:02:37

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


This message is addressed to everyone interested in the future
of the conference TLCA (Typed Lambda Calculi and Applications).
The bi-annual conference started in 1993 and will have its 11th
edition this June in Eindhoven as part of RDP. After 20 years
it seems reasonable to ask some questions about the future.
In particular there is an emerging discussion on whether TLCA
should merge with RTA or perhaps develop into a new conference
of a broader scope. In order to gain opinions from as large part
of TLCA community as possible, we have created a Google Group:

     https://groups.google.com/forum/#!forum/tlca-list

We invite everybody who feels part of TLCA community to contribute
to the discussion with their opinions and suggestions.

Samson Abramsky, Pierre-Louis Curien,
Mariangiola Dezani-Ciancaglini,
Masahito Hasegawa, Luke Ong,
Simona Ronchi Della Rocca,
Paweł Urzyczyn

Re: [TYPES] John Reynolds

David Naumann — 2013-04-30T16:09:14

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

A guiding spirit indeed.  Another opportunity for reflection is this recent 
interview:
http://link.cs.cmu.edu/article.php?a=763


http://link.cs.cmu.edu/article.php?a=763

On Mon, 29 Apr 2013, Uday S Reddy wrote:

[TYPES] John Reynolds

Uday S Reddy — 2013-04-29T19:39:48

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear friends and colleagues,

I am sorry to bring the sad news that John Reynolds, whose work and insights
I have mentioned and recounted in my recent exchanges, has passed away on
Sunday in Pittsburgh.

John has not only done seminal work on a wide range of programming language
topics, but he was also a guiding spirit and a great friend to many of us.
We will dearly miss him.

At this juncture, we might take a moment to reflect on his life time of
accomplishment:

  http://www.cs.cmu.edu/~jcr/

Uday