I was going through the following paper: http://www-formal.stanford.edu/jmc/recursive.pdf

In the last part of the second section (at the end of page 7) he speaks about the inadequacy of lambda notion for naming functions described recursively.

The right hand side of the following expression $$\text{sqrt} = \lambda((a,x,\epsilon),(|x^2 -a|<\epsilon \to x,T \to\text{sqrt}(a,\frac{1}{2}(x+\frac{a}{x}),\epsilon)))$$ cannot serve as an expression of function because there would be nothing to indicate that the reference to $\text{sqrt}$ within the expression stood for the expression as a whole. I did not get what it meant. Why should there be a further indication that the expression stood for whole? Please explain this point.

  • $\begingroup$ Welcome to CS.SE! Can you edit the question to provide a reference to the paper that is more robust over time, and make it easier with others who have the same question to find this question? We have collected some advice here. Thank you! $\endgroup$ – D.W. Feb 17 '17 at 1:06

In pure untyped lambda calculus functions are anonymous. Generally, when you want to define a function recursively, you can simply have it "call" itself, for example:

if $n=0$ then $f(n) = 1$

if $n>0$ then $f(n) = nf(n-1)$.

In lambda calculus we don't have the same luxury, functions don't even have "names" in the first place, they are defined in terms of variable binding and variable substitution.

Still, there is a way to implement recursion, discovered by Haskell Curry, by using a particular lambda-term, called fixed-point combinator (if you are interested in details, any reasonable source on lambda calculus covers this aspect).

With the new notation, the authors are effectively introducing a mechanism to give names to functions, removing the problem entirely.

  • $\begingroup$ Actually, I don't know lambda calculus , I was starting up with the book "SICP" and saw the name of the paper ,so thought it would be a better idea to go through this paper first . Is lambda calculus necessary to understand this paper ? $\endgroup$ – Agnivesh Singh Feb 17 '17 at 4:05
  • 2
    $\begingroup$ @AgniveshSingh This paper is one of the earliest papers on LISP or on any high level language. You should probably not read this paper as a means to learn about programming or the theory of programming languages, but mostly out of historical interest (if you have such interests). The notation used in this paper is somewhat archaic and there were serious issues with early LISPs, so this paper is from a time where people didn't understand many of the issues very well. $\endgroup$ – Derek Elkins left SE Feb 17 '17 at 4:23
  • $\begingroup$ @quicksort : On thinking again , what problem does the absence of names of functions create in this context ? Could you elaborate a bit more about what binding is ? $\endgroup$ – Agnivesh Singh Feb 18 '17 at 9:09

If you view the $\text{sqrt} = \dots$ as meaning a syntactic abbreviation, that is, every place you see $\text{sqrt}$ you can replace it with the right hand side, then a "recursive" syntactic abbreviation doesn't make sense since it would expand into an infinitely large expression. $\text{sqrt}$ isn't a term in the lambda calculus, and so it doesn't make sense to even begin talking about "evaluating" ($\beta$-reducing) until we expand it (and all other syntactic abbreviations) fully. In other words, expanding syntactic abbreviations is a "preprocessing" step.

Now, since lambda calculus talks in terms of anonymous functions, there is no way to refer to a containing lambda term from a term within it and so there is no direct way of even writing down a recursive function. However, as I would've expected McCarthy to know, there is a way to handle recursion in the untyped lambda calculus, which is more or less the system he's describing (omitting $\text{label}$). This is the (now) well-known fixed-point combinator or $Y$ combinator. So McCarthy is mistaken (or at best unclear) when he talks about the inadequacy of lambda notation for recursive functions. On the other hand, in most typed lambda calculi the $Y$ combinator is either ill-typed or inexpressible. In those cases, a fixed point combinator needs to be added as a primitive or a mechanism akin to McCarthy's $\text{label}$ needs to be added. This is usually in the form of recursive let expressions.

  • $\begingroup$ I guess that's what we are supposed to do in recursions ,substituting the right hand side. Do you mean that , like in any recursive function , we need a last point ,where we return a value and in the above expression there is no information about the point where the recursion should terminate to yield a definite value ? $\endgroup$ – Agnivesh Singh Feb 17 '17 at 4:10
  • $\begingroup$ @AgniveshSingh No. I mean the sqrt = ... is a meta-notation like, for example, a C pre-processor #DEFINE if you are familiar with the C pre-processor (CPP). We don't interleave the expansion of CPP macros with the execution of the C code. Instead, the C compiler never sees any of these macros since the pre-processor expands them all out beforehand. CPP macros aren't allowed to be recursive since you'd never finish expanding them, and so you'd never even get to the point where the C compiler compiled the code, let alone execution of the resulting binary. $\endgroup$ – Derek Elkins left SE Feb 17 '17 at 4:35
  • $\begingroup$ Any other example that you can use to illustrate this ? $\endgroup$ – Agnivesh Singh Feb 18 '17 at 9:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.