<p>You program in it! Take a look at <a href="http://en.wikipedia.org/wiki/Church_encoding">church encodings</a>. You can see how pretty much all arithmetic can be performed which should probably convince you that it is extremely powerful. I like to look at operations on lists however. You can define most any data structure in terms of a function that does the most important operation on it.</p>

<p>For instance an encoding of a list is the fold function that folds over it. Note this is not Church's encoding but one I got from Percie's types and programming languages. Church's pair encodings do not give us recursion we have to add it back in ourselves with some kind of recursion combinator.</p>

<p>so a list takes two arguments, a function to do the folding, and a initial value to plug into the fold at some point.</p>

<pre><code>cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a
</code></pre>

<p>now we can define a summation given an add function (see church encodings from above)</p>

<pre><code>sum xs = xs add 0
</code></pre>

<p>we can do more and define a map function</p>

<pre><code>consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil
</code></pre>

<p>if you are still not convinced that there is computation going on here and want to make sure that you can perform any computation then check out <a href="http://en.wikipedia.org/wiki/Fixed-point_combinator">the fixed point combinator</a>. It hurts my head a bit to think about sometimes however so I'm not sure I would call it intuitive but if you manually evaluate it with some arguments you can see what is going on.</p>

CC BY-SA 3.0
2015-02-12T05:36:45.077Z
2015-02-12T05:36:45.077Z
Jake
<p>You're in good company. Kurt Gödel criticized $\lambda$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it is not intuitive, or that it does not sufficiently explain what is going on. In contrast, he found Turing's analysis of computability and the ensuing notion of machine totally convincing. So, don't worry.</p>

<p>On the other hand, to get some idea on how a model of computability works, it's best to write some programs in it. But you do not have to do it in pure $\lambda$-calculus, although it's fun (in the same sort of way that firewalking is). You can use a modern descendant of $\lambda$-calculus, such as Haskell.</p>

CC BY-SA 3.0
2015-02-12T08:45:22.410Z
If firewalking is as fun as you say, then I _must_ to try it.
Radu GRIGore
CC BY-SA 3.0
2015-02-12T09:42:10.640Z
Andrej, do you know any reference for these? Godel didn't accept Chruch's model as capturing _all_ commutable functions but I don't remember seeing anywhere that he criticized the model much further than that. His criticism of Church's lambada calculus model was on par with his criticism of his own Godel-Herbrand general recursive functions as far as I know.
Kaveh
CC BY-SA 3.0
2015-02-12T10:01:05.587Z
I think you want K. Godel: "Some Remarks on the Undecidability Results", In Solomon Feferman, John Dawson & Stephen Kleene (eds.), Kurt Gödel: Collected Works Vol. Ii. Oxford University Press. 305--306 (1972). See https://books.google.si/books?id=lgDGTYNcOY4C&lpg=PA305&ots=SEawOHK0Nd&dq=Godel%2C%20Kurt%20%E2%80%9CSome%20Remarks%20on%20the%20Undecidability%20Results%E2%80%9D%2C&pg=PA305#v=onepage&q&f=false
Andrej Bauer
CC BY-SA 3.0
2015-02-12T07:07:50.590Z
2015-02-23T04:12:27.697Z
2015-02-23T04:12:27.697Z
Andrej Bauer
<p>I've been trying to wrap my head around the what, why and how of $\lambda$-calculus but I'm unable to come to grips with "why does it work"?</p>

<p>"Intuitively" I get the computability model of Turing Machines (TM). But this $\lambda$-abstraction just leaves me confounded. </p>

<p>Let's assume, TMs don't exist - then how can one be "intuitively" convinced about $\lambda$-calculus's ability to capture this notion of computability. How does having a bunch of functions for everything and their composobility imply computability? What am I missing here? I read Alonzo Church's paper on that but I'm still confused and looking for a more "dummed down" understanding of the same. </p>

