2009年5月アーカイブ



一昨日急にid:ranha先生に「いっしょにやらない?」と誘われたのでホイホイついていくと、案の定そこにはラムダ計算な世界がアッー!...というのは冗談として、まったくその方面の知識のない僕が混ざることで、見事に足を引っ張りまくることになりました(´・ω・`)


まあそれはそれとして、とりあえず学んだことをまとめておきます。


PCFとは何か


Programming language for Computable Functions。直訳すると、計算可能関数のためのプログラミング言語。わかるような、わからないような...。


参考文献の一部を抜粋してみます。


プログラミング言語の意味論(※PDF)



PCF は型付きラムダ計算を基盤とした単純な文法を持つプログラミング言語である。


(中略)


PCF は自然数とその上の高階関数の計算に特化しており、自然数の加減と(再帰) 関数の生成や呼び出しといった機構を備えている。一方で現実のプログラミング言語が備える実用的な機能、例えばファイル入出力、画面表示、ネットワークといった機器の操作や、オブジェクトやポインタ、配列といった機構は備えていない。



大雑把にいうとたぶんいわゆる関数型言語、なイメージでいいのかな(漠然としすぎ


ラムダ計算とは何か


tnzkはラムダ計算についてほとんど理解していないので、これについて先に教えてもらうことに(これが(時間的な意味で)ドツボにはまる結果になるわけですが...)。


関数とは何か

これは偶然、解析の授業でやったことが思い出されたので併記しておくのですが、関数とは何かという話。


ある集合Rを実数の集合への写像とするとき、この対応付けを関数と呼んで、f(x) = yみたいに表すとのことです。単純に言うと数と数の対応関係に他ならない。


数学よりも先にプログラミングで関数という概念に触れた人間としては、やはり「引数をほげほげして結果を返すもの」といったようなイメージがあるので、単純な対応付け(即座に結果が返ってくる)と考えるのはどうも違和感を覚えてしまいますが、あくまで対応関係でしかない、というのが一般的な解釈だそうです(その対応付けの詳細を記述するために数式を用いるのであって、普遍的にその対応関係が理解されうるなら数式さえ必要なくらいの勢いで)。


ただWikipediaを見ると、上記の理解はあくまで「現代的解釈」だそうで、昔の人(オイラーさんだとからしいです)はそれとはまた違った考え方を持っていたみたいです。


ラムダ計算における関数

普通、数学では関数をf(x) = x + 2とか表すわけですが、これが意味するのは「値xを関数fに引数として渡すと、それに対して値yが得られる」といった事実を記述しているので、別に表記方法に対した重要性はなく、別な表記方法を考えることもできるらしいです。


で、ラムダ計算では、上の関数を次のように書きます:



λx.x + 2

基本的にはこれだけです。λのあとに引数が並んで、「.」のあとに関数の内容(?)を記述するわけですね。


体系的に調べたわけではないですが、らんはさんなどの喋りを聞いているとどうやら「.」以降の記述を「ボディ:Body」と呼ぶようです。これに対して「λx」のほうを「ヘッド/ヘッダ」と呼ぶのかどうかは定かではないです。


チャーチ数

ラムダ計算の狙いは、「なるべく小さな規則のセットですべての計算可能な関数が表現できるようにする」というのがあるようです。CPUでいうところのRISCを目指すもので、必然的に常用するには不便ですが、抽象的であり小回りが利くというか、移植性に優れるみたいなところがあるみたいです。


そいで、さっきの関数を見てみましょう。



λx.x + 2

「x + 2」とか書いてあるわけですけど、xに2を足すってのはどういうことなんでしょう?そもそも2ってどういう数なんでしょう?


プログラマの視点から考えてみると、コンピュータというのは数のことなんて理解しているわけじゃないので、まずはその辺を定義し直さないといけない気がします。


小学生のとき、先生に数字のことを習ったとき、「1の次に2がきて、その次に3で...」とか言ってたと思います。それをもう少しラムダ計算的な言葉で定義してみましょう!


※念のため: 「x := expr」はxをexprと定義するといった感じの意味です



0 := λfx.x
1 := λfx.fx
2 := λfx.f(fx)
3 := λfx.f(f(fx)

たぶん直感的にわかると思いますが、要するにxに対してfを適用した回数がその数となるわけです。IIIまでのローマ数字や漢数字と同じですし、性質としては小学校で習うものとも同じです。


このように、ラムダ式で数を定義する方法は上記のもののほかにもいくつかあり、その中で上記の手法を「チャーチ数」と呼びます(教会とは関係なく、チャーチさんが考えたからチャーチ数なんだと思います。ちなみにラムダ計算を考えたのもチャーチさんです)。


ただし、チャーチ数はいわゆる「自然数」、つまり数の部分集合である実数の部分集合である整数の部分集合であるそれとは本質的に異なるものです。いわゆる自然数の性質はすべてチャーチ数には当てはまりません。たとえば自然数であれば「0での除算は未定義」というのが良く知られていますが、チャーチ数に関してはこれは今のところ特にないです。まず除算を定義して、その上で0除算できないことを確認しないといけないです。実際どうなるのかは僕は知りません...


こうすることで何がうれしいかというと、ラムダ計算での数少ない規則のひとつである「関数の適用」だけで数が表現できる、ということで、逆に言えば「関数の適用さえできるようにすれば数が使える」ということになるわけです。


これに関して僕は最初若干懐疑的な気持ちがあって、というのはこれって数学という道具を使って身振り手振りをしてるのと何ら変わらんのじゃないかなーとか思ったのですが、極論ですが、人類が滅びたあとに唯一残った文献を宇宙人が発見したとして、それがラムダ計算の文献であるのと、小学生の算数の教科書であるのとだと、後者のほうが数の理解自体はあっさり済むとは思うものの、人類の育てた数学の全体像は伝えられない。ラムダ計算であれば最小の規則のセットでそれを表現することができる(宇宙人がそれに気づくかどうかは別として)、というようなメリットがある。


といったところで、


ラムダ計算・チャーチ数についてはこんなところでまとめを終えておく。PCFの概要と、PCFでの操作的意味論を明日まとめるかー。


参考



  1. ラムダ計算 - Wikipedia

  2. 計算可能関数 - Wikipedia

  3. λ版 チャーチ数(再)|Chandler@Berlin

  4. λ計算とは - はてなキーワード

  5. プログラミング言語の意味論(PDF)

  6. 表示的意味論(PDF)

このアーカイブについて

このページには、2009年5月に書かれたブログ記事が新しい順に公開されています。

前のアーカイブは2009年4月です。

次のアーカイブは2009年6月です。

最近のコンテンツはインデックスページで見られます。過去に書かれたものはアーカイブのページで見られます。

ウェブページ

Powered by Movable Type 4.32-ja