不動点コンビネータのソースを表示

{{Redirect3|Yコンビネータ|不動点演算子|カリフォルニア州の企業|Yコンビネータ (企業)}}

'''不動点コンビネータ'''（ふどうてんコンビネータ、{{lang-en-short|fixed point combinator}}、'''不動点結合子'''、ふどうてんけつごうし）とは、与えられた[[サブルーチン|関数]]の[[不動点]]（のひとつ）を求める[[高階関数]]である。'''不動点演算子'''（ふどうてんえんざんし、{{lang-en-short|fixed-point operator}}）、'''パラドキシカル結合子'''（{{lang-en-short|paradoxical combinator}}）などとも呼ばれる。ここで関数 <math>f</math> の'''不動点'''とは、<math>f(x) = x</math> を満たすような <math>x</math> のことをいう。

すなわち高階関数 <math>\boldsymbol{g}</math> が不動点コンビネータであるとは、
:任意の関数 <math>f</math> に対し、<math>p = \boldsymbol{g}(f)</math> とすると, <math>f(p) = p</math> が成立する
事を指す。

あるいは全く同じことだが、不動点コンビネータの定義は、任意の関数 <math>f</math> に対し、
:<math>f(\boldsymbol{g}(f))=\boldsymbol{g}(f)</math>
が成立する事であるとも言い換えられる。

<!--
なお関数'''f''' が[[一階関数]]（{{lang-en-short|first-order function}}、高階関数に対して[[整数]]などの単純な値を取って返す関数）であれば'''f'''の不動点'''p'''　は第一級値（{{lang-en-short|first-class value}}）となるが、'''f''' が高階関数であればぞの不動点'''p''' は関数となる。
-->

