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

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 confusio

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
t

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

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

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

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

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
co

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

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 scien

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

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

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 n

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