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 <[email protected]> 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 <[email protected]> >> 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/[email protected]/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 [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---
