不動点コンビネータの型付けに苦戦

最近ふと不動点コンビネータについて調べたのですが，直感的に理解しづらい部分が多くあったので整理がてら文章に起こしてみようと思います．特に不動点コンビネータに型を付ける話は再帰型などが登場して混乱しがちだと思います．自分は情報学徒で数学は毛の生えた中学生程度にしかできないので怪しい点もあるかと思いますが，そこは指摘いただけると助かります．

始めに不動点とYコンビネータの話をして，Yコンビネータが評価戦略によっては無限再帰に陥ることにふれ，評価戦略によってはZコンビネータが必要な理由を述べます．それからZコンビネータに型を付ける話をしてみたいと思います．

不動点

（名前がかっこいい）

一般的な関数の不動点（あるいは固定点，定常点）は色々なところで出てくる話かと思います．自分はロジスティック写像で知りました．不動点とは特殊な点のことで，その点においては関数の入力と出力が一致するという性質があります．関数に点の値を入れても点が動かないから不動点というわけです．

不動点の性質を式で書き表すと次式のようになります．

$$f(x) = x$$

このような形の式は人生の中で少なくとも一度はみたことあるんじゃないでしょうか．自分は記憶にないですが．しかし，ここで例えば $f(x)$ を $x^2 + 3$ とかにすれば二次の多項式になります．そして，固定点を求める行為は二次方程式を解くのと同じことになります．人は誰しも一度は不動点を求めていたということになりますね．この例は多項式における不動点ですが，多項式に限らずもっと広い概念で不動点というものを考えることができるみたいです．

不動点コンビネータ

（かっこいい）

コンビネータ論理というラムダ計算と近い関係にある計算モデルがあるらしいです．ラムダ計算からラムダ抽象をなくすかわりに幾つかの原始関数を用意し，これの組み合わせでさまざまな関数を構成できるみたいです（そうなのか）．

不動点コンビネータはコンビネータの一種で，与えられた関数の不動点を求める高階関数です．ラムダ計算やコンビネータ計算では関数の中から自分自身を名前で参照することができません．なので，別の手法で再帰呼出しを実現しなくてはならないのです．そこで役に立つのが不動点コンビネータとなります．発見されている不動点コンビネータはいくつかあるみたいですが，中でも有名なYコンビネータを取り上げようと思います．

Yコンビネータ

(つよそう)

Yコンビネータはハスケル・カリーによって発見されました．その定義はラムダ式では以下のようになります．

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

これを何かしらの関数に適用してみましょう．適用する関数をここでは$g$としておきます．

$$\begin{split} Y g &= (λf\ .\ (λx\ .\ f\ (x\ x))(λx\ .\ f\ (x\ x)))\ g \\ &\longrightarrow (λx\ .\ g\ (x\ x))(λx\ .\ g\ (x\ x)) \\ &\longrightarrow g\ ((λx\ .\ g\ (x\ x))\ (λx\ .\ g\ (x\ x))) \end{split}$$

上の簡約過程をみると，2段目がそのまま3段目のカッコの内側に現れていることがわかります．そして，2段目はそもそも $Y\ g$ であるから結局，

$$Y\ g \equiv g\ (Y\ g)$$

となります．この結果は不動点の定義 $f\ (x) = x$ と同じ形をしています．（左辺と右辺をいれかえ $f = g$，$x = Y\ g$ と読み替えれば一致することが確認できます）

Yコンビネータの悲しい運命

