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

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.


On Tue, May 19, 2009 at 11:25 AM, Bruno Marchal <> 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
> 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
> >

Abram Demski

You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To post to this group, send email to
To unsubscribe from this group, send email to
For more options, visit this group at

Reply via email to