固定点コンビネータ

古典的な型なしラムダ計算では、すべての関数は不動点を持つ。${\displaystyle \mathrm {fix} }$は、ハスケル・カリーの逆説的コンビネータ Y であり、^{[ 2 ] : 131 [注 1 ] [注 2 ]で与えられます。}

${\displaystyle \mathrm {Y} =\lambda f.\ (\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))}$

（ここではラムダ計算の標準的な表記法と慣例を使用します。Y は引数fを 1 つ受け取り、最初の小数点に続く式全体を返す関数です。式${\displaystyle \lambda xf\ (x\ x)}$は、関数とみなされる引数x を1 つ受け取り、式を返す関数を表します。${\displaystyle f\ (x\ x)}$、 どこ${\displaystyle (x\ x)}$は、 x をそれ自身に適用したことを意味します。式の並置は関数適用を表し、左結合性を持ち、ピリオドよりも優先順位が高くなります。

以下の計算により、${\displaystyle \mathrm {Y} g}$これは確かに関数の不動点である。${\displaystyle g}$:

ラムダ項${\displaystyle g\ (\mathrm {Y} \ g)}$一般的には、β還元によって次の項に還元されない可能性がある${\displaystyle \mathrm {Y} \ g}$しかし、示されているように、両方の項はβ還元によって同じ項になります。

以下に、 R 言語におけるYの実装例を示します。

Y <- \ ( f ) { g <- \ ( x ) f ( x ( x )) g ( g ) }

これを利用して、階乗を以下のように実装できます。

fact <- \ ( f ) \ ( n ) if ( n == 0 ) 1 else n * f ( n - 1 ) Y ( fact )( 5 ) # 5! = 120 を出力

Yは関数名がない場合にのみ必要です。関数名が不要になるようにすべての定義を1行に置き換えると次のようになります。

( \ ( f ) ( \ ( x ) f ( x ( x )))( \ ( x ) f ( x ( x )))) ( \ ( f ) \ ( n ) if ( n == 0 ) 1 else n * f ( n - 1 )) ( 5 )

これは、Rが遅延評価を使用しているため機能します。

Python、C++、その他の厳密なプログラミング言語など、厳密な評価を使用する言語は、多くの場合Yを表現できます。しかし、スタックオーバーフローによって終了するまで無限にループするため、実際にはどの実装も役に立ちません。

多くの関数には固定点がありません。例えば${\displaystyle f:\mathbb {N} \to \mathbb {N} }$と${\displaystyle f(n)=n+1}$チャーチ符号化を用いると、自然数をラムダ計算で表現することができ、この関数fもラムダ計算で定義できます。ただし、その定義域には自然数を表すラムダ式だけでなく、すべてのラムダ式が含まれるようになります。fに Y コンビネータを適用すると、fの不動点が得られますが、この不動点は自然数を表すものではありません。実際のプログラミング言語で Y fを計算しようとすると、無限ループが発生します。

不動点コンビネータは数学で定義され、その後他の言語で実装されることがあります。一般的な数学では、関数は外延的性質に基づいて定義されます。^{[ 3 ]}つまり、2 つの関数が同じマッピングを実行する場合、それらは等しいとみなされます。ラムダ計算とプログラミング言語では、関数の同一性は内包的性質とみなされます。関数の同一性は、その実装に基づいています。

ラムダ計算における関数（または項）は、数学関数の実装です。ラムダ計算には、不動点コンビネータの数学的定義を満たすコンビネータ（実装）が多数存在します。

組み合わせ論理は高階関数理論の一種です。コンビネータは閉じたラムダ式であり、自由変数を持ちません。コンビネータを組み合わせることで、値を変数として明示的に指定することなく、式内の適切な場所に配置することができます。

階乗関数は、不動点コンビネータを使用して再帰関数を定義する方法の良い例です。数学における階乗関数の標準的な再帰的定義は次のように記述できます。

