Bruno,
> What are those proofs doing, as program, is still rather
> mysterious, and it is a subject in development.
This is what makes the use of such things hard to understand for me. :) Ah well.
I suppose the correspondance is useful in establishing the
computational complexity (and computability where that is in question)
of type checking?
--Abram
On Thu, May 28, 2009 at 4:07 PM, Bruno Marchal <marchal.domain.name.hidden> wrote:
>
> Abram,
>
>>
>> Bruno,
>>
>> I knew already about combinators, and the basic correspondence between
>> arrow-types and material conditionals. If I recall, pairs correspond
>> to &, right? I do not yet understand about adding quantifiers and
>> negation.
>>
>> Still, I do not really see the usefulness of this. It is occasionally
>> invoked to justify the motto "programs are proofs", but it doesn't
>> seem like it does any such thing.
>
>
> The interesting part, which is particularly amazing concerning
> classical logic is not the (quasi-trivial) fact that programs are
> proofs, but that all proofs are programs. All proof becomes program,
> even non constructive proofs, when the CH is extended to classical
> logic. What are those proofs doing, as program, is still rather
> mysterious, and it is a subject in development. But I am a bit out of
> this in the moment. I intend to come back sometime.
> Apparently they provide neat semantics for GOTO instruction, TRY
> CATCH, handling of error, continuation passing, etc.
>
> Bruno
>
>
>
>
>
>> On Tue, May 19, 2009 at 11:25 AM, Bruno Marchal <marchal.domain.name.hidden>
>> wrote:
>>> Hi Abram,
>>>
>>> On 18 May 2009, at 21:53, Abram Demski wrote:
>>>
>>> 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.
>>>
>>> Let me give the shorter and simple example. Do you know the
>>> combinators? I
>>> have explained some time ago on this list that you can code all
>>> programs in
>>> the SK combinator language. The alphabet of the language is "(",
>>> ")", K S.
>>> Variables and equality sign "=" are used at the metalevel and does
>>> not
>>> appear in the program language.
>>> The syntax is given by the (meta)definition:
>>> K is a combinator
>>> S is a combinator
>>> if x and y are combinators then (x y) is a combinator.
>>> The idea is that all combinators represent a function of one
>>> argument, from
>>> the set of all combinators in the set of all combinators, and ( x y)
>>> represents the result of applying x to y. To increase readability
>>> the left
>>> parenthesis are not written, so ab(cd)e is put for ((((a b) (c d)) e)
>>> So example of combinators are: K, S, KK, KS, SK, SS, KKK, K(KK),
>>> etc.
>>> Remember that KKK is ((KK)K).
>>> The (meta)axioms (or the scheme of axioms, with x and y being any
>>> combinators) are
>>> Kxy = x
>>> Sxyz = xz(yz)
>>> If you give not the "right" number of argument, the combinators
>>> give the
>>> starting expression (automated currying): so SK gives SK, for
>>> example. But
>>> KKK gives K, and SKSK gives KK(SK) which gives K. OK?
>>> The inference rule of the system are simply the equality rule: from
>>> x = y
>>> you can deduce y = x, and from x = y and y = z you can deduce x = z,
>>> together with: from x = y you can deduce xz = yz, and, from x = y
>>> you can
>>> deduce zx = zy.
>>> This gives already a very powerful theory in which you can prove all
>>> Sigma_sentences (or equivalent). It defines a universal dovetailer,
>>> and
>>> adding some induction axioms gives a theory at least as powerful as
>>> Peano
>>> Arithmetic.
>>> See my Elsevier paper Theoretical computer science and the natural
>>> sciences
>>> for a bit more. Or see
>>> http://www.mail-archive.com/everything-list.domain.name.hidden/msg05920.html
>>> and around.
>>> The Curry Howard isomorphism arrives when you introduce types on the
>>> combinators. Imagine that x is of type a and y is of type b, so that
>>> a combinator which would transform x into y would be of type a -> b.
>>> What is the type of K? (assuming again that x if of type a and y is
>>> of type
>>> b). You see that Kx on y gives x, so K take an object of type a,
>>> (x), and
>>> transforms it into an object (Kx) which transform y in x, so K
>>> takes an
>>> object of type a, and transform it into an object of type (b -> a),
>>> so K is
>>> of type
>>> a -> (b -> a)
>>> And you recognize the "well known" a fortiori axioms of classical
>>> (and
>>> intuitionistic) logic. If you proceed in the same way for S, you
>>> will see
>>> that S is of type
>>> (a -> (b -> c)) -> ((a -> b) -> (a -> c))
>>> And you recognize the arrow transitivity axiom, again a classical
>>> logic
>>> tautology (and a well accepted intuistionistic formula). So you see
>>> that
>>> typing combinators gives propositional formula. But something else
>>> happens:
>>> if you take a combinator, for example the simplest one, I, which
>>> compute the
>>> identity function Ix = x. It is not to difficult to "program" I
>>> with S and
>>> K, you will find SKK (SKKx = Kx(Kx) = x). Now the step which leads
>>> to the
>>> program SKK, when typed, will give the (usual) proof of the
>>> tautology a -> a
>>> from the a fortiori axiom and the transitivity axiom. The rules
>>> works very
>>> well for intuitionistic logic associating type to logical formula,
>>> and proof
>>> to programs. The application rule of combinators correspond to the
>>> modus
>>> ponens rule, and the deduction theorem correspond to lambda
>>> abstraction. It
>>> leads thus to a non trivial and unexpected isomorphism between
>>> programming
>>> and proving.
>>> For a long time this isomorphism was thought applying only to
>>> intuitionistic
>>> logic, but today we know it extends on the whole of classical logic
>>> and
>>> classical theories like set theory. Typical classical rule like
>>> Pierce
>>> axioms ((a -> b) -> a) -> a) gives try-catch error handling
>>> procedure, and
>>> Krivine seems to think that Gödel's theorem leads to decompiler
>>> (but this I
>>> do not yet understand!). This gives constructive or partially
>>> constructive
>>> interpretation of logical formula and theorems, and this is a
>>> rather amazing
>>> facts.
>>>
>>>
>>>
>>>
>>> In the end, I don't really see any *use* to the
>>> curry-howard isomorphism!
>>>
>>> I thought a long time that it can be used only in program
>>> specification and
>>> verification analysis in conventional programming, but the fact
>>> that the CH
>>> iso extends to classical logic forces me to revise my opinion.
>>> Krivine seems
>>> to believe it transforms the field of logic into a study of the
>>> brain as a
>>> decompiler or desassembler of platonia (to be short). And I think
>>> he could
>>> be near a deep discovery. I am searching the CH for the modal
>>> logics, but I
>>> get trapped in technical difficulties, and l am not sufficiently
>>> familiar
>>> with the notion of typing, in general.
>>>
>>>
>>> Sure, the correspondence is interesting, but
>>> what can we do with it? Perhaps you can answer this.
>>>
>>> The interest relies in the fact that the CH links two things which
>>> were
>>> studied by different logicians with different tools, in different
>>> ivory
>>> towesr, and now we know it is the same thing, basically. It is like
>>> in the
>>> Strings Theories, or in the link between knots and quantum
>>> computation. It
>>> is too much amazing for not having some significance, even if
>>> applications
>>> are not directly obvious (apart from program specification proving
>>> and
>>> verifying).
>>> CH with combinators links Hilbertian logic and programs. CH with
>>> lambda
>>> terms links natural deduction system and programs. I think CH links
>>> sequent
>>> calculus and category theory. In the whole CH links logic with
>>> computation
>>> theory.
>>> I hope this could open your logical appetite,
>>> Bruno
>>>
>>> http://iridia.ulb.ac.be/~marchal/
>>>
>>>
>>>
>>>>
>>>
>>
>>
>>
>> --
>> Abram Demski
>> http://dragonlogic-ai.blogspot.com/
>>
>> >
>
> 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 Thu May 28 2009 - 18:30:41 PDT