日々の流転

λ. セマンティクス

セマンティクスって？ - ひげぽん OSとか作っちゃうかMona- あたりの話。すご〜〜く大雑把に説明してみる。

「(2*3)+(4*5)」という式は、(2*3)+(4*5) → 6+(4*5) → 6+20 → 26 と書き換えできるよね、というのが操作的意味論(operational semantics)。正確にはsmall-stepの操作的意味論。どういう書き換えが出来るかを通常は再帰的に定義する。操作的意味論は良く知らないので、詳しい人にお任せ。

「(2*3)+(4*5)」という式は26という数を表しているよね、とか「明けの明星」は金星を指す表現だよね、というのが表示的意味論(denotational semantics)。何を表しているか、何を指し示しているかが意味。発想としては一番簡単だと思う。こちらも部分式の意味から再帰的に意味を定義する。

公理的意味論(axiomatic semantics)は、命令型言語のプログラムというのは状態を書き換えるコマンドだという立場。それで、プログラムの実行前の状態で成り立っている条件と、プログラムの実行後の状態で成り立っている条件との間の関係によって、プログラムの意味を考えたり検証したりしましょうというアプローチ。例えば、「i = i + 1」というプログラムがあって、その実行後の状態で i==5 が成り立っていたら、実行前には i==4 が成り立っていたに違いない、とかそんなの。

すご〜〜く大雑把にしか説明してないけど、どれも本当は奥が深いです。

蛇足

操作的意味論も表示的意味論も言語の研究にはずいぶん使われているけど、一般のプログラマにとって馴染み深いのは「契約による設計(Design By Contract)」とかJMLとかの背景にある公理的意味論ではないかと思う。