Why is abstraction in lambda calculus called abstraction?

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.

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

StackExchange Computer Science Q#93006, answer score: 5