コンビネータ

ラムダ計算の親戚みたいな理論として、コンビネータ理論がありますがこのページの趣旨は、理論的なことはさておきコンビネータを使って遊んでみようというものです。例えばコンビネータを使うと「引数の順序を入れ替えたり、入れ替えて適用する」といったことができます。なお、ここではλ式について少し知識があることを仮定しています。最初にコンビネータとは何かというと「自由変数を含まないλ式」、と定義されています。自由変数とはλ式において束縛されていない変数のことで letによる関数定義をλ式の定義とみなすと　引数が束縛変数、　既に定義されてる識別子が自由変数になります。

自由変数と束縛変数

let x = 10;;
//λx.yxのつもり
let f y = y x;;	//x:自由変数、y:束縛変数

コンビネータに関する本としてスマリヤンの本「To mock a mocking bird」 (邦題：数学パズルものまね鳥をまねる―愉快なパズルと結合子論理の夢の鳥物語) は有名です。この本の楽しいところは、様々なコンビネータに鳥の名前を付けていて特定のコンビネータの組み合わせで表現出来るもの全体を森(forest)と呼んだりしてるところです。 (ex.KestrelとStarlingがいる森には、ものまね鳥(Mockingbird)がいる　M=S(SKK)(SKK)といった風に計算できるため) ちなみに、Starlingはムクドリで Kestrelはチョウゲンボウだそうです。いくつか見てみましょう。

コンビネータの例

let i x = x;;            //Identity bird
let istar x y = x y;;    //Identity bird once removed
let b x y z = x (y z);;  //Blue bird：瑠璃鶇(ルリツグミ)
let t x y = y x;;        //Thrush：鶫(ツグミ)
let c x y z = x z y;;    //Cardinal：コウカンチョウ

最初のIコンビネータは、引数をそのまま返すコンビネータです。 istarはI*というコンビネータで、これもIコンビネータの仲間です。 (starは短く発音するために私が勝手につけた名前です) 以下の2つの結果は同じになります。

I*コンビネータ

      (fun x -> x+1) 2 |> printfn "%d";;
istar (fun x -> x+1) 2 |> printfn "%d";;

こんなのが何の役に立つんだ！と思うかもしれないですが高階関数と組み合わせたりすると便利なことがあります。 (Iコンビネータはidだとか identityだとかいう名前で見かけることが多い) 以下はIコンビネータを利用した例です。

木構造へのfold関数を作る

type Tree = L of int | B of Tree * Tree;;
let rec tfold_fg f g tree =
    match tree with
        | L(i) -> f i
        | B(l,r) -> g (tfold_fg f g l) (tfold_fg f g r);;
tfold_fg i (fun x y -> x+ y) (B(B(L(1),L(2)),L(3))) |> printfn "%A";;

Treeは木構造を表すデータ型(Lが葉、Bが枝)で tfold_fgは　・木構造の葉に作用する関数f 　・左右のノードの結果に作用する関数g を使って値を折りたたむ関数です。この例では、単に和を求めたいだけだったので葉に対する処理は何もしないという意味でIコンビネータを渡しています。 I*に関しては F#で演算子を定義すれば演算子の優先順位と結合性を変更出来ることを利用して関数呼び出しの括弧を減らすのにもつかえます。

I*コンビネータの利用

let ( ** ) = istar;; //let ( ** ) x y = istar x y;;
let ( ||>) = istar;;

let f x = x + 1;;
let g x = x * 2;;
printfn "%d" (f (g 10));;
printfn "%d" ** f ** g 10;;
//printfn "%d" ||> f ||> g 10;;	//エラー

ライブラリを作る際はI,I*,I**,...コンビネータはシンタックスシュガー作りにも使えそうです

シンタックスシュガー

let pen = "pen";;
let a x = x;;		//Iコンビネータ
let is x = a x;;		//I*コンビネータ
let this x = is x;;	//I**コンビネータ
> this is a pen;;
val it : string = "pen"</a>

Bコンビネータは関数合成に相当するコンビネータです。 TやCは引数の順序を入れ替えるのに使えるコンビネータです。 Tは1番目と2番目、Cは2番目と3番目を入れ替えます。ちなみに、これ以後は 3番目と4番目を入れ替えるC*, 4番目と5番目を入れ替えるC**, C***,...と続きます。

Cコンビネータの利用

c List.map [1..10] ((+)1) |> printfn "%A";;