(かなしい）

Yコンビネータを実装しようとすると評価戦略によってはうれしくない問題が発生します．引数を先に評価する評価戦略の場合，簡約が無限に発生し評価が止まらないことになります．

$$Y\ g \longrightarrow g\ (Y\ g) \longrightarrow g\ (g\ (Y\ g)) \longrightarrow \cdots$$

実際にPythonでYコンビネータを用いた階乗の計算をしてみると再帰の上限回数を超えて実行次エラーになります．

>>> Y = (lambda f: (lambda x: f(x(x)))(lambda x: f(x(x))))
>>> Y(lambda f: lambda n: 1 if n == 0 else n * f(n-1))(5)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 1, in <lambda>
  File "<stdin>", line 1, in <lambda>
  File "<stdin>", line 1, in <lambda>
  [Previous line repeated 996 more times]
RecursionError: maximum recursion depth exceeded

これを回避するためには評価戦略を遅延評価（名前渡し）にしたり，Zコンビネータという別種のコンビネータを用いたりする必要があります．やったことないのであまり詳しくないですが，Haskellは遅延評価らしいのでHaskellならYコンビネータをそのまま実装してもよさそうですね．しかし，多くのプログラミング言語処理系は先行評価（正格評価）を採用しているためYコンビネータをそのまま実装すると，Pythonの例で示したようにスタックオーバーフローが発生してしまいます．

Zコンビネータ

（すき）

先に述べた先行評価により簡約が無限に続くという問題はYコンビネータに遅延評価を組み込むことで解決できます．Yコンビネータを先行評価なシステムで用いようとすると，引数の評価が先に先に行われ続けてしまうことが問題でした．これを解消するために，引数をラムダ抽象でラップするのがミソとなっています．この方法で得られるコンビネータは一般的にZコンビネータと呼ばれるようです．この操作は$\eta$-同値性という関数の外延性に基づく同値性によって保証されます．

Zコンビネータの定義を次に示します．下線で示した箇所がYコンビネータから変化があった部分です．

$$Z = λf\ .\ (λx\ .\ f\ (\underline{λy\ .\ x\ x\ y})) (λx\ .\ f\ (\underline{λy\ .\ x\ x\ y}))$$

$Z$が不動点コンビネータであることを確認してみましょう．先ほどと同じように適当な関数$g$を考えます．ちなみにラムダ計算の適用は左結合というのが一般的なようです．なので $(x\ x\ y)$ と $((x\ x)\ y)$ は意味的に同じということですね．自分はよく右結合なのか左結合なのか忘れます．

$$\begin{split} Z\ g &= (λf\ .\ (λx\ .\ f\ (λy\ .\ x\ x\ y)) (λx\ .\ f\ (λy\ .\ x\ x\ y)))\ g \\ &\longrightarrow (λx\ .\ g\ (λy\ .\ x\ x\ y)) (λx\ .\ g\ (λy\ .\ x\ x\ y)) \\ &\longrightarrow g\ (λy\ .\ (λx\ .\ g\ (λy\ .\ x\ x\ y))\ (λx\ .\ g\ (λy\ .\ x\ x\ y))\ y) \end{split}$$

Yコンビネータのときと同様に，3行目のカッコ内と2行目が同じであるため結局，以下のようになることがわかります．

$$Z\ g = g\ (λy\ .\ Z\ g\ y)$$

ここまでは簡約できたのですが，この状態だとパッと見 $x = f(x)$ の形には見えないですね．何か引数を与えたら簡約が進みそうに思えそうです．しかしラムダ計算における関数適用が左結合である点に注意してください．焦って簡約を進めようとして間違えるのはもったいないです．自分も危うく間違えそうになりましたが先人の指摘を発見し修正できました．

ちゃんとカッコをつけると，以下のようになり，間違った例に示すようなベータ簡約（関数適用）は不可能です．

$$Z\ g = (g\ (λy\ .\ Z\ g\ y))$$

以下は間違った例

$$\begin{split} Z\ g\ n =&\ g\ (λy\ .\ Z\ g\ y)\ n \\ \longrightarrow&\ g\ (Z\ g\ n) \end{split}$$

さて，Zコンビネータが不動点コンビネータであることの説明をもう少し厳密に与えてみたいものですが，これ以上簡約が進まないとなると難しいのでしょうか．あるいは，ZコンビネータがYコンビネータの $\eta$-変換であることに注意して，$λy\ .\ Z\ g\ y \iff_\eta\ Z\ g$ と考えるのが妥当なのでしょうか．（このあたりは調べても出てこなかったので助言をいただけると幸いです．）

Zコンビネータを使う

上で示したZコンビネータをまずは型を考えずにプログラミング言語で実装してみます．Zコンビネータの定義を再掲しておきます．

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

この定義をそのままお好きなプログラミング言語のプログラムに置き換えていただくことでZコンビネータが簡単に手に入ります．プログラムに起こす際はラムダ式の結合などにご注意ください．以下はPythonでの実装例です．

Z = lambda f:(lambda x: f (lambda y: x(x)(y))) (lambda x: f (lambda y: x(x)(y)))

階乗

Zコンビネータが得られることがわかりましたが，問題は得たZコンビネータをどう利用するかというところにあります．

Zコンビネータを定義しているラムダ式の内部をよくみると，$f\ (λy\ .\ x\ x\ y)$ という部分項があることがわかります．これは $f$ のとる引数が $λy\ .\ x\ x\ y$ というラムダ抽象（関数）であることを意味します．このラムダ抽象は遅延評価のために導入したもので，これを引数に適用することで必要なタイミングで再帰が発生します．

階乗を例にして考えてみます．四則演算と条件分岐 $\mathtt{if\ e_0\ then\ e_1\ else\ e_2}$ が使えるものとして階乗の源となるプログラムを以下のように定義します．

$$\it{fact} = λf\ .λn\ .\ \texttt{if\ n\ ==\ 0\ then\ 1\ else\ n\ *\ f\ (n-1)}$$

ここからは地道にラムダ式を計算していくだけです．飛ばしても内容的には問題ないと思います．自分は手を動かして試してみないと納得できなかったので地道に計算してみました．おかげでちょっとは納得できたと思います．

$$\begin{split} &Z\ fact\ 2\\ &\longrightarrow_{\beta*} \mathit{fact}\ (λy\ .\ Z\ \mathit{fact}\ y)\ 2\\ &= λf\ .\ λn\ .\ (\texttt{if\ n\ ==\ 0\ then\ 1\ else\ n\ *\ f\ (n-1)})\ (λy\ .\ Z\ \mathit{fact}\ y)\ 2\\ &\longrightarrow_\beta λn\ .\ (\texttt{if\ n\ ==\ 0\ then\ 1\ else\ n\ *}\ (λy\ .\ Z\ {fact}\ y)\ \texttt{(n-1)})\ 2 \\ &\longrightarrow_\beta \texttt{if\ 2\ ==\ 0\ then\ 1\ else\ 2\ *}\ (λy\ .\ Z\ \mathit{fact}\ y)\ \texttt{(2-1)} \\ &\longrightarrow_\texttt{IfF} 2 * (λy\ .\ Z\ \mathit{fact}\ y)\ (2 - 1) \\ &\longrightarrow_\beta 2 * (Z\ \mathit{fact}\ (2 - 1)) \\ \end{split}$$

式が展開されることで $2 * (Z\ \mathit{fact}\ (2-1))$ という形が見えてきました．残りの $Z\ \mathit{fact}\ (2-1)$ の部分も展開してみます．

$$\begin{split} &2 * (Z\ \mathit{fact}\ (2 - 1)) \\ &\longrightarrow_{\beta*} 2 * (\mathit{fact}\ (λy\ .\ Z\ \mathit{fact}\ y)\ (2 - 1))\\ &= 2 * (λf\ .\ λn\ .\ (\texttt{if\ n\ ==\ 0\ then\ 1\ else\ n\ *\ f\ (n-1)}))\ (λy\ .\ Z\ \mathit{fact}\ y)\ (2 - 1)\\ &\longrightarrow_{\beta*} 2 * (\texttt{if 1 == 0 then 1 else 1 * } (λy\ .\ Z\ \mathit{fact}\ y)\ (1 - 1))\\ &\longrightarrow_\texttt{IfF} 2 * 1 * (λy\ .\ Z\ \mathit{fact}\ y)\ 0) \\ &\longrightarrow_{\beta*} 2 * 1 * (\texttt{if 0 == 0 then 1 else 0 * } (λy\ .\ Z\ \mathit{fact}\ y)\ (0 - 1)) \\ &\longrightarrow_\texttt{IfT} 2 * 1 * 1 \\ &= 2 \end{split}$$