[[第一級関数]]をサポートしている[[プログラミング言語]]では、不動点コンビネータを用いて[[識別子]]に[[束縛 (情報工学)#名前束縛|束縛]]されない関数の[[再帰]]を定義することができる。そういったテクニックは、しばしば[[無名再帰]]と呼ばれる。<ref>This terminology appear to be largely [[Mathematical folklore|folklore]], but it does appear in the following:

* Trey Nash, ''Accelerated C# 2008'', Apress, 2007, ISBN 1590598733, p. 462--463. Derived substantially<!--gives him credit!--> from [http://www.linkedin.com/pub/wes-dyer/2/727/a39 Wes Dyer]'s blog (see next item).
* Wes Dyer [http://blogs.msdn.com/wesdyer/archive/2007/02/02/anonymous-recursion-in-c.aspx Anonymous Recursion in C#], February 02, 2007, contains a substantially similar example found in the book above, but accompanied by more discussion.</ref><ref name=ifworks>The If Works [http://blog.jcoglan.com/2008/01/10/deriving-the-y-combinator/ Deriving the Y combinator], January 10th, 2008</ref>

不動点コンビネータは高階関数であるため、その歴史は[[ラムダ計算]]の発達と深く関係している。[[型無しラムダ計算]]（{{lang-en-short|untyped lambda calculus}}）においては、[[ハスケル・カリー]]の <code>'''Y''' = λf·(λx·f (x x)) (λx·f (x x))</code> という不動点コンビネータがよく知られている。型無しラムダ計算には無数の不動点コンビネータが存在するが、一方で[[型付きラムダ計算|単純型付きラムダ計算]]などのより限定的な[[計算模型|計算モデル]]では、不動点コンビネータは必ずしも存在するとは限らない。

== 不動点コンビネータによる再帰の実現 ==
不動点コンビネータにより、第一級関数をサポートしているプログラミング言語において、明示的に[[再帰]]を書かずに再帰を実現する為に用いる事ができる。なお、一般にそういった言語では普通に再帰が使えるので、プログラミングにおいてはパズル的なテクニック以上の意味は無い。一方、循環なく関数の意味を定義する（できる）、ということは、計算理論の上では重要である。

まず、再帰関数の性質を簡単に振り返り、記号をいくつか定義する。関数 <math>a</math> が再帰的に定義されているとき、 <math>a</math> の定義式は何らかの高階関数 <math>U</math> を用いて、

{{NumBlk|:|<math id="1">a(x) = U(a,x)</math>|{{EquationRef|Eq. 1}}}}

と書ける。たとえば <math>a(x)</math> が <math>x</math> の[[階乗]]を計算する関数である場合、 <math>U</math> として

: <math>U(f,x) = \begin{cases}
  1 & \text{if } x=0 \\
  x f(x-1) & \text{otherwise}
\end{cases}</math>

を取る事ができる。上述のように定義された <math>U</math> が({{EquationNote|Eq. 1}})を満たすのは明らかであろう。

<math>U</math> を用いて高階関数 <math>V</math> を

{{NumBlk|:|<math>V~:~f \mapsto U(f,\cdot)</math>|{{EquationRef|Eq. 2}}}}

と定義する。
（すなわち <math>V</math> は関数 <math>f</math> を入力として受け取ると
関数「<math>x \mapsto U(f,x)</math>」を出力する高階関数である。
[[ラムダ計算]]の用語で言えば、 <math>V
</math> は <math>U</math>  の[[カリー化]]<math>\lambda f. (\lambda x. U)</math>にあたる。）
<math>V</math> の定義より、<math>V(f)</math>はそれ自身関数であり、任意の <math>x</math> に対し、

{{NumBlk|:|<math>V(f)(x)=U(f,x)</math>|{{EquationRef|Eq. 3}}}}

が成り立つ。ここで <math>V(f)(x)</math> は関数<math>V(f)</math>に <math>x</math> を入力したときの値。



さて、'''''g''''' を不動点コンビネータとするとき、不動点コンビネータの定義より特に、
<math>\boldsymbol{g}(V)</math>は <math>V</math> の定義域の元である事が分かる。
<math>V</math> の定義域は関数の集合だったので、これはすなわち <math>\boldsymbol{g}(V)</math> はそれ自身関数である事を意味する。
この関数 <math>\boldsymbol{g}(V)</math> が式で定義された再帰関数 <math>a</math> と一致する事を示す事ができる（後述）。

よって以下のようにすれば不動点コンビネータ'''''g''''' で再帰関数 <math>a</math> を実現できる事になる：

# ''U'' のプログラムを書く。
# ''V'' を{{EquationNote|Eq. 2}}式のように定義し、<math>a=\boldsymbol{g}(V)</math>とする。

=== <math>a=\boldsymbol{g}(V)</math> の証明 ===
最後に<math>\boldsymbol{g}(V)</math>が {{EquationNote|Eq. 1}} で定義された再帰関数 <math>a</math> と一致する事を示す。
不動点コンビネータの定義より、<math>\boldsymbol{g}(V)</math>は

{{NumBlk|:|<math>V(\boldsymbol{g}(V))=\boldsymbol{g}(V)</math>|{{EquationRef|Eq. 4}}}}

を満たす。

前述したように<math>\boldsymbol{g}(V)</math>はそれ自身関数なので、値''x''に対し<math>\boldsymbol{g}(V)(x)</math>を考える事ができる。
<math>\boldsymbol{g}(V)(x)</math>は以下を満たす：

{| cellpadding="0"
| <math>\boldsymbol{g}(V)(x) </math>    
| <math>=V(\boldsymbol{g}(V))(x) </math>
|style="padding-left:30px;"| ({{EquationNote|Eq. 4}}より)
|-
| 
| <math>=U(\boldsymbol{g}(V),x) </math>、
|style="padding-left:30px;"| ({{EquationNote|Eq. 3}}より)
|}

すなわち

{{NumBlk|:|<math>\boldsymbol{g}(V)(x)=U(\boldsymbol{g}(V),x)</math>|{{EquationRef|Eq. 5}}}}

{{EquationNote|Eq. 1}} と {{EquationNote|Eq. 5}} を見比べると、{{EquationNote|Eq. 5}} は {{EquationNote|Eq. 1}} で <math>a</math> を <math>\boldsymbol{g}(V)</math> に置き換えたものに等しい事が分かる。
{{EquationNote|Eq. 1}}は <math>a</math> の（再帰的な）定義式であったので、これはすなわち <math>\boldsymbol{g}(V)</math> が <math>a</math> の定義式を満たす事を意味する。
よって

: <math>a=\boldsymbol{g}(V)</math>。  

が成立する事が分かった。<!--
ここでは関数に不動点コンビネータを適用するとどのように動くかを説明する（実際の不動点コンビネータの例については後述）。計算過程を簡単に追えるようにするため、プログラミング言語として型無しラムダ計算を用いる。不動点コンビネータの定義式から導き出される式は、ラムダ計算のβ簡約に対応する。

不動点コンビネータを適用する関数の具体例として、ここでは[[階乗]]関数を用いる。

:'''fact'''(''n'') = if ''n''=0 then 1 else ''n'' * '''fact'''(''n''-1)

この再帰の単一段階は、真偽値を通常の方法で符号化し、数値をチャーチ符号化したラムダ抽象を用いて次のように表現することができる。

 '''F''' = λf. λx. IFTHENELSE (ISZERO x) 1 (MULT x (f (PRED x)))

なお、大文字で示した関数はすべてラムダ抽象を用いて定義される。'''F'''の中のfは階乗関数自身のプレースホルダー引数である。

不動点コンビネータFIXを'''F'''に適用したときに何が起こるか、そして得られた抽象が実際に階乗関数であるかどうかを調べ、それに今度はチャーチ数を適用する。

 (FIX '''F''') n = ('''F''' (FIX '''F''')) n =  --- FIXの定義式を展開
           = (λx. IFTHENELSE (ISZERO x) 1 (MULT x ((FIX '''F''') (PRED x)))) n --- 最初の'''F'''を展開
           = IFTHENELSE (ISZERO n) 1 (MULT n ((FIX '''F''') (PRED n))) --- nに抽象を適用する

いまFIX '''F'''をFACTとおくと、抽象FACTへの任意のチャーチ数の適用が実際に階乗を計算していることが分かる。

 FACT n = IFTHENELSE (ISZERO n) 1 (MULT n (FACT (PRED n))).

ラムダ計算の考え方では、すべてのラムダ抽象は本質的に無名であり、名前を与えることは単なる[[糖衣構文]]にすぎない。したがって、ここで再帰関数FACTと何らかの「再帰でない」Fを対比させることは無意味である。不動点演算子の真の価値はその再帰方程式を解く能力にある。すなわち、FACTの方程式を満たすようなラムダ抽象は存在するか?という質問に置き換えることができる。答えはイエスであり、そのような抽象を作り出す「機械的な」手続きが存在する。上記のように'''F'''を単純に定義し、任意の不動点コンビネータFIXを使用して、FIX '''F'''としてFACTを得ることができる。

プログラミングにおいては、関数の呼び出し側でFACTをFIX '''F'''で置き換えることはしばしば無名再帰と呼ばれる。ラムダ抽象'''F'''では、FACTは[[自由変数と束縛変数|束縛変数]]fによって表現されており、これはプログラミング言語における引数に該当する。したがって'''F'''は識別子に束縛される必要がない。引数fはそれ自身が関数として呼ばれているので'''F'''は高階関数である。プログラミング言語は引数として関数を渡すことを許容しなければならない。さらに関数リテラルもサポートしなければならない。というのは、FIX '''F'''は識別子というよりはむしろ式だからである。なお、実地ではプログラミング環境や型チェッカが採用している評価戦略に依存するので、FIXにはさらなる制限がかかる（後述）。-->

== 不動点コンビネータの例 ==
型無しラムダ計算や[[組合せ論理]]などの特定の数学的な計算形式化においては、すべての式は高階関数とみなすことができる。これらの形式化では、不動点コンビネータが存在することはすなわち、'''すべての関数が少なくとも1つの不動点を持つ'''ことを意味する。さらに、関数は複数の異なる不動点を持つことができる。

単純型付きラムダ計算などの他のいくつかの体系では、十分に型付けされた不動点コンビネータを書くことはできない。それらの体系で再帰をサポートするには、明示的に言語体系に組み込む必要がある。それでも[[再帰データ型]]によって拡張された単純型付きラムダ計算などでは不動点演算子を書くことができるが、ある種の「実用的な」不動点演算子（常にいずれかの適用を返すもの）は制限される。[[多相ラムダ計算]]（{{lang-en-short|polymorphic lambda calculus}}、[[システムF]]、{{lang-en-short|System F}}）では多相不動点コンビネータは型 <math>\forall{a} .(a \rightarrow a) \rightarrow a</math> を持つ（ただし <math>a</math> は型変数である）。

===Yコンビネータ===
型無しラムダ計算においてよく知られた（そしておそらく最もシンプルな）不動点コンビネータは'''Y'''コンビネータと呼ばれる。これはハスケル・カリーによって発見されたもので、次のように定義される。

<code>'''Y''' = (λf . (λx . f (x x)) (λx . f (x x)))</code>

実際に関数''g''を適用することによって、この関数が不動点コンビネータとして動作するのが分かる。

{| cellpadding="0"
| <code>'''Y''' g</code>
| <code>= (λf . (λx . f (x x)) (λx . f (x x))) g</code>
|style="padding-left:30px;"| ('''Y'''の定義より)
|-
|
| <code>= (λx . g (x x)) (λx . g (x x))</code>
|style="padding-left:30px;"| (λfのβ簡約、主関数をgに適用)
|-
|
| <code>= (λy . g (y y)) (λx . g (x x))</code> 
|style="padding-left:30px;"| (α変換、束縛変数の名前を変える)
|-
|
| <code>= g ((λx . g (x x)) (λx . g (x x)))</code> 
|style="padding-left:30px;"| (λyのβ簡約、左の関数を右の関数に適用)
|-
|
| <code>= g ('''Y''' g)</code> 
|style="padding-left:30px;"| (第2式より)
|}

これをそのまま[[ラムダ計算]]で使うと、[[評価戦略]]が値渡しだった場合には <code>('''Y''' g) が (g ('''Y''' g))</code> と展開された後も、引数の値を先に求めようとして <code>(g (g ('''Y''' g))) →...→ (g ... (g ('''Y''' g))...)</code> のように無限に展開され続けて止まらなくなってしまうので、次節で示すZコンビネータのように修正する。評価戦略が名前渡しの場合はこのまま使える。

このカリーによるコンビネータのみをYコンビネータとすることもあるが、実装などでは不動点コンビネータを指す名前として他の形であってもYという名前を使っていることもある（[[#グラフ簡約]]の節の注を参照せよ）。

[[SKIコンビネータ計算]]では次のようになる。
:<code>'''Y''' = S (K (S I I)) (S (S (K S) K) (K (S I I)))</code>

===Zコンビネータ===
{{see also|無名再帰}}
値渡し評価（適用順序）でも使用可能なバージョンの'''Y'''コンビネータは、通常の'''Y'''コンビネータの一部をη変換することで与えられる。

:<code>'''Z''' = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))</code>

[[Python]] での実装。その他のプログラミング言語での実装は[[無名再帰]]を参照。
<syntaxhighlight lang="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)
</syntaxhighlight>

===チューリング不動点コンビネータ===
もう一つの一般的な不動点コンビネータは、チューリング不動点コンビネータである（発見者である[[アラン・チューリング]]の名にちなむ）。
:<code>'''Θ''' = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))</code>
これはシンプルな値渡し形式も持つ。
:<code>'''Θ'''<sub>'''v'''</sub> = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))</code>

