<p>The idea of how to 'mechanize mathematical proof' was a hot topic at the time; more specifically, Hilbert posed the <em>Entscheidungsproblem</em> - 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?</p>

<p>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'. </p>

<p>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 <em>constructibility</em> problem; the mere existence is not useful when your main goal is to actually evaluate this function on given inputs.</p>

<p>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'. </p>

<p>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 <em>specific</em> inputs where we can evaluate that function)</p>

CC BY-SA 3.0
2015-02-23T07:37:48.263Z
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.
ibid
CC BY-SA 3.0
2015-02-23T09:52:16.707Z
@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.
Giorgio Mossa
CC BY-SA 3.0
2015-02-25T06:49:51.847Z
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!
Joe Bebel
CC BY-SA 3.0
2015-02-22T06:24:44.300Z
2015-02-22T06:24:44.300Z
Joe Bebel
<p>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.</p>

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

<p>Some papers on the history:</p>

<ul>
<li>J. Barkley Rosser: Highlights of the History of the Lambda-Calculus. Annals of the History of Computing 6(4), 337-349, 1984. <a href="http://dx.doi.org/10.1109/MAHC.1984.10040" rel="nofollow">link</a></li>
<li>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.  <a href="http://www.pps.univ-paris-diderot.fr/~saurin/Enseignement/LMFI/articles/HindleyCardone06.pdf" rel="nofollow">manuscript available online</a></li>
<li>Robert I. Soare: Computability and Recursion.  Bulletin of Symbolic Logic 2(3), 284-321, 1996. <a href="http://www.jstor.org/stable/420992" rel="nofollow">link</a></li>
<li>Robert I. Soare: Computability and Incomputability.  Computation and Logic in the Real World, LNCS 4497, 705-715, 2007. <a href="http://dx.doi.org/10.1007/978-3-540-73001-9_75" rel="nofollow">link</a></li>
</ul>

CC BY-SA 3.0
2015-02-23T08:23:43.717Z
2015-02-23T08:23:43.717Z
ibid
<p>This is just a very long comment to Joe Babel answer above.</p>

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

<p>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 <em>computation</em> as a process which takes some input and return some output, which is exactly the concept of function.</p>

CC BY-SA 3.0
2015-02-23T15:21:27.770Z
2015-02-23T15:21:27.770Z
Giorgio Mossa
<p>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 <em>functional</em> notation? Why is everything a function?</p>

<p>It seems it has something to do with the evolution of Logic (See <a href="http://en.wikipedia.org/wiki/History_of_the_function_concept#The_logicians.27_.22function.22_1850.E2.80.931950" rel="nofollow">History of the Function Concept</a>) and trying to "nail down" what was really meant by a <em>function</em>. 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 <em>function-oriented</em> 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 <em>functions</em> as the vehicle of choice, for getting there. </p>

CC BY-SA 3.0
2015-02-22T07:43:32.280Z
What other choice would there have been? It was long before the invention of object-orientation.
Dave Clarke
CC BY-SA 3.0
2015-02-22T09:40:23.207Z
@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.
David Richerby
CC BY-SA 3.0
2015-02-23T02:55:28.463Z
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.
Vijay D
CC BY-SA 3.0
2015-02-23T07:39:37.957Z
@DavidRicherby, Turing machines are several years younger than lambda calculus.
ibid
CC BY-SA 3.0
2015-02-23T08:27:24.557Z
@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.
ibid
<soft-question><big-picture><lambda-calculus><ho.history-overview><intuition>
Why is lambda calculus so "function" oriented?
PhD
# Why is lambda calculus so "function" oriented?

(Asked by: username_0 on 2015-02-18)

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](http://en.wikipedia.org/wiki/History_of_the_function_concept#The_logicians.27_.22function.22_1850.E2.80.931950)) 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.

**Tags:** soft-question, big-picture, lambda-calculus, ho.history-overview, intuition
> **Comments:**
> **username_1**: What other choice would there have been? It was long before the invention of object-orientation.  
> **username_2**: @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.  
> **username_3**: 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.  
> **username_4**: @DavidRicherby, Turing machines are several years younger than lambda calculus.  
> **username_4**: @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.  

---

## 3 answers

### Answer by username_5 on 2015-02-22. Score: 7

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)

> **Comments:**
> **username_4**: 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.  
> **username_6**: @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.  
> **username_5**: 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!  

---

### Answer by username_4 on 2015-02-23. Score: 3

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](http://dx.doi.org/10.1109/MAHC.1984.10040)
* 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](http://www.pps.univ-paris-diderot.fr/~saurin/Enseignement/LMFI/articles/HindleyCardone06.pdf)
* Robert I. Soare: Computability and Recursion. Bulletin of Symbolic Logic 2(3), 284-321, 1996. [link](http://www.jstor.org/stable/420992)
* Robert I. Soare: Computability and Incomputability. Computation and Logic in the Real World, LNCS 4497, 705-715, 2007. [link](http://dx.doi.org/10.1007/978-3-540-73001-9_75)


---

### Answer by username_6 on 2015-02-23. Score: 1

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.


---

