Re: logic mailing list

On 18 May 2009, at 21:53, Abram Demski wrote:

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@.../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.

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.

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