===SとKによる最もシンプルな不動点コンビネータ===
[[SKIコンビネータ計算]]のSとKによる最もシンプルな不動点コンビネータは、[[ジョン・トロンプ]]によって発見された以下であり、
:<code>'''Y'''' = S S K (S (K (S S (S (S S K)))) K)</code>
これは次のラムダ式と対応する。
:<code>'''Y'''' = (λx. λy. x y x) (λy. λx. y (x y x))</code>

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

次のようないくつかの不動点コンビネータ（[[ジャン・ウィレム・クロップ]]によって組み立てられた）は、主として遊びに使われる。
:<code>'''Y<sub>k</sub>''' = (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)</code>
ここで
:<code>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))</code>

===非標準不動点コンビネータ===
型無しラムダ計算には不動点演算子と同じ[[ベーム木]]（{{lang-en-short|Böhm tree}}）を持つラムダ式がある。すなわちそれらは <code>λx.x(x(x ... ))</code> と同じ無限の拡張を持つ。これは'''非標準不動点コンビネータ'''（{{lang-en-short|non-standard fixed point combinators}}）と呼ばれる。定義より、あらゆる不動点コンビネータは非標準でもあるが、すべての非標準不動点コンビネータが不動点コンビネータであるわけではない。それらのいくつかは「標準」の定義を満たさないからである。これらの変わったコンビネータは特に strictly non-standard fixed point combinators と呼ばれる。例として、<code>B = λx.xx</code> かつ <code>M = λxyz.x(yz)</code> としたときのコンビネータ <code>N = BM(B(BM)B)</code> が挙げられる。非標準不動点コンビネータの集合は帰納的可算集合ではない。<ref name=gold/>