引数を入れ替えたい時ってのはわりとあるもので結構便利に使えます。ただし、あまり順番を入れ替えすぎてしまうとコードがわかりにくくなってしまう恐れもあり使いすぎには注意したほうが良いと思います。 Bコンビネータを次のように使えばC*,C**,...を定義するのにも使えます。 C*=B C C**= B C* ... (ただ、B T≠Cです) Wコンビネータ(Warbler：うぐいす)なんかも同様にしてW*,W**が定義できます。他のコンビネータにも興味がある方はこの素晴らしいページへ。鳥の名前一覧もあって、しかもコンビネータ計算機付きです

F#での制限事項

次の例を動かそうとすると

Bコンビネータで

let cstar a b c d = a b d c;;	//OK
//(('a -> 'b -> 'c -> 'd) -> 'a -> 'c -> 'b -> 'd)
let cstar2 = b c;;	//NG
//(('_a -> '_b -> '_c -> '_d) -> '_a -> '_c -> '_b -> '_d)と推論

cstar2は型エラーのため定義できません。これは、結論から言えば「書き換え可能な変数」があるために型推論の規則に制限(value restriction)があるからだそうです。こうした制約はML系の言語は何らかの形で持っているそうで F#の場合は「メンバ、コンストラクタ、関数、type functionではない任意の要素の　結果のシグニチャはfree inference type variablesを含んではならない」　　The resulting signature of any item that is not a member, 　　constructor, function, or type function 　　must not contain any free inference type variables; 　　if so, a value restriction. error is reported. となっています(12.1) 他のML系言語関連の説明も役に立つと思いますのでプログラミングin OCamlの78-79,162-163ページやここやここなども参考に挙げてみます。 StackOverflowのスレッドには上のエラーに対して次の2つの解決策が載っています。　1.型注釈を付ける(これはそのままの意味) 　2.η変換(の逆の操作)を利用する η(イータ)変換というのは、関数fについて、fun x -> f xをfに変換することです。 (fun x -> f x)とfは、どちらも同じ引数に対して同じ結果を返すので、これらを同じものと見なしてしまうというのが基本的なアイデアです。先ほどのコンビネータでの型エラーは、部分適用によって未解決のfree inference type variableが残ってしまったのが原因なので具体的には次のようにします(η変換の逆の操作) エラーメッセージから、推論された型は4つの引数をとることがわかるので引数を4つほど追加して

Bコンビネータで

let cstar3 x y z w = b c x y z w;;

このようにするとfree inference type variableが無くなるためエラーが出なくなります。 F#ではこういう制限があったりするのでコンビネータ自体について興味があるなら先ほど紹介したcombinator birdsの計算機や petit lambdaなどのソフトウェアを使ったほうが面倒がなくて良いかもしれません。次のサイトにはλ項のみで様々な計算を行う方法が紹介してあるので興味を引かれた人はコンビネータ版への書き換えに挑戦してみてはいかがでしょうか (参考：Church Numerals と Lambda Calculus ところでλ計算には型のあり/なしという観点での分類があってオリジナルのコンビネータの理論は型無しλ計算(untyped lambda calculus)と対応していますが、 F#は型付きλ計算(typed lambda calculus)を背景としています。 (※2、※3型付きのコンビネータの理論はCartesian Closed Categoryというものに対応してるそうです) Churchが型のないλ計算に変わって、型付きのλ計算を導入したのはラッセルのパラドックスが起こらないようにするためだったという経緯があるため(※1) 型付きのλ計算の中でも単純型付きλ計算(simply typed lambda calculus)と呼ばれているものは型なしλ計算よりも計算出来る範囲が狭くなります。おそらくそのあたりのことが原因で λ計算の世界で再帰を実現するためのコンビネータとして有名なYコンビネータは、単純型付きλ計算の世界では定義できません。 F#でも、普通にやると型エラーが起きてしまいます。しかし、型ありのλ計算に再帰型を加えれば型なしのλ計算と同じ計算能力になることがわかっているそうで F#でも再帰的な型を使って、Yコンビネータが定義できます。 ※1 Proofs are Programs: 19th Century Logic and 21st Century Computingの3 Typed lambda calculus ※2 P.-L. Curien (1986) Combinators Categoriques. Algorithmes Sequentiels et Programmation Applicative. These de Doctorat detat. Univ. Paris VII. または P.-L. Curien (1993) Categorical Combinators, Sequential Algorithms and Functional Programming. Progress in Theor. Comp. Sci., Birkhauser. ※3 J. Lambek (1980) From types to sets. Adv. in Math. 36. 113-164