[Flirts] RE: Curry-Howard isomorphism for Institutions

Wed Aug 10 18:45:16 MEST 2005

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.

>they idea of using sets of sentences as objects is new and useful, 
>or did we miss something there also?
Well, I don't think it is useful, as *when* you can do your categorical modelling properly, sets of sentences are modelled for free, either in the case where there's a connective that internalizes the comma (like a categorical tensor) or using the fibration mechanism. So no, I don't see the usefulness at the moment, it doesn't buy me anything new. Maybe you'd like to expand on that?

About:
>it seems a bit extreme to say that it doesn't really do any proof theory;
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?

>I find this dialogue very useful and hope that we can continue it further - i look forward to learning more!
So do I, thanks for the discussion!

Best regards,

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: Tuesday, August 09, 2005 8:31 PM
To: Formalism, Logic, Institution - Relating, Translating and Structuring
Cc: till at informatik.uni-bremen.de; de Paiva, Valeria <Valeria.dePaiva at parc.com>
Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions

Dear Valeria,

Thanks so much for your remarks!  If you have a nicer way of including proofs into institutions, such that, for example, classical logic works well by something other than proof terms for sequents, that would be very welcome and interesting to us.  Ive heard about the work you mention in various theses but have never looked at it; your summary is a bit on the discouraging side, i must admit - too many answers, all likely to be rather complicated, and no clear tradeoffs.

About the origin of institutions with proofs, it goes back to at least 1980 in conversations between Rod Burstall and i; Rod didnt much like the idea then but i put it in our JACM paper anyway, where it appeared after a 7 year delay (submitted 1985, but earlier drafts exist, also with the proof  idea).

About the formulation in "What is a logic?" it seems a bit extreme to say that it doesnt really do any proof theory; although it is clear that it is far from doing everything that proof theorists find interesting, it does allow defining many basic proof theoretic concepts in a nice abstract way, especially those that connect with models.  Also, as far as i know, they idea of using sets of sentences as objects is new and useful, or did we miss something there also?

With all best regards,

    joseph

Valeria.dePaiva at parc.com wrote:

