13
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 12, 2015 at 4:50
  • 2
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 12, 2015 at 4:55
  • 1
    $\begingroup$ 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) $\endgroup$
    – dspyz
    Feb 12, 2015 at 22:09
  • 1
    $\begingroup$ Smullyans book is about combinatory logic $\endgroup$
    – Trismegistos
    Feb 24, 2015 at 10:44

2 Answers 2

Reset to default
22
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ If firewalking is as fun as you say, then I must to try it. $\endgroup$
    – Radu GRIGore
    Feb 12, 2015 at 8:45
  • $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 12, 2015 at 9:42
  • 3
    $\begingroup$ 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 books.google.si/… $\endgroup$
    – Andrej Bauer
    Feb 12, 2015 at 10:01
6
$\begingroup$

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.

Improve this answer
$\endgroup$

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.