anonymous lambda functions (functional programming)

What are anonymous (lambda) functions? What is the formal definition of an anonymous function in a functional programming language?

In my simple terms, when I am programming in scheme/lisp I would say an anonymous (lambda) function is a function that is not bound to an identifier.

Is that all that you can say formally about a lambda function? I think there is more detail that can be added to this simple definition. Please elaborate, and thank you!

In the lambda calculus, all functions (terms) are anonymous. This is an essential property of the lambda calculus: you can compose complex functions from simpler ones without giving them names.

In programming languages, it is in most cases desirable to give names to functions, because this is the way we think and it makes code readable for humans. But compilation eventually removes the names when producing an executable (if we disregard debugging information).

If a language allows expressing anonymous functions (that is functions without names), it can give an advantage to both programmers and compilers: Programmers can often write shorter code, and compilers can better optimize, knowing that an anonymous function is used just at the given place and not anywhere else.

StackExchange Computer Science Q#9655, answer score: 11