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. --Abram On Tue, May 19, 2009 at 11:25 AM, Bruno Marchal <marc...@ulb.ac.be> 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@googlegroups.com/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/ --~--~---------~--~----~------------~-------~--~----~ 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@googlegroups.com To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---