相互再帰の不動点コンビネータ
型無しラムダ計算において，Yコンビネータ
$$
\mathbf{Y} := \lambda f. \ (\lambda x. \ f \ (x \ x)) \ (\lambda x. \ f \ (x \ x))
$$
によりラムダ項$F$の不動点$\mathbf{Y} \ F = F \ (\mathbf{Y} \ F)$が得られ，再帰関数が実現できることはよく知られている．実は，Yコンビネータを用いることでラムダ項$F, G$に対し
\begin{eqnarray}
\left\{
\begin{array}{l}
M = F \ M \ N \\
N = G \ M \ N
\end{array}
\right.
\end{eqnarray}
なる相互再帰の不動点の組$(M, N)$を作ることができる．そのためにはタプルが必要なので，型無しラムダ計算の枠組みの中でタプルを扱うためにいくつかのエイリアスを定義する．
$$
[a, b] := \lambda p. \ p \ a \ b \\
\mathbf{proj_1} := \lambda t. \ t \ (\lambda a. \ \lambda b. \ a) \\
\mathbf{proj_2} := \lambda t. \ t \ (\lambda a. \ \lambda b. \ b)
$$
これで$\mathbf{proj_1} \ [a, b] = a$, $\mathbf{proj_2} \ [a, b] = b$と書ける．続いて,$F, G$のタプルを受け取るバージョン
$$
F' := \lambda t. \ F \ (\mathbf{proj_1} \ t) \ (\mathbf{proj_2} \ t) \\
G' := \lambda t. \ G \ (\mathbf{proj_1} \ t) \ (\mathbf{proj_2} \ t)
$$
を用意する．これらを用い，$F, G$をタプルにまとめて不動点を取ればよい．すなわち，
$$
P := \mathbf{Y} \ (\lambda t. \ [F' \ t, G' \ t])
$$
とすると，
$$
\mathbf{proj_1} \ P = \mathbf{proj_1} \ ((\lambda t. \ [F' \ t, G' \ t]) \ P) = \mathbf{proj_1} \ [F' \ P, G' \ P] = F' \ P \\
\mathbf{proj_2} \ P = \mathbf{proj_2} \ ((\lambda t. \ [F' \ t, G' \ t]) \ P) = \mathbf{proj_2} \ [F' \ P, G' \ P] = G' \ P
$$
なので，$M := \mathbf{proj_1} \ P$, $N := \mathbf{proj_2} \ P$とおけば，
\begin{eqnarray}
\left\{
\begin{array}{l}
M = F' \ P = F \ M \ N \\
N = G' \ P = G \ M \ N
\end{array}
\right.
\end{eqnarray}
を得る．これは直ちにn個のラムダ項$F_1, \dots, F_n$の相互再帰に一般化できる．n個のタプルを
$$
[a_1, \dots, a_n] := \lambda p. \ p \ a_1 \dots a_n \\
\mathbf{proj_i} := \lambda t. \ t \ (\lambda a_1. \ \dots \ \lambda a_n. \ a_i)
$$
とし，
$$
F_i' := \lambda t. \ F \ (\mathbf{proj_1} \ t) \dots (\mathbf{proj_n} \ t)
$$
とおいて
$$
P := \mathbf{Y} \ (\lambda t. \ [F_1' \ t, \dots, F_n' \ t]) \\
M_i := \mathbf{proj_i} \ P
$$
とすれば，
\begin{eqnarray}
\left\{
\begin{array}{l}
M_1 = F_1 \ M_1 \dots M_n \\
\vdots \\
M_n = F_n \ M_n \dots M_n
\end{array}
\right.
\end{eqnarray}
なる不動点の組$(M_1, \dots, M_n)$を得る．ここでタプルに対する$\mathbf{map}$関数を
$$
\mathbf{map} := \lambda f. \ \lambda t. \ [f \ (\mathbf{proj_1} \ t), \dots, f \ (\mathbf{proj_n} \ t)]
$$
で定義すると，Yコンビネータを用いて$P$を計算する部分は
$$
\mathbf{Y^*} = \lambda g. \ \mathbf{Y} \ (\lambda t. \ \mathbf{map} \ (\lambda f. \ f \ t) \ g) \\
[M_1, \dots, M_n] := \mathbf{Y^*} \ [F_1', \dots, F_n']
$$
と書ける．この$\mathbf{Y^*}$をY*コンビネータと言う（らしい）．
