[ericbb]

> `lambda` and function application alone are Turing-complete, as McCarthy would have known. The credit here belongs with Turing and Church, not McCarthy. `atom`, `cons`, `car` and all the rest are just icing on the cake of the lambda calculus when it comes to computability.

This point reminds me of something interesting that I noticed recently despite having been familiar with basic LISP ideas for a long time.

If you carefully read McCarthy's original presentation of LISP, you can see that he seemed to be influenced at least as much by Kurt Gödel's work as by Alonzo Church's work.

In Church's lambda calculus, functions are abstract values that can only be used by means of function application. LISP evolved toward this style over time, but in the early history of LISP, functions were not abstract values but were represented by encoding into S-expressions. This encoding process resembles Gödel numbering.

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.

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