というように，先ほどの $\mathit{fact}$ の定義で階乗の計算ができることがイメージできたと思います．（ちょっと長くなったのでどこかミスってそうですけど）

また，これをPythonで実装しても階乗の計算が行えることが確認できます．

factorial = Z(lambda f: lambda n: 1 if n == 0 else n * (f(n-1)))
factorial(5) # 120

型をつける

いよいよ不動点コンビネータに型付けを行ってみたいと思います．と言っても同様のこと自体はこちらの記事で先に試されているようです．

Zコンビネータに関数を適用して得られる階乗の再帰関数は $\texttt{int} \to \texttt{int}$ という型になるはずです．階乗の例だと，整数を入力して整数が返ってきますから，このことは納得いただけるでしょう．$\texttt{int} \to \texttt{int}$ の関数をJavaの関数インタフェースをで書くと以下のようなになります．

Function<Integer, Integer> fact = Z(...);

次に，今省略した部分，つまり不動点コンビネータに渡す関数 $f$ の型を考えます．不動点コンビネータに渡るのは以下のラムダ式です．なのでこのラムダ式の型を考えればいいことになります．

(Function<Integer, Integer> f) -> (Integer n) -> n == 0 ? 1 : n * f.apply(n - 1);

コード自体は先ほどPythonなどで実装した階乗の例をそのままJavaで書き直しただけです．fとnに型がついている点だけが異なります．順番的には逆になりますがnの型を考えます．といっても整数なのでIntegerということは容易でしょう．そしてfの型なのですが，fこそが階乗の関数そのものであるため $\texttt{int} \to \texttt{int}$ という型を持つことになります．

