意味関数
meaning function
式や文に意味を与える関数
横内『プログラム意味論』.iconでは、
式の方を$ M_\mathrm{exp}[\![E]\!]\phi
文の方を$ M_\mathrm{cmd}[\![C]\!]\phi
文はCommandとみなしてCらしい
と書いてるがめんどいので以下のように書くmrsekut.icon
式は$ M_e(x)\phi、文は$ M_s(x)\phi
式の意味関数
$ M_e:\mathrm{Exp}\rightarrow(\mathrm{Env}\rightarrow\mathrm{Val})
Expは式、Envは環境、Valは値
この関数に式$ \mathrm{Exp}、環境$ \phiを通して得られる値を$ M_e(\mathrm{Exp})\phiと書く
ある環境$ \phiにおいてその変数が何を表すか
定数を入れたら定数がそのまま出てくる
ex
例えば環境$ \phiの中に$ x=42という定義が含まれていれば、$ M_\mathrm{exp}(x)\phi=42
また定数の場合は$ M_\mathrm{exp}(33)\phi=33になる
引数であるExpはただの記号列だが、返り値であるValは秩序を持ったものである
つまり関数を通すことで「意味」が与えられている
例えば自然数世界を考えるなら、
引数の4+3とかはただの記号の並びだが、
返り値の4+3や7は自然数である
文の意味関数
$ M_s:\mathrm{Stmt}\rightarrow(\mathrm{Env}\rightarrow\mathrm{Env})
この関数に文$ sを通して得られる値を$ M_s(s)\phiと書く
返り値は環境である
文を適用したあとの環境を返す
代入文を想像するとわかりやすい
返り値はEnv->Envの関数$ \phiなので、これを式の意味関数の引数に使えばいい
Stmtは具体的な式なので、例えば
x:=E
if E1 = E2 then C1 else C2
etc.
while文の意味づけは難しい
while文は無限ループがありうる
無限ループは、$ M_sの返り値$ M_s(S)\phiが未定義であるという意味
つまり$ M_s(S)の返り値のEnv->Envが、部分関数になっている