檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2009-02-25 (水)

紙芝居:ラムダ抽象

| 09:30 | 紙芝居:ラムダ抽象を含むブックマーク

石井君*1が、2月19日セミナーのツイン・ホワイトボードを撮影してくれていたので、ハイライト(?)部分を紙芝居にしました。

紙と鉛筆の準備はいいかな -- では、はじまりはじまり。


g = <a, b, x| a*x + b> という関数があるとき、これを2回“ラムダ抽象”してみます。ラムダ抽象とは、右肩ハット(^)または大文字ラムダ(Λ)で表されるオペレータです。ラムダ抽象とカリー化は同義語です*2。ラムダ抽象すると、n引数関数は(n-1)引数関数に変化し、その代わり戻り値が関数型になります。ただし、ここで言う「関数型」は数学的な関数の型ではなくて、とある実行エンジンEで実行する関数コードのデータ型のことです。

gの2回ラムダ抽象g^^を絵に描くとこうです。


gの1回ラムダ抽象 g^ = Λg と、gの2回ラムダ抽象 g^^ = Λ(Λg) を計算してみます。Λの計算規則*3を使えば、こうなって、こうして、こうですね(ホワイトボード 1行から4行)。

さて、出来上がった g^^ = <a| λb.λx.(a*x + b)> は1引数(変数a)の関数なので、具体的な引数値(実引数)として値3を渡してみましょう(5行目)。



変数aが3に具体化されて、小さなラムダ式が値として吐き出されます。g^^(3) = λb.λx.(3*x + b) ですね。小さなラムダ式が、g^^の戻り値として出力されるわけです。


λb.λx.(3*x + b) のbを5に具体化しましょう。(λb.λx.(3*x + b))(5) ってしたくなるでしょうが、それは出来ませんよ。小さいラムダ式はこれ自体としては関数(働き、入力と出力を持つ箱)じゃありませんから。実行エンジンEの第1引数となるべきデータなんです。セミナー第1回を受けた方は、箱とカードの区別を思い出してね。

実行エンジンEを経由して、g^^(3) = λb.λx.(3*x + b) に引数5を渡します。E(g^^(3), 5) ですね。

基本等式を使うと、 E(g^^(3), 5) = g^(3, 5) = <a, b| λx.(a*x + b)>(3, 5) である点にも注意。


g^^(3)に具体的引数5が渡るところを絵で描いてみると、こんな。

下側のオダング(光っちゃっている場所)は実行エンジンEです。Eの第2引数(右側のワイヤー)として5を入力すると、結果的に g^^(3) = λb.λx.(3*x + b) のbが5に具体化されます。


曲がったワイヤーを伸ばしてしまうと、Eを経由して5を渡したE(g^(3), 5)と、直接右上から5を流し込んだg^(3, 5)は同じでしょ、ホラ。


bが5に具体化されたので、λx.(3*x + 5)という小さなラムダ式が出現しました。これは、変数xだけを持つ1次関数を表します。でも正確にいうと、「1次関数を表す関数コード」なので、実行エンジンEを経由しないと評価できません。

もう一度Eを使って、xの具体的な値として7を渡しましょう。


絵はこんな。

3*x + 5 のxに具体的な値7が渡されますよ。ワイヤーを伸ばせばもちろん、g(3, 5, 7)ですから、もとの関数gに3つの実引数を同時に渡したのと同じです。

3*7 + 5 を実際に計算すれば、g(3, 5, 7) = E(g^(3, 5), 7) = E(E(g^^(3), 5), 7) = 26 です。もう少し詳しく書けば:

   <a, b, x| a*x + b>(3, 5, 7)
 = E(<a, b| λx.(a*x + b)>(3, 5), 7)
 = E(E(<a| λb.λx.(a*x + b)>(3), 5), 7)
 = E(E(λb.λx.(3*x + b), 5), 7)
 = E(λx.(3*x + 5), 7)
 = 3*7 + 5
 = 26

Eを中置演算子「・」に置き換えて後半の計算を再掲すると、次のようです(リアルワールド向けラムダ計算も参照)。

 = (λb.λx.(3*x + b))・5・7
 = (λx.(3*x + 5))・7
 = 3*7 + 5
 = 26

大きなラムダ式は、リアルな、今そこに居る関数の表現。大きなラムダ式=リアルな関数から吐き出される値である小さなラムダ式は、関数コードというデータであり、実行エンジンEに渡すと評価(eval, exec, run)されます。


オマケの説明: λb.λx.(a*x + b) のように自由変数(この場合はa)を含む小さなラムダ式は、大きなラムダ式のボディ内には存在できますが、大きなラムダ式の外に出ることはできないのです。「小さなラムダ式の自由変数=大きなラムダ式の引数変数」になっています。小さなラムダ式の自由変数がすべて束縛されたとき、大きなラムダ式=関数の箱から外にプイッと吐き出されます。もし、自由変数が残った状態(開いたまま)で小さなラムダ式が外に出てしまったら、それを解釈する実行エンジンが途方にくれてしまいますからね*4

*1:口頭で「石井君」なんて呼んだことは一度もないけどね。

*2:ここで言っているラムダ抽象=カリー化は、単なる記号操作ではありません。デカルト閉圏Cにおいて、C(A×B, C)とC(A, CB)の同型を与えるオペレータのことです。

*3:大きなラムダ式の一番右の引数、この場合はxを消して、大きなラムダ・ボディ内の式をλx.で囲む(束縛する)、という規則です。

*4:ここらで「クロージャって何だろう?」とか考えてみるのも一興かも知れません。