Semantics with Applications を読んで denotational semantics について知る (2)

先に進む前に、前回みた while 文の意味の定義を振り返る。

文の semantic function から while 文のところだけを抜き出すと、

| While(condition, stm1) ->
    let f g = cond (b condition) (g $ (s stm1)) id in
    fix f

だった。ただし fix f は「f g = g になるような g」を返すものとする。この定義がそもそもどうやって出てくるのかを見ていきたい。まずは次のことがいえる。

「while b do S は if b then (S; while b do S) else skip と書き換えてもよい。」

これはどうやらその通りだ。というわけで、

| While(condition, stm1) ->
    s Cond(condition, Seq(stm1, While(condition, stm1)), Skip)

とする。条件文に対する semantic function の定義は、

| Cond(condition, stm1, stm2) -> cond (b condition) (s stm1) (s stm2)

だったから、

| While(condition, stm1) ->
    cond (b condition) (s Seq(stm1, While(condition, stm1))) (s Skip)

となる。順次実行の定義は、

| Seq(stm1, stm2) -> (s stm2) $ (s stm1) 

だったから、

| While(condition, stm1) ->
    cond (b condition) ((s While(condition, stm1)) $ (s stm1)) (s Skip)

となる。NOPの定義は、

| Skip -> id

だったから、さらに、

| While(condition, stm1) ->
    cond (b condition) ((s While(condition, stm1)) $ (s stm1)) id

となる。これはまだ、s While(condition, stm1) の内容を定義するために s While(condition, stm1) の全体を必要としているから、「統語範疇の意味はその構成要素だけから」決まるようにするという denotational semantics の目標に達していない。

ところでこの節は s の中の While に関する定義なのだから、必要とされる「s While(condition, stm1)」は「cond (b condition) (s While(condition, stm1)) $ (s stm1)) id」の戻り値でもある。

これを頭において、

cond (b condition) ((s While(condition, stm1)) $ (s stm1)) id : State.t -> State.t

の s While(condition, stm1) のところに穴をあけて関数化する、つまり、

fun g -> cond (b condition) (g $ (s stm1)) id : (State.t -> State.t) -> (State.t -> State.t)

としたときに、「s While(condition, stm1) : State.t -> State.t はこの関数の引数でもあるし戻り値でもある」ということになる。

ということはこの関数について「引数＝戻り値となるような値」を見つけることができればどうだろうか。

fix をそのような手段とすれば While の定義は、

| While(condition, stm1) ->
    let f g = cond (b condition) (g $ (s stm1)) id in
    fix f

と書ける。この定義はもはや構成要素だけから決まるようになっている。これが while 文の定義がこんな形になっている理由だった。

なお、ある関数について「引数＝戻り値となるような値」、つまり「f g = g となるような g」のことをその関数の fixed point と呼ぶ。

前回確認したのは関数の fixed point は複数ある場合があり、この定義だと fix が関数ではなく、したがって semantic function 全体も関数にならず、そうすると denotational semantics の目標が達成できないということだった。

だから fix は「fixed point が複数ある場合にもその中から適切な1つを選び取る」ように改修しなければならない。問題はその適切な1つをどのように定義するかだ。

Exercise 5.2 では while ~(x=0) do x := x-1 というプログラムには少なくとも次の2つの関数がその意味になってしまうということを見た。

let g2 = fun state ->
  if lookup "x" state >= 0
  then update "x" 0 state
  else undef ()
 
let g4 = fun state -> update "x" 0 state

「適切な1つ」は g2 のほうだ。この2つを見比べると、x が0以上の場合の結果は同じで、0未満だった場合の結果が違うことが見て取れる。0未満のとき g2 は停止せず、g4 は x を 0 にする。「0未満のとき停止せず」っていうのは「0未満の引数に対しては戻り値が定義されていない」ということだ。つまり関数の定義域に関していうと g2 のほうが g4 より小さい。これは g2 を選び取る基準に使えるのではないだろうか？

これ以降 fix を改修していくアイデアのあらすじは次のようなものになる。

- 関数を「順序付け」する方法を導入する
- fix は「一番小さい fixed point」を選び取るようにする

ここからまた様々な問題が立ちあがってくる。関数を順序付けするってどういうことか？その中で「一番小さいもの」って本当に決められるのか？