本文へジャンプ

学科概要
  • HOME
  • 学科概要
  • 学生による学科紹介

学生による学科紹介

実際の授業をいくつか文書におこしてみました。先生方の仮想講義を体験してみてください。情報科学科の講義は90分授業です。午前中の講義は10時15分から、午後の講義は13時から始まります。14時45分からの講義がある曜日もあります。

言語モデル論 | 米澤 明憲
開講時間:月曜2限 | 1
シラバス
プログラミング言語の基礎理論、プログラミング言語のモデル、意味論について講義する。
授業細目: (1)計算とは、 (2)帰納的関数とプログラミング、 (3)ラムダ計算、 (4)プログラム言語の意味論、 (5)作用型プログラミングと並列処理、 (6)型推論
概要
プログラミング言語について基本的なことを学びます。
前半にはプログラムによる計算について、理論的な面白い話が聴けます。
後半では型理論の片鱗を垣間見ることができます。
本講義には lambda 計算をはじめとする、基本的かつ重要な話題が盛り沢山で、
すべて消化するのは大変ですが、プログラミング言語を自作したいという意欲的な人には勿論、
そうでない場合も情報科学者の常識としてきっと役に立つ、聴いておいて損はない講義であると言えます。
Church の提唱
私たちがコンピュータを使って何かしようというとき、
多くの場合、望みの動作を記述したプログラムというものを用います。
言うなればプログラムはコンピュータに対する指令書であり、
その指令書を書くための言語がプログラミング言語です。
あなたがパソコンを使うときにお世話になってる OS だって、立派なプログラムの一つです。
プログラムに記述された動作の手順をアルゴリズムと言います。
簡単に言ってしまうと、アルゴリズムは何らかの関数を計算する手順のことです。
OS が関数・・・。変だと感じる人が多いのではないでしょうか?
とりあえず、ゲーデルの算術化を考えれば大丈夫なんだ、と難しそうなことを言って誤魔化しておきます。
(興味のある人は首を突っ込んでみて、その真偽を確認してみて下さい)
さてそうすると、計算可能な関数を考えるとアルゴリズムがどんなものなのか分かりそうです。
それでは計算可能な関数って何でしょうね?
上の考えをひっくり返すと、それがどんなアルゴリズムかはさておいて、
(実行可能な) アルゴリズムが存在する関数のことではないかと考えられます。

ここまで読んで、「いったい何が言いたいんだ?」と思った人もいるでしょう。
噛み砕いて言うと、アルゴリズムと計算可能な関数を同一視できそうですね、ということです。

話は変わって、ちょっとだけ歴史の話をしましょう。
偉大なる先人達は様々な計算モデルを考案してきました。
チューリングマシン、lambda 計算、帰納的関数などなど。
これらのモデルは実は等価なものであるということが分かり、
これを計算可能な関数であると考えよう、という主張をする人物が現れたのでした。
こうして計算可能な関数は厳密な定義を与えられることになりました。
(実際のところ、筆者はこの辺りの話に明るくないので、インターネット上でサラッと調べたものです。本当にお話程度に考えて下さい。)

話を戻しましょう。
アルゴリズムと計算可能関数を同一視することで、
アルゴリズムを厳密な計算モデルを用いて定義することができます。
こうした主張は Church の提唱と呼ばれており、本講義の始まりを飾ることになります。
講義とは無関係ですが、先の計算可能関数を超える関数を考える場合、Hypercomputing という分野になります。
興味のある人は調べてみて下さい。
プログラムの意味
ところで、アルゴリズムが厳密に定義されると何が嬉しいのでしょうか?
それはプログラムの意味を扱えることにあるのかもしれません。
話が飛躍してしまったように感じるかもしれませんが、
アルゴリズムが決定されればプログラムの動作は自然に決まりますので、
アルゴリズムとプログラムを同一視できることになります。

詳しくは説明しませんが、本講義では次の三つの意味論をとりあげます。

* 操作的意味論
o プログラムを解釈・実行する抽象機械を定義する
* 公理的意味論
o プログラムの性質・機能の仕様を記述し、証明する
* 表示的意味論
o プログラムに対応する数学的なモデルを与える


こうした意味論を用いることで、
プログラムの仕様記述を厳密にできたり、
プログラムの動作を明確に表現したりできます。
lambda 計算
先に述べたように、アルゴリズムを定義する方法として計算モデルがあります。
本講義では帰納的関数と lambda 計算について勉強します。
ここでは lambda 計算について紙面を割いてみようと思います。

参考までに帰納的関数についても簡単に触れておきます。
講義では実際に帰納的関数を定義し、
それが N プログラムというプログラム (で記述されたアルゴリズム) によって計算可能であることを示し、
続いて N プログラムで計算可能な関数が帰納的関数であることを示すという手法で、
N プログラムにより計算可能な関数の全体が帰納的関数に一致するということを証明します。
帰納的関数については 3 年生夏学期の情報論理でも勉強すると思いますが、
情報論理とは少し見方が違いますので、良い復習になると同時に帰納的関数の重要性を再確認する機会にもなります。