CC BY-SA 3.0
2015-02-12T04:50:26.243Z
Do you have the same issue with rewriting systems and grammars? In lambda calculus the basic operations are quite simple: function abstraction, function application by substitution, and computation is beta normalization. In other words, I don't see what your problem with it being a reasonable model of computation.
Kaveh
CC BY-SA 3.0
2015-02-12T04:55:14.343Z
I haven't seen anyone doubt that lambda calculus definable functions are computable. Historically the question was if these are the only intuitively computable functions, which is a completely different issue from what you seem to ask.
Kaveh
CC BY-SA 3.0
2015-02-12T22:09:55.980Z
One thing that I found helpful was Raymond M Smullyan's book, "To Mock a Mockingbird" which replaces functions with birds in a magic forest (and is a good read)
dspyz
CC BY-SA 3.0
2015-02-24T10:44:06.337Z
Smullyans book is about combinatory logic
Trismegistos
<soft-question><computability><lambda-calculus><ho.history-overview><intuition>
How exactly does lambda calculus capture the intuitive notion of computability?
PhD
# How exactly does lambda calculus capture the intuitive notion of computability?

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

I've been trying to wrap my head around the what, why and how of $\lambda$-calculus but I'm unable to come to grips with "why does it work"?

"Intuitively" I get the computability model of Turing Machines (TM). But this $\lambda$-abstraction just leaves me confounded.

Let's assume, TMs don't exist - then how can one be "intuitively" convinced about $\lambda$-calculus's ability to capture this notion of computability. How does having a bunch of functions for everything and their composobility imply computability? What am I missing here? I read Alonzo Church's paper on that but I'm still confused and looking for a more "dummed down" understanding of the same.

**Tags:** soft-question, computability, lambda-calculus, ho.history-overview, intuition

> **Comments:**
> **username_1**: Do you have the same issue with rewriting systems and grammars? In lambda calculus the basic operations are quite simple: function abstraction, function application by substitution, and computation is beta normalization. In other words, I don't see what your problem with it being a reasonable model of computation.  
> **username_1**: I haven't seen anyone doubt that lambda calculus definable functions are computable. Historically the question was if these are the only intuitively computable functions, which is a completely different issue from what you seem to ask.  
> **username_2**: One thing that I found helpful was Raymond M Smullyan's book, "To Mock a Mockingbird" which replaces functions with birds in a magic forest (and is a good read)  
> **username_3**: Smullyans book is about combinatory logic  

---

## 2 answers

### Answer by username_5 on 2015-02-12. Score: 22 | Accepted answer

You're in good company. Kurt Gödel criticized $\lambda$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it is not intuitive, or that it does not sufficiently explain what is going on. In contrast, he found Turing's analysis of computability and the ensuing notion of machine totally convincing. So, don't worry.

On the other hand, to get some idea on how a model of computability works, it's best to write some programs in it. But you do not have to do it in pure $\lambda$-calculus, although it's fun (in the same sort of way that firewalking is). You can use a modern descendant of $\lambda$-calculus, such as Haskell.

> **Comments:**
> **username_6**: If firewalking is as fun as you say, then I _must_ to try it.  
> **username_1**: Andrej, do you know any reference for these? Godel didn't accept Chruch's model as capturing _all_ commutable functions but I don't remember seeing anywhere that he criticized the model much further than that. His criticism of Church's lambada calculus model was on par with his criticism of his own Godel-Herbrand general recursive functions as far as I know.  
> **username_5**: I think you want K. Godel: "Some Remarks on the Undecidability Results", In Solomon Feferman, John Dawson & Stephen Kleene (eds.), Kurt Gödel: Collected Works Vol. Ii. Oxford University Press. 305--306 (1972). See https://books.google.si/books?id=lgDGTYNcOY4C&lpg=PA305&ots=SEawOHK0Nd&dq=Godel%2C%20Kurt%20%E2%80%9CSome%20Remarks%20on%20the%20Undecidability%20Results%E2%80%9D%2C&pg=PA305#v=onepage&q&f=false  

---

### Answer by username_4 on 2015-02-12. Score: 6

You program in it! Take a look at church encodings. You can see how pretty much all arithmetic can be performed which should probably convince you that it is extremely powerful. I like to look at operations on lists however. You can define most any data structure in terms of a function that does the most important operation on it.
For instance an encoding of a list is the fold function that folds over it. Note this is not Church's encoding but one I got from Percie's types and programming languages. Church's pair encodings do not give us recursion we have to add it back in ourselves with some kind of recursion combinator.
so a list takes two arguments, a function to do the folding, and a initial value to plug into the fold at some point.
cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a

now we can define a summation given an add function (see church encodings from above)
sum xs = xs add 0

we can do more and define a map function
consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil

if you are still not convinced that there is computation going on here and want to make sure that you can perform any computation then check out the fixed point combinator. It hurts my head a bit to think about sometimes however so I'm not sure I would call it intuitive but if you manually evaluate it with some arguments you can see what is going on.


---

