読者です 読者をやめる 読者になる 読者になる

一歩前進

プログラミングに関する雑多なメモ

不動点とfix演算子

プログラム言語理論 OCaml

ある関数fに対する不動点p とは、  p = f\;p なる p です。 例えば、べき乗^2を関数とみなすと、0^{2}=0, 1^{2}=1 となり、1と0はべき乗^2不動点となります [1]。

プログラム言語の教科書では \mathsf{fix} という演算子が登場します [2,3,4]。 この \mathsf{fix} と先の不動点はどう関係があるのか、フィボナッチ数の例で考えてみます。

フィボナッチ数を求める関数fibは、再帰的に定義すると次のようになります。
 fib(n) := \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;fib(n-1) + fib (n-2)

これをλ式で書くと
  fib = \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;\color{blue}{fib} (n-1) + \color{blue}{fib} (n-2)
となります。しかしfibは、λ抽象の本体に\color{blue}{fib}という自由変数が現れています。

自由変数が現れているので、OCamlで書くとエラーになります(ただし、型なしラムダ計算では許されます)。

# let fib = fun n -> if n==0 || n==1 then 1 else fib (n-1) + (n-2);;
Error: Unbound value fib

不動点

このままでは型付きの言語で再帰が書けません!
考え方を変えてみましょう。 次のような高階関数F_{fib}を定義します。

F_{fib} := \lambda \color{red}{f}. \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;\color{red}{f} (n-1) + \color{red}{f} (n-2)

ここで本体の式にある\color{red}{f}は、λによって束縛された変数であることに注意してください。 このF_{fib}を先ほどのfibに適用してみます。

\begin{align} F_{fib}\,fib &= (\lambda f. \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; f (n-1) + f (n-2))\;fib \\ &= \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; \color{red}{fib} (n-1) + \color{red}{fib} (n-2) \\ &= fib \end{align}

なんと、F_{fib}\,fib = fib という等式を満たすではありませんか!すなわち、fibF_{fib}不動点ということです。

しかし、fib は自由変数が含まれており、実際には定義するとエラーになりました。 ということは F_{fib}fibに適用することだって、本当はできません。 でも、高階関数F_{fib} は定義できました!

不動点コンビネータ

先のfibを定義せず、F_{fib}から不動点なるfibを求めるにはどうしたらいいんでしょうか?

不動点コンビネータは、任意の関数からその関数の不動点を対応させてくれます。 代表的な不動点コンビネータの1つに\mathbf{Y}コンビネータ [1]があり、次のように定義されます。

\mathbf{Y} = \lambda f . (\lambda x. f (xx))(\lambda x.f(xx))

Yコンビネータを使うと、

f:id:succzero:20150618125343p:plain:w400

となり、\mathbf{Y}Fn = F(\mathbf{Y}F)n であることがわかります。

F(\mathbf{Y}Fn)になるのはわかりましたが、これをどうやって計算したらいいんでしょうか? この計算には、

  • (1) 型を考えない(型なしラムダ計算)
  • (2) 名前呼び戦略で計算する

という2点を知っておく必要があります。

(1) 型なしラムダ計算

型なしラムダ計算においては、どんな2つのλ式M, N であっても、MNに適用できます[5]。*1

例として、先の \lambda x . F (\color{red}{x x})の赤字部分は、xを自分自身に適用しています。これって型を考えるとおかしいですよね。 まずFの型はF : (\mathsf{int} \to \mathsf{int}) \to  (\mathsf{int} \to \mathsf{int}) です (最初に定義したfactの型は \mathsf{int} \to \mathsf{int}でした)。 ということは、F (x x)(x x)の型は \mathsf{int} \to \mathsf{int}でなければなりません。

では、関数適用の型付け規則をみてみます。

\displaystyle \frac{e_1 : \tau_1 \to \tau_2 \;\;\; e_2 : \tau_1}{e_1\;e_2 : \tau_2}

ここで、\tau_2 の型は  \mathsf{int} \to \mathsf{int} のはずなので、

\displaystyle \frac{F : \tau_1 \to (\mathsf{int} \to \mathsf{int}) \;\;\; (xx) : \tau_1}{F\;(xx) : \mathsf{int} \to \mathsf{int}}

となります。

(x x) という式は、\tau_1型を要求されています。 これは\mathsf{int} \to \mathsf{int}でなければならないはずです。
では、(x x)xの型についてはどうでしょうか? (x x)だとわかりづらいので、(x_1\,x_2)と表記します。 いま不明な型を\alphaと表します。関数適用の型付け規則から(x_1\,x_2)の型は次のようになります。

\displaystyle \frac{x_1 : \alpha \to (\mathsf{int} \to \mathsf{int}) \;\;\; x_2 : \alpha}{(x_1\;x_2) : \mathsf{int} \to \mathsf{int}}

