セマンティクス

「意味」って一言で言っても、「意味ってなに？」という問題があって、「何が意味なのか」によってフォーマルなセマンティクスの書き方には流儀があります。プログラミング言語の話をするときには、次の三つがメジャーかと。

  1. 表示的意味論(denotational semantics)
  2. 操作的意味論(operational semantics)
  3. 公理的意味論(axiomatic semantics)

プログラマにとって一番イメージしやすいのが操作的意味論だと思うのですが、これは「そのプログラムを実行すると何が起きるのか？」が意味だという立場です。この立場から言えば、「意味」というのはつまりインタプリタになります。

表示的意味論は、私も良くわかっていないのですが、「プログラムの意味を返す辞書」みたいな関数を定義して、それが意味だって言います。わかってないので、あんまり触れたくない。

公理的意味論は「そのプログラムについて何が証明できるか」が意味だという立場。

で、さらにいい加減なことを言うと、現在、プログラミング言語の形式意味論は、操作的意味論が殆どになっているような感じがあります。R6RSも操作的意味論だったりとか。TAPLも操作的意味論で説明してますし。大堀先生の教科書(ちょっと古い)は、三つとも書いてあるけど。


ちなみにちょっと卑怯な方法だと、ある(すでに意味が与えられた)プログラミング言語への変換を示すことによって、他のプログラミング言語の意味を与える、という方法もあったりします。(let ( (x e1) ) e2)の意味は( (lambda (x) e2) e1)と一緒、みたいな感じ。これで、letが無いSchemeの意味が与えられている場合は、letがあるSchemeに意味を与えることができるわけです。