FW: [Flirts] RE: Curry-Howard isomorphism for Institutions
Valeria.dePaiva at parc.com
Valeria.dePaiva at parc.com
Wed Aug 17 02:35:59 MEST 2005
Dr Valeria de Paiva
PARC
3333 Coyote Hill Road
Palo Alto, CA 94304
USA
-----Original Message-----
From: de Paiva, Valeria <Valeria.dePaiva at parc.com>
Sent: Monday, August 15, 2005 10:24 PM
To: 'Joseph Goguen'
Cc: 'flirts at informatik.uni-bremen.de'
Subject: RE: [Flirts] RE: Curry-Howard isomorphism for Institutions
Dear Joseph,
I'm glad you've enjoyed Phil's paper.
> My impression (e.g., looking at recent POPL proceedings) is that there
>is indeed a lot of work that applies ideas from type theory to
>programming languages, but the systems used are far from beautiful,
>while the beautiful systems are not directly useful.
My point was that the work represented in POPL, etc
> owes its existence to programmers picking up the CHI and using it for
>their own purposes.
Maybe it is too much to ask for the systems that come from logic, to
carry-on being pretty. But I guess one may hope and I do.
I also enjoyed very much David Walker's invited talk at IMLA this year,
when he was asking the logicians in the audience for help with his type
systems for memory management. But I guess there's no paper written
about it, (yet, perhaps, I don't know).
I have written some of my own take on these ideas, as far as CHI for
modal logics is concerned, in the preface of the special issue of the
JLC dedicated to the second IMLA (2002 in Copenhagen). You can read it
from http://www.cs.bham.ac.uk/%7Evdp/publications/final-preface.pdf
if interested. But this is of course just a subcase of the general
picture.
Best,
Valeria
-----Original Message-----
From: Joseph Goguen [mailto:goguen at cs.ucsd.edu]
Sent: Monday, August 15, 2005 6:52 PM
To: de Paiva, Valeria <Valeria.dePaiva at parc.com>
Cc: flirts at informatik.uni-bremen.de
Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
Dear Valeria,
Thanks for the pointer to Phil's paper, i enjoyed reading it!
This paper does not make the claims for Curry-Howard that you mention,
but instead makes the much more modest claim that systems were "designed
by researchers in functional languages and they depend heavily on logics
and type systems whose roots were traced in this paper" (these roots are
work of Church, Gentzen, Girard, etc.). On the whole, there are
pleasingly few exaggerated claims in the paper.
My impression (e.g., looking at recent POPL proceedings) is that there
is indeed a lot of work that applies ideas from type theory to
programming languages, but the systems used are far from beautiful,
while the beautiful systems are not directly useful. It would be
surprising to me if anyone worked out a Curry-Howard isomorphism for any
of these ugly type systems.
- joseph
Valeria.dePaiva at parc.com wrote:
>Dear Joseph,
>
>While I do agree with
>
>
>>The basic Curry-Howard isomorphism ("CHI") is one of the most
>>beautiful
>>
>>
>pieces of mathematics that is
>
>
>>associated with computer science, and its extension to much more
>>
>>
>general types is
>
>
>>something that theoretical computer scientists can be proud of.
>>
>>
>
>I beg to differ on
>
>
>>As far as practice goes, not much has happened,
>>
>>
>I guess it all depends on what kind of practice you're thinking of. It
>seems to me that quite a lot of the practical work that goes under the
>rubric of "programming languages" design&implementation (including the
>design of Java and other recent typed programming languages) owes its
>existence to programmers picking up the CHI and using it for their own
>purposes. Phil Wadler had a nice note on Dr. Dobbs about the CHI
>called
>
>Proofs are Programs: 19th Century Logic and 21st Century Computing.
>
>I think the URL is
>
>http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
>
>But back to the subject at hand:
>
>
>>i even have some ideas which i hope to write up a bit later on.
>>
>>
>Looking forward to seeing you this,
>
>Valeria
>
>-----Original Message-----
>From: Joseph Goguen [mailto:goguen at cs.ucsd.edu]
>Sent: Friday, August 12, 2005 8:03 AM
>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>; Formalism, Logic,
>Institution - Relating, Translating and Structuring
>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>
>Dear Valeria,
>
>It seems to me that your definition of "proof-theoretical" is too
>narrow to capture what mathematical logicians actually do; it seems to
>me that "proofs about proofs" is a more accurate definition for "proof
>theory", since in practice proofs about proofs are often done with
>respect to models, and experience shows that when you have the right
>models, such proofs are often easier that way.
>
>Im thinking that the origin of these divergences of view may go back to
>some discussions you and Till had about what's in the title of this
>thread, "Curry-Howard isomorphism for Institutions" and your research
>focus on type theory?
>
>The basic Curry-Howard isomorphism ("CHI") is one of the most beautiful
>pieces of mathematics that is associated with computer science, and its
>extension to much more general types is something that theoretical
>computer scientists can be proud of. As far as practice goes, not much
>has happened, but it seems plausible to me that someday, for some class
>of useful programs, it may be possible for users to specify what they
>want in a "Visual Type Theory" language, which then an automatic
>theorem can constructively prove inhabited, yielding a program that can
>then be optimized by sophisticated transformations into a practical
>program that can be run. After all, computers continue to follow
>Moore's law, which means still lots of power to come, while theorem
>proving and compiler optimization technologies continue to improve (but
not exponentially!).
>So it seems worth continuing research on type theory in pursuit of the
>dream of automatic programming (and other some dreams).
>
>But i dont think this should be allowed to dictate the research
>programmes of institutions, which have always had different goals from
>type theory, one of which is to capture mathematical practice in logic,
>including model theoretic reasoning, not just formal manipulations of
>proofs. Nevertheless, i think it could be very interesting to see what
>can be done with CHI in an institutional setting, and i even have some
>ideas which i hope to write up a bit later on.
>
>By the way, some time ago i put forward the slogan "types as theories"
>as a view of programming, and i also tried to show that if you have a
>nice module system of the sort supported by institutions, then you do
>not really need higher order logic to reason about typical higher order
>functions. See
>
> http://www.cs.ucsd.edu/~goguen/pps/utyop.pdf
>
>But this is not to say that i am against type theory or against higher
>order functions. In fact, i endorse Till's proposal for research on
>IL, except that i do not think that the model aspect of morphisms
>should be optional.
>
>I look forward to further discussion of all this.
>
> -- joseph
>
>Valeria.dePaiva at parc.com wrote:
>
>
>
>>Dear Joseph,
>>A small clarification:
>>
>>
>>
>>
>>>im just reponding to your request for proof theory stuff that we can
>>>do in insitutions - do you remember that request?
>>>
>>>
>>>
>>>
>>My request (may be I wasn't clear enough) was for proof-theoretical
>>stuff that you could do with (the proof-theoretical side of)
>>
>>
>"institutions with proofs".
>
>
>>So Craig interpolation done by model theoretical means doesn't count,
>>even if I do think it pretty. It's the `method' of proof that's at
>>
>>
>stake in the request, not the statement itself.
>
>
>>Cheers,
>>
>>Valeria
>>
>>-----Original Message-----
>>From: Joseph Goguen [mailto:goguen at cs.ucsd.edu]
>>Sent: Thursday, August 11, 2005 8:02 AM
>>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>; Formalism, Logic,
>>Institution - Relating, Translating and Structuring
>>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>>
>>hi again Valeria!
>>
>>Valeria.dePaiva at parc.com wrote:
>>
>>
>>
>>
>>
>>>Craig interpolation I believe we can do totally proof-theoretically
>>>in
>>>
>>>
>many situations -- without infinite sets of sentences. Compactness, as
>I said, I have a problem seeing it as proof theory, but maybe it's
>just lack of trying.
>
>
>>>
>>>
>>>
>>>
>>i never said craig interpolation needs infinite sets of sentences, and
>>
>>
>i never said you couldnt do it proof theoretically! im just reponding
>to your request for proof theory stuff that we can do in insitutions -
>do you remember that request? and please note that compactness is
>normally formulated as an assertion about proofs even though it is
>normally proved model theoretically.
>
>
>> - joseph
>>
>>
>>
>>
>>
>>>Best,
>>>Valeria
>>>-----Original Message-----
>>>From: flirts-bounces at informatik.uni-bremen.de
>>>[mailto:flirts-bounces at informatik.uni-bremen.de] On Behalf Of Joseph
>>>Goguen
>>>Sent: Wednesday, August 10, 2005 6:25 PM
>>>To: Formalism, Logic, Institution - Relating, Translating and
>>>Structuring
>>>Cc: till at informatik.uni-bremen.de
>>>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>>>
>>>Dear Valeria and others,
>>>
>>>This is fun, we are getting a lot of different points of view.
>>>
>>>Valeria.dePaiva at parc.com wrote:
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>>Dear Joseph,
>>>>Thanks for the friendly message.
>>>>First, let me make it clear that, no, I do not have "a nicer way of
>>>>
>>>>
>including proofs into institutions", at the moment. I had proposed to
>Till that we could investigate this problem together, as I had become
>interested in the idea around 1999. I'm attaching some slides from a
>talk I gave at NASA Ames then when I was trying to sell them a work
>proposal along these lines. I thought this was a cool idea, which you
>probably agree since you've had the same idea some 15 years before me.
>But I only worked on that for a couple of weeks, preparing the talk,
>which is just a proposal for some work. Not the work itself.
>
>
>>>>
>>>>
>>>>
>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>I'm afraid I don't think it excessive. I went back to the paper
>>>>"What
>>>>
>>>>
>
>
>
>>>>is a Logic?" to see if I was forgetting any basic interesting
>>>>proof-theoretic notion, given that you've said
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>>it does allow defining many basic proof theoretic concepts in a
>>>>>nice
>>>>>
>>>>>
>
>
>
>>>>>abstract way,
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>But I don't see these many concepts. Would you like to discuss them
>>>>
>>>>
>one by one?
>
>
>>>>
>>>>
>>>>
>>>>
>>
>>
>>
>>
>
>
>
More information about the Flirts
mailing list