==不動点コンビネータの実装==
これまでの節で実装というよりは主に理論の観点から述べてきた、[[評価戦略]]が名前渡しの場合と値渡しの場合の違いは、実装においては、非正格(non-strict)な[[プログラミング言語]]（ないし処理系）と正格(strict)な言語の場合にほぼそのまま対応する。非正格な（[[遅延評価]]の、と言い換えてもだいたい同じ。具体的には[[Haskell]]などがそう）言語ないし処理系においては、ほぼ不動点コンビネータの意味そのままに循環的に実装できる。正格な場合は修正が必要であり、後述する。理論的には循環が無いことに意味があったが、実装においては循環的で普通は問題が無く、そのほうが効率的でもある。以下にHaskellによる不動点コンビネータの実装を示す。この不動点コンビネータはHaskellにおいては伝統的に<code>fix</code>と呼ばれる。<code>fix</code>は多相不動点コンビネータであることに注意せよ（前述のシステムFに関する議論も参照）。なお、Haskellには[[型推論]]があるが、以下では曖昧さをなくすために型は明記する（一般に、こういった特殊な型を使う場合は型を明記したほうが良いし、推論の実装の限界のために明記が必要なこともある）。定義の後に使用例が続く。

なお、型無しラムダ計算における'''カリーのYコンビネータ'''は、そのまま実装しようとすると、Haskellの型チェッカによって拒否される。<ref>Haskell mailing list thread on [http://groups.google.co.uk/group/fa.haskell/browse_frm/thread/f0a62b6de1416d8b How to define Y combinator in Haskell], 15 Sep 2006</ref>

<!--<syntaxhighlight lang=Haskell> はconstを予約語として表示する。このケースでは非常に紛らわしい。 -->
<pre>
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と評価される
</pre>

<code>fix</code>の適用は遅延評価されるので[[無限ループ]]にはならない。たとえば<code>fix (const 9)</code>が<code>(const 9)(fix f)</code>として展開されるとき、部分式<code>fix f</code>は評価されない。ところが、Haskellによるfixの定義を正格(strict)プログラミング言語に持ち込むと無限ループになる。なぜなら、fへ渡した引数は事前に展開され、無限の呼び出しの連続<code>f (f ... (fix f) ... ))</code>を生み出すからである。

