Well, in 1936 Church invented the LC in order to serve as a foundational logic for mathematics. This was around the time that Hilbert's Program was attempting t

Well, in 1936 Church invented the LC in order to serve as a foundational logic for mathematics. This was around the time that Hilbert's Program was attempting to totally mechanize reasoning through rich logical languages and Church wanted to use LC to define the notion of "efficiently computable" which was part of Hilbert's specification. The Y-combinator was discovered originally as a flaw in the LC. It meant that you couldn't use LC as a logical language because you could form infinite loops which are not just not efficiently computable (in a sense, har har) but also correspond to vacuous logical statements like "If A proves A then A is true" which, in the context of rules like reflexivity "If A then A" (provable in LC as λ x . x) is logical nonsense. To be more clear, here's the Y combinator λ f . (λ x . f (x x)) (λ x . f (x x)) and here's the Y-combinator applied to `id = λ x . x` (λ x . (x x)) (λ x . (x x)) which reduces into itself—a dead loop and a logical inconsistency (named "omega" as the end of LC!) Anyway, Church worked for the next 4 years to invent the Simply Typed Lambda Calculus which imposes a Russell-like typing discipline on the LC in order to outlaw the Y-combinator. This made LC more useful for logic (and indeed STLC models Gentzen's Natural Deduction logical system) but it threw away its ability to compute any "recursively enumerable" function. That latter thing was what eventually came to be the definition of "efficiently computable" (after corroboration between Church's LC, Turing's Turing Machines invented the next year). And now we happen to care about writing programs which, in general, may be r.e. and so we use either untyped LC or typed LC which has logically unsound recursion principles.