[rntz]

> Also, recursion arises in a different form in lambda calculus than it does in the approach to computability that is based on general recursive functions. Again, I think that LISP is closer to Gödel here than to Church.

I think I understand most of the rest of your post, but I got lost here. Could you describe what difference you see here, and how it applies to LISP?

[ericbb]

When I mentioned "general recursive functions", I was thinking about systems that define functions using a system of functional equations rather than using a lambda term.

Example:

    odd 0 = False
    odd n = even (n - 1)
    even 0 = True
    even n = odd (n - 1)

I think "rewriting system" is something similar. (I'm not an expert in this stuff so I'm providing hints for further reading more than anything else).

In these systems, recursion is "built in" to the formal language itself.

On the other hand, lambda calculus does not have recursion "built in". All variables are bound by function application so it is not possible to have recursive bindings like you see in these recursive function systems. You can define recursive functions using mechanisms like the Y combinator but these work by reconstructing something over and over as the computation evolves. It's different.

In McCarthy's paper, there is a system of toplevel recursive functions and there is a LABELS form that behaves in a similar way. Lambda calculus has neither of these.

One resource that describes recursive function systems of the kind I'm thinking of is the book "Lambda-Calculus and Combinators, an Introduction" by Hindley and Seldin (especially chapter 4).