Why is the introduction of the Ycombinator in λ-calculus necessary?

Question

I am reading a book on λ-calculus "Functional programming Through Lambda Calculus" (Greg Michaelson). In the book the author introduces a short-hand notation for defining functions. For example

def identity = λx.x

and goes on saying that we should insist that when using such shorthand "all defined names should be replaced by their definitions before the expression is evaluated"

Later on, when introducing recursion he uses as an example a definition of the addition function such as:

def add x y = if iszero y then x else add (succ x) (pred y)

and goes to say, that had we not had the restriction mentioned above we would be able to evaluate this function by slowly expanding it. However since we have the restriction of replacing all defined names before the evaluation of the expression, we cannot do that since we go on indefinetely replacing add and thus the need of thinking about recursion in a more detailed way.

My question is thus the following: What are the theoritical or practical reasons for placing this restriction upon ourselves? (of having to replace all defined names before the evaluation of the function)? Are there any?

Answer 1

I was trying to show how to build a rich language from a very simple one, by adding successive layers of syntax, where each layer could be translated into the previous layer. So it's important to distinguish translation, which must terminate, from evaluation which needn't. I think it's really interesting that recursion can be translated into non-recursion. I'm sorry if my explanation isn't helpful.

Answer 2

I will try to post my own answer, the way I understand it.

For the untyped lambda calculus there is no practical reason, we need the Y combinator. By practical I mean that if someone wants to build an expression evaluator, it is possible to do it without needing the combinator and just slowly expanding the definition.

For theoretical reasons though, we need to make sure that when we define a function this definition has some meaning and is not defined in terms of itself. e.g. there is not much meaning in the following definition:

def something = something

For this reason, we need to see if it is possible to rewrite the definition in a way that it is not self-referential, i.e. it is possible to define something without referring to itself. It turns out that in the untyped lambda calculus we can always do that through the Y-combinator.

Using the Y-combinator we can always construct the solution to the equation x=f(x)=f(f(x))=...=f(f(f(f(x)))=.... for any f,

i.e. we can always rewrite a self-referential definition to a definition that it does not include itself

Answer 3

The reason is that we want to stay within the rules of the lambda calculus. Allowing names for terms to mean anything other than immediate substitution would mean adding a recursive let expression to the language, which would mean we would need a truly more expressive system (no longer the lambda calculus).

You can think of the names as no more than syntactic sugar for the original lambda term. The Y-combinator is exactly the way to introduce recursion into a system that does not have it built in. If the book you are currently reading confuses you, you might want search for some additional resources on the internet explaining the Y-combinator.