Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
In mathematics and computer science, higher-order functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a function...
In mathematics, a fixed point of a function is a point that is mapped to itself by the function. A set of fixed points is sometimes called a fixed set...
of other functions. A fixed point of a function f is a value x such that x = f(x). For example, 0 and 1 are fixed points of the function f(x) = x2, because 0 = 02 and 1 = 12. 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 functionp such that p = f(p). A fixed-point combinator, then, is a function g which produces such a fixed point p for any function f:
g(f) = p, where p = f(p)
or, alternatively:
g(f) = f(g(f)).
Because fixed-point combinators are higher-order functions, their history is intimately related to the development of lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
. One well-known fixed-point combinator in the untyped lambda calculus is Haskell Curry
Haskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
's Y = λf·(λx·f (x x)) (λx·f (x x)). The name of this combinator is sometimes incorrectly used to refer to any fixed-point combinator. The untyped lambda calculus however, contains an infinitude of fixed-point combinators. Fixed-point combinators do not necessarily exist in more restrictive models of computation. For instance, they do not exist in simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
In programming language theory, an anonymous function is a function defined, and possibly called, without being bound to an identifier. Anonymous functions are convenient to pass as an argument to a higher-order function and are ubiquitous in languages with first-class functions such as Haskell...
s, fixed-point combinators allow the definition and use of anonymous recursive functions
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
In programming languages, name binding is the association of objects with identifiers. An identifier bound to an object is said to reference that object. Machine languages have no built-in notion of identifiers, but name-object bindings as a service and notation for the programmer is implemented...
An identifier is a name that identifies either a unique object or a unique class of objects, where the "object" or class may be an idea, physical [countable] object , or physical [noncountable] substance...
s. In this setting, the use of fixed-point combinators is sometimes called anonymous recursion.
How it works
Ignoring for now the question whether fixed-point combinators even exist (to be addressed in the next section), we illustrate how a function satisfying the fixed-point combinator equation works. To easily trace the computation steps, we choose untyped lambda calculus as our programming language. The (computational) equality from the equation that defines a fixed-point combinator corresponds to beta reduction in lambda calculus.
As a concrete example of a fixed-point combinator applied to a function, we use the standard recursive mathematical equation that defines the factorial function
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 the lambda abstraction F = λf. λn. IFTHENELSE (ISZERO n) 1 (MULT n (f (PRED n)))
In mathematics, 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...
for numerals. The functions in CAPITALS above can all be defined as lambda abstractions with their intuitive meaning; see lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
for their precise definitions. Intuitively, f in F is a place-holder argument for the factorial function itself.
We now investigate what happens when a fixed-point combinator FIX is applied to F and the resulting abstraction, which we hope would be the factorial function, is in turn applied to a (Church-encoded) numeral.
(FIX F) n = (F (FIX F)) n --- expanded the defining equation of FIX
= (λx. IFTHENELSE (ISZERO x) 1 (MULT x ((FIX F) (PRED x)))) n --- expanded the first F
= IFTHENELSE (ISZERO n) 1 (MULT n ((FIX F) (PRED n))) --- applied abstraction to n.
If we now abbreviate FIX F as FACT, we recognize that any application of the abstraction FACT to a Church numeral calculates its factorial
FACT n = IFTHENELSE (ISZERO n) 1 (MULT n (FACT (PRED n))).
Recall that in lambda calculus all abstractions are anonymous, and that the names we give to some of them are only syntactic sugar
Syntactic sugar
Syntactic sugar is a computer science term that refers to syntax within a programming language that is designed to make things easier to read or to express....
. Therefore, it's meaningless in this context to contrast FACT as a recursive function with F as somehow being "not recursive". What fixed point operators really buy us here is the ability to solve recursive equations. That is, we can ask the question in reverse: does there exist a lambda abstraction that satisfies the equation of FACT? The answer is yes, and we have a "mechanical" procedure for producing such an abstraction: simply define F as above, and then use any fixed point combinator FIX to obtain FACT as FIX F.
In the practice of programming, substituting FACT at a call site
Call site
In programming, a call site of a function is a line in the code which calls a function. A call site passes zero or more arguments to the function, and receives zero or more return values.-Example:...
by the expression FIX F is sometimes called anonymous recursion. In the lambda abstraction F, FACT is represented by the bound variable f, which corresponds to an argument in a programming language, therefore F need not be bound
Name binding
In programming languages, name binding is the association of objects with identifiers. An identifier bound to an object is said to reference that object. Machine languages have no built-in notion of identifiers, but name-object bindings as a service and notation for the programmer is implemented...
In mathematics and computer science, higher-order functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a function...
because the argument f is itself called as a function, so the programming language must allow passing functions as arguments. It must also allow function literals because FIX F is an expression
Expression (programming)
An expression in a programming language is a combination of explicit values, constants, variables, operators, and functions that are interpreted according to the particular rules of precedence and of association for a particular programming language, which computes and then produces another value...
rather than an identifier. In practice, there are further limitations imposed on FIX, depending on the evaluation strategy
Evaluation strategy
In computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
employed by the programming environment and the type checker. These are described in the implementation section.
Existence of fixed-point combinators
In certain mathematical formalizations of computation, such as the untyped lambda calculus and combinatory logic
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
, 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.
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a 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 type
Recursive type
In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type...
s, fixed-point operators can be written, but the type of a "useful" fixed-point operator (one whose application always returns) may be restricted. In polymorphic lambda calculus (System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
) a polymorphic fixed-point combinator has type ∀a.(a→a)→a, where a is a type variable
Type variable
In type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.Programming languages that...
.
Y combinator
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
Haskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
, and is defined as:
Y = λf.(λx.f (x x)) (λx.f (x x))
We can see that this function acts as a fixed-point combinator by applying it to an example function g and rewriting:
Y g
= (λf . (λx . f (x x)) (λx . f (x x))) g
(by definition of Y)
= (λx . g (x x)) (λx . g (x x))
(β-reduction of λf: applied main function to g)
= (λy . g (y y)) (λx . g (x x))
(α-conversion: renamed bound variable)
= g ((λx . g (x x)) (λx . g (x x)))
(β-reduction of λy: applied left function to right function)
= g (Y g)
(by second equality)
In programming practice, the Y combinator is useful only in those languages that provide a call-by-name evaluation strategy
Evaluation strategy
In computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
, since (Yg) diverges (for any g) in call-by-value settings.
Factorial definition using Y Combinator
(define fact
(Y (lambda (f)
(lambda (n)
(if (<= n 0)
1
(* n (f (- n 1))))))))
Example in Common Lisp
(defun y (func)
((lambda (x) (funcall x x))
(lambda (y)
(funcall func
(lambda (&rest args)
(apply (funcall y y) args))))))
Factorial program using the Y combinator
(funcall
(y (lambda (f)
(lambda (x)
(if (<= x 1) 1 (* x (funcall f (1- x))))))) 5)
Other fixed-point combinators
In untyped lambda calculus fixed-point combinators are not especially rare. In fact there are infinitely many of them. In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus is recursively enumerable.
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:
Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
Here is an example of this in Python:
>>> Z = lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args)))
>>> fact = lambda f: lambda x: 1 if x 0 else x * f(x-1)
>>> Z(fact)(5)
120
The Y combinator can be expressed in the SKI-calculus
SKI combinator calculus
SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus. It can be thought of as a computer programming language, though it is not useful for writing software...
as
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))
This fixed-point combinator is simpler than the Y combinator, and β-reduces into the Y combinator; it is sometimes cited as the Y combinator itself:
X = λf.(λx.x x) (λx.f (x x))
Another common fixed point combinator is the Turing fixed-point combinator (named after its discoverer, Alan Turing
Alan Turing
Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...
):
Θ = (λ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)))
Some fixed point combinators, such as this one (constructed by Jan Willem Klop
Jan Willem Klop
Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinatorwhere- External links :*...
) 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))
Strictly non-standard fixed-point combinators
In untyped lambda calculus there are terms that have the same Böhm tree
Böhm tree
The concept of a Böhm tree arises in lambda calculus, a discipline within mathematical logic and computer science. It is named after Corrado Böhm....
as a fixed-point combinator, that is they have the same infinite extension λx.x(x(x ... )). These are called non-standard fixed-point combinators. Evidently, any fixed-point combinator is also a non-standard one, but not all non-standard fixed-point combinators are fixed-point combinators because some of them fail to satisfy the equation that defines the "standard" ones. These strange combinators are called strictly non-standard fixed-point combinators; an example is the following combinator N = BM(B(BM)B), where B = λxyz.x(yz) and M = λx.xx. The set of non-standard fixed-point combinators is not recursively enumerable.
Implementing fixed-point combinators
In a language that supports lazy evaluation
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
, like in Haskell, it is possible to define a fixed-point combinator using the defining equation of the fixed-point combinator. A programming language of this kind effectively solves the fixed-point combinator equation by means of its own (lazy) recursion mechanism. This implementation of a fixed-point combinator in Haskell is sometimes referred to as defining the Y combinator in Haskell. This is incorrect because the actual Y combinator is rejected by the Haskell type checker (but see the following section for a small modification of Y using a recursive type which works). The listing below shows the implementation of a fixed-point combinator in Haskell that exploits Haskell's ability to solve the fixed-point combinator equation. This fixed-point combinator is traditionally called fix in Haskell. Observe that fix is a polymorphic fixed-point combinator (c.f. the discussion in previous section on System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
); its type is only shown for clarity—it can be inferred
Type inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
in Haskell. The definition is followed by some usage examples.
fix :: (a -> a) -> a
fix f = f (fix f)
fix (const 9) -- const is a function that returns its first parameter and ignores the second;
-- this evaluates to 9
factabs fact 0 = 1 -- factabs is F from our lambda calculus example
factabs fact x = x * fact (x-1)
(fix factabs) 5 -- evaluates to 120
In the example above, the application of fix does not loop infinitely, because of lazy evaluation; e.g., in the expansion of fix (const 9) as (const 9)(fix f), the subexpression fix f is not evaluated. In contrast, the definition of fix from Haskell loops forever when applied in a strict programming language
Strict programming language
A strict programming language is one in which only strict functions may be defined by the user. A non-strict programming language allows the user to define non-strict functions, and hence may allow lazy evaluation.- Examples :Nearly all programming languages in common use today are strict...
, because the argument to f is expanded beforehand, yielding an infinite call sequence f (f ... (fix f) ... )), which causes a stack overflow
Stack overflow
In software, a stack overflow occurs when too much memory is used on the call stack. The call stack contains a limited amount of memory, often determined at the start of the program. The size of the call stack depends on many factors, including the programming language, machine architecture,...
in most implementations.
In a strict language like OCaml, we can avoid the infinite recursion problem by forcing the use of a closure
Closure (computer science)
In computer science, a closure is a function together with a referencing environment for the non-local variables of that function. A closure allows a function to access variables outside its typical scope. Such a function is said to be "closed over" its free variables...
. The strict version of fix shall have the type ∀a.∀b.((a→b)→(a→b))→(a→b). In other words, it works only on a function which itself takes and returns a function. For example, the following OCaml code implements a strict version of fix:
let rec fix f x = f (fix f) x (* note the extra x *)
let factabs fact = function (* factabs now has extra level of lambda abstraction *)
0 -> 1
| x -> x * fact (x-1)
let _ = (fix factabs) 5 (* evaluates to "120" *)
The same idea can be used to implement a (monomorphic) fixed combinator in strict languages that support inner class
Inner class
In object-oriented programming , an inner class or nested class is a class declared entirely within the body of another class or interface. It is distinguished from a subclass.-Overview:...
es inside methods (called local inner classes in Java
Java (programming language)
Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
), which are used as 'poor man's closures' in this case. Even when such classes may be anonymous, as in the case of Java, the syntax is still cumbersome. Java code. Function object
Function object
A function object, also called a functor, functional, or functionoid, is a computer programming construct allowing an object to be invoked or called as though it were an ordinary function, usually with the same syntax.-Description:...
C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...
, simplify the calling syntax, but they still have to be generated, preferably using a helper function such as boost::bind. C++ code.
In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type...
s (see System Fω), it is possible to type the Y combinator by appropriately accounting for the recursion at the type level. The need to self-apply the variable x can be managed using a type (Rec a), which is defined so as to be isomorphic to (Rec a -> a).
For example, in the following Haskell code, we have In and out being the names of the two directions of the isomorphism, with types:
In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)
which lets us write:
newtype Rec a = In { out :: Rec a -> a }
y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))
Or equivalently in OCaml:
type 'a recc = In of ('a recc -> 'a)
let out (In x) = x
let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))
Anonymous recursion by other means
Although fixed point combinators are the standard solution for allowing a function not bound
Name binding
In programming languages, name binding is the association of objects with identifiers. An identifier bound to an object is said to reference that object. Machine languages have no built-in notion of identifiers, but name-object bindings as a service and notation for the programmer is implemented...
to an identifier to call itself, some languages like JavaScript
JavaScript
JavaScript is a prototype-based scripting language that is dynamic, weakly typed and has first-class functions. It is a multi-paradigm language, supporting object-oriented, imperative, and functional programming styles....
In programming language theory, an anonymous function is a function defined, and possibly called, without being bound to an identifier. Anonymous functions are convenient to pass as an argument to a higher-order function and are ubiquitous in languages with first-class functions such as Haskell...
s to refer to themselves. For example, in Javascript one can write the following, although it has been removed in the strict mode of the latest standard edition.
function(x) {
return x 0 ? 1 : x * arguments.callee(x-1);
}
