etareduction

Eta-reduction, or eta-conversion, is a transformation in the lambda calculus that identifies a function that simply applies another function to its argument. The basic eta-reduction rule states that the term λx. f x can be simplified to f, provided x is not a free variable in f. The corresponding eta-expansion is the opposite direction: f can be expanded to λx. f x when x is not free in f.

Eta-reduction expresses a form of functional extensionality, where two functions are considered equal if they give the same result for all inputs. It is commonly used alongside beta-reduction, which handles the application of functions to arguments. Together, beta and eta conversions define a broader notion of lambda-term equality in certain formal settings.

In practice, eta-reduction is subject to context. It requires that the bound variable x does not occur free in the function part f; otherwise the reduction may change meaning. Eta-conversion is more standard in simply typed lambda calculus, where it often yields a convenient notion of equivalence. In untyped lambda calculus, eta-reduction can interact with termination and fixed-point behavior in ways that require care, so some evaluators omit eta-reduction or treat it as a separate equivalence rule.

Example: (λx. g x) reduces to g if x is not free in g. Conversely, g can be expanded to λx. g x if desired.

See also: beta-reduction, beta-normal form, eta-expansion, lambda calculus, functional extensionality.