<!--TODO: ここを書き直す -->
[[ML (プログラミング言語)|ML]]のような正格言語においては、クロージャの使用を強制することによって無限再帰問題を回避することができる。<code>fix</code>の正格なバージョンは型 <math>\forall{a}.\forall{b}.((a \rightarrow b) \rightarrow (a \rightarrow b)) \rightarrow (a \rightarrow b)</math> を持つべきである。要するに、これは関数を取って返す関数でのみ動く。例として、以下は<code>fix</code>の正格なバージョンのOCamlコード実装である。

<syntaxhighlight lang=ocaml>
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" と評価される *)
</syntaxhighlight>

以下は [[Python]] での実装。
<syntaxhighlight lang="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)
</syntaxhighlight>

Java 8 や C++11 では無名関数（ラムダ式）が使えるので上記と同じ方法で実装できる。それよりも前の時代の Java や C++ では少々複雑だった<ref>[http://arcfn.com/2009/03/y-combinator-in-arc-and-java.html The Y Combinator in Arc and Java] - Javaコード</ref><ref>[http://stackoverflow.com/questions/152084/fixed-point-combinators-in-c/154267#154267 bind - Fixed point combinators in C++ - Stack Overflow] - C++コード</ref>。

===再帰型による符号化の例===
再帰データ型（[[システムF#システムFω|システムF<sub>ω</sub>]]を参照）をサポートしているプログラミング言語では、型レベルで再帰を適切に計算することによってYコンビネータの型付けが可能になる。変数xを自己適用する必要性は同型の (Rec a -> a) を用いて定義される型 (Rec a) によって管理することができる。

例として、以下のHaskellコードは、型とともに同型写像のInとoutの2つの方向の名前を持つ。

<pre>
In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)
</pre>

そして次のように書くことができる。

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

OCamlによる等価なコードは以下。

<syntaxhighlight lang="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))
</syntaxhighlight>

=== グラフ簡約 ===
[[File:FixedPointCombinatorGraphReduction.svg|left]]
グラフ簡約（[[:en:Graph reduction]]を参照）による計算系では、不動点コンビネータへの適用(apply, application)は理論通り展開しても良いが、左の図のように循環のあるグラフに簡約するという一種の、のぞき穴的[[コンパイラ最適化|最適化]]が知られている。また、これは'''カリーのYコンビネータ'''ではないが(この図のように)便宜的にYという名前で呼ばれていることもある<ref>たとえば、[[:en:David Turner (computer scientist)|Turner]]の"A New Implementation Technique for Applicative Languages"（{{doi|10.1002/spe.4380090105}}）の Figure. 3 と、その直前の説明を見よ。</ref>。
{{-}}

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

==関連項目==
* [[不動点反復法]]
* [[無名関数]]
* [[固有関数]]

==脚注==
{{reflist}}

==参考文献==
* Werner Kluge, ''Abstract computing machines: a lambda calculus perspective'', Springer, 2005, ISBN 3540211462, pp. 73-77<!-- covers the how it works section, but does not use Wikipedia/Javascript/C# terminology like "anonymous recursion". -->
* Mayer Goldberg, (2005) ''[http://www.brics.dk/RS/05/1/BRICS-RS-05-1.pdf On the Recursive Enumerability of Fixed-Point Combinators]'', BRICS Report RS-05-1, University of Aarhus<!--covers most of the theory-->

{{DEFAULTSORT:ふとうてんこんひねた}}
[[Category:ラムダ計算]]
[[Category:数理論理学]]
[[Category:理論計算機科学]]
[[Category:計算理論]]
[[Category:形式手法]]
[[Category:関数型プログラミング]]
[[Category:不動点]]
[[Category:数学に関する記事]]
[[Category:コンビネータ論理]]
[[Category:再帰]]