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 <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/
--~--~---------~--~----~------------~-------~--~----~
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 Wed May 20 2009 - 14:08:54 PDT