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/
--~--~---------~--~----~------------~-------~--~----~
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 - 22:07:39 PDT