Re: Help with Lambda Calculus


On Sun, 27 Sep 2009 19:10:35 -0500, rpw3@xxxxxxxx (Rob Warnock) said:

kunjaan <kunjaan@xxxxxxxxx> wrote:
...
+---------------
| 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

In any case treatments of computability need to be based on
something that is _simple_, not necessarily intuitive, so that it is
clear, if not self-evident, that a _machine_ can perform the
respective primitive operations (the reductions in lambda-calculus,
or the application of tape-rewriting and state-changing rules in a
Turing machine, etc.).

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

One reason why Church numerals are there is to show that recursive
functions can be implemented on top of lambda-calculus [*], which is
part of the proof of one of the central results of theory of
computability, namely that all known definitions of algorithm are
equivalent (and thus part of the support for the Church-Turing
thesis).

_________
[*] Recursive functions map natural numbers to natural numbers,
therefore a representation of the latter by means of the
constructs of lambda-calculus is needed.

---Vassil.


--
"Even when the muse is posting on Usenet, Alexander Sergeevich?"
.

Relevant Pages

  • Re: Lambda calculus numerals book recommendation?
    ... I haven't heard of 'numerals', ... Typed Church numerals are peculiar - you get the whole range of Church ... I don't know why Sander is talking about function Y here, recursion is ... taken for granted in application oriented lambda calculus, ...
    (sci.logic)
  • Re: is forth a functional language?
    ... One can regard the Y-combinator as a kind of recursion (or at ... But neither the simply type lambda lambda calculus nor the second order ... Now I really don't know what you mean by pure program. ...
    (comp.lang.functional)
  • A lambda calculus puzzle
    ... Church Numerals are a way of representing numbers as iterated functions in the lambda calculus. ... The value of the following lambda calculus expression is also a Church Numeral: ...
    (comp.lang.scheme)
  • Re: A lambda calculus puzzle
    ... Church Numerals are a way of representing numbers as iterated functions in the lambda calculus. ... The value of the following lambda calculus expression is also a Church Numeral: ...
    (comp.lang.scheme)
  • Re: What is math? And my thoughts...
    ... but for example Church numerals can express all positive natural ... Church numerals based on lambda calculus formal language ... 'mathematics' is best put so narrowly as to be confined to formal ...
    (sci.math)