この記事はみす裏 Advent Calendar 2017５日目のために書かれました。

友達に「意味論、意味論ってなんだ」と聞かれたので、自分に分かる範囲でなるべく簡単に説明してみよう。読者としては「プログラミングはしたことあるけど、プログラミング言語論って何？」という人を想定している。なので、「IMPとかλ算法は分かるよ、でもSystem F（とその派生）はちょっと自信ないかな……」って人は読んでも無駄です。暇で暇で仕方ないなら、この記事のどこに間違いがあるか探してみよう。

この記事を読むことで、この分野の人たちってこんなことしてるんだなあとか、もしくは面白そうだから少し勉強してみようかな、とか思ってもらえれば成功。よくわからん！　ってなったら私の失敗なのでそういう時はコメントに書いておくと優しい人が教えてくれるかも。

言語＝構文＋意味

プログラミング言語をしっかりと定義するときには、まず構文、次に意味が与えられる。どのように構文を決めるかを構文論、どのように意味を決めるかを意味論という。これでは知ってる人にしか伝わらないので、身近な例で説明しよう。次の式は計算するといくつになるだろうか？

(1) 1 + 2 × 3

答えは「7」だ。では、次の式はどうだろう。

(2) 1 + × 2 3

これには答えられない。そもそも「正しい」式ではない。では、次の式は？

(3) 1 + 2 ^ 3

これは「9」と答える人もいれば、人によっては「0」と答えるかもしれない。

私たちが(1)に「7」と答えられるのは、「数式」の構文と意味についての共通理解があるからだ。つまり、+は左側の項と右側の項の和を計算し、×は積を計算するが+より優先順位が高いという認識がある。(2)では、私たちの考える数式の体を成していない。これは、「+と×の両側には項がある」とか、「数字が連続することはない」といった構文の規則にしたがっていないからである。(3)では^が２項演算であると予想がつけば構文は想像できる。しかし、^の意味（＝^がどのような演算をするのか）については色々な流儀がある。

どのように議論するのか？

ここからは少し難しいかも？

構文論は構文を（たいていの場合帰納的に）定義する。その書き方にはいくつかあるが、BNF（Backus-Naur form）が使われることが多い。数式の例でいえばこんな感じだ。(数字)と書いたところは0、1、...のような整数を表す文字が入ると思ってほしい。

E ::= T | E + E
T ::= (数字) | T × T

この構文規則によって1 + 2 × 3が生成されるので、1 + 2 × 3は正しい構文を持つと言える。一方、1 + × 2 3は生成できないので正しくない。

意味論は正しい構文を持つ項が何を表しているかを定義する。意味論の書き方には横線を使った記法が使われることが多い。横線の上には前提をいくつか並べ、下にはそれらの前提から導ける結論を書く。上に何もないときはそれが自明であるという意味になる。

前提1 前提2 前提3 ...
-------------------
       結論

ここで、ある式Eが計算の結果nになることをE → nと書くことにすると、上で与えた構文に対応する数式の意味は次のようになる。


--------------
(数字) → (数値)

  E1 → m   E2 → n
--------------------
E1 + E2 → （mとnの和）

  T1 → m   T2 → n
--------------------
T1 × T2 → （mとnの積）

一番上は13869948と書いてあったらそれはそのまま13869948という整数の１つを表すということである。2番目は+の左側と右側がそれぞれmとnと計算できるなら、それらの和が計算できるということを表している。3番目も同様。

初めはもう少しプログラミング言語らしくif-then-elseを定義しようとか思ってたけど、長くなってきたからやめておこう。調べればいくらでも出てくるし。

何が嬉しいんだ？

「よくわからないけど、そんなことしなくてもプログラミングはできるし、一体何が嬉しいの？」というのが普通の感想だろう。実際、現実に使われているプログラミング言語は非常に複雑で、それを上手く扱える理論を構築することは不可能に近い。

しかし例えば、現実には直線や円、正三角形などの理想的な図形は存在しないが、幾何学は図形について多くの性質を証明しているし、それらは現実に生かされてもいる。それと同じく、簡略化されていてもこのように定義を与えることで数学的に厳密な議論が可能になり、プログラミング言語が満たす性質を証明することができるようになる。このことはソフトウェアの形式的検証（型理論、モデル検査など）では大いに活用され、堅牢なソフトウェアを作るために利用されている。

本当はもっとくだらない記事を書きたいんだけど、投稿する場がなくて……