: fixed point combinator: fixed-point operator: paradoxical combinator   

 

  , 



 





[1][2]

: untyped lambda calculus Y= λf·(λx·f (x x)) (λx·f (x x)) 

不動点コンビネータによる再帰の実現

編集

使

         

 

(Eq. 1)


         

 

   (Eq. 1)

     

 

(Eq. 2)


                       

 

(Eq. 3)


       




g                   

g    
  1. U のプログラムを書く。
  2. VEq. 2式のように定義し、 とする。

  の証明

編集

最後に Eq. 1 で定義された再帰関数   と一致する事を示す。 不動点コンビネータの定義より、 

 

(Eq. 4)

を満たす。

前述したように はそれ自身関数なので、値xに対し を考える事ができる。  は以下を満たす:

    (Eq. 4より)
  (Eq. 3より)

すなわち

 

(Eq. 5)


Eq. 1  Eq. 5 Eq. 5  Eq. 1        Eq. 1         

 


不動点コンビネータの例

編集

1

: polymorphic lambda calculusF: System F      

Yコンビネータ

編集

Y

Y = (λf . (λx . f (x x)) (λx . f (x x)))

g
Y g = (λf . (λx . f (x x)) (λx . f (x x))) g (Yの定義より)
= (λx . g (x x)) (λx . g (x x)) (λfのβ簡約、主関数をgに適用)
= (λy . g (y y)) (λx . g (x x)) (α変換、束縛変数の名前を変える)
= g ((λx . g (x x)) (λx . g (x x))) (λyのβ簡約、左の関数を右の関数に適用)
= g (Y g) (第2式より)

使 (Yg)  (g (Yg))  (g (g (Yg))) ... (g ... (g (Yg))...) Z使

YY使#

SKI
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))

Zコンビネータ

編集

使YYη

Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

Python 
Z = lambda f: (lambda x: f(lambda *y: x(x)(*y)))(lambda x: f(lambda *y: x(x)(*y)))
# 利用方法(5の階乗の計算)
Z(lambda f: lambda n: 1 if n == 0 else n * f(n - 1))(5)

チューリング不動点コンビネータ

編集

もう一つの一般的な不動点コンビネータは、チューリング不動点コンビネータである(発見者であるアラン・チューリングの名にちなむ)。

Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))

これはシンプルな値渡し形式も持つ。

Θv = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))

SとKによる最もシンプルな不動点コンビネータ

編集

SKIコンビネータ計算のSとKによる最もシンプルな不動点コンビネータは、ジョン・トロンプによって発見された以下であり、

Y' = S S K (S (K (S S (S (S S K)))) K)

これは次のラムダ式と対応する。

Y' = (λx. λy. x y x) (λy. λx. y (x y x))

その他の不動点コンビネータ

編集

型無しラムダ計算における不動点コンビネータは無数に存在するので、特に珍しいわけではない。2005年、メイヤー・ゴールドバーグ (Mayer Goldberg) は型無しラムダ計算の不動点コンビネータの集合が帰納的可算集合であることを示した。[3]

次のようないくつかの不動点コンビネータ(ジャン・ウィレム・クロップによって組み立てられた)は、主として遊びに使われる。

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)

ここで

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))

非標準不動点コンビネータ

編集

: Böhm tree λx.x(x(x ... )) : non-standard fixed point combinators strictly non-standard fixed point combinators B = λx.xx  M = λxyz.x(yz)  N = BM(B(BM)B) [3]

不動点コンビネータの実装

編集

(non-strict)(strict)HaskellHaskellHaskellfixfixFHaskell使使

YHaskell[4]
fix :: (a ->a) -> a
fix f = f (fix f)

fix (const 9) -- constは第1引数を返し、第2引数を捨てる関数。9と評価される

factabs fact 0 = 1 -- factabsはラムダ計算の例のFから拝借
factabs fact x = x * fact (x-1)

(fix factabs) 5 -- 120と評価される

fixfix (const 9)(const 9)(fix f)fix fHaskellfix(strict)ff (f ... (fix f) ... ))

ML使fix   fixOCaml
let rec fix f x = f (fix f) x (* 余分なxに注目 *)

let factabs fact = function (* factabsはエクストラレベルのラムダ抽象 *)
 0 -> 1
 | x -> x * fact (x-1)

let _ = (fix factabs) 5 (* "120" と評価される *)

以下は Python での実装。

def fix(f):
    return lambda x: f(fix(f))(x)
# 利用方法(5の階乗の計算)
fix(lambda f: lambda n: 1 if n == 0 else n * f(n - 1))(5)

Java 8 や C++11 では無名関数(ラムダ式)が使えるので上記と同じ方法で実装できる。それよりも前の時代の Java や C++ では少々複雑だった[5][6]

再帰型による符号化の例

編集

FωYx (Rec a ->a)  (Rec a) 

HaskellInout2
In :: (Rec a ->a) -> Rec a
out :: Rec a -> (Rec a ->a)


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)))

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))

グラフ簡約

編集
 

en:Graph reduction(apply, application)Y()便Y[7]

関数の自己参照による無名再帰

編集

不動点コンビネータは識別子に束縛されていない関数が自分自身を呼び出す一般的な方法であるが、言語によっては特別な名前などで自分自身を呼び出すことができる。詳細は無名再帰を参照。

関連項目

編集

脚注

編集
  1. ^ This terminology appear to be largely folklore, but it does appear in the following:
    • Trey Nash, Accelerated C# 2008, Apress, 2007, ISBN 1590598733, p. 462--463. Derived substantially from Wes Dyer's blog (see next item).
    • Wes Dyer Anonymous Recursion in C#, February 02, 2007, contains a substantially similar example found in the book above, but accompanied by more discussion.
  2. ^ The If Works Deriving the Y combinator, January 10th, 2008
  3. ^ a b Goldberg, 2005
  4. ^ Haskell mailing list thread on How to define Y combinator in Haskell, 15 Sep 2006
  5. ^ The Y Combinator in Arc and Java - Javaコード
  6. ^ bind - Fixed point combinators in C++ - Stack Overflow - C++コード
  7. ^ たとえば、Turnerの"A New Implementation Technique for Applicative Languages"(doi:10.1002/spe.4380090105)の Figure. 3 と、その直前の説明を見よ。

参考文献

編集