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 my opinion, that's all you can really say about them.
The idea is that in a higher-order language, a function is just another kind of value. The same way you can have (3+4) without an identifier in C, you can have (lambda (x) +(3 x))) without an identifier in scheme.
The key here isn't that there's anything special about anonymous functions. It's only the restrictions of other languages that require functions be treated differently from any other value. The special definitions are for procedural languages which don't allow them, not for functional languages with do.
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.
It depends on which part of your question you put the emphasis. If it is specifically the property of being anonymous for anonymous functions, then indeed the only answer is that they are unbound values. If you are talking about functions in general, anonymous functions are probably the most visible manifestation of the use of lambda calculus in a functional setting, for applicative languages.
In fact, from the lambda calculus point of view, lambda expressions are the very syntactic construct used to create bindings. Recall the notation used in lambda calculus:
$\lambda f.\lambda x. f x$
where $f$ and $x$ are bound within the inner expression $f x$. Each lambda expression there defines the binding, and thus acts as a local context for name bindings.
A language usually offers ways, such as let (ML like languages, scheme), or define (scheme) to create bindings usable at the top level (or within syntactic constructs more complex than functions, like modules or objects), but the only needed tool for bindings is the lambda at lower levels.
If you look at languages like scheme or lisp dialects, their very fundation is lambda calculus, and many special forms are really sugar coated lambdas.
For concatenative languages, the story is slightly different. Lambdas are not necessary, and actually counter-productive. What's the point of defining anonymous lambdas, when everything is a function?
There is somehow a duality between these two kind of manguages. The later is focused on point free function combination and thus tries to represent everything as functions, while the former works on a more elaborated calculus, and makes an effort to have functions as first class values, like any other values of the language. In this respect, one could see lambdas as the result of that effort.
Some pointers on the topic introduced (poorly) in this answer:
