from 横内『プログラム意味論』

式や文に意味を与える関数

では、

式の方をM_\mathrm{exp}[\![E]\!]\phi

文の方をM_\mathrm{cmd}[\![C]\!]\phi

文はCommandとみなしてCらしい

と書いてるがめんどいので以下のように書く

式は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 は具体的な式なので、例えば

etc.

while文の意味づけは難しい

while文は無限ループがありうる

無限ループは、M_sの返り値M_s(S)\phiが未定義であるという意味

つまりM_s(S)の返り値の Env->Env が、部分関数になっている