ブックレビューじゃないよ。ごめんね。
某数学者のたまわく、最も効率よい勉強の秘訣は一に論文を書くこと、二に教えること。
ってわけで(?)、ヤル気が花粉のように湧き出ているうちにまとめ、まとめ。まぁ多分僕以外全然面白くないと思うけど、ひょっとしたらどんな内容か知りたい人もいるかもしれないので。
テキストはGlynn WinskelのThe Formal Semantics of programming Languages:An Introductionという本に添っているが今のところどうでもよい。
プログラム言語の意味論には3通りある。操作的意味論operational semantics、表示的意味論denotational semantics、公理的意味論axiomatic semanticsである。後者になるほど抽象化するのだが、ここではまず操作的意味論を扱い、小さな命令型プログラミング言語IMP(Imperativeの略)を想定して話を進めるようだ。
まず面白い、と思ったのはプログラムの実行過程における状態の定義。実行状態σとは、算術式の集合から整数の集合への関数である。算術式とは3とかa+3とかx*yとかそういう式だと思えばよい。状態σのもとで算術式aを評価（要するに計算）した値がnであるとき、これを<a,σ>→nと書く。これは表記上の問題で大したことではない。参考までにこれは状態の集合と算術式の集合と整数の集合の直積上の三項関係であるが、これもσが一変数関数なのだから当然だ。
プログラムは状態σのもとで一つ一つコマンドを実行する。これは例えばソースコードの1行に相当する。操作的意味論における評価の表現は先の通りだが、コマンドの表現は<c,σ>→σ'である。これはコマンドcが状態σをσ'に変化させるという意味を表す。
状態の定義から自然に状態の同値性が定義される。ある二つの状態σ1、σ2のもとで『同じ算術式a1,a2,...を評価した値がそれぞれ常に同じ』ならばこの二つの状態は同値とみなしてよい。同様に、二つの算術式a,a'が『任意の状態σと任意の整数nに対して<a,σ>→nと<a',σ>→nが同値』を満たすときa,a'は同値である（言い換えれば、どんな状態でも常に同じ値を返す2式は等しい）といい、二つのコマンドc,c'が『任意の2状態σ,σ'に対して<c,σ>→σ'と<c',σ>→σ'が同値』を満たすときc,c'は同値であるという。要するに、どんな状態に与える影響もそれぞれ常に等しい二つのコマンドは等しいとみなすということだ。
コマンドの同値性を使うと一見ナンセンスな命題が導かれる。どの状態からスタートしても発散して答えが出ないプログラムは、互いに同値である。これは『<c,σ>→σ'⇔<c',σ>→σ'』という条件の(σ、σ')にはまる状態対が存在しない、つまり両辺が常にfalseということによるのである。ただプログラムの発散と停止の違いがまだ僕にはよくわかっていない。
最後にやったのは、IMPにおいて
こんなところでいいのかな。kawayuさんあたり、補正があれば頼みたいです。なかなか要約の難しい内容だ。さてどこが面白いのか。状態と変数という数学的概念があって、ある状態のもとで変数を評価（計算）するとある数値がポンっと出る。何かに似てません？そう、量子力学ですよ。評価ってのを測定に変えるだけでそっくりそのまま。といっても僕がかじってたのはDiracの行列力学の方だけで、化学とかで扱う波動力学の方ではどうなってるのかさっぱりなんですが・・・素人目にもこんな類似があるとは思わなかった。まぁ、だからって量子コンピュータすごいとかそういう安易な展開にはならないわけですがｗ ってかもう操作的意味論の話終わったっぽい。はえぇ。
解ける問題のうち常に現実的な時間で解けるものを実際に解ける問題という。例えば素因数分解は実際には解けない問題である。最大公約数を求める問題は実際に解ける問題だが、それを解くアルゴリズムは一つとは限らない。さらにEuclidの互除法という一つのアルゴリズムをとっても、それを記述するプログラム（ソースコード）は何通りもある。
話変わって、整数から整数への関数の集合(N→Nと書くことにする)が可算（整数添字をつけて全ての要素を数えることができる）ではないことの証明。参考までに、有理数や有限集合は可算、実数は不可算である。背理法を使うが、そんなに難しくないので気構えないで頂きたい。仮にN→Nが可算とすると、f_0(x),f_1(x),f_2(x),...と全ての関数を列挙することができる。ここでg(x)=f_x(x)+1を考える。gは明らかに整数に対して整数を返す関数で、従ってN→Nの元だから整数kが存在してg(x)=f_k(x)と書けるはずだが、ここでx=kを代入するとおかしなことになる。つまりf_k(k)=g(k)=f_k(k)+1となるのだ。目からウロコである。このように矛盾を導く論法を対角線論法と呼ぶが、確かGoedelの不完全性定理の証明にも対角線論法が使われていたような気がしてびっくりである。
P.S.明らかに文章がおかしいところを修正しました。どうやら<と>をブログで編集しようとするとバグに悩まされるようです。
某数学者のたまわく、最も効率よい勉強の秘訣は一に論文を書くこと、二に教えること。
ってわけで(?)、ヤル気が花粉のように湧き出ているうちにまとめ、まとめ。まぁ多分僕以外全然面白くないと思うけど、ひょっとしたらどんな内容か知りたい人もいるかもしれないので。
計算機科学
テキストはGlynn WinskelのThe Formal Semantics of programming Languages:An Introductionという本に添っているが今のところどうでもよい。
プログラム言語の意味論には3通りある。操作的意味論operational semantics、表示的意味論denotational semantics、公理的意味論axiomatic semanticsである。後者になるほど抽象化するのだが、ここではまず操作的意味論を扱い、小さな命令型プログラミング言語IMP(Imperativeの略)を想定して話を進めるようだ。
まず面白い、と思ったのはプログラムの実行過程における状態の定義。実行状態σとは、算術式の集合から整数の集合への関数である。算術式とは3とかa+3とかx*yとかそういう式だと思えばよい。状態σのもとで算術式aを評価（要するに計算）した値がnであるとき、これを<a,σ>→nと書く。これは表記上の問題で大したことではない。参考までにこれは状態の集合と算術式の集合と整数の集合の直積上の三項関係であるが、これもσが一変数関数なのだから当然だ。
プログラムは状態σのもとで一つ一つコマンドを実行する。これは例えばソースコードの1行に相当する。操作的意味論における評価の表現は先の通りだが、コマンドの表現は<c,σ>→σ'である。これはコマンドcが状態σをσ'に変化させるという意味を表す。
状態の定義から自然に状態の同値性が定義される。ある二つの状態σ1、σ2のもとで『同じ算術式a1,a2,...を評価した値がそれぞれ常に同じ』ならばこの二つの状態は同値とみなしてよい。同様に、二つの算術式a,a'が『任意の状態σと任意の整数nに対して<a,σ>→nと<a',σ>→nが同値』を満たすときa,a'は同値である（言い換えれば、どんな状態でも常に同じ値を返す2式は等しい）といい、二つのコマンドc,c'が『任意の2状態σ,σ'に対して<c,σ>→σ'と<c',σ>→σ'が同値』を満たすときc,c'は同値であるという。要するに、どんな状態に与える影響もそれぞれ常に等しい二つのコマンドは等しいとみなすということだ。
コマンドの同値性を使うと一見ナンセンスな命題が導かれる。どの状態からスタートしても発散して答えが出ないプログラムは、互いに同値である。これは『<c,σ>→σ'⇔<c',σ>→σ'』という条件の(σ、σ')にはまる状態対が存在しない、つまり両辺が常にfalseということによるのである。ただプログラムの発散と停止の違いがまだ僕にはよくわかっていない。
最後にやったのは、IMPにおいて
while b do c（これをwとする）と
if b then c;w else skipという二つのコマンドが同値であることを導出木の計算を使って証明する、ということだったが、ここらへんはチマチマしてるので省略。
こんなところでいいのかな。kawayuさんあたり、補正があれば頼みたいです。なかなか要約の難しい内容だ。さてどこが面白いのか。状態と変数という数学的概念があって、ある状態のもとで変数を評価（計算）するとある数値がポンっと出る。何かに似てません？そう、量子力学ですよ。評価ってのを測定に変えるだけでそっくりそのまま。といっても僕がかじってたのはDiracの行列力学の方だけで、化学とかで扱う波動力学の方ではどうなってるのかさっぱりなんですが・・・素人目にもこんな類似があるとは思わなかった。まぁ、だからって量子コンピュータすごいとかそういう安易な展開にはならないわけですがｗ ってかもう操作的意味論の話終わったっぽい。はえぇ。
コンピュータサイエンス入門
目下のキーワードは問題、アルゴリズム、プログラムの3つである。コンピュータサイエンスにおける問題には入力だけでなく必ず出力（答え）がなければならない。一つの問題を解くのに必要なアルゴリズムが存在する場合は解ける問題、しない場合は解けない問題とよぶ。プログラムの停止性問題、最速のプログラムを見つける問題、Hilbertの第10問題（整数係数のDiophantos方程式が整数解をもつか判定する）は解けない問題に属する。講義は解ける問題と解けない問題の境界線を探る。解ける問題のうち常に現実的な時間で解けるものを実際に解ける問題という。例えば素因数分解は実際には解けない問題である。最大公約数を求める問題は実際に解ける問題だが、それを解くアルゴリズムは一つとは限らない。さらにEuclidの互除法という一つのアルゴリズムをとっても、それを記述するプログラム（ソースコード）は何通りもある。
話変わって、整数から整数への関数の集合(N→Nと書くことにする)が可算（整数添字をつけて全ての要素を数えることができる）ではないことの証明。参考までに、有理数や有限集合は可算、実数は不可算である。背理法を使うが、そんなに難しくないので気構えないで頂きたい。仮にN→Nが可算とすると、f_0(x),f_1(x),f_2(x),...と全ての関数を列挙することができる。ここでg(x)=f_x(x)+1を考える。gは明らかに整数に対して整数を返す関数で、従ってN→Nの元だから整数kが存在してg(x)=f_k(x)と書けるはずだが、ここでx=kを代入するとおかしなことになる。つまりf_k(k)=g(k)=f_k(k)+1となるのだ。目からウロコである。このように矛盾を導く論法を対角線論法と呼ぶが、確かGoedelの不完全性定理の証明にも対角線論法が使われていたような気がしてびっくりである。
P.S.明らかに文章がおかしいところを修正しました。どうやら<と>をブログで編集しようとするとバグに悩まされるようです。
>2.7
(2)が特にわからない。
>あと、「２．５簡単な性質の証明」の証明の順序って逆だよね？
うん、そう。細かいところはまだ斜め読みだけどｗ