「Emacsのトラノマキ」連載第14回「Lispの世界」(袖山剛)

Tweet

* はじめに 今回は著者がelispで書いたLispインタープリタsLispを元にLispの世界を紹介していきます。 ラムダ計算、Yコンビネータやschemeで有名な継続をsLispの実装を元に解説します。 sLispのソース全文を記載したgithubへのリンクを書いておくので興味のある方は実際に動かしてみてください。 http://github.com/sodeyama/slisp/blob/master/slisp-ycc.el 注・sLispはemacs 22.2.1上のみで動作検証をしています。 * ラムダ計算 Yコンビネータは、プログラミング言語Lispが基礎としている理論「ラムダ計算」に深く関係しているため、 まずは簡単にラムダ計算について説明します。 ** ラムダ記法 ラムダ計算を知るにはまずラムダ記法を知る必要があります。 ラムダ記法は"関数"の記述を簡便に扱うための記法です。 例えば自然数上の1変数関数 f(x) = x^3 + x のような関数fが与えられた時、それをラムダ記法で書くと以下のようになります。 \x. x^3 + x この式中の\を「ラムダ」と読みます。ドット(.)より右側の式は関数本体を表します。 ラムダは変数xが関数本体で束縛されている事を表しています。 このように関数の引数（プログラミングの世界では仮引数）となっている変数の事を 束縛変数と呼びます。 また、ラムダ記法の利点として、以下のようなラムダ式が与えられた場合、 変数はa,b,xのどれが「束縛変数」であるかを明示できる事があげられます。 \x. a * x^3 + x + b このラムダ式の場合、xが束縛変数でa,bは束縛されていない変数です。 プログラミングのレベルで考えると 関数定義 Lispの例: (defun foo (x) (+ x 5)) 関数呼び出し Lispの例: (foo 3) 関数呼び出し時に実引数で値が決まる変数(プログラミングの用語を使うと仮引数)が束縛変数です。 参考のため、ラムダ式の正式な定義を計算論 P.63 定義2.1.1によりあげておきます。 - ラムダ式の定義 - ラムダ式とは下記の(1)(2)(3)により再帰的に定義される式の事である (1) 変数 x_0, x_1, ... はラムダ式である (2) Mがラムダ式でxが変数のとき (\x. M)はラムダ式である (3) MとNがラムダ式のとき(MN)はラムダ式である この定義中の (\x. M) の形式を関数抽象と呼び、MNの形式をMのNに対する関数適用と呼びます。 ** ベータ変換 (beta reduction) 次に以下のようなラムダ式を考えます。 (\x. M) N これはラムダ式 (\x. M)のラムダ式Nに対する適用です。 このラムダ式を、ラムダ式Mに含まれている変数xを全てラムダ式Nで置き換える事をベータ変換と呼び、以下のように記述します。 (\x. M) N ->_beta M[x:=N] M[x:=N] はMの式中のxを全てNで置き換えられた式を意味します。 CやJavaなどの世界で関数呼び出しやメソッド呼び出しの実引数というと、値やオブジェクトをイメージしがちですが ラムダ計算（及びそれを基礎にしている関数型言語）の世界では実引数には値の他に関数自体を渡す事が出来ます。 上の例でいうと (\x. M)に対応するのが例えば (lambda (x) (x 1)) で Nに対応する式が (lambda (y) (+ y 1)) とすると ベータ変換は ((lambda (x) (x 1)) (lambda (y) (+ y 1))) ->_beta ((lambda (y) (+ y 1)) 1) のようなイメージになります。 この記法を用いてベータ変換を以下のように再帰的に定義します。 - ベータ変換の定義 - (1) (\x. M) N ->_beta M[x:=N] (2) M ->_beta N ならば 任意の変数xと任意のラムダ式Pに対して (\x. M) ->_beta (\x. N), PM ->_beta PN, MP ->_beta NP ここでベータ変換に関する等号 ( =_beta )を以下のように定義しておきます。 ラムダ式 P, Qに対して P = P_1 < ->_beta P_2 < ->_beta ... < ->_beta P_n = Q (ただし、 M < ->_beta N は (M ->_beta N or N ->_beta M)を満たすベータ変換と定義) が成り立つ時 P =_beta Q と記述します。 例えば 1. P = P_1 ->_beta P_2 ->_beta P_3 = Q 2. P = P_1 < -_beta P_2 ->_beta P_3 = Q 3. P = P_1 < -_beta P_2 <-_beta P_3 = Q などが P =_beta Qとなります。 ラムダ計算とは上記のラムダ記法を用いてベータ変換を繰り返す計算の事です。 注意・正確にはアルファ変換もありますが、ここでは割愛します。 * Yコンビネータ ** 理論 Yコンビネータとは、あるラムダ式Mに対して YM =_beta M(YM) ... (式3) を満たすラムダ式の事です。 これは、あるラムダ式M（関数fとする）をYコンビネータに適用させると、 そのラムダ式Mを何度適用しても元のラムダ式とベータ等号になる関係です。 誤解を恐れずにやや柔らかい言葉で言うと以下のような関係の事です。 関数を受け取る関数fに関数g(=YM)を与えると g = f(g) となる関係があり f(f(g)) = f(g) = g f(f(f(g))) = ... = g ... f(f..f(g)..) = ... = g と再帰的にいつまでも続きます。 Yコンビネータのラムダ式は以下のように与えられます。 Y = \y. (\x. y(x x)) (\x. y(x x)) ... (式4) このYコンビネータのラムダ式を用い、(式3)を証明しておきます。 YM ≡ (\y. (\x. y(x x)) (\x. y(x x))) M ... (1) ->_beta (\x. M(x x)) (\x. M(x x)) (ここで、このラムダ式をM'とおく) ... (2) ->_beta M((\x. M(x x)) (\x. M(x x))) ... (3) = MM' ... (4) =_beta M(YM) ... (5) (1)から(2)のベータ変換は、ラムダ式Yの束縛変数yをMで置き換えています。 (2)から(3)のベータ変換は、はラムダ式 (\x. M(x x)) の束縛変数xを後半のラムダ式(\x. M(x x))で置き換えています。 (3)から(4)は(2)で定義したラムダ式M'を用いて書き直しています。 (4)から(5)は (1),(2)よりYM ->_beta M'が成り立っているので < ->_betaの定義より YM < ->_beta M'が成り立ち、=_betaの定義よりYM =_beta M'の関係も成り立つ事より導かれます。 よって、 YM =_beta M(YM) が成り立つ。 と、数学的な定理はこのようになっています。 実際にプログラミングの世界でYコンビネータを使う際には以下のような変換だけを考えておけば十分です。 YM ->_beta (\x. M(x x)) (\x. M(x x)) ->_beta M((\x. M(x x)) (\x. M(x x))) ->_beta M(M((\x. M(x x)) (\x. M(x x))) ... ** 実装 Yコンビネータの理論はこれくらいにして、 sLispのYコンビネータに関連する実装の肝の部分であるベータ変換のコードを見てみましょう サンプル１ - elispによるLisp実装 ベータ変換 - 1: (defun beta-reduction (exp trans_exp key env) 2: (let ((ret '()) 3: (check_exp exp) 4: (have_key nil)) 5: (cond ((lambda? check_exp) 6: (progn 7: (setq check_exp (cddr exp)) 8: (let ((func-args (cdr check_exp))) 9: (dolist (arg func-args) 10: (if (and (not (listp arg)) 11: (equal (symbol-name arg) key)) 12: (setq have_key t)))))) 13: ((let? check_exp) 14: (progn 15: (setq check_exp (cddr exp)) 16: (let ((func-args (cdr check_exp))) 17: (dolist (arg func-args) 18: (if (and (not (listp arg)) 19: (equal (symbol-name arg) key)) 20: (setq have_key t))))))) 21: (if (eq have_key t) 22: exp 23: (if (listp check_exp) 24: (let ((len (length check_exp))) 25: (dolist (i check_exp) 26: (if (listp i) 27: (let ((in_exp (beta-reduction i trans_exp key env))) 28: (if (= len 1) 29: (setq ret in_exp) 30: (setq ret (cons in_exp (if (eq ret nil) '() ret))))) 31: (let ((ii (if (symbolp i) (symbol-name i) i))) 32: (if (= len 1) 33: (setq ret (if (equal ii key) trans_exp i)) 34: (setq ret (cons 35: (if (equal ii key) 36: trans_exp 37: i) 39: (if (eq ret nil) '() ret)))))))) 40: (setq ret (cons 41: (if (eq (symbol-name check_exp) key) 42: trans_exp 43: check_exp) 44: ret))) 45: (if (> (length check_exp) 1) 46: (setq ret (nreverse ret))) 47: (cond ((lambda? exp) 48: (progn 49: (setq ret (list "lambda" (cadr exp) ret)))) 50: ((let? exp) 51: (progn 52: (setq ret (list "let" (cadr exp) ret))))) 53: ret))) beta-reductionに与える引数はexpが変換対象のS式、trans_expは置き換わるS式、keyは置き換える時のキー文字列、envは このスコープで名前変換する場合に使用するためのハッシュテーブルです。 また、2行目〜4行目の変数の意味は、retはベータ変換した結果、check_expはベータ変換対象となるS式で、have_keyは 変換時のkeyがlambda式やlet式の引数と同じであった場合にtrueになります (lambda式やlet式の"lambda"と"let"と引数のS式は変換対象から外しています)。 5行目から19行目はlambdaやletがある場合、"lambda", "let"というprimitiveな文字列と引数を変換対象から外す事と 引数に変換対象となるkeyが一致するかどうかのチェックをしています。 21,22行目でlambda, letの引数とkeyが一致した場合は特に変換せずにS式を返しています。これは、変換対象のS式が keyの文字列で新たに束縛されているので、ベータ変換の定義から変換出来ません。 23行目から44行目は変換対象のS式がリストかどうかで場合分けし、さらにベータ変換が必要な場合は再帰的に beta-reductionを呼び出しています。その中で34行目から39行目と40行目から43行目で実際にkeyとS式を変換しています。 45行目と46行目でretがlistならば逆順にセットしなおしています(retには逆順でlistに追加されていくため)。 47行目から52行目で最初に与えられた変換対象のS式(exp)がlambdaかletの場合、5行目から20行目で"lambda", "let", と引数部分の S式を削っていたのでそれを元に戻しています。 最後に53行目で変換後（変換されていなければそのまま）のS式を返しています。 ** sLispで書くYコンビネータ Yコンビネータが動くインタープリタは、ラムダ式をベータ変換していく事で実装出来ます。 理論で説明しましたが、ベータ変換は式に対する評価は行いません。 束縛変数の置換が行われるだけで、実際の式の評価は別に必要です。 ベータ変換された式はまたラムダ式となるので、いついかなるタイミングで式の評価をしても問題ありません。 そこで、sLispではベータ変換が完全に終了したらそこで式の評価をするような戦略としています。 しかし、現実的に無限にベータ変換が終わらないといつまで待っても計算が終わらないので、 どこかでベータ変換が終わるような仕組みが必要です。 それにはYコンビネータに与えるラムダ式側に仕組みが必要です。 実際、階乗計算をさせるような関数の場合は以下のようになります。 - 階乗計算をさせる関数 sLispに与えるS式 - 1:(defun fact0 (f) 2: (lambda (n) 3: (if (= n 0) 4: 1 5: (* n (f (- n 1)))))) - 普通の階乗計算をさせる関数 - 1:(defun fact (n) 2: (if (= n 0) 3: 1 4: (* n (fact (- n 1))))) fact0は関数を受け取る関数で、引数nの値が0の時は1を返して、0以外の時は引数の関数fに (- n 1) を適用し、 その結果とnを掛けた数字を返しています。 普通の階乗計算をさせる関数と違い、fact0自身は再帰的な処理をしません。 再帰を発生させるのはYコンビネータの役目となります。 fact0は関数fを引数として受け取り、lambda式を返すのですが、そのlambda式が受け取る引数nが0の時に 関数fを評価しないので、ここで再帰の連鎖が止まるようになっています。 では肝心のYコンビネータのS式は以下のようになります。 - Yコンビネータ sLispに与えるS式 - 1:(defun Y (f) 2: ((lambda (x) 3: (f (x x))) 4: (lambda (x) 5: (f (x x))))) これはYコンビネータのラムダ式 (式4)と全く同じ式です。 実際に ((Y fact0) 1) をsLispでベータ変換及び評価していってみます。 ((Y fact0) 1) (ベータ変換) -> (((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x)))) 1) (網掛け指定は 最初の(lambda (x)(fact0 (x x))) です) (ベータ変換) -> ((fact0 ((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x))))) 1) (網掛け指定は 最初のfact0です) (ベータ変換) -> ((lambda (n) (if (= n 0) 1 (* n ((fact0 ((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x))))) (- n 1))))) 1) (網掛け指定は (lambda (n) (if (= n 0) 1 (* n ((fact0 ((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x))))) (- n 1))))) です) (ベータ変換) -> (if (= 1 0) 1 (* 1 ((fact0 ((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x))))) (- 1 1)))) (ここは網掛け指定ありません) (評価) -> (* 1 ((fact0 ((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x))))) (- 1 1))) (網掛け指定は 最初のfact0です) (ベータ変換) -> (* 1 ((lambda (n) (if (= n 0) 1 (* n (((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x)))) (- (- 1 1) 1))))) (- 1 1))) (網掛け指定は (lambda (n) (if (= n 0) 1 (* n (((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x)))) (- (- 1 1) 1))))) です) (ベータ変換) -> (* 1 (if (= (- 1 1) 0) 1 (* (- 1 1) (((lambda (x) (fact0 (x x))) (lambda (x) (fact0 (x x)))) (- (- 1 1) 1))))) (網掛け指定はありません) (評価) -> (* 1 1) (評価) -> 1 この例ではYやfact0といった関数名を持ち出しましたが、Yコンビネータはこのような間数名を用いずに 書くことが出来ます。 - lambdaだけで書いた再帰 sLispに与えるS式 - 1: (((lambda (f) 2: ((lambda (x) 3: (f (x x))) 4: (lambda (x) 5: (f (x x))))) 6: (lambda (f) 7: (lambda (n) 8: (if (= n 0) 9: 1 10: (* n (f (- n 1))))))) 1) * 継続 ** 概念 ある瞬間の継続とは、その瞬間以前の計算結果を使ってその後計算すべき物の事です。 Lispにおける継続の例を出します 例1: (* (+ 3 2) (/ 4 2)) 上記の例は部分式を左から評価していくとすると (/ 4 2)を評価しようとする瞬間の継続は 「これから得られる結果 (/ 4 2)に5を掛ける」と表せます。 これはlambdaを使って (lambda (x) (* 5 x)) と表現できます。実際にこの継続から計算を続けたい時は ((lambda (x) (* 5 x)) (/ 4 2)) とすれば例1と同じ結果を得られます。 schemeやsLispでは、継続はデータとして生成し使う事が出来ます。 継続の生成にはcall-with-current-continuationやcall/ccメソッドを使います。sLispではcall/ccです。 例2: (* (+ 3 2) (call/cc (lambda (cc) (/ 4 2)))) この例2をみてください。部分式にcall/ccメソッドがあります。 継続の生成にはこのcall/ccの部分式をそっくりそのまま適当な変数xに置き換え、それをlambdaで包むと 覚えてください。 すなわち (lambda (x) (* 5 x)) がこのcall/ccメソッドが生成する継続です。 この継続はcall/cc内部のlambdaの引数ccに渡されます。 例2ではcall/ccのlambda式内部で継続ccが使われていません。 このような場合、call/ccメソッドは内部の式を評価して返します。 すなわち (/ 4 2)を評価して返すので (* 5 2) となります。 例3: (* (+ 3 2) (call/cc (lambda (cc) (cc 2)))) この例では先ほどの例2と違い、継続ccがcall/ccメソッドのlambda式で使われています。 この場合、例3のS式全体は (cc 2) を返します。 すなわち ((lambda (x) (* 5 x)) 2) の評価結果である10を返します。 これは継続の特徴である、「継続が呼ばれたらトップレベルの次のS式に評価が移る」という性質に依ります。 例3の場合 (* 5 (cc 2)) が返ると勘違いしそうですが、この性質により(cc 2)が返ります。 継続は単なるlambda式ではなく「トップレベルにあるS式の評価が終わったら次のS式に評価が移るよ！」 という命令も含まれていることを意味しています。 継続は保存しておくことも出来ます。 例4: 1: (setq hoge nil) 2: (* (+ 3 2) 3: (call/cc 4: (lambda (cc) 5: (progn 6: (setq hoge cc) 7: (cc 2))))) 8: (hoge 3) 例4のように継続ccを変数hogeに保存しておくと、その継続をあとで使いまわす事が出来ます。 このような継続を複数保存しておき、その継続をスケジューリングして動かす事により、擬似的なマルチスレッド のような動作をさせる事も可能です。 それではsLispにおける継続の実装を見ていきましょう。 ** 実装 サンプル２ - elispによるLisp実装 継続のパース1 - 1: (defun slisp-callcc-parse (exp env) 2: (catch 'exit 3: (dolist (seed (cdr exp)) 4: (let* ((ret (slisp-callcc-getcc seed env)) 5: (find (slisp-get-findcallcc ret)) 6: (cc (slisp-get-callcc ret))) 7: (if find 8: (progn 9: (let ((sexp (list "lambda" (list (make-symbol "variable-for-callcc")) (list "throw" cc)))) 10: (puthash "callcc" (slisp-eval sexp env) env)) 11: (throw 'exit t))))))) slisp-callcc-parseは与えられたS式をパースし終わって、構文木が作成された後に呼ばれます。 引数に与えられるexpはその構文木です。 3行目の(cdr exp)で得られるリストはトップレベルのS式のリストです。 それぞれのS式を探索し、call/ccが見つかればthrowしてslisp-callcc-parseを終了します。 このようにsLispでは今のところcall/ccが一つしか書けません。 4行目で呼んでいるslisp-callcc-getccが実質、継続の本体です。継続メソッドcall/ccが存在していれば5行目のfindがt となり、9行目で継続用のlambda式を生成しています。ここで変数名に"variable-for-callcc"を使っています。 これは与えられたS式の他の変数とかぶらないようにしなければなりませんが、ここでは便宜的にこのような、 かぶらないであろう変数名"variable-for-callcc"を明示的に指定しています。 lambda式の生成が出来たら、10行目でそれをスコープ用ハッシュテーブルenvに"callcc"というkeyでpushしています。 このcallccというkeyも他の変数名とかぶってはいけません。 サンプル３ - elispによるLisp実装 継続のパース2 - 1: (defun slisp-callcc-getcc (exp env) 2: (catch 'exit 3: (let ((cc '()) 4: (find_callcc nil)) 5: (dolist (i exp) 6: (if (listp i) 7: (let ((find (slisp-get-findcallcc (slisp-callcc-getcc i env))) 8: (ret (slisp-get-callcc (slisp-callcc-getcc i env)))) 9: (setq find_callcc find) 10: (setq cc (slisp-callcc-setlist ret cc)) 11: (if (and (symbolp ret) 12: (equal (symbol-name ret) "variable-for-callcc")) 13: (setq find_callcc t))) 14: (if (and (stringp i) 15: (equal i "call/cc")) 16: (throw 'exit (list t (make-symbol "variable-for-callcc"))) 17: (setq cc (slisp-callcc-setlist i cc))))) 18: (if (listp cc) 19: (list find_callcc (nreverse cc)) 20: (list find_callcc cc))))) 21: (defun slisp-get-findcallcc (exp) 22: (car exp)) 23: (defun slisp-get-callcc (exp) 24: (cadr exp)) 25: (defun slisp-callcc-setlist (exp l) 26: (if (eq l nil) 27: (list exp) 28: (cons exp l))) サンプル３は継続の本体です。 与えられた構文木expにcall/ccメソッドがあるかどうか再帰的にチェックしています。 14,15行目でcall/ccメソッドが発見出来た場合、16行目で(t "variable-for-callcc") というリストを返しています。 slisp-callcc-getccを呼び出す側は返った値からcall/ccが見つかったかどうかの booleanとcallccの本体をそれぞれ21行目slisp-get-findcallcc, 23行目slisp-get-callccで取得しています。 call/ccが見つかった場合、slisp-callcc-getccは最終的にcall/ccがある部分式を"variale-for-callcc"で置き換えた S式と、call/ccが見つかったという印のtのlistを返します。 見つからなかった場合は引数で渡したS式と、全く同じ物と見つからなかった印のnilのlistを返します。 * さいごに 今回はLispの基礎をなすラムダ計算と、それを元に導かれたYコンビネータを説明し、 また継続の概念と実装を説明していきました。 Yコンビネータはプログラミング的に何か役に立つ関数というわけではなく、 ラムダ式だけで再帰を表現出来るという1点においてのみ意味があります。 全ての計算には、等価なラムダ式が存在するという事の一端としてご紹介しました。 実装に関しては今回お見せした例のようにそれぞれ数十行程度で実現出来ます。 如何にLispが強力で素晴らしいかわかっていただけたかと思います。 次回はelispの実装をemacsのソースコードを元に解説していきたいと思います。 お楽しみに。 * 参考文献 - 計算論 計算可能性とラムダ計算　高橋正子著 ISBN 978-4-7649-0184-1 - http://d.hatena.ne.jp/sodex/ 著者のブログ

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553

