Conheça Walt Disney World

:''Y_combinator redirects here; for the technology venture capital firm, see Y_Combinator.'' A '''fixed point combinator''' (or '''fixed-point operator''') is a Higher-order_function which computes a fixed point of other functions. 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'') = x², because 0² = 0 and 1² = 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. 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 : '''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 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. 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'''. == Example == Consider the factorial function (under Church_encoding). The usual recursive mathematical equation is :'''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: : '''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 : '''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): : '''Θ''' = (λ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: : '''Y_k''' = (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 * Untyped_lambda_calculus * Typed_lambda_calculus * Anonymous_recursion * Eigenfunction == External links == * http://okmij.org/ftp/Computation/fixed-point-combinators.html * http://www.cs.brown.edu/courses/cs173/2002/Lectures/2002-10-28-lc.pdf * http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/ * http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/Y/ (executable) * http://www.ececs.uc.edu/~franco/C511/html/Scheme/ycomb.html Category:Lambda_calculus Category:Mathematics_of_computing Category:Fixed_points Et:Püsipunktikombinaator Zh:不动点组合子