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/




--~--~---------~--~----~------------~-------~--~----~
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
-~----------~----~----~----~------~----~------~--~---

Reply via email to