FOUNDATIONS OF COMBINATORY LOGIC IBD

Sinopsis

Curry',s PhD dissertation áIntroduction to Combinatory Logic, represents a first major work on a new subject. áCurry',s interest in the subject started when he noticed the complicated form of substitution in Principia Mathematica and set about trying á to find a simpler form áof this rule. This led him by 1926 to some of the combinators. In 1928 Curry went to G ottingen and completed his dissertation in 1929 under the direction of David Hilbert. áThis book is a translation of the dissertation.ááCurry',s dissertation was the first publication to give a complete formal ádevelopment of combinatory logic as a formal system in which the terms are built up from ávariablesáand a number of áconstants (combinators including B, Cáand K) by means of application. The proof of the consistency of the system faced the ámajor difficulty áthat the only reduction relation Curry had was what we now call weak reduction. áThis made it impossible to prove the Church-Rosser Theorem, which is now the standard way one proves the consistency of systems of this kind. áInstead, Curry was looking at sequences based on what we now call weak contractions with strings of variables added on the right.áAfter his dissertation, Curry developed further ground-breaking ideas áthat continue to be very influential. áThese include, functionalityá(which became the basis of what we now call type assignment), the correspondence between types and implication formulas á(the beginning of the idea of propositions as types) and generalised functionality (a form of ádependent types in modern type systems). á áCurry',s ideas continue to influence developments in mathematics, logic and computation. áWe hope that making his original thesis available in English will help make his ideas clearer.áWe have made use of all information we could find by Curry, mostly from marginal notes in his copy of the dissertation, indicating corrections to the original German.