さて、x_1x_2の型は同じはずです。 x_1の型はいま \alpha \to (\mathsf{int} \to \mathsf{int})なので、 x_2 \alpha \to (\mathsf{int} \to \mathsf{int}) であるべきです。

\displaystyle \frac{x_1 : \color{red}{\alpha} \to (\mathsf{int} \to \mathsf{int}) \;\;\; x_2 : \color{red}{ \alpha \to (\mathsf{int} \to \mathsf{int})}}{(x_1\;x_2) : \mathsf{int} \to \mathsf{int}}

おっと、\alpha\alpha \to (\mathsf{int} \to \mathsf{int})であることを要求されてしまった!

\alpha = \alpha \to (\mathsf{int} \to \mathsf{int}) というように自身の型が再帰的に現れています。 これは再帰型と呼ばれるものだそうです。 ということは、再帰型を扱えれば型付けされたYコンビネータが扱えるということでしょうか。 試してみましょう。

$ ocaml
        OCaml version 4.01.0

#  let y = fun f -> ((fun x -> f (x x)) (fun x -> f (x x)));;
Error: This expression has type 'a -> 'b
       but an expression was expected of type 'a
       The type variable 'a occurs inside 'a -> 'b

$ ocaml -rectypes
        OCaml version 4.01.0

# let y = fun f -> ((fun x -> f (x x)) (fun x -> f (x x)));;
val y : ('a -> 'a) -> 'a = <fun>

OCaml-rectypes を使ってYコンビネータを定義できました。 しかし、OCamlは値呼び戦略の言語であるため、これを実行すると延々と再帰し続け(後述)、スタックオーバーフローになります。 なおこのオプションは、より多くの値を受け付けてしまい、読みづらい型を与えてしまう傾向があるようです [6]。

ここでは単純な型の世界で再帰関数を実現したいので、再帰型は考えないことにします。 ともかく、Yコンビネータは型なしの世界で有効なのです。

(2) 名前呼び戦略 Call by Name

型を考えないとしても、F(\mathbf{Y}Fn) すなわち、 F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) nをどのように計算すればいいでしょうか?

値呼び戦略 (Call by Value, CBV) だと延々と適用が繰り返されてしまいます。 CBVは関数適用の前に引数を先に計算して、その結果の値を関数に渡します。 試しに計算してみます。 Fの引数は(\lambda x. F (x x) ) (\lambda x. F (x x) )ですから、先にそれを計算します。

\begin{align} & F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F ( (\lambda x. F (x x) ) (\lambda x. F (x x) ) ) n \\ &= F (F ( (\lambda x. F (x x)) (\lambda x. F (x x) ) ) ) n \\ &= F (F (F ( (\lambda x. F (x x)) (\lambda x. F (x x) ) ) ) ) n \\ & \dots \end{align}

やはり延々と続いてしまいます。

では名前呼び戦略(Call by Name, CBN)はどうでしょうか? CBNでは、式の評価は名前を呼ばれるまで後回しにします。 ここで、読みやすさのためF' = (\lambda x. F (x x) ) とします。 そして、FF = \lambda \color{red}{f}.\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;\color{red}{f} (n-1) + \color{red}{f} (n-2) です。また、n=5としておきます。

ではCBNで計算してみます。

\begin{align} & F (F' F') 5 \\ &= (\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;(\color{red}{F' F'}) (n-1) + (\color{red}{F' F'}) (n-2)) 5 \\ &= \mathsf{if}\;5=0 \lor 5=1\;\mathsf{then}\;1\;\mathsf{else}\;(\color{red}{F' F'}) (5-1) + (\color{red}{F' F'}) (5-2) \end{align}

おお!5への適用ができました! 引き続き、\mathsf{if}式の中を計算していきます。 \mathsf{if}の条件は\mathsf{false}になりますから、\mathsf{else}節を計算していきます。

