プログラムの3つの意味論のまとめ

　Wikipediaのプログラム意味論のページによると、プログラムに関する意味論は公理的意味論 (axiomatic semantics)、操作的意味論 (operational semantics)、表示的意味論 (denotaional semantics) の3つに大別されるそうだ。
　しかし、説明を読んでも、なにがなんやらさっぱりわからない、という人の方が多いのではないだろうか。「操作的意味論: 何らかの変換を施すのではなく、その言語の実行によって直接的に意味を説明する。」という説明で膝を打つ人がいるとしたら、もうその人はWikipedia読んでる場合じゃないだろう。
　たかが論理、されど論理によれば、公理的意味論とはHoareの体系の推論規則を通してプログラムの意味を与える物であり、操作的意味論とは「仮想機械の定義と、プログラムから仮想機械のコードへの変換規則(早い話がコンパイルのし方) を定め、それでプログラミング言語の意味論が定義されたとしてしまう、全く節操のない意味論」であり、表示的意味論とは「プログラムにλcalculus という形式体系のλ項というものを対応させることによって、プログラムの意味を定義する」ものであるそうだ。
　結局、Hoareの体系やラムダ計算について知らなければ、何が何やらという感じだろう。しかし、知りたければここら辺を勉強すれば良いのだな、という程度の事は分かる。
　Hoareの体系については、先ほどのたかが論理、されど論理にさわりだけちょっと書いてある。ラムダ計算について知りたい場合は、論理と計算のしくみ(AA)とか買えばいいんじゃないかな。
　もちろん、これらの定義はやや乱暴なもので、厳密な事を言い出すともっと抽象的な話になっていくのだろうけれど。概ねそんな感じ、と理解しておくのはあながち間違いではないだろうと思う。
　なお、R5RSには形式的意味論と言う節があるが、読んでみると「この節は形式的な表示的意味論を定める」とあった。R5RSのアレは、lambda calculusらしい。