Lambda-calculus with no constants, only functions expressed as lambda abstractions. (1994-10-27)

<theory> A term from lambda-calculus for beta reduction or beta abstraction. (1999-01-15)

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine.

<theory> In lambda-calculus and reduction, the renaming of a formal parameter in a lambda abstraction. This does not change the meaning of the abstraction. For example: x . x+1 <--> y . y+1 If the actual argument to a lambda abstraction contains instances of the abstraction's formal parameter then it is necessary to rename the parameter before applying the abstraction to avoid name capture. (1995-05-10)

eta conversion

A term in lambda-calculus denoting a function. A lambda abstraction begins with a lower-case lambda (represented as "" in this document), followed by a variable name (the "bound variable"), a full stop and a lambda expression (the body). The body is taken to extend as far to the right as possible so, for example an expression, x . y . x+y is read as x . ( y . x+y). A nested abstraction such as this is often abbreviated to: x y . x + y The lambda expression ( v . E) denotes a function which takes an argument and returns the term E with all free occurrences of v replaced by the actual argument. Application is represented by juxtaposition so ( x . x) 42 represents the identity function applied to the constant 42. A lambda abstraction in Lisp is written as the symbol lambda, a list of zero or more variable names and a list of zero or more terms, e.g. (lambda (x y) (plus x y)) Lambda expressions in Haskell are written as a backslash, "", one or more patterns (e.g. variable names), "->" and an expression, e.g. x -> x. (1995-01-24)

[lambda-calculus] The application of a {lambda abstraction} to an argument expression. A copy of the body of the lambda abstraction is made and occurrences of the {bound variable} being replaced by the argument. E.g. ( x . x+1) 4 --> 4+1 Beta reduction is the only kind of reduction in the {pure lambda-calculus}. The opposite of beta reduction is {beta abstraction}. These are the two kinds of beta conversion. See also name capture.

<theory> In lambda-calculus, the eta conversion rule states x . f x <--> f provided x does not occur as a free variable in f and f is a function. Left to right is eta reduction, right to left is eta abstraction (or eta expansion). This conversion is only valid if bottom and x . bottom are equivalent in all contexts. They are certainly equivalent when applied to some argument - they both fail to terminate. If we are allowed to force the evaluation of an expression in any other way, e.g. using seq in Miranda or returning a function as the overall result of a program, then bottom and x . bottom will not be equivalent. See also observational equivalence, reduction.

eta conversion

<mathematics> (Normally written with a Greek letter lambda). A branch of mathematical logic developed by Alonzo Church in the late 1930s and early 1940s, dealing with the application of functions to their arguments. The pure lambda-calculus contains no constants - neither numbers nor mathematical functions such as plus - and is untyped. It consists only of lambda abstractions (functions), variables and applications of one function to another. All entities must therefore be represented as functions. For example, the natural number N can be represented as the function which applies its first argument to its second N times (Church integer N). Church invented lambda-calculus in order to set up a foundational project restricting mathematics to quantities with "effective procedures". Unfortunately, the resulting system admits Russell's paradox in a particularly nasty way; Church couldn't see any way to get rid of it, and gave the project up. Most functional programming languages are equivalent to lambda-calculus extended with constants and types. Lisp uses a variant of lambda notation for defining functions but only its purely functional subset is really equivalent to lambda-calculus. See reduction. (1995-04-13)