* はじめに   今回は著者がelispで書いたLispインタープリタsLispを元にLispの世界を紹介していきます。 ラムダ計算、Yコンビネータやschemeで有名な継続をsLispの実装を元に解説します。   sLispのソース全文を記載したgithubへのリンクを書いておくので興味のある方は実際に動かしてみてください。   http://github.com/sodeyama/slisp/blob/master/slisp-ycc.el   注・sLispはemacs 22.2.1上のみで動作検証をしています。   * ラムダ計算 Yコンビネータは、プログラミング言語Lispが基礎としている理論「ラムダ計算」に深く関係しているため、 まずは簡単にラムダ計算について説明します。   ** ラムダ記法 ラムダ計算を知るにはまずラムダ記法を知る必要があります。 ラムダ記法は"関数"の記述を簡便に扱うための記法です。   例えば自然数上の1変数関数 f(x) = x^3 + x  のような関数fが与えられた時、それをラムダ記法で書くと以下のようになります。   \x. x^3 + x   この式中の\を「ラムダ」と読みます。ドット(.)より右側の式は関数本体を表します。 ラムダは変数xが関数本体で束縛されている事を表しています。 このように関数の引数（プログラミングの世界では仮引数）となっている変数の事を 束縛変数と呼びます。     また、ラムダ記法の利点として、以下のようなラムダ式が与えられた場合、 変数はa,b,xのどれが「束縛変数」であるかを明示できる事があげられます。   \x. a * x^3 + x + b   このラムダ式の場合、xが束縛変数でa,bは束縛されていない変数です。   プログラミングのレベルで考えると   関数定義 Lispの例:  (defun foo (x) (+ x 5))   関数呼び出し Lispの例:  (foo 3)   関数呼び出し時に実引数で値が決まる変数(プログラミングの用語を使うと仮引数)が束縛変数です。     参考のため、ラムダ式の正式な定義を計算論 P.63 定義2.1.1によりあげておきます。     - ラムダ式の定義 - ラムダ式とは下記の(1)(2)(3)により再帰的に定義される式の事である   (1) 変数 x_0, x_1, ... はラムダ式である (2) Mがラムダ式でxが変数のとき (\x. M)はラムダ式である (3) MとNがラムダ式のとき(MN)はラムダ式である   この定義中の (\x. M) の形式を関数抽象と呼び、MNの形式をMのNに対する関数適用と呼びます。     ** ベータ変換 (beta reduction) 次に以下のようなラムダ式を考えます。   (\x. M) N   これはラムダ式 (\x. M)のラムダ式Nに対する適用です。 このラムダ式を、ラムダ式Mに含まれている変数xを全てラムダ式Nで置き換える事をベータ変換と呼び、以下のように記述します。   (\x. M) N ->_beta M[x:=N]   M[x:=N] はMの式中のxを全てNで置き換えられた式を意味します。   CやJavaなどの世界で関数呼び出しやメソッド呼び出しの実引数というと、値やオブジェクトをイメージしがちですが ラムダ計算（及びそれを基礎にしている関数型言語）の世界では実引数には値の他に関数自体を渡す事が出来ます。 上の例でいうと (\x. M)に対応するのが例えば (lambda (x) (x 1)) で Nに対応する式が (lambda (y) (+ y 1)) とすると ベータ変換は   ((lambda (x) (x 1)) (lambda (y) (+ y 1))) ->_beta ((lambda (y) (+ y 1)) 1)   のようなイメージになります。     この記法を用いてベータ変換を以下のように再帰的に定義します。   - ベータ変換の定義 - (1) (\x. M) N ->_beta M[x:=N] (2) M ->_beta N ならば 任意の変数xと任意のラムダ式Pに対して (\x. M) ->_beta (\x. N), PM ->_beta PN, MP ->_beta NP   ここでベータ変換に関する等号 ( =_beta )を以下のように定義しておきます。   ラムダ式 P, Qに対して P = P_1 < ->_beta P_2 < ->_beta ... < ->_beta P_n = Q (ただし、 M < ->_beta N は (M ->_beta N or N ->_beta M)を満たすベータ変換と定義) が成り立つ時 P =_beta Q と記述します。   例えば 1. P = P_1 ->_beta P_2 ->_beta P_3 = Q 2. P = P_1 < -_beta P_2 ->_beta P_3 = Q 3. P = P_1 < -_beta P_2 <-_beta P_3 = Q などが P =_beta Qとなります。   ラムダ計算とは上記のラムダ記法を用いてベータ変換を繰り返す計算の事です。 注意・正確にはアルファ変換もありますが、ここでは割愛します。   * Yコンビネータ ** 理論 Yコンビネータとは、あるラムダ式Mに対して   YM =_beta M(YM) ... (式3)   を満たすラムダ式の事です。 これは、あるラムダ式M（関数fとする）をYコンビネータに適用させると、 そのラムダ式Mを何度適用しても元のラムダ式とベータ等号になる関係です。   誤解を恐れずにやや柔らかい言葉で言うと以下のような関係の事です。   関数を受け取る関数fに関数g(=YM)を与えると g = f(g) となる関係があり   f(f(g)) = f(g) = g f(f(f(g))) = ... = g ... f(f..f(g)..) = ... = g   と再帰的にいつまでも続きます。   Yコンビネータのラムダ式は以下のように与えられます。   Y = \y. (\x. y(x x)) (\x. y(x x)) ... (式4)   このYコンビネータのラムダ式を用い、(式3)を証明しておきます。   YM ≡ (\y. (\x. y(x x)) (\x. y(x x))) M  ... (1)    ->_beta (\x. M(x x)) (\x. M(x x)) (ここで、このラムダ式をM'とおく)  ... (2)    ->_beta M((\x. M(x x)) (\x. M(x x)))  ... (3)    = MM' ... (4)    =_beta M(YM) ... (5)   (1)から(2)のベータ変換は、ラムダ式Yの束縛変数yをMで置き換えています。 (2)から(3)のベータ変換は、はラムダ式 (\x. M(x x)) の束縛変数xを後半のラムダ式(\x. M(x x))で置き換えています。 (3)から(4)は(2)で定義したラムダ式M'を用いて書き直しています。 (4)から(5)は (1),(2)よりYM ->_beta M'が成り立っているので < ->_betaの定義より YM < ->_beta M'が成り立ち、=_betaの定義よりYM =_beta M'の関係も成り立つ事より導かれます。 よって、 YM =_beta M(YM) が成り立つ。     と、数学的な定理はこのようになっています。 実際にプログラミングの世界でYコンビネータを使う際には以下のような変換だけを考えておけば十分です。   YM ->_beta (\x. M(x x)) (\x. M(x x))    ->_beta M((\x. M(x x)) (\x. M(x x)))    ->_beta M(M((\x. M(x x)) (\x. M(x x)))    ...   ** 実装 Yコンビネータの理論はこれくらいにして、 sLispのYコンビネータに関連する実装の肝の部分であるベータ変換のコードを見てみましょう   サンプル１ - elispによるLisp実装 ベータ変換 - 1:  (defun beta-reduction (exp trans_exp key env) 2:    (let ((ret '()) 3:          (check_exp exp) 4:          (have_key nil)) 5:      (cond ((lambda? check_exp) 6:             (progn 7:               (setq check_exp (cddr exp)) 8:               (let ((func-args (cdr check_exp))) 9:                 (dolist (arg func-args) 10:                  (if (and (not (listp arg)) 11:                           (equal (symbol-name arg) key)) 12:                      (setq have_key t)))))) 13:           ((let? check_exp) 14:            (progn 15:              (setq check_exp (cddr exp)) 16:              (let ((func-args (cdr check_exp))) 17:                (dolist (arg func-args) 18:                  (if (and (not (listp arg)) 19:                           (equal (symbol-name arg) key)) 20:                      (setq have_key t))))))) 21:     (if (eq have_key t) 22:         exp 23:       (if (listp check_exp) 24:           (let ((len (length check_exp))) 25:             (dolist (i check_exp) 26:               (if (listp i) 27:                   (let ((in_exp (beta-reduction i trans_exp key env))) 28:                     (if (= len 1) 29:                         (setq ret in_exp) 30:                       (setq ret (cons in_exp (if (eq ret nil) '() ret))))) 31:                 (let ((ii (if (symbolp i) (symbol-name i) i))) 32:                   (if (= len 1) 33:                       (setq ret (if (equal ii key) trans_exp i)) 34:                     (setq ret (cons 35:                                (if (equal ii key) 36:                                    trans_exp 37:                                  i) 39:                                (if (eq ret nil) '() ret)))))))) 40:         (setq ret (cons 41:                    (if (eq (symbol-name check_exp) key) 42:                        trans_exp 43:                      check_exp) 44:                    ret))) 45:       (if (> (length check_exp) 1) 46:           (setq ret (nreverse ret))) 47:       (cond ((lambda? exp) 48:              (progn 49:                (setq ret (list "lambda" (cadr exp) ret)))) 50:             ((let? exp) 51:              (progn 52:                (setq ret (list "let" (cadr exp) ret))))) 53:       ret)))   beta-reductionに与える引数はexpが変換対象のS式、trans_expは置き換わるS式、keyは置き換える時のキー文字列、envは このスコープで名前変換する場合に使用するためのハッシュテーブルです。 また、2行目〜4行目の変数の意味は、retはベータ変換した結果、check_expはベータ変換対象となるS式で、have_keyは 変換時のkeyがlambda式やlet式の引数と同じであった場合にtrueになります (lambda式やlet式の"lambda"と"let"と引数のS式は変換対象から外しています)。   5行目から19行目はlambdaやletがある場合、"lambda", "let"というprimitiveな文字列と引数を変換対象から外す事と 引数に変換対象となるkeyが一致するかどうかのチェックをしています。   21,22行目でlambda, letの引数とkeyが一致した場合は特に変換せずにS式を返しています。これは、変換対象のS式が keyの文字列で新たに束縛されているので、ベータ変換の定義から変換出来ません。   23行目から44行目は変換対象のS式がリストかどうかで場合分けし、さらにベータ変換が必要な場合は再帰的に beta-reductionを呼び出しています。その中で34行目から39行目と40行目から43行目で実際にkeyとS式を変換しています。 45行目と46行目でretがlistならば逆順にセットしなおしています(retには逆順でlistに追加されていくため)。 47行目から52行目で最初に与えられた変換対象のS式(exp)がlambdaかletの場合、5行目から20行目で"lambda", "let", と引数部分の S式を削っていたのでそれを元に戻しています。   最後に53行目で変換後（変換されていなければそのまま）のS式を返しています。     ** sLispで書くYコンビネータ   Yコンビネータが動くインタープリタは、ラムダ式をベータ変換していく事で実装出来ます。 理論で説明しましたが、ベータ変換は式に対する評価は行いません。 束縛変数の置換が行われるだけで、実際の式の評価は別に必要です。 ベータ変換された式はまたラムダ式となるので、いついかなるタイミングで式の評価をしても問題ありません。 そこで、sLispではベータ変換が完全に終了したらそこで式の評価をするような戦略としています。 しかし、現実的に無限にベータ変換が終わらないといつまで待っても計算が終わらないので、 どこかでベータ変換が終わるような仕組みが必要です。 それにはYコンビネータに与えるラムダ式側に仕組みが必要です。 実際、階乗計算をさせるような関数の場合は以下のようになります。   - 階乗計算をさせる関数 sLispに与えるS式 - 1:(defun fact0 (f) 2:  (lambda (n) 3:    (if (= n 0) 4:        1 5:      (* n (f (- n 1))))))   - 普通の階乗計算をさせる関数 - 1:(defun fact (n) 2:  (if (= n 0) 3:      1 4:    (* n (fact (- n 1)))))   fact0は関数を受け取る関数で、引数nの値が0の時は1を返して、0以外の時は引数の関数fに (- n 1) を適用し、 その結果とnを掛けた数字を返しています。 普通の階乗計算をさせる関数と違い、fact0自身は再帰的な処理をしません。 再帰を発生させるのはYコンビネータの役目となります。 fact0は関数fを引数として受け取り、lambda式を返すのですが、そのlambda式が受け取る引数nが0の時に 関数fを評価しないので、ここで再帰の連鎖が止まるようになっています。   では肝心のYコンビネータのS式は以下のようになります。   - Yコンビネータ sLispに与えるS式 - 1:(defun Y (f) 2:  ((lambda (x) 3:     (f (x x))) 4:   (lambda (x) 5:     (f (x x)))))   これはYコンビネータのラムダ式 (式4)と全く同じ式です。 実際に ((Y fact0) 1) をsLispでベータ変換及び評価していってみます。   ((Y fact0) 1)   (ベータ変換) -> (((lambda (x)     (fact0 (x x)))    (lambda (x)     (fact0 (x x)))) 1)   (網掛け指定は 最初の(lambda (x)(fact0 (x x))) です)   (ベータ変換) -> ((fact0 ((lambda (x)            (fact0 (x x)))          (lambda (x)            (fact0 (x x))))) 1)   (網掛け指定は 最初のfact0です)   (ベータ変換) -> ((lambda (n)    (if (= n 0)        1      (* n         ((fact0 ((lambda (x)                    (fact0 (x x)))                  (lambda (x)                    (fact0 (x x))))) (- n 1))))) 1)   (網掛け指定は (lambda (n)    (if (= n 0)        1      (* n         ((fact0 ((lambda (x)                    (fact0 (x x)))                  (lambda (x)                    (fact0 (x x))))) (- n 1))))) です)   (ベータ変換) -> (if (= 1 0)       1    (* 1       ((fact0 ((lambda (x)                  (fact0 (x x)))                (lambda (x)                  (fact0 (x x))))) (- 1 1))))   (ここは網掛け指定ありません)   (評価) -> (* 1     ((fact0 ((lambda (x)                (fact0 (x x)))              (lambda (x)                (fact0 (x x))))) (- 1 1)))   (網掛け指定は 最初のfact0です)   (ベータ変換) -> (* 1     ((lambda (n)        (if (= n 0)            1          (* n             (((lambda (x)                 (fact0 (x x)))               (lambda (x)                 (fact0 (x x)))) (- (- 1 1) 1))))) (- 1 1)))   (網掛け指定は (lambda (n)        (if (= n 0)            1          (* n             (((lambda (x)                 (fact0 (x x)))               (lambda (x)                 (fact0 (x x)))) (- (- 1 1) 1))))) です)   (ベータ変換) -> (* 1     (if (= (- 1 1) 0)         1       (* (- 1 1)          (((lambda (x)              (fact0 (x x)))            (lambda (x)              (fact0 (x x)))) (- (- 1 1) 1)))))   (網掛け指定はありません)   (評価) -> (* 1 1)   (評価) -> 1   この例ではYやfact0といった関数名を持ち出しましたが、Yコンビネータはこのような間数名を用いずに 書くことが出来ます。   - lambdaだけで書いた再帰 sLispに与えるS式 - 1: (((lambda (f) 2:     ((lambda (x) 3:        (f (x x))) 4:      (lambda (x) 5:        (f (x x))))) 6:   (lambda (f) 7:     (lambda (n) 8:       (if (= n 0) 9:           1 10:        (* n (f (- n 1))))))) 1)         * 継続 ** 概念   ある瞬間の継続とは、その瞬間以前の計算結果を使ってその後計算すべき物の事です。 Lispにおける継続の例を出します   例1: (* (+ 3 2) (/ 4 2))   上記の例は部分式を左から評価していくとすると (/ 4 2)を評価しようとする瞬間の継続は 「これから得られる結果 (/ 4 2)に5を掛ける」と表せます。 これはlambdaを使って   (lambda (x) (* 5 x))   と表現できます。実際にこの継続から計算を続けたい時は   ((lambda (x) (* 5 x)) (/ 4 2))   とすれば例1と同じ結果を得られます。 schemeやsLispでは、継続はデータとして生成し使う事が出来ます。 継続の生成にはcall-with-current-continuationやcall/ccメソッドを使います。sLispではcall/ccです。   例2: (* (+ 3 2) (call/cc (lambda (cc) (/ 4 2))))   この例2をみてください。部分式にcall/ccメソッドがあります。 継続の生成にはこのcall/ccの部分式をそっくりそのまま適当な変数xに置き換え、それをlambdaで包むと 覚えてください。   すなわち (lambda (x) (* 5 x)) がこのcall/ccメソッドが生成する継続です。 この継続はcall/cc内部のlambdaの引数ccに渡されます。   例2ではcall/ccのlambda式内部で継続ccが使われていません。 このような場合、call/ccメソッドは内部の式を評価して返します。 すなわち (/ 4 2)を評価して返すので (* 5 2) となります。   例3: (* (+ 3 2) (call/cc (lambda (cc) (cc 2))))   この例では先ほどの例2と違い、継続ccがcall/ccメソッドのlambda式で使われています。 この場合、例3のS式全体は (cc 2) を返します。 すなわち ((lambda (x) (* 5 x)) 2) の評価結果である10を返します。 これは継続の特徴である、「継続が呼ばれたらトップレベルの次のS式に評価が移る」という性質に依ります。 例3の場合 (* 5 (cc 2)) が返ると勘違いしそうですが、この性質により(cc 2)が返ります。 継続は単なるlambda式ではなく「トップレベルにあるS式の評価が終わったら次のS式に評価が移るよ！」 という命令も含まれていることを意味しています。   継続は保存しておくことも出来ます。   例4: 1: (setq hoge nil) 2: (* (+ 3 2) 3:    (call/cc 4:     (lambda (cc) 5:       (progn 6:         (setq hoge cc) 7:         (cc 2))))) 8: (hoge 3)   例4のように継続ccを変数hogeに保存しておくと、その継続をあとで使いまわす事が出来ます。 このような継続を複数保存しておき、その継続をスケジューリングして動かす事により、擬似的なマルチスレッド のような動作をさせる事も可能です。       それではsLispにおける継続の実装を見ていきましょう。   ** 実装   サンプル２ - elispによるLisp実装 継続のパース1 - 1: (defun slisp-callcc-parse (exp env) 2:   (catch 'exit 3:     (dolist (seed (cdr exp)) 4:       (let* ((ret (slisp-callcc-getcc seed env)) 5:              (find (slisp-get-findcallcc ret)) 6:              (cc (slisp-get-callcc ret))) 7:         (if find 8:             (progn 9:               (let ((sexp (list "lambda" (list (make-symbol "variable-for-callcc")) (list "throw" cc)))) 10:                (puthash "callcc" (slisp-eval sexp env) env)) 11:              (throw 'exit t)))))))   slisp-callcc-parseは与えられたS式をパースし終わって、構文木が作成された後に呼ばれます。 引数に与えられるexpはその構文木です。 3行目の(cdr exp)で得られるリストはトップレベルのS式のリストです。 それぞれのS式を探索し、call/ccが見つかればthrowしてslisp-callcc-parseを終了します。 このようにsLispでは今のところcall/ccが一つしか書けません。 4行目で呼んでいるslisp-callcc-getccが実質、継続の本体です。継続メソッドcall/ccが存在していれば5行目のfindがt となり、9行目で継続用のlambda式を生成しています。ここで変数名に"variable-for-callcc"を使っています。 これは与えられたS式の他の変数とかぶらないようにしなければなりませんが、ここでは便宜的にこのような、 かぶらないであろう変数名"variable-for-callcc"を明示的に指定しています。 lambda式の生成が出来たら、10行目でそれをスコープ用ハッシュテーブルenvに"callcc"というkeyでpushしています。 このcallccというkeyも他の変数名とかぶってはいけません。   サンプル３  - elispによるLisp実装 継続のパース2 - 1: (defun slisp-callcc-getcc (exp env) 2:   (catch 'exit 3:     (let ((cc '()) 4:           (find_callcc nil)) 5:       (dolist (i exp) 6:         (if (listp i) 7:             (let ((find (slisp-get-findcallcc (slisp-callcc-getcc i env))) 8:                   (ret (slisp-get-callcc (slisp-callcc-getcc i env)))) 9:               (setq find_callcc find) 10:              (setq cc (slisp-callcc-setlist ret cc)) 11:              (if (and (symbolp ret) 12:                       (equal (symbol-name ret) "variable-for-callcc")) 13:                  (setq find_callcc t))) 14:          (if (and (stringp i) 15:                   (equal i "call/cc")) 16:              (throw 'exit (list t (make-symbol "variable-for-callcc"))) 17:            (setq cc (slisp-callcc-setlist i cc))))) 18:      (if (listp cc) 19:          (list find_callcc (nreverse cc)) 20:        (list find_callcc cc))))) 21: (defun slisp-get-findcallcc (exp) 22:   (car exp)) 23: (defun slisp-get-callcc (exp) 24:   (cadr exp)) 25: (defun slisp-callcc-setlist (exp l) 26:   (if (eq l nil) 27:       (list exp) 28:     (cons exp l)))   サンプル３は継続の本体です。 与えられた構文木expにcall/ccメソッドがあるかどうか再帰的にチェックしています。 14,15行目でcall/ccメソッドが発見出来た場合、16行目で(t "variable-for-callcc") というリストを返しています。 slisp-callcc-getccを呼び出す側は返った値からcall/ccが見つかったかどうかの booleanとcallccの本体をそれぞれ21行目slisp-get-findcallcc, 23行目slisp-get-callccで取得しています。 call/ccが見つかった場合、slisp-callcc-getccは最終的にcall/ccがある部分式を"variale-for-callcc"で置き換えた S式と、call/ccが見つかったという印のtのlistを返します。 見つからなかった場合は引数で渡したS式と、全く同じ物と見つからなかった印のnilのlistを返します。     * さいごに 今回はLispの基礎をなすラムダ計算と、それを元に導かれたYコンビネータを説明し、 また継続の概念と実装を説明していきました。 Yコンビネータはプログラミング的に何か役に立つ関数というわけではなく、 ラムダ式だけで再帰を表現出来るという1点においてのみ意味があります。 全ての計算には、等価なラムダ式が存在するという事の一端としてご紹介しました。 実装に関しては今回お見せした例のようにそれぞれ数十行程度で実現出来ます。 如何にLispが強力で素晴らしいかわかっていただけたかと思います。 次回はelispの実装をemacsのソースコードを元に解説していきたいと思います。 お楽しみに。     * 参考文献 - 計算論 計算可能性とラムダ計算　高橋正子著 ISBN 978-4-7649-0184-1 - http://d.hatena.ne.jp/sodex/ 著者のブログ

Tweet

Leave a Reply

Cancel

You must be logged in to post a comment.