${\displaystyle \operatorname {fact} \ n={\begin{cases}1&{\text{if}}~n=0\\n\times \operatorname {fact} (n-1)&{\text{otherwise.}}\end{cases}}}$

ここでnは非負の整数である。

しかし、これは問題となる。${\displaystyle \operatorname {fact} }$定義の中で${\displaystyle \operatorname {fact} }$これは、定義全体をそれ自体の中に包含することを意味するものでは決してありません。むしろ、通常はほとんど気づかれないように、定義をその名前で参照することを意味します。これは、いわゆる「環境」と呼ばれる、名前のグローバルなレジストリの存在を前提としています。そして、ラムダ計算にはこれが全く欠けています。

それでも、ラムダ計算には名前参照が存在する。ローカル名、特定の関数のパラメータ名などである。したがって、上記は次のように書き換えることができる。

${\displaystyle {\begin{aligned}&\operatorname {fact} (n)=\operatorname {f} (\operatorname {f} ,n)\\&\quad {\text{ただし}}\\&\quad \operatorname {f} (s,n)={\begin{cases}1&{\text{if}}~n=0\\n\times s(s,n-1)&{\text{それ以外の場合}}\end{cases}}\end{aligned}}}$

別のコピーを分割する${\displaystyle \operatorname {f} }$そしてそれを引数として自身に渡すと、必要に応じて自身内部で呼び出すことができるようになります。そのような呼び出しでは、次の呼び出しで使用できるように、再び引数として渡されなければなりません。呼び出しの連鎖が進むにつれて、同様に続きます。${\displaystyle \operatorname {f} }$オープン再帰であり、呼び出し${\displaystyle \operatorname {f} }$最上位の引数としてそれ自体を用いることで、円環が閉じられる。

これをラムダ計算で実装するのは今や自明であり、固定点コンビネータの1つのインスタンスであるYコンビネータの定義に直接つながり、${\displaystyle \operatorname {fix} f=f\,(\operatorname {fix} f)}$または、直接、 2つの引数fとnを持つ関数Fを定義します。

${\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))}$

（ここ${\displaystyle (\operatorname {IsZero} \ n)}$これは、2つの引数を取り、 n =0の場合は最初の引数を返し、それ以外の場合は2番目の引数を返す関数です。${\displaystyle \operatorname {pred} \ n}$n -1と評価される。）

定義${\displaystyle \operatorname {fact} ={\textsf {fix}}\ F=F\ ({\textsf {fix}}\ F)}$。 それから${\displaystyle \operatorname {fact} }$はFの不動点であり、

${\displaystyle {\begin{aligned}\operatorname {fact} n&=F\ \operatorname {fact} \ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))\ \end{aligned}}}$

ご希望に応じて。

型なしラムダ計算では、不動点コンビネータは特に珍しいものではありません。実際、それらは無限に存在します。^{[ 5 ]} 2005年にメイヤー・ゴールドバーグは、型なしラムダ計算の不動点コンビネータの集合が再帰的に列挙可能であることを示しました。^{[ 6 ]}

YコンビネータはSKI計算で次のように表現できます。

${\displaystyle {\mathsf {Y=S(K(SII))(S(S(KS)K)(K(SII)))=SS(S(S(KS)K))(K(SII))}}}$

追加のコンビネータ（B、C、K、Wシステム）を使用すると、より短いエンコーディングが可能になります。${\displaystyle {\mathsf {U=SII}}}$自己適用コンビネータは、${\displaystyle {\mathsf {S}}({\mathsf {K}}x)yz=x(yz)={\mathsf {B}}xyz}$そして${\displaystyle {\mathsf {S}}x({\mathsf {K}}y)z=xzy={\mathsf {C}}xyz}$上記は次のようになる

${\displaystyle {\mathsf {Y=S(KU)(SB(KU))=BU(CBU)}}\ \ \$ ;\ \ {\mathsf {Y=SSI(BWB)}}}

