Fixed-point Combinator - Existence of Fixed-point Combinators

Existence of Fixed-point Combinators

In certain mathematical formalizations of computation, such as the untyped lambda calculus and combinatory logic, 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 some other systems, for example in 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. In polymorphic lambda calculus (System F) a polymorphic fixed-point combinator has type ∀a.(a→a)→a, where a is a type variable.

Read more about this topic:  Fixed-point Combinator

Famous quotes containing the words existence of and/or existence:

    No cause is left but the most ancient of all, the one, in fact, that from the beginning of our history has determined the very existence of politics, the cause of freedom versus tyranny.
    Hannah Arendt (1906–1975)

    The duty of the State toward the citizen is the duty of the servant to its master.... One of the duties of the State is that of caring for those of its citizens who find themselves the victims of such adverse circumstances as makes them unable to obtain even the necessities for mere existence without the aid of others.... To these unfortunate citizens aid must be extended by government—not as a matter of charity but as a matter of social duty.
    Franklin D. Roosevelt (1882–1945)