4
$\begingroup$

I've always had this question nagging at me subconsciously but have never been able to intuitively grasp it. Why does $\lambda$-calculus have a functional notation? Why is everything a function?

It seems it has something to do with the evolution of Logic (See History of the Function Concept) and trying to "nail down" what was really meant by a function. Going through the history - FO-logic, intuitionistic logic, combinatory logic, lambda calculus etc., I still am a bit unsure about why did Church go with the function-oriented view of things. I know he was trying to work on a system for foundations of logic/math which led to the creation of $\lambda$-calculus. But what I wish to understand is his thinking and reasoning that led to the use of functions as the vehicle of choice, for getting there.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ What other choice would there have been? It was long before the invention of object-orientation. $\endgroup$
    – Dave Clarke
    Feb 22, 2015 at 7:43
  • $\begingroup$ @DaveClarke And Turing machines were either not yet "invented" or very new, so it wouldn't have been obvious that some sense of "algorithm" might make a good alternative to function. $\endgroup$
    – David Richerby
    Feb 22, 2015 at 9:40
  • 2
    $\begingroup$ Rather than thinking of it in terms of functions, you could understand it in terms of variables. The lambda calculus nails down the general notion of a variable in mathematics and operations performed with variables such as substitution. $\endgroup$
    – Vijay D
    Feb 23, 2015 at 2:55
  • $\begingroup$ @DavidRicherby, Turing machines are several years younger than lambda calculus. $\endgroup$
    – ibid
    Feb 23, 2015 at 7:39
  • $\begingroup$ @DavidRicherby, the lambda calculus was first published in 1932, and I believe it was at that point alredy several years old. That makes Turing machines much younger, as I said. $\endgroup$
    – ibid
    Feb 23, 2015 at 8:27

3 Answers 3

Reset to default
7
$\begingroup$

The idea of how to 'mechanize mathematical proof' was a hot topic at the time; more specifically, Hilbert posed the Entscheidungsproblem - could we have a machine in some factory somewhere that takes mathematical statements in, and outputs proofs of the truth or falseness of those statements, as easily as machines might weave cotton or drill holes in steel?

If one was 'merely' dealing with the mathematical concept of a function, then we can define such a function whose input is a mathematical statement (formally, a first order sentence in the language of number theory) and whose output is either 'True' or 'False'.

This is perfectly satisfactory as a mathematical function (once one has properly defined what it means for a statement to be true or false) but now one has a constructibility problem; the mere existence is not useful when your main goal is to actually evaluate this function on given inputs.

The purpose of the lambda calculus, and equivalent models such as Turing machines, is to provide this construction. When a mathematical function matches the input/output behavior of a Turing machine, or (equivalently) has a representation in terms of the lambda calculus, then such a function is called 'computable'.

Gödel's Incompleteness Theorem states that the true/false function described above is not computable. It is generally believed that the only mathematical functions that can be evaluated in the 'real world' are exactly the computable ones (this is the Church-Turing Thesis). Therefore, despite existing as a mathematical function, we have absolutely no way to evaluate that function in general (of course, there are still specific inputs where we can evaluate that function)

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ Gödel's Incompletness theorem is not about computability, it is about completeness. If it were, there would not have been any work to be done for Church and Turing. $\endgroup$
    – ibid
    Feb 23, 2015 at 7:37
  • 4
    $\begingroup$ @ibid Gödel's incompleteness theorem is a theorem of computability. That's because it's a theorem about provability: it states that there are formulas in Peano arithmetic which cannot be proven nor disproved, i.e. there are formulas for which is not possible to compute a proof of the formula or of its negation. The proof of Gödel's theorem make use of computability theory: it was this problem that made him build the concept of primitive recursive functions. Church and Turing's work was aimed to decidability of logic, which is a related but different problem. $\endgroup$
    – Giorgio Mossa
    Feb 23, 2015 at 9:52
  • 2
    $\begingroup$ One of the brilliant insights of that era was that, once your language is 'expressive enough', completeness and computability become mutually exclusive. If we ignore computability, then completeness is always automatic: just choose all true statements as axioms! $\endgroup$
    – Joe Bebel
    Feb 25, 2015 at 6:49
3
$\begingroup$

I do not know of a source that would allow me to state why Church went for functions. All I can state with confidence is that the concept of a function was of significant interest and controversy at the time. This was, recall, before Gödel proved it impossible to formalize mathematics completely, and a lot of effort was poured in developing a consistent and complete formal system that could handle all of mathematics. Functions are a pretty big part of math.

This goes a bit afar from your question, but I believe this needs to be said, in light of the comments and the other answer: For many years, it was by no means obvious that the lambda calculus could be powerful enough to model computability (and I believe nobody even considered that it could). Eventually, the usual Church encodings were discovered, which led Church to posit that lambda calculus actually does model all effectively calculable functions. At least Gödel was not convinced. It was after Turing had published his machine (the correspondence of which with effective calculability is easy to argue for) and proved it equally capable to lambda calculus that what was later called Church's thesis was taken seriously by all.

Some papers on the history:

  • J. Barkley Rosser: Highlights of the History of the Lambda-Calculus. Annals of the History of Computing 6(4), 337-349, 1984. link
  • Felice Cardone and J. Roger Hindley: History of Lambda-Calculus and Combinatory Logic. A Chapter of "Handbook of the History of Logic" volume 5, 2006. manuscript available online
  • Robert I. Soare: Computability and Recursion. Bulletin of Symbolic Logic 2(3), 284-321, 1996. link
  • Robert I. Soare: Computability and Incomputability. Computation and Logic in the Real World, LNCS 4497, 705-715, 2007. link
Improve this answer
$\endgroup$
1
$\begingroup$

This is just a very long comment to Joe Babel answer above.

As said above Church invented $\lambda$-calculus to approach the Entscheidungsproblem (i.e. the decision problem for first-order logic) which asked whether it was possible to provide an effective (i.e. computable) method that for a given input formula can either prove or disprove the formula.

In order to solve this problem it was necessary to define what computable means: Church gave a definition in term of computable functions which are called $\lambda$-terms. I guess that this choice was motivated by the intuitive notion of computation that they have at time: a computation as a process which takes some input and return some output, which is exactly the concept of function.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.