Eta conversion in lambda calculus is a syntactic transformation that replaces a lambda abstraction of the form "λx.Mx" with "M", where "x" does not occur free in "M". In other words, if the argument of a lambda abstraction is immediately applied to the function, then the function can be simplified by removing the lambda abstraction and replacing it with the body of the function. Formally, given a lambda term (function) "λx.Mx", where "M" is any lambda term and "x" is a variable, we can apply eta conversion to obtain an equivalent lambda term "M" if and only if "x" does not occur free in "M". This can be denoted as: λx.Mx ≡ M (if x ∉ FV(M)) where FV(M) represents the set of free variables occurring in M. It is important to note that eta conversion is applicable only under certain conditions, specifically when it does not change the behavior or meaning of a lambda term. Eta conversion allows for simplification and reduction of functions to their more concise forms. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Eta Expansion") or contains(subject, "eta expansion") or contains(subject, "Eta Abstraction") or contains(subject, "eta abstraction") or contains(subject, "Eta Conversion") or contains(subject, "eta conversion") or contains(subject, "thirdness") ```