Re: Help with Lambda Calculus

kunjaan <kunjaan@xxxxxxxxx> wrote:
| But what I am confused is that if a function gets another function and
| an argument and just returns the argument, how can that be 0? It still
| has something in it, right?

Others have discussed Church numerals at length, so I won't comment
further about that except to point you here, especially to the section
on "Translation with other representations":

| It is just so counter intuitive.

Well, yes. There nothing particularly "intuitive" (or useful!) about
pure lambda calculus. It's just a formalism (a "calculus") that permits
certain axioms to be stated and certain theorems to be proved, especially
about computability or recursion theory, see:

Note that despite their claims to being "based on" the lambda calculus,
Lisp & Scheme are actually quite far from the original untyped lambda
calculus that inspired them, using as they do quite traditionally encoded
dynamically-typed values, and allowing mutation. [The earliest Lisps
even used only dynamic scope for variables, which is *definitely* not
the case in the lambda calculus!! Fortunately, Scheme & CL fixed that.]

So if you're studying lambda calculus for a course in computability
theory, my advice would be to just put aside your questions about
why Church numerals are used there -- they just are, because it's
traditional to do so. That's what your professor will expect you
to use in the proofs you turn in.

On the other hand, if you're studying lambda calculus in order to
learn something about programming in Scheme or Common Lisp or ML
or Haskell, etc., then I'd say to put aside your curiosity about
the precise details of formal lambda calculus and just study the
syntax/semantics of the particular language in which you plan to
be coding, since the lambda calculus has very little to do with
the day-to-day practicalities of programming.

On the third hand, a cursory overview of lambda calculus *is* a
useful thing to have in the intellectual arsenal of *any* programmer
[e.g., the notions of closures & currying & combinators and when
and when not to use them], if you don't take it too far. ;-}


Rob Warnock <rpw3@xxxxxxxx>
627 26th Avenue <URL:>
San Mateo, CA 94403 (650)572-2607


Relevant Pages

  • Re: My take on ARC
    ... > quixotic one because it invariably leads you to the lambda calculus. ... to find a "sweet spot" that balances expressivity and minimalism. ... improvements over the original formula for common programming idioms. ... here in minneapolis the moment the word "Lisp" crosses my mouth ...
  • Re: CAS, Lambda Calculus, Continuation and Functional Programming
    ... >> the programming style of symbolic math packages as partly functional ... see that I strive to learn the language which we use to understand the ... languages don't have recursion. ... Thus it doesn't seem to me that lambda calculus if fully implemented ...
  • Re: Trying to remember ....
    ... operations of scheme and lisp could be reduced to a very small ... The keyword for search is "combinatory logic", ... "lambda calculus" would also lead there. ...
  • Re: Lambda calculus numerals book recommendation?
    ... > I am devouring what I can find about the lambda calculus. ... > particularly interested in the numerals aspect, writing computable ... > functions in lambda calculus using numerals, ... programming in lambda calculus is a lot like functional ...
  • Re: Why dont we have "C" machines? (was Re: [OT] Re: Should *most* memory be release back to the sys
    ... Lisp and Scheme are at their core functional languages based on the lambda calculus with "enough" imperative features, macros and side effects to get work done. ...