ジョン・トランプによって発見された、SコンビネータとKコンビネータのみを使用したSK計算における最短の不動点コンビネータは、

${\displaystyle {\mathsf {Y'=SSK(S(K(SS(S(SSK))))K)=WC(SB(C(WC)))}}}$

ただし、これは通常の形式ではなく、より長いことに注意してください。このコンビネータはラムダ式に対応します。

${\displaystyle {\mathsf {Y}}'=(\lambda xy.xyx)(\lambda yx.y(xyx))}$

以下の不動点コンビネータはYコンビネータよりも単純であり、β還元するとYコンビネータになります。これはYコンビネータそのものとして引用されることもあります。

${\displaystyle {\mathsf {X}}=\lambda f.(\lambda x.xx)(\lambda xf(xx))\ \ \$ ;\ \ {\mathsf {Xf=U(BfU)}}}

もう1つの一般的な固定点コンビネータは、チューリング固定点コンビネータ（発見者であるアラン・チューリングにちなんで名付けられた）である。^{[ 7 ] [ 2 ]： 132}

${\displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))={\mathsf {SII(S(K(SI))(SII))=U(B(SI)U)}}}$

その利点は${\displaystyle {\mathsf {Y}}}$それは${\displaystyle \Theta \ f}$ベータ還元により${\displaystyle f\ (\Theta f)}$[^{注3 ]} 一方${\displaystyle {\mathsf {Y}}\ f}$そして${\displaystyle f\ ({\mathsf {Y}}f)}$共通項にのみベータ還元する。

${\displaystyle \Theta }$また、シンプルな値渡し形式も備えています。

${\displaystyle \Theta _{v}=(\lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))}$

相互再帰の類似物は多変数不動点コンビネータ^{[ 8 ] [ 9 ] [ 10 ]}であり、Y*と表記されることがある。

厳密なプログラミング言語では、Y コンビネータはスタックオーバーフローするまで展開するか、末尾呼び出し最適化の場合は停止しません。^{[ 11 ]} Z コンビネータは厳密な言語（適用評価順序が適用される、いわゆるイーガー言語）で動作します。Z コンビネータでは次の引数が明示的に定義されているため、展開が防止されます。${\displaystyle Zg}$定義の右側：^{[ 12 ]}

${\displaystyle Zgv=g(Zg)v\ .}$

そしてラムダ計算においては、それはYコンビネータのイータ展開である。

${\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .}$

Fが型なしラムダ計算における不動点コンビネータである場合、以下が成り立つ。

${\displaystyle {\mathsf {F}}=\lambda x.Fx=\lambda x.x(Fx)=\lambda x.x(x(Fx))=\cdots }$

固定点コンビネータと同じベーム木を持つ項、つまり同じ無限拡張を持つ項${\displaystyle \lambda x.x(x(x\cdots ))}$これらは非標準固定点コンビネータと呼ばれます。すべての固定点コンビネータは非標準でもありますが、非標準固定点コンビネータのすべてが固定点コンビネータであるとは限りません。なぜなら、それらのいくつかは「標準」の固定点コンビネータを定義する固定点方程式を満たさないからです。これらのコンビネータは厳密に非標準固定点コンビネータと呼ばれます。次のコンビネータはその例です。

${\displaystyle {\mathsf {N=BU(B(BU)B)}}}$

どこ

${\displaystyle {\mathsf {B}}=\lambda xyz.x(yz)}$

${\displaystyle {\mathsf {U}}=\lambda x.xx\ }$

以来

${\displaystyle {\mathsf {N}}=\lambda x.Nx=\lambda x.x(N_{2}x)=\lambda x.x(x(x(N_{3}x)))=\lambda x.x(x(x(x(x(x(N_{4}x))))))=\cdots }$

どこ${\displaystyle {\mathsf {N}}_{i}}$は${\displaystyle {\mathsf {N}}}$オンザフライで作成され、${\displaystyle i}$事例${\displaystyle x}$すぐにチェーンに組み入れられ、置き換えられる${\displaystyle {\mathsf {N}}_{i+1}}$。

非標準固定点コンビネータの集合は再帰的に列挙可能ではない。^{[ 6 ]}

Haskellのように遅延評価をサポートする言語では、慣習的に と呼ばれる固定点コンビネータの定義式を使用して固定点コンビネータを定義することが可能です。Haskell には遅延データ型があるため、このコンビネータはデータ コンストラクタの固定点を定義するためにも使用できます (再帰関数を実装するためだけではありません)。定義はここに示され、続いていくつかの使用例があります。Hackage の元のサンプルは次のとおりです。^{[ 13 ]}fix

fix 、fix' :: ( a -> a ) -> a fix f = let x = f x in x -- ラムダが削除されました。共有。-- 元の定義は Data.Function にあります。-- 代替: fix' f = f ( fix' f ) -- ラムダが持ち上げられました。非共有。fix ( \ x -> 9 ) -- これは 9 と評価されますfix ( \ x -> 3 : x ) -- 遅延評価される無限リスト [3,3,3,...]fact = fix fac -- 階乗関数に評価されます。ここでfac f 0 = 1 fac f x = x * f ( x - 1 )事実5 -- 120と評価される

厳密な関数型言語では、以下にOCamlで示すように、 fへの引数は事前に展開され、無限の呼び出しシーケンスが生成されます。

${\displaystyle f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x}$。

これは、fix関数にパラメータを追加して定義することで解決できる可能性があります。

let rec fix f x = f ( fix f ) x (* 余分な x に注意。したがって fix f = \x-> f (fix f) x *)let factabs fact = function (* factabs にはラムダ抽象化の追加レベルがあります *) 0 -> 1 | x -> x * fact ( x - 1 )let _ = ( fix factabs ) 5 (* "120" と評価される *)

Lispのようなマルチパラダイム関数型言語（命令型機能を備えた言語）では、Peter Landinは変数代入を使用して固定点コンビネータを作成することを提案しました^{[ 14 ]} 。以下はSchemeを使用した例です。

( define Y! ( lambda ( f ) (( lambda ( g ) ( set! g ( f ( lambda ( x ) ( g x )))) ;; (set! g expr) は g に expr の値gを代入します) ;; g の初期値 #f を置き換えて#fを作成します))) ;; これにより、g の真の自己参照値が実現します

Y!代入文の公理を持つラムダ計算を使用すると、値渡し Y コンビネータと同じ不動点法則を満たすことが示されます。 ^{[ 15 ] [ 16 ]}

${\displaystyle (Y_{!}\ \lambda x.e)e'=(\lambda x.e)\ (Y_{!}\ \lambda x.e)e'}$

より慣用的な現代のSchemeの使い方では、これは通常、式を使って処理されます。letrecなぜなら、Lispには1970年代に字句スコープが導入されたからです。

( define Y* ( lambda ( f ) ( letrec ;; (letrec ((g expr)) ...) は g を局所的に定義します(( g ;; expr として再帰的に: expr 内の g は( f ( lambda ( x ) ( g x ))))) ;; 同じ g が定義されているので、g = f (λx. gx) g ))) ;; ((Y* f) ...) = (g ...) = ((f (λx. gx)) ...)

または、内部ラベルなしの場合：

( define Y * ( lambda ( f ) (( lambda ( i ) ( ii ) ) ( lambda ( i ) ( f ( lambda x ( apply ( ii ) x )))))))

この例は、固定小数点コンビネータのやや解釈的な実装です。クラスを使用してfix()、 と呼ばれる関数を格納しますFixedPointCombinator。固定対象の関数は、fixer を継承するクラスに含まれています。関数は、を呼び出すための概念fix()を使用して、固定対象の関数にアクセスします。厳密な関数定義と同様に、 には明示的に追加のパラメータ が渡されるため、遅延評価は不要です。apply()fix()x

std :: same_asを使用します。template < typename Ret , typename Arg , typename T > concept FixedPointApplicable = requires ( Arg x ) { { T :: apply ( x ) } -> same_as < Ret > ; };template < typename Ret , typename Arg , FixedPointApplicable < Ret , Arg > Derived > class FixedPointCombinator { public : static Ret fix ( Arg x ) noexcept { return Derived :: apply ( x ); } };class Factorial : public FixedPointCombinator < long , long , Factorial > { static long apply ( long x ) noexcept { if ( x == 0 ) { return 1 ; } return x * fix ( x - 1 ); } };long result = Factorial :: fix ( 5 );

ラムダ式のみを使用して、次のような不動点コンビネータを作成できます。

auto fix = []( auto f ) { return [ f ]( auto && ... args ) -> decltype ( auto ) { return f ( f , std :: forward < decltype ( args ) > ( args )...); }; };auto factorial = fix ([]( auto self , long n ) -> long { return n == 0 ? 1 : n * self ( self , n - 1 ); });std :: println ( "5! = {}" , factorial ( 5 )); // 120と出力されます

別の例として、SKIコンビネータ計算（組み合わせ論理から与えられた鳥の名前を使用）を用いてZコンビネータを構築し、トランポリン運動を通してテールコールのような動作を実現する方法を示すことができます。

// コンビネータconst K = < A , B > ( a : A ) => ( _b : B ) => a ; // チョウゲンボウconst S = < A , B , C > ( a : ( x : C ) => ( y : B ) => A ) => ( b : ( x : C ) => B ) => ( c : C ) => a ( c )( b ( c )); // ムクドリ// 派生コンビネータconst I = S ( K )( K ); // 恒等式const B = S ( K ( S ))( K ); // ルリツグミconst C = S ( B ( B )( S ))( K ( K )); // ショウジョウコウカンチョウ const W = C ( S )( I ); // ウグイスconst T = C ( I ); // ツグミconst V = B ( C )( T ); // ヒメドリconst I1 = C ( C ( I )); // 恒等式 鳥 1 回削除; C(B(B)(I))(I) と同じconst C1 = B ( C ); // ショウジョウコウカンチョウ 1 回削除const R1 = C1 ( C1 ); // コマドリ 1 回削除const V1 = B ( R1 )( C1 ); // ヒメドリ 1 回削除const I2 = R1 ( V ); // 恒等式 鳥 2 回削除// Zコンビネータconst Z = B ( W ( I1 ))( V1 ( B )( W ( I2 )));const Z2 = S ( K ( S ( S ( K ( S ( S ( K )( K ))( S ( K )( K ))))( S ( K ( S ( K ( S ))( K )))( S ( K ( S ( S ( K )( K ))))( K ))))( K ( S ( S ( K ) ) ))))( S ( S ( K ( S ( S ( K ( S ( K )) S ))( K )))( S ))( K ( K ))))( S ( K ( S ( S ( K ( S ( K ( S ))( K )))( S ))( K ( K ))))( S ( K ( S ))( K ))))( K ( S ( S ( K ( S ( S ( K )( K ))( S ( K )( K ))))( S ( K ( S ( K ( S ))( K )))( S ( K ( S ( S ( K )( K ))))( K ))))( K ( S ( K ( S ( S ( K ( S ( S ( K ( S ( K ( S )))( K )))( S ))( K ( K ))))( S ( K ( S ( S (K ( S ( K ( S ))( K )))( S ))( K ( K ))))( S ( K ( S ( S ( K )( K ))))( K ))))))( K )))))); // 完全に展開された別の形式。const Z3 = S ( S ( K ( S ( S )( K ( S ( S ( K )( K ))( S ( K )( K ))))))( K ))( S ( S ( K ( S )) ( K ))( K ( S ( S ( K ( S ))( S ( K ( S ( K ( S ( K ( S ( S ) ( K ( K ) )))( K )))( S )))( S ( S ( K )( K )))))( K ) ) )( K ( K ( S ( S ( K ) ( K ))( S ( K )( K )))))))); // 別の短いバージョン。const trampoline = < T > ( fn : T | (() => T )) : T => { let ctx = fn ; while ( typeof ctx === "function" ) { ctx = ( ctx as () => T )(); } return ctx ; };const countFn = ( self : ( n : number ) => any ) => ( n : number ) : any => n === 0 ? ( console . log ( n ), n ) : () => self ( n - 1 ); // 代わりにサンク "() => self(n - 1)" を返します。// 例trampoline ( Z ( countFn )( 10 )); trampoline ( Z2 ( countFn )( 10 )); trampoline ( Z3 ( countFn )( 10 ));

名前付き再帰データ型をサポートするプログラミング言語では、無限再帰は${\displaystyle t:=t\to a}$無限型になる可能性のある型を作成する${\displaystyle t}$型に名前を付けると壊れます${\displaystyle t}$明示的に、例えば型として${\displaystyle R\ a}$これは、型と同型である（または単に同義語である）ように定義されています。${\displaystyle R\ a\to a}$。 したがって${\displaystyle R\ a:=R\ a\to a}$再帰型として認識されます。型データ（値）${\displaystyle R\ a}$型が関数である値をタグ付けするだけで作成されます${\displaystyle R\ a\to a}$型に対するデータコンストラクタタグによって${\displaystyle R\ a}$。

例えば、次の Haskell コードでは、 をRecそのタグ名とし、 と を同型性の 2 つの方向の名前とし、型を としますRec。^{[ 19 ] [ 20 ]}app

Rec :: ( R a -> a ) -> R a app :: R a -> ( R a -> a )

（どこ${\displaystyle$ ::} は「型を持つ」という意味です。これにより、次のように記述できます。

newtype R a = Rec { app :: R a -> a } -- app (Rec g) = g -- g :: R a -> a -- Rec g :: R a -- app :: R a -> (R a -> a)y :: ( a -> a ) -> a y f = ( \ x -> f ( app x x )) ( Rec ( \ x -> f ( app x x ))) -- x :: R a -- app x :: R a -> a -- app xx :: a

通常のラムダ計算の定義${\displaystyle \operatorname {Y} f=\operatorname {U} (\lambda x.f\ (\operatorname {U} x))}$（どこ${\displaystyle \operatorname {U} x=x\ x}$したがって、この用語は${\displaystyle \operatorname {U} (\lambda x.f\ (\operatorname {U} x))}$同等性を目撃する${\displaystyle x\ x=f\ (x\ x)}$）は、その核心に自己適用性を含んでいる。${\displaystyle x\ x}$app x xこれは静的型付けプログラミング言語では型付けできません。しかし、上記の式は型付け可能です。同様に、自己適用コンビネータを再定義することもできます。${\displaystyle \operatorname {U} }$そしてそれを

U' g = g ( Rec g ) y f = U' ( \ Rec g -> f ( U' g )) -- g (Rec g) = f (g (Rec g))U'' x = app x x y f = U'' ( Rec ( \ x -> f ( U'' x ))) -- app xx = f (app xx)

またはOCamlでは：

type ' a recc = In of ( ' a recc -> ' a ) let out ( In x ) = xlet y f = ( fun x a -> f ( out x x ) a ) ( In ( fun x a -> f ( out x x ) a ))

または：

let y f = ( fun x -> f ( fun z -> out x x z )) ( In ( fun x -> f ( fun z -> out x x z )))

一部の言語では、名前を付けなくても一般型を再帰的であると明示的にマークすることができます。そうすることで、${\displaystyle \operatorname {Y} }$このような言語におけるコンビネータ。