中島玲二著　数理情報学入門　-スコット・プログラム理論- 1982年



一般のソフトウェアエンジニアにとってこの本に書かれている内容を理解するのは大変難しい
ように思われます。その理由は、文字や式による説明が中心のため概念のイメージが掴み
にくいためです。著者はおそらく丁寧に説明したつもりでしょうが、その考えに慣れていない
人にとっては中々読み進めないと思います。

ここでは、この本を読んでいて分かり難かった点を中心に補足説明を述べます。

１．プログラムの表示的意味論
　この本では、第１章の「プログラムに意味を与える」がプログラムの表示的意味論の考え方を
説明しています。ここで、まず引っかかるのは、「プログラムの意味とは？」何かです。

プログラム言語には構文規則があり、そこでどんな記号の列が認められるかを定めていますが
それはあくまで記号の列に過ぎません。この記号の列に意味を与えるのがプログラムの意味論
です。ここで、プログラムの意味とは、プログラムを実行することにより得られる効果（結果）の
ことです。例えば、簡単なプログラムの行で[suc 0」があった場合、これは構文規則では記号の列
ですが、これを実行することにより得られる結果は「0に続く次の数、すなわち1」です。これがsuc 0
というプログラムの行の意味です。
したがって、プログラムの意味論とは、
　構文規則の記号列に、その実行結果（これが記号列の意味）を与えることです。また、記号列に
　その意味を対応させる関数を「意味関数」と言います。


■構文規則の簡単な例：プログラム言語Little

上記の構文規則によりLittleプログラムがどんな記号の列で表されるかが決まりました。

次に、これに意味を与えます。
■Littleプログラムの意味は、構文規則の各構成要素にその意味を与えればよいので
次のように意味を与えます；

以上のことを図示すると、次のようになります；

この図がLittleプログラムの意味論を表しています。
すなわち、構文規則の記号列に、意味領域でその実行結果（これが記号列の意味）を与えています。

このような意味の与え方のアナロジーとして「車の操作の意味論」を考えることができます。
（以降、続く）