>Dear Till,
>  
>
>>This means that for classical logic, the approach of identifying 
>>different calculi (say, Gentzen or natural
>>deduction) via (2-)categories of proofs seems to be hopeless, because 
>>everything is the same thin category, namely essentially the usual Lindenbaum-Tarski algebra.
>>Or am I missing something?
>>    
>>
>Well, you're missing the gigantic amount of work put into this problem since the early 90's with the theses of Griffin, Murthy, Stewart, Harbelin, Urban, Parigot, etc. It is true that classical logic is harder to model categorically than intuitionistic logic and it's true that despite all this work it's not clear (to me at least) what are the trade-offs between different kinds of classical Curry-Howard systems and their categorical semantics. But I guess by now it's clearly understood by most in the community that the old dictum that "classical logic has no categorical semantics" is dead and buried. Which kind of solution you prefer for the problem (Selinger's control cats or fibrations or order-enriched models or even special kinds of  polycategories, etc...I'm sure I'm forgetting half the decent solutions, for which I apologize) is up to you. As I said I don't know of a list of trade-offs or cost/benefits analysis of the several solutions. It's not my main area of research!
>   (I like my logic intuitionistic, by and large), so if you do happen to be able to compile such a list, I'd be very interested in seeing it.
>
>If you'd like more information you could check David Pym's page on Semantics of Classical Proofs, which is mostly devoted to his own solution with Carsten Führmann and others, but should, I hope, give pointers to other work:
>http://www.cs.bath.ac.uk/~pym/semclasspro.html
>
>Hope this helps,
>Best,
>Valeria
>Ps I was forgetting the work of Lutz Strassburger and Francois Lamarche, which I shouldn't, check it at:
>http://www.ps.uni-sb.de/~lutz/
>Dr Valeria de Paiva
>PARC
>3333 Coyote Hill Road
>Palo Alto, CA 94304
>USA
>
>-----Original Message-----
>From: Till Mossakowski [mailto:till at informatik.uni-bremen.de]
>Sent: Tuesday, August 09, 2005 10:20 AM
>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>
>Cc: FLIRTS
>Subject: Re: Curry-Howard isomorphism for Institutions
>
>Dear Valeria,
>
>thank you for agreeing to continue this interesting discussion on the FLIRTS mailing list.
>
>The paper "What is a logic?" (for those who do not have it: 
>http://www.tzi.de/~till/papers/nel05.pdf) takes the following
>perspective: we wanted to clarify what the "identity" of a logic is, and when two logics are considered to be essentially equal (or different). While on the model-theoretic side, we have good notions in the paper (and also some results), the proof-theoretic side is much weaker developed. The main perspective of the paper is to distinguish different proof theories by the different connectives they allow, and the different behaviour of these connectives (regardless whether these connectives are actually present in the logic or not - the connectives are defined only in terms of the vocabulary of an institution with proofs). To do this, we use some standard tools from categorical logic. You are right, proof term normalization is completely ignored. This is mainly because we could not see how it would help us to identify connectives in a logic independent way, or otherwise contribute to the "identity" of a logic.
>
>However, we say in the conclusion of the paper:
>
>   There are some further proof-theoretic properties that we have not
>   treated, like (strong) normal forms for proofs (this would require
>   $Sen(\Sigma)$ to become 2-category of sentences, proof terms and proof
>   term reductions).  A related topic is cut elimination, which
>   would require an even finer structure on $\Sen(\Sigma)$,
>   with proof rules of particular format.
>   We hope this essay provides a good starting point for
>   such investigations.
>
>This finer structure might be seen as inessential for the logic itself (e.g. FOL with Gentzen style proofs and FOL with natural deduction proofs are "essentially the same" from this perspective), but of course this would not preclude a much more fine-grained "identity of prood system", based on 2-categories of proofs. Does this meet your point?
>
>I must admit that I do not really know much about normal forms of proofs, and still need to look in your papers more thoroughly. But before doing that, I want to discuss some point. What me puzzles me a bit already with the approach of defining connectives in a proof-theoretic way within 1-categories is the following (citing from another mail from me written in connection with the paper):
>
>   Note that arrows in proof categories are proofs up to equivalence.
>   And we impose certain conditions on this equivalence.
>   A simple example: if we infer A/\B from A/\B by conjunction
>   elimination and conjunction introduction, then this proof must
>   be equivalent to the proof infering A/\B directly from itself,
>   because conjunction is product, and <pi_1,pi_2>=id.
>   Basically, for propositional logic, our axioms of proof-theoretic
>   institutions say that the category of proofs is bicartesian closed
>   (ie cartesian closed + finite coproducts, including inital objects).
>   Lambek and Scott, "Introduction to categorical higher-order logic",
>   show on p.67, that in any bicartesion closed category, for an object
>   A, either Hom(A,0) is empty, or else A is isomorphic to 0 (where 0 is
>   the initial object). From this it follows that any classical
>   bicartesion closed category (i.e. one with A is isomorphic to
>   (A=>0)=>0 ) is equivalent to a Boolean algebra, i.e. equivalent
>   to a thin category, and hence thin itself.
>
>This means that for classical logic, the approach of identifying different calculi (say, Gentzen or natural deduction) via (2-)categories of proofs seems to be hopeless, because everything is the same thin category, namely essentially the usual Lindenbaum-Tarski algebra.
>Or am I missing something?
>
>Greetings,
>Till
>
>Valeria.dePaiva at parc.com wrote:
>  
>
>>Dear Till,
>>
>>I noticed that you actually went ahead and did some  of the work we 
>>discussed a long time ago (see below) on adding "categorical logic" to 
>>institutions on a joint paper with Diaconescu, Goguen and Tarlecki 
>>("What is a Logic?). I was invited speaker at the Universal Logic in 
>>Montreux, where Diaconescu talked about it.
>>
>>While I did feel a bit miffed that my original suggestion of the 
>>problem wasn't mentioned at all, my problem with the paper is not 
>>that. My problem is that your approach seems to be the proverbial 
>>"throwing the baby away with the bathwater". The point of putting real 
>>proofs (as opposed to entailment relations) into institutions was to 
>>try to use the proofs-as-lambda-term-representations to do some real 
>>work for us, ie to connect to the paradigm of extracting programs from 
>>proofs, or to help with abstract analysis or to extend type systems in 
>>a principled and logical way, etc. i.e. any of the usual applications 
>>of categorical proof theory would do here.
>>
>>You say in page 2 of your joint paper that your new definition of 
>>(proof
>>theoretic) institution "fully supports proof theory", but the notion 
>>of proof theoretic institution (or of equivalence of institutions) 
>>introduced in the paper has nothing much to do with proof theory as 
>>people normally know it. What you call "proof theoretic institutions"
>>do not overcome the suggested limitation of "categorical logic", 
>>because proof theoretic institutions do not  model the significant 
>>aspect of proofs, which is their reduction behavior.
>>
>>The point of the Curry_Howard isomorphism is not that you can model 
>>propositions as objects in a category and proofs as equivalence 
>>classes of morphisms: the point is that the behaviour of proofs is 
>>preserved under this modelling. This is why some people think that the 
>>Curry-Howard isomorphism should be called Curry-Howard-Tait isomorphism.
>>The  crucial point is that if proof pi reduces to pi' via 
>>alpha-beta-eta reductions than the corresponding morphisms are related 
>>in the target category (either by equality or reduction). Nothing like 
>>that happens in the proof-theoretic institutions, which is why they 
>>are only proof-theoretical in name.
>>The functor Pr: Sign -> Cat is only about proofs in its name, which 
>>you presumably realize, as  it is not even spelled out in the 
>>definition on (page 125 of the book) that Pr stands for proofs. I 
>>guess my main complaint is that the paper does not define a 
>>"proof-theoretical institution" in the sense of an institution that 
>>preserves proofs, but simply as an institution that preserves 
>>entailment. But I guess this is all right, people will have different 
>>perspectives on what is important, mathematically speaking.
>>
>>Best regards,
>>Valeria
>>
>>
>>
>>-----Original Message-----
>>From: Till Mossakowski [mailto:till at Informatik.Uni-Bremen.DE]
>>Sent: Friday, January 31, 2003 12:14 AM
>>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>
>>Subject: Re: CHI for Institutions
>>
>>Dear Valeria,
>>
>>agreed, let's devide the work as you suggested.
>>
>>For a definition of (some variant of) parchment you might look at p 5ff.
>>of "Combingn and representing logical systems using model-theoretic 
>>parchments", available at my publications page.
>>
>>Concerning the Lisbon work: I think it shouldn't be difficult to have 
>>a meta notion of sequent calculus, like the meta notion of Hilbert 
>>calculus.
>>
>>Concerning the more complex Curry-Howard isos:
>>you seem to have one in the paper with Biermann. Then I'll have a look 
>>on that, before going on with trying to look at Curry-Howard in the 
>>institutional framework
>>
>>Greetings,
>>Till
>>
>>Valeria.dePaiva at parc.com schrieb:
>>    
>>
>>>Dear Till,
>>>Thanks for the very interesting message. Now I have to do some
>>>      
>>>
>>reading, I don't even know what a parchment is...
>>    
>>
>>>But one small thought: your last paragraph about translating the
>>>      
>>>
>>Curry-Howard isomorphism in terms of institutions is very interesting 
>>and seems a more concrete way of pushing forward towards my goal, 
>>which is different though. My goal is really enriching the whole 
>>framework of institutions so that it can cope with proofs (and when I 
>>say proofs I don't mean in a single proof calculus: I usually want a 
>>logic to be given in different several proof calculi all proved 
>>equivalent, like for instance for IPL you can give axioms, sequents or 
>>Natural deduction and you know how to translate proofs from one 
>>calculi to the others). So another way of pushing forward would be to 
>>see if the Lisbon work you've mentioned can be "translated" into sequent calculus, for example.
>>    
>>
>>>Now about your question: no I don't think I know of any reference for
>>>      
>>>
>>the diagram in page 26. The first problem  is  that Oyster, PVS and 
>>NuPRl are computer systems and first of all we would need papers 
>>called "The essence of Oyster, PVS and NuPRL", or Alf, but I guess 
>>these might exist. I just haven't had the time or disposition to look 
>>for them. This would be a different research project altogether it seems to me.
>>    
>>
>>>Thus a modest proposal: I will read the stuff you've mentioned and 
>>>try
>>>      
>>>
>>to come back with questions/suggestions. Maybe you could try to add 
>>some details to the suggestion of looking at Curry-Howard in the 
>>institutional framework?
>>    
>>
>>>Cheers,
>>>Valeria
>>>      
>>>
>
>
>  
>

_______________________________________________
Flirts mailing list
Flirts at mail.informatik.uni-bremen.de
http://www.informatik.uni-bremen.de/mailman/listinfo/flirts
-------------- next part --------------
A non-text attachment was scrubbed...
Name: nasa.ps
Type: application/postscript
Size: 214440 bytes
Desc: nasa.ps
Url : http://www.informatik.uni-bremen.de/pipermail/flirts/attachments/20050810/2ce618e8/nasa-0004.ps