\begin{align} &= (\color{red}{F' F'}) (5-1) + (\color{red}{F' F'}) (5-2) \\ &= F (F' F')(5-1) + (\color{red}{F' F'}) (5-2) \\ &= (\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\; (\color{red}{F' F'}) (n-1) + (\color{red}{F' F'}) (n-2) ) (5-1) + (\color{red}{F' F'}) (5-2) \\ &= (\mathsf{if}\;(5-1)=0 \lor (5-1)=1 \\ &\phantom{=(}\;\mathsf{then}\;1 \\ &\phantom{=(}\; \mathsf{else}\;(\color{red}{F' F'}) ( (5-1)-1) + (\color{red}{F' F'}) ( (5-1)-2) ) (5-1) + (\color{red}{F' F'}) (5-2) \end{align}

あとは先ほどの繰り返しです。 以上のように、Yコンビネータ再帰処理が実現できました。

fix

Yコンビネータは型のない世界では有効ですが、型付きの世界では使えません。 そこで\mathsf{fix}演算子です。 これはYと同じように不動点コンビネータとして作用します。

\mathsf{fix}は教科書によっては\mathsf{fix}\;e と書いたり、\mathsf{fix}\;f\;eと書いたりします。 先ほどのFに対して、
前者: \mathsf{fix}\;(\lambda \color{red}{f}. \lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;f (n-1) + f (n-2))
後者: \mathsf{fix}\;\color{red}{f}\;(\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;f (n-1) + f (n-2))
と書きます。後者はe中のfをλで束縛するのではなく、\mathsf{fix}で束縛します。fのスコープは前者同様に、eです。 ここでは後者の定義を用います。

各規則を以下に示します。

評価規則

\frac{\displaystyle \lbrack \mathsf{fix}\;f\;e\,/\,f \rbrack\;e \hookrightarrow V}{\displaystyle \mathsf{fix}\;f\;e \hookrightarrow V}

\lbrack e'/x \rbrack e は式e中の変数xを式e'に置き換える 代入 (substitution) と呼ばれる操作を行います。 これによってF (F'F')のときのように、再帰を実現しています。

型付け規則

\displaystyle \frac{\Gamma,f:\tau \vdash e : \tau}{\Gamma \vdash \mathsf{fix}\;f\;e:\tau}

\tauは関数型を含みます。

実際に式 \mathsf{fix}\;\color{red}{f}\;(\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;f (n-1) + f (n-2))を型付けしてみます。式 (\lambda n. \mathsf{if}\;n=0 \lor n=1\;\mathsf{then}\;1\;\mathsf{else}\;f (n-1) + f (n-2))は型\mathsf{int} \to \mathsf{int}ですから、\tau = \mathsf{int} \to \mathsf{int}になります。

そしてlet recへ

\mathsf{let}\,\mathsf{rec}は、\mathsf{let}\mathsf{fix}の組み合わせで、以下のように定義できます [7]。

\mathsf{let}\,\mathsf{rec}\;x\;=\;e_1\;\mathsf{in}\;e_2\;\; \equiv\;\; \mathsf{let}\;x\;=\;\mathsf{fix}\;x\;e_1\;\mathsf{in}\;e_2

\mathsf{let}\,\mathsf{rec}のほうが使いやすいですが、\mathsf{fix}を使ったほうが計算の意味が見えてくると思います。

fixを実際に使ってみたい

\mathsf{fix} を実際に使ってみたい方(あるいは自分で実装してみたい方)は、 https://github.com/succzero/fino をどうぞ。(なお評価規則は、代入ではなく環境を使ったものになっています。) cabal build すれば使えるはずです。

OCamlではlet recを使ってしまえば、次のように\mathsf{fix}を定義できます。

# let rec fix f x = f (fix f) x;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let fibo = fun f -> fun n -> if n==0||n==1 then 1 else f (n-1) + f (n-2);;
val fibo : (int -> int) -> int -> int = <fun>
# fix fibo 10;;
- : int = 89

Haskellの場合はfix関数が用意されています。

Prelude> import Data.Function
Prelude Data.Function> :i
fix :: (a -> a) -> a    -- Defined in ‘Data.Function’
Prelude Data.Function> let fact = fix (\f -> \n -> if n==0||n==1 then 1 else f (n-1) + f (n-2))
Prelude Data.Function> fact 10
89

まとめ

不動点コンビネータは、任意の関数から不動点を対応付けるものです。 型なしの世界で考えられた不動点コンビネータ(Yコンビネータ)は、単純な型付きの世界では型付けできないものでした。 型付きの不動点コンビネータとして作用する\mathsf{fix}は、式あるいは型式中に再帰的に現れるfに対して、代入操作を行うことで定義できました。 そして、再帰関数を束縛できる\mathsf{let}\,\mathsf{rec}は、\mathsf{let}\mathsf{fix}によって定義付けでき、再帰関数の定義には不動点コンビネータが深く関わっていることをみてきました。

参考文献

[1] Fixed-point combinator - Wikipedia, the free encyclopedia. 2015年6月アクセス.
[2] Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA.
[3] Professor Robert Harper. 2012. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA.
[4] Gilles Dowek and Jean-Jacques Lvy. 2010. Introduction to the Theory of Programming Languages (1st ed.). Springer Publishing Company, Incorporated.
[5] 高橋正子 (1991). 計算論. 近代科学社.
[6] Jeremy Siek. Extensions the the Simply Typed Lambda Calculus. 2015年6月アクセス.
[7] Emmanuel Chailloux, Pascal Manoury, Bruno Pagano. Developing Applications With Objective Caml, Appendix A Cyclic Types, Option -rectypes. 2015年6月アクセス.

*1:対して、型付きλ計算では、型によって定義域・値域が一致する関数適用のみを許します。 こう言うと、型なしのλ計算は不要であるように思えます。しかし、チャーチロッサー定理など、型がなくても議論できるものは型なしで考えるほうが計算の本質を掴みやすいですし、不動点コンビネータとfixでみるように、型なしラムダ計算は型付き言語の基礎を与えています。