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:
“Truth exists. The sole purpose of this proposition is to assert the existence of truth against imbeciles and sceptics.”
—Edward Herbert Of Cherbury, Lord (1583–1648)
“Each of us, even the lowliest and most insignificant among us, was uprooted from his innermost existence by the almost constant volcanic upheavals visited upon our European soil and, as one of countless human beings, I can’t claim any special place for myself except that, as an Austrian, a Jew, writer, humanist and pacifist, I have always been precisely in those places where the effects of the thrusts were most violent.”
—Stefan Zweig (18811942)