Why is abstraction in lambda calculus called abstraction?

Question

The term abstraction as I understand it, is used in many different contexts, but has one essential meaning, namely that it refers to the “general properties of some class of objects that doesn’t rely on their details”. For example, abstraction in programming is e.g. interfaces that allow you to constrain a set of objects without specifying certain implementation details.

But in lambda calculus, I don’t see what “function abstraction” has to do with something like “independence of details”. It seems to me like “function application” or “argument substitution” makes more sense.

Am I missing something?

Ps. Note that I have only read an introductory chapter of a book on lambda calculus.

Answer 1

Abstraction in the context of lambda calculi means turning some part of a term into a variable. Let's do an example. Consider the following terms (which use a notation richer than pure lambda calculus):

• $1 + 2$
• $\sin^2(\varphi) + \cos^2(\varphi)$
• $\frac1{n + 1}t^{n + 1} + C$

They have one thing in common. They all are built from smaller terms using $+$. Now, if we want to abstract away from the details and focus on the general common property of these terms, we just turn everything that is not $+$ into variables and end up with $\lambda x.\lambda y.x + y$, a function abstraction (if that is the name your introductory text uses; I am more familiar with the name "lambda abstraction").

Answer 2

A key result from lambda calculus is that to perform arbitrary computation all you need are anonymous functions. These anonymous functions are called abstractions, and the way you use them is by applying them to arguments, which are also other anonymous functions. So why are they called abstractions, or in other words, what are they abstracted from? Other such functions. So it just means that functions are detached and separate from one another. In fact, the word abstract comes from latin abstractus, which literally means drawn away.