|
A fixed point combinator (or fixed-point operator) is a higher-order function which computes a fixed point of other functions. In mathematics and computer science, higher-order functions are functions which can take other functions as arguments, and may also return functions as results. ...
In mathematics, a fixed point of a function is a point that is mapped to itself by the function. ...
A fixed point of a function f is a value x such that f(x) = x. For example, 0 and 1 are fixed points of the function f(x) = x2, because 02 = 0 and 12 = 1. Whereas a fixed-point of a first-order function (a function on "simple" values such as integers) is a first-order value, a fixed point of a higher-order function f is another function g such that f(g) = g. A fixed point operator, then, is any function fix such that for any function f,
- f(fix(f)) = fix(f).
Fixed point combinators allow the definition of anonymous recursive functions (see the example below). Somewhat surprisingly, they can be defined with non-recursive lambda abstractions. A Sierpinski triangle —a confined recursion of triangles to form a geometric lattice. ...
A fixed point combinator (or fixed-point operator) is a higher-order function which computes a fixed point of other functions. ...
A lambda abstraction is an abstract lambda expression. ...
One well-known (and perhaps the simplest) fixed point combinator in the untyped lambda calculus is called the Y combinator. It was discovered by Haskell B. Curry, and is defined as In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...
Haskell Brooks Curry (September 12, 1900, Millis, Massachusetts - September 1, 1982, State College, Pennsylvania) was an American mathematician and logician. ...
- Y = λf.(λx.f (x x)) (λx.f (x x))
Existence of fixed point combinators
In certain formalizations of mathematics, such as the untyped lambda calculus and combinatorial calculus, every expression can be considered a higher-order function. In these formalizations, the existence of a fixed-point combinator means that every function has at least one fixed point; a function may have more than one distinct fixed point. In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. ...
In some other systems, for example the simply typed lambda calculus, a well-typed fixed-point combinator cannot be written -- in those systems any support for recursion must be explicitly added to the language. In still others, such as the simply-typed lambda calculus extended with recursive types, fixed-point operators can be written, but the type of a "useful" fixed-point operator (one whose application always returns) may be restricted. A typed lambda calculus is a typed formalism which uses the lambda-symbol () to denote anonymous function abstraction. ...
In computer programming languages, a recursive type is a data type for values that may contain other values of the same type. ...
For example, in Standard ML the call-by-value variant of the Y combinator has the type ∀a.∀b.((a→b)→(a→b))→(a→b), whereas the call-by-name variant has the type ∀a.(a→a)→a. The call-by-name (normal) variant loops forever when applied in a call-by-value language -- every application Y(f) expands to f(Y(f)). The argument to f is then expanded, as required for a call-by-value language, yielding f(f(Y(f))). This process iterates "forever" (until the system runs out of memory), without ever actually evaluating the body of f. SML (Standard ML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. ...
Parameters are a way of allowing the same sequence of commands to operate on different data without re-specifying the instructions. ...
Parameters are a way of allowing the same sequence of commands to operate on different data without re-specifying the instructions. ...
Example Consider the factorial function (under Church encoding). The usual recursive mathematical equation is Church encoding is a means of embedding data and operators into the lambda calculus, the most familiar form being the church numerals, a representation of the natural numbers using lambda notation. ...
- fact(n) = if n=0 then 1 else n * fact(n-1)
We can express a "single step" of this recursion in lambda calculus as - F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),
where "f" is a place-holder argument for the factorial function to be passed to itself. The function F performs a single step in the evaluation of the recursive formula. Applying the fix operator gives - fix(F)(n) = F(fix(F))(n)
- fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n)
- fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n)))
We can abbreviate fix(F) as fact, and we have - fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))
So we see that a fixed-point operator really does turn our non-recursive "factorial step" function into a recursive function satisfying the intended equation.
Other fixed point combinators A version of the Y combinator that can be used in call-by-value (applicative-order) evaluation is given by η-expansion of part of the ordinary Y combinator: In functional programming languages, we are thinking of ourselves as recursively evaluating some mathematical expression. ...
In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...
- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
The Y combinator can be expressed in the SKI-calculus as SKI combinator calculus is a computational system that is a reduced, untyped version of Lambda calculus. ...
- Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
The simplest fixed point combinator in the SK-calculus, found by John Tromp, is - Y = S S K (S (K (S S (S (S S K)))) K)
which corresponds to the lambda expression - Y = (λx. λy. x y x) (λy. λx. y (x y x))
Another common fixed point combinator is the Turing fixed-point combinator (named for its discoverer, Alan Turing): Alan Turing is often considered the father of modern computer science. ...
- Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))
It also has a simple call-by-value form: - Θv = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))
Fixed point combinators are not especially rare (there are infinitely many of them). Some, such as this one (constructed by Jan Willem Klop) are useful chiefly for amusement: - Yk = (L L L L L L L L L L L L L L L L L L L L L L L L L L)
where: - L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))
See also Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. ...
In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...
Typed versions of the lambda calculus extend the standard lambda calculus with types. ...
This article needs to be cleaned up to conform to a higher standard of quality. ...
External links | 
Feeds |
Contact