さて，このラムダ式の型ですが，引数は(Function<Integer, Integer> f) -> ...という点からFunction<Integer, Integer>という型を持つことがわかるでしょう．そして出力の方は，(Integer n) -> [整数を返す式]ですからこちらの型もFunction<Integer, Integer>です．ということで，ラムダ式の型はFunction<Function<Integer, Integer>, Function<Integer, Integer>>ということがわかりました．

ここまでの結果をまとめると以下のようになります．...は今から考えるのでこの部分は省略してあります．

static Function<Integer, Integer> Z(Function<Function<Integer, Integer>, Function<Integer, Integer>> f) {
    ... // 今から考える
}

public void perform() {
    Function<Function<Integer, Integer>, Function<Integer, Integer>> _fact =
        (Function<Integer, Integer> f) -> (Integer n) ->
            n == 0 ? 1 : n * f.apply(n - 1);
    Function<Integer, Integer> fact = Z(_fact);
}

再帰する型

（こわい）

Zコンビネータには $(λx\ .\ f\ (λy\ .\ x\ x\ y))$ という部分項が含まれていました．これの，$x\ x$ という部分に注目すると， $x$ に $x$ 自体を適用すると言っているわけですから，これがただの関数適用ではないことが感じ取れます．関数の型を表現するときは $\texttt{param\_type} \to \texttt{return\_type}$ というように型を指定する必要がありますが，この $\texttt{param\_type}$ 自体が関数の型でもあるのです．つまり，型を表現するために自分自身の型に対する自己言及をしなくてはいけないのです^[1]．自己言及的な関数の型を表現できるかどうかは体系によって異なります．単純型システムや純粋なSystem Fではできないです．

階乗の例で考えると$x$ の型を $\alpha$ とすると $x$ の型判断は以下のようになります．

$$\alpha : (\alpha \to \alpha)$$

単純型システムでは型定義から $\alpha$ を消去しなくてはいけませんが，消去するために置換えを行うと再び $\alpha$ が現れてしまい永遠に消去することができません．無限ループこわい．こういう項は少し工夫しないと表現できません．以降はJavaでの表現を試してみます．他の言語だとまた違った表現になったりするようです．さまざまな記事で色々な表現方法が試されていて面白いです．

再帰型でZコンビネータの型付け

@FunctionalInterface
interface R<X> {
    public X apply(R<X> f);
}

かなり唐突ですが，上で定義した関数インタフェースRを用いると $x\ x$ に型付けを行うことができます．具体的には以下のようになります．xの型はR<X>ですが，関数インタフェースの定義より引数の型もR<x>であるため，x.apply(x)というコードが型検査に違反しないというわけです．

大した変化ではないですがIntegerといった具体的な型で指定していたところを型変数Xに変えています．

private static <X> Function<X, X> Z(Function<Function<X, X>, Function<X, X>> f) {
    R<Function<X, X>> x1 = (x) -> {
        return f.apply((X y) -> x.apply(x).apply(y));
    };
    R<Function<X, X>> x2 = (x) -> {
        return f.apply((X y) -> x.apply(x).apply(y));
    };

    return x1.apply(x2);
}

そして，実際にこの型付けされたZコンビネータを用いて階乗を計算することができます！！
長かったですがカタがついてよかったです．

Function<Function<Integer, Integer>, Function<Integer, Integer>> _fact =
    (Function<Integer, Integer> f) -> (Integer n) ->
        n == 0 ? 1 : n * f.apply(n - 1);
Function<Integer, Integer> fact = Z(_fact);

IntStream.range(0, 10).forEach(i -> {
    System.out.printf("fact %d = %d%n", i, fact.apply(i));
});

出力

 [exec] fact 0 = 1
 [exec] fact 1 = 1
 [exec] fact 2 = 2
 [exec] fact 3 = 6
 [exec] fact 4 = 24
 [exec] fact 5 = 120
 [exec] fact 6 = 720
 [exec] fact 7 = 5040
 [exec] fact 8 = 40320
 [exec] fact 9 = 362880

最後に

長いしまとまりのない文章になりました．まだ整理しきれいていない部分や理解が足りていない部分があります．特に多相型システムや再帰型などの型理論のあたりはもっと理解したいと思いました．

参考にした文献・記事など

1. https://nowokay.hatenablog.com/entry/20090409/1239268405
2. https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_fixed-point_combinator
3. https://scrapbox.io/miyamonz/Zコンビネータ
4. https://ja.wikipedia.org/wiki/ラムダ計算#η-変換
5. https://zenn.dev/mineel5/articles/lambdalambdalambda
6. https://qiita.com/mod_poppo/items/4a8128121b11b436d64a

脚注

1. 「自分自身の型に対する自己言及」という表現はフォーマルではないし専門用語ではないです．自分がそのように捉えることで理解しやすいため用いているだけということに注意してください