さて lambda 計算についてですが、
Scheme とか ML とかいったプログラミング言語をご存知でしょうか?
Scheme は 2 年生冬学期に、ML についてはその方言である OCaml を 3 年生夏学期に勉強するはずです。
これらは関数型のプログラミング言語と呼ばれますが、
この関数型言語の基底概念こそ、ここで学ぶ lambda 計算なのです。
簡単に言ってしまうと、lambda 計算とは記号の書き換えが計算とみなされる、シンプルな体系です。
例えば

x + 1

という式を考えます。
このとき x + 1 の意味するものは x を変数とする関数のことでしょうか?それとも x という値に 1 を加えた結果のことでしょうか?
lambda 計算においてはこれらははっきりと区別されます。

x + 1

というのは x という値に 1 を加えた結果を表し、

lambda x. x + 1

というのは x を変数とする x + 1 という関数を表します。
つまり式の前に lambda x と書くことで x が変数であることを明示しているのです。
このことを x に関する lambda 抽象と言います。
また

(lambda x. x + 1) 1

と書くと、変数 x の値を 1 にするということを意味します。
このことを関数適用といいます。
この関数適用についてですが、
すぐ上で「変数 x の値を 1 にする」と書きました。
これは x + 1 を 1 + 1 にするということです。
つまり

(lambda x. x + 1) 1



1 + 1

と (直観的な意味としては) 等しいということになります。
実はこの変換操作は lambda 計算における基本的かつ唯一の計算操作にあたり、beta 変換と呼ばれます。
少しだけ一般的に書くと、beta 変換は

(lambda x. f x) y

という形の式を

f y

という形に変換する操作であり、
この操作こそが lambda 計算が計算 たる所以であると言えます。
式を記号列であるとみなせば、前述した通り lambda 計算は記号の置き換えが計算にみなされる体系である、となる訳です。

上では 1 とか何も考えずに書いてきた訳ですが、
厳密に言うと整数は lambda 式ではありません。
(lambda 式自体は lambda 抽象と関数適用を用いて再帰的に定義されるものです)
lambda 記法では lambda 式以外は許されないので、何も考えずに使ってはいけないのです。
「なんだ、整数も使えないのか」と思ったかもしれませんが、
整数などは lambda 式で符号化することで表現可能です。
例えば 0 は、lambda 計算の考案者 Church に従うと、

0 := lambda f. lambda x. x

となります。
やっぱり講義とは直接関係ありませんが、
集合論をご存じの方は自然数の定義方法に共感を覚える場合もあるのではないでしょうか。

型理論
上で述べた lamdba 計算ですが、
世の中には型付き lambda 計算というものがあります。
その名の通り型が付いた lambda 計算なのですが、
型とは何でしょう?

という訳で、本講義の最後には、型理論について基本的なことを学びます。
型とは値の集合ですが、
式の値に対する制約、
もしくは対象領域に登場する実体をモデル化した表現であると考えることができます。
後者をクラスと呼ぶこともあります。
型を使うことで、
型検査によるエラーの発見ができたり、
型情報を用いたプログラムコードの最適化が可能になったりします。
例えば変数 x と y があり、

x + y

という式を考えているとします。
x や y が自然数であれば算術的な加算ですし、
文字列であれば連結かもしれません。
そんなとき x が自然数であると明示してあれば x + y は加算であると考えられます。
もしも y が文字列であると明示してあればプログラマの間違いである可能性があります。
つまり自然数であるとか文字列であるとかが明示してあれば、それだけでエラーの発見につながる訳です。
このような自然数とか文字列とかを型といい、x の型は自然数である、と表現します。
上手く利用すれば色々と嬉しい型ですが、
プログラムの随所に型を指定することは、冗長で煩雑なコーディングにつながる可能性があります。
そこで登場するのが型推論です。
例えば

x - 1

という式があれば、何も指定がなくとも x は数であると考えるのが妥当です。
型推論を使うことで無用な記述を省くことができます。
まとめ
以上、講義の流れを簡単に追いかけてみましたが、
紙幅の都合で記述できなかった部分も多々ありますし、
回りくどい文章で伝わりにくかったところもあることでしょう。
是非ご自分の目で見、耳で聞き、興味を追求し、本講義を通じて情報科学の深淵へと踏み出してみて下さい。
進行
本講義では内容豊富なレジュメが配布され、基本的にはそれに従って進行していきます。
板書も少しありますが、米澤先生のご説明をよく聞き、理解に傾注した方が実り多いのではないかと思われます。
レジュメの随所には課題が記されています。
なかなか頭を使う課題もあるので、復習の意味合いも込めてチャレンジしてみると良いでしょう。
評価
基本的には試験で、出来が悪いときのボーナスとして課題レポートが評価される、という形式のようです。
原則として講義内容がそのまま出題されますので、
しっかり覚えていればそれほど難しい試験ではないと思います。
また、試験対策の意味でも保険の意味でも、課題はやるに越したことはないです。
中でも、年の変わり目辺りで出題される、lambda 計算をシミュレートするプログラムを Scheme で実装せよ、という課題はなかなか楽しめると思います。
是非チャレンジを。