Bruno,
I know just a little about the curry-howard isomorphism... I looked
into it somewhat, because I was thinking about the possibility of
representing programs as proof methods (so that a single run of the
program would correspond to a proof about the relationship between the
input and the output). But, it seems that the curry-howard
relationship between programs and proofs is much different than what I
was thinking of. In the end, I don't really see any *use* to the
curry-howard isomorphism! Sure, the correspondence is interesting, but
what can we do with it? Perhaps you can answer this.
--Abram
On Mon, May 18, 2009 at 12:54 PM, Bruno Marchal <marchal.domain.name.hidden> wrote:
>
> Hi Abram,
>
>
> On 24 Apr 2009, at 18:55, Abram Demski wrote:
>
>>
>> I'm starting a mailing list for logic, and I figured some people from
>> here might be interested.
>>
>> http://groups.google.com/group/one-logic
>
> Interesting! Thanks for the link. But logic is full of mathematical
> mermaids and I am personally more problem driven. I may post some day
> an argument for logical pluralism (even a classical logical argument
> for logical pluralism!), though. Ah! but you can easily guess the
> nature of the argument ...
>
>
>>
>>
>> I've looked around for a high-quality group that discusses these
>> things, but I haven't really found one. The logic-oriented mailing
>> lists I've seen are either closed to the public (being only for
>> professional logicians, or only for a specific university), or
>> abandoned, filled with spam, et cetera.
>
>
>
> But it is a very large domain, and a highly technical subject. It is
> not taught in all the universities. It is not a well known subject.
> Unlike quantum mechanics and theoretical computer science, the
> difficulty is in grasping what the subject is about.
> It take time to understand the difference between formal implication
> and deduction. I have problem to explain the difference between
> computation and description of computation ...
>
>
>
>
>> So, I figured, why not try to
>> start my own?
>
>
> Why not? Actually I have many questions in logic, but all are
> technical and long to explain. Some have been solved by Eric, who then
> raised new interesting question.
>
> Have you heard about the Curry Howard isomorphism? I have send posts
> on this list on the combinators, and one of the reason for that is
> that combinators can be used for explaining that CH correspondence
> which relates in an amazing way logic and computer science.
>
> Do you know Jean-Louis Krivine? A french logician who try to extend
> the CH (Curry Howard) isomorphism on classical logic and set theory. I
> am not entirely convinced by the details but I suspect something quite
> fundamental and important for the future of computer science and logic.
> You can take a look, some of its paper are in english.
> http://www.pps.jussieu.fr/~krivine/
> Jean-Louis Krivine wrote also my favorite book in set theory.
> The CH correspondence of the (classical) Pierce law as a comp look!
>
> Don't hesitate to send us link to anything relating computer science
> and logic (like the Curry-Howard isomorphism), because, although I
> doubt it can be used easily in our framework, in a direct way, it
> could have some impact in the future. Category theory is a very nice
> subject too, but is a bit technically demanding at the start. Yet, it
> makes possible to link knot theory, quantum computation, number
> theory, gravity, ...
> Not yet consciousness, though. Intensional free mathematics still
> resist ...
>
>
>>
>>
>> In fact, I originally joined this list hoping for a logic-oriented
>> mailing list. I haven't been entirely disappointed there,
>
> You are kind!
>
>
>> but at the
>> same time that isn't what this list is really intended for.
>
> Logic is a very interesting field. Too bad it is not so well known by
> the large public. The everything list is more "theory of everything"
> oriented. Logic has a big role to play, (assuming comp) but physics,
> cognitive science and even "theology" can hardly be avoided in a truly
> unifying quest ... And we try to be as less technic as possible, which
> is for me very hard, ... oscillating between UDA and AUDA.
>
> Best,
>
> Bruno
>
>
>
> http://iridia.ulb.ac.be/~marchal/
>
>
>
>
> >
>
--
Abram Demski
http://dragonlogic-ai.blogspot.com/
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to everything-list.domain.name.hidden
To unsubscribe from this group, send email to everything-list+unsubscribe.domain.name.hidden
For more options, visit this group at http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Mon May 18 2009 - 15:53:57 PDT