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/
--~--~---------~--~----~------------~-------~--~----~
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 Tue May 19 2009 - 17:25:14 PDT