プログラム意味論の分かりやすい紹介
巷に膾炙しているプログラム意味論の説明は、正直言って何を言っているのか、部外者にはよく分からないように感じられる。プログラムの意味を論じる「プログラム意味論」の意味がよくわからないというのは本末転倒だろう。ここでは、プログラム意味論を分かりやすく紹介したい。
プログラムの意味
プログラム意味論とは、プログラムの意味に関する理論だ。
そもそも「意味」とはなんだろうか。「意味」の意味を知るために、デジタル大辞泉で調べてみよう。
１ 言葉が示す内容。また、言葉がある物事を示すこと。「単語の―を調べる」「愛を―するギリシャ語」
２ ある表現・行為によって示され、あるいはそこに含み隠されている内容。また、表現・行為がある内容を示すこと。「慰労の―で一席設ける」「―ありげな行動」「沈黙は賛成を―する」
３ 価値。重要性。「―のある集会」「全員が参加しなければ―がない」
いみ【意味】の意味 - goo国語辞書
「意味」の語義が3つ示されているが、要約すると、ひとつめは「言葉が示す物事」、ふたつめは「行為が示す物事」、みっつめは「行為が持つ価値」だ。この3つの「意味」の意味は無関係なものではなく、共通した構造が存在している。それは、何か言葉や行為という表に見えている表現は、その裏にある物事や価値に繋がっているという構造だ。
たとえば、店で「ビールあり〼」という看板を見たとする。ビールの実物を見ずとも、その店には実際にビールが用意されていて、店はそのビールを売る意図があって、自分はそれを注文して飲むことができるという場面を想像できる。その想像された場面や、その場面の持っている価値が、「ビールあり〼」の意味だと言える。
プログラムの意味も同様だ。プログラムの意味とは、そのプログラムによって実現される物事や場面のことだと言える*1。例えばalert(1)というJavaScriptのプログラムは、実行するとダイアログ・ボックスで“1”を表示する。すなわち、alert(1)の意味は「ダイアログ・ボックスで“1”を表示する」という場面だ。
プログラムの意味は、そのプログラムを動かしてみれば分かるように思うかもしれないが、プログラムを動かすにもコストやリスクが存在する場合がある。誤作動を起こすプログラムを実際に動かしてしまえば、重大な事故を引き起こすかもしれない。それを避けるためには、プログラムを動かすことなく、その意味を知る必要があるのだ。
優れたプログラマーが頭の中で考えたプログラムを一発で動かしてしまうのも、プログラムの意味を体得しているからだと言える。しかし、プログラムの意味を個人の経験によって身に付けるのは時間がかかるだけではなく、その厳密さにも限界がある。見慣れない種類のプログラムがどのように動くかは、経験からでは分からないのだ。そういう場合でも、プログラム意味論でプログラムの表現と物事の間にある関係を詳細に学ぶことで、プログラムの意味を正確に把握できるようになるだろう。
形式的意味論
意味論は表現と物事の対応を論じるものではあるけれど、現実の物事はすごく複雑で、それをありのままに考えて厳密に論じるのはとても難しい。そこで、普通は物事を抽象化した上で、厳密に考えることになる。*2物事を抽象化した上で、数学や論理学を使って厳密に論じられる意味論が、形式的意味論だ。形式的意味論には操作的意味論、表示的意味論、公理的意味論といった大別がある。
操作的意味論は、表現を操作する規則や抽象機械を使ってプログラムの意味を考える。この意味論では表現の操作過程や抽象機械の動作が、表現の意味となる。この意味論は、現実のコンピューターの動作に一番近い形で表現された意味論で、プログラムに対して、機械がどれほどの計算資源を使い、どのように動作するのかを厳密に議論するのに適した表現だと言える。その一方で、操作的意味論が扱った規則以外の方法でプログラムを処理することについては考慮しないので、プログラムの読みやすさや編集しやすさを議論するには適していないだろう。
表示的意味論は、表現から物事への写像（表示）を使ってプログラムの意味を考える。この意味論においては、表現からの写像が定義できる好きな領域を意味としてよい。この手法は、言語の意味を数理論理学や言語哲学と同様の手法を用いて考えており、プログラムを読み書き・編集するときの性質を分析するのに向いている。例えばプログラミング言語が「構成性」という性質を持っていることが意味論から分かるので、その性質を利用したプログラムの最適化を行う、といったことに使える。
公理的意味論は、表現と物事の間に成り立つ関係（仕様）を使ってプログラムの意味を考える。この意味論においては、仕様を公理として証明できる物事が、表現の意味となる。この意味論では、仕様にないプログラムの具体的な動き方は分からないが、プログラムの「停止性」のような抽象度のより高い性質を証明するのに向いている。
