is one of these fixed points, i.e. Fixed-point combinators can be defined in the lambda calculus and in functional programming languages and provide a means to allow for recursive definitions.
In the classical untyped lambda calculus, every function has a fixed point.
is Haskell Curry's paradoxical combinator Y, given by[2]: 131 [note 1][note 2] (Here we use the standard notations and conventions of lambda calculus: Y is a function that takes one argument f and returns the entire expression following the first period; the expression
Juxtaposition of expressions denotes function application, is left-associative, and has higher precedence than the period.)
More interesting results are obtained by applying the Y combinator to functions of two or more variables.
The heart of Curry's paradox is that untyped lambda calculus is unsound as a deductive system, and the Y combinator demonstrates this by allowing an anonymous expression to represent zero, or even many values.
Substituting all the definitions into one line so that function names are not required gives:This works because R uses lazy evaluation.
Languages that use strict evaluation, such as Python, C++, and others, can often express Y; however, any implementation is useless in practice since it loops indefinitely until terminating through stack overflow.
Fixed-point combinators may also be easily defined in other functional and imperative languages.
In this case particular lambda terms (which define functions) are considered as values.
A mathematician may see the Y combinator applied to a function as being an expression satisfying the fixed-point equation, and therefore a solution.
In contrast, a person only wanting to apply a fixed-point combinator to some general programming task may see it only as a means of implementing recursion.
If trying to compute Y f in an actual programming language, an infinite loop will occur.
General mathematics defines a function based on its extensional properties.
Lambda calculus and programming languages regard function identity as an intensional property.
The standard recursive definition of the factorial function in mathematics can be written as where n is a non-negative integer.
If we want to implement this in lambda calculus, where integers are represented using Church encoding, we run into the problem that the lambda calculus does not allow the name of a function ('fact') to be used in the function's definition.
[5] In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus is recursively enumerable.
also has a simple call-by-value form: The analog for mutual recursion is a polyvariadic fix-point combinator,[8][9][10] which may be denoted Y*.
In a strict programming language the Y combinator will expand until stack overflow, or never halt in case of tail call optimization.
Since Haskell has lazy datatypes, this combinator can also be used to define fixed points of data constructors (and not only to implement recursive functions).
In Hackage, the original sample is: [13] In a strict functional language, as illustrated below with OCaml, the argument to f is expanded beforehand, yielding an infinite call sequence, This may be resolved by defining fix with an extra parameter.
In a multi-paradigm functional language (one decorated with imperative features), such as Lisp, Peter Landin suggested the use of a variable assignment to create a fixed-point combinator,[14] as in the below example using Scheme: Using a lambda calculus with axioms for assignment statements, it can be shown that Y!
satisfies the same fixed-point law as the call-by-value Y combinator:[15][16] In more idiomatic modern Scheme usage, this would typically be handled via a letrec expression, as lexical scope was introduced to Lisp in the 1970s: Or without the internal label: This example is a slightly interpretive implementation of a fixed-point combinator.
As for the strict functional definition, fix is explicitly given an extra parameter x, which means that lazy evaluation is not needed.
No fixed-point combinator can in fact be typed; in those systems, any support for recursion must be explicitly added to the language.
For example, in the following Haskell code, we have Rec and app being the names of the two directions of the isomorphism, with types:[19][20] which lets us write: Or equivalently in OCaml: Alternatively: Because fixed-point combinators can be used to implement recursion, it is possible to use them to describe specific types of recursive computations, such as those in fixed-point iteration, iterative methods, recursive join in relational databases, data-flow analysis, FIRST and FOLLOW sets of non-terminals in a context-free grammar, transitive closure, and other types of closure operations.
The remarkable property of a fixed-point combinator is that it constructs a fixed point for an arbitrary given function
Other functions have the special property that, after being applied once, further applications don't have any effect.
For example, we obtain where the resulting term can only reduce to itself and represents an infinite loop.