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