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

これからの一連のエントリは私が "Semantics with Applications" (Nielson & Nielson) の第5章 "Denotational Semantics" を読みながら記録を残していくものです。注意点としては別に翻訳ではないし、理解に間違いを含むかもしれません。この本の第1版はウェブで読めるので怪しいぞと思ったらそちらを参照されるとよいでしょう。

http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

Denotational semantics の目標

Denotational semanticsではプログラミング言語の統語的な構成素それぞれについて、「統語的表現から数学的な対象への関数」を定義する。これをsemantic functionと呼ぶ。統語的な表現というのはベタなプログラムのテキストというよりは構文木をイメージしたい。数学的な対象というのは関数の場合が多い。だからsemantic functionは「構文木の断片を関数に変換する関数」だ。

ところで semantics function は厳密な意味で関数である。ということは入力となる構文のすべてに対して結果が定義されてなければいけないし、その結果というのは一意でなければいけない。このような semantics function が定義できればその言語の denotational semantics を定義するのに成功したことになる。

While 言語

この本ではWhileという簡易言語を例に使って説明をしている。算術式と真偽式と文の区別があって文には代入とNOPと順次実行と条件分岐と繰り返しがある。変数には数値だけが入って真偽値は入らない。文法は以下の通り。

a ::= n | x | a1 + a2 | a1 * a2 | a1 - a1
b ::= true | false | a1 = a2 | a1 <= a2 | ~b | b & b2
S ::= x := a | skip | S1; S2 | if b then S1 else S2 | while b do S

ここで n は数値リテラル（整数のみ）で、x は変数シンボル。これに対する semantic function の定義の仕方をどうするかというと、(1) 算術式、真偽式、文のそれぞれの統語範疇に対して定義し、また、(2) 統語範疇の意味はその構成要素だけから一意に決まるようにする。後者は semantic function が関数だとしたことの帰結でもあるし、フレーゲの構成性原理を満たすための要請でもある。

算術式の semantic function

まず a1 + a2 みたいな算術式に対応する semantic function の型は以下のようなものになる。（なお、以降の型の表記方法やその他の数学的表記は適当に OCaml 風に改変しています。そのほうがブログに書きやすいし、それに私の場合、数学的表記には拒否感が働くけどプログラムならイメージしやすいから。でも本当はプログラムではなく数学的関数などを表現するものです）

val a: aexp -> (State.t -> int)

a というのが semantic function の名前だ。aexp というのが算術式の構文木の型で、これを semantic function である a に通すことによって State.t -> int という（関数の）型になる。これが算術式の意味だ。

ところで算術式は数値（整数）を表すのだからその semantic function は単純に aexp -> int ではいけないのか。算術式は変数を含むかもしれないのでそうはいかないのだ。変数を含む算術式は環境の影響を受ける。

State.t は現在の環境（変数の状態）を表す型だ。直観を助けるために State.t 型には以下のようなシグニチャがあるのだと思いたい。

module type State =
  sig
    type t
    val initial_state : t
    val lookup : string -> t -> int
    val update : string -> int -> t -> t
  end

aとaexpはOCaml風に書くと以下のようになるのだろう。

type aexp = Val of int | Var of string | Add of aexp * aexp ...
let rec a aexp state = match aexp with
| Val(n) -> n
| Var(x) -> lookup x state
| ...

真偽式の semantic function

同様にして真偽式に対する b: bexp -> (State.t -> bool) という semantic function も存在する。変数に入るのは数値だけだけど x <= 1 みたいな式ではやはり環境の影響を受けるので State.t -> bool になる。

type bexp = T of bool | Eq of bexp * bexp | Neg of bexp | ...
let rec b bexp state = match bexp with
| T(tf) -> tf
| Eq(a1, a2) -> if (a a1 state) = (a a2 state) then true else false
| Neg(b1) -> not (b b1 state)
| ...

文の semantic function

式が State.t -> int や State.t -> bool のような関数になったのに対して、文は State.t -> State.t のような関数になる[1]。前者の State.t が実行前の状態で後者の State.t が実行後の状態というわけだ。文の構文木の型が stm だとして、文に対する semantic function の型はこうなる。

val s: stm -> (State.t -> State.t)

この s はどういう内容の関数か。これも OCaml 風に書きあらわすことにする。

まずstmが、

type stm = Assign of string * aexp | Skip | Seq of stm * stm | Cond of bexp * stm * stm | While of bexp * stm

という型だということにしてsは以下のように書き表せる。

(* auxiliary functions *)
let id x = x;;
let ($) f g x = f (g x);;
let cond b s1 s2 = fun state -> if (b state) then (s1 state) else (s2 state);;

let rec s stm = match stm with
| Assign(var, val) -> fun (state : State.t) -> update var (a val state) state
| Skip -> id
| Seq(stm1, stm2) -> (s stm2) $ (s stm1) 
| Cond(condition, stm1, stm2) -> cond (b condition) (stm stm1) (stm stm2)
| While(condition, stm1) ->
    let f g = cond (b condition) (g $ (s stm1)) id in
    fix f

場合分けの最初の4つは特に難しくないけど最後の While の部分はよくわからない。第一 fix っていう関数をどこでも定義していない。fix については OCaml で考えるのをやめて、「(State.t -> State.t) -> (State.t -> State.t) という型の関数 f を引数に与えられた時に f g = g になるような g を返す関数」と日本語で定義することにする。fix f の戻り値は State.t -> State.t だ。let f g = ... の g は State.t -> State.t で f g の戻り値も State.t -> State.t だ。

ということで fix の型はこうなる。

val fix: ((State.t -> State.t) -> (State.t -> State.t)) -> (State.t -> State.t)

繰り返し文を含むプログラムの例 (Example 5.1)

本当にこれでうまくいくのだろうか。ということで while ~(x=0) do skip というプログラムを考えて確かめる。構文木は While(<<~(x=0)>>, Skip) のような感じになる。（面倒くさいので Camlp4 風のクォーテーションを導入して <<~(x=0)>> で Neg(Eq(Var("x"),Val(0))) を意味することにします）

そうするとまずは While が出てくるが、f は

f g = cond (b <<~(x=0)>>) (g $ (s Skip)) id

となる。

s Skip は id で、g $ id は g と同じだから結局は

f g = cond (b <<~(x=0)>>) g id

と書き換えてよい。さらに cond の定義にしたがって、

f g = fun state -> if (b <<~(x=0)>> state) then (g state) else (id state)

その後 bexp の中身をいろいろすると結局は、

f g = fun state -> if not (lookup "x" state = 0) then (g state) else state

になる。

この f について「f g = g になるようなg」を考えないといけない。以下の g1 はそういう g である。

let rec undef () = undef ();; 
let g1 = fun state ->
  if not (lookup "x" state = 0)
  then undef ()
  else state

本当に f g1 = g1 になるかどうか確かめよう。g1 を f に渡して置き換えると、

fun state ->
  if not (lookup "x" state = 0)
  then
    (fun state -> if not (lookup "x" state = 0) then undef () else state)
    state
  else state

となるが、これをリファクタリングすると、まず外側の then の中身を簡単にして、

fun state ->
  if not (lookup "x" state = 0)
  then if not (lookup "x" state = 0) then undef () else state
  else state

さらにこの then に入るときは x≠0 なのだから結局は内側の if も簡単にできて、

fun state ->
  if not (lookup "x" state = 0)
  then undef ()
  else state

これは g1 と同じである。

ところで undef は無限ループする関数なのでこの関数の内容は「x がゼロでないとき無限ループ、ゼロであれば元と同じ状態」ということになる。これは while ~(x=0) do skip というプログラムの意味としてまことに適当である。

繰り返し文はこの定義では実はうまくいかない

こんな感じで行けばうまくいきそうな気がするのだけど実際には以下の2点の問題が存在するという。

問題1:「f g = g になるような g」は複数あるかもしれない。そうだとしたら fix 関数は関数のような顔をしながら実は関数ではないということになるし、プログラムの意味が多義的であってもいいということになる。

問題2:「f g = g になるような g」は1つもないかもしれない。もしそうだとしたらそのプログラムには denotational semantics では意味を与えられないことになってしまう。

問題1が問題だというのは我々がプログラミング言語の意味論を考えているからだ。自然言語であれば文の意味は実際に多義的であるかもしれないので、多義的な表現に多義的な意味を付与する意味論は（実際に観察される言語と一致していれば）むしろ好ましいかもしれない。でもプログラミング言語では普通そういうことはない。

問題2は問題1に比べると小さい問題だけど統語解析が終わって型検査も通ったプログラムはとにかく実行できるのだから、それに意味が付与できないことがあるような意味論はやはり頼りないということなのだろう。

というわけで最初に述べた denotational semantics の目標設定に戻ってくる。数学的な関数という意味での semantic function を定義するのがこの意味論の目標なのだ。fix が関数でなければ全体としての semantic function も関数にならない。

Exercise 5.2 をやろう

問題1のことを考えながら Exercise 5.2 の while ~(x=0) do x := x-1 というプログラムの意味を確かめてみる。構文木は While(<<~(x=0)>>, <<x := x-1>>) だ。（クォーテーションは式にも文にも使えることにしました）

そうすると f は、

f g = cond (b <<~(x=0)>>) (g $ (s <<x := x-1>>)) id

で、condの定義にしたがって、

f g = fun state ->
  if (b <<~(x=0)>> state)
  then (g $ (s <<x := x-1>>)) state
  else (id state)

関数合成のところをちょっとわかりやすくして、

f g = fun state ->
  if (b <<~(x=0)>> state)
  then g (s <<x := x-1>> state)
  else state

またいろいろして、

f g = fun state ->
  if not (lookup "x" state = 0)
  then g (update "x" ((lookup "x" state) - 1) state) 
  else state

となる。

さて、この f の「f g = gになるような g」は次の g1 から g5 のうちのどれか、というのが問いである。

let g1 = fun state -> undef ()

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

let g4 = fun state -> update "x" 0 state

let g5 = fun state -> state

元の while ~(x=0) do x := x-1 を頭の中で実行してみれば g2 が適切というのは自明だ。でも一応1つ1つ確かめてみよう。

g1

まず g1 を f に与える。

fun state ->
  let g1 = fun state -> undef () in
  if not (lookup "x" state = 0)
  then g1 (update "x" ((lookup "x" state) - 1) state) 
  else state

g1 は引数に何を取ろうと undef なので、

fun state ->
  if not (lookup "x" state = 0)
  then undef ()
  else state

となる。この関数は元の g1 と同じではない。よって g1 は違う。

g2

次に g2 を f に与える。

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

ここで内側の g2 に与えられる state は外側の state とは違って x をマイナス1したものであることに注意しないといけない。ちょっとこまかく場合分けしよう。

fun state ->
  let g2 = fun state ->
    if lookup "x" state >= 0
    then update "x" 0 state
    else undef ()
  in
  let state' = update "x" ((lookup "x" state)   1) state in
  match (lookup "x" state) with
  | x when x >= 1 -> g2 state'
  | x when x <= -1 -> g2 state'
  | x when x = 0 -> state

まず x>=1 のとき、state' の x は x>=0 である。だからこの場合は、

  | x when x >= 1 -> update "x" 0 state'

次に x<=-1 のとき、state' の x は x<=-2 である。だから、

  | x when x <= -1 -> undef ()

となる。state と state' が違うのは x の値だけであるということを考慮してもう1度書き直すと、

fun state ->
  match (lookup "x" state) with
  | x when x >= 1 -> update "x" 0 state
  | x when x <= -1 -> undef ()
  | x when x = 0 -> state

ここで3つ目のパターンは x が 0 なのだから update "x" 0 state と書き換えても同じである。したがって結局は1つ目と3つ目をまとめてしまって、

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

と書き直せる。これは元々の g2 と同じである。

g3

次はg3。

fun state ->
  let g3 = fun state ->
    if lookup "x" state >= 0
    then update "x" 0 state
    else state
  in
  if not (lookup "x" state = 0)
  then g3 (update "x" ((lookup "x" state) - 1) state) 
  else state

また場合分けして、

fun state ->
  let g3 = fun state ->
    if lookup "x" state >= 0
    then update "x" 0 state
    else state
  in
  let state' = update "x" ((lookup "x" state) 1) state in
  match (lookup "x" state) with
  | x when x >0 -> g3 state'
  | x when x = 0 -> state
  | x when x < 0 -> g3 state'

書き直して、

fun state ->
  let state' = update "x" ((lookup "x" state) 1) state in
  match (lookup "x" state) with
  | x when x >0 -> update "x" 0 state
  | x when x = 0 -> state
  | x when x < 0 -> state'

これは元の g3 と同じではない。

g4

次にg4。

fun state ->
  let g4 = fun state -> update "x" 0 state in
  if not (lookup "x" state = 0)
  then g4 (update "x" ((lookup "x" state) - 1) state) 
  else state

g4 には x をマイナス1した環境を与えているけど、結局 g4 の中で一律 0 にされるので、

fun state ->
  if not (lookup "x" state = 0)
  then update "x" 0 state
  else state

これはつまり x が 0 じゃないときは 0、0 のときはそのままということなので、

fun state -> update "x" 0 state

あれ？これは元の g4 と同じだ。

g5

最後に g5 はどうか。

fun state ->
  let g5 = fun state -> state in
  if not (lookup "x" state = 0)
  then g5 (update "x" ((lookup "x" state) - 1) state) 
  else state

g5 は何もしないので書き直して、

fun state ->
  if not (lookup "x" state = 0)
  then update "x" ((lookup "x" state) - 1) state
  else state

おしまい。これは元の g5 とは違う。

ここまでの話を振り返ると、我々の semantic function の定義にしたがうと while ~(x=0) do x := x-1 というプログラムに対しては少なくとも g2 と g4 の2つの関数がその意味として割り当てられてしまうということだ。つまり fix の定義の「f g が g になるような g」という定義では fix が関数になっていない。

というわけで denotational semantics が while ~(x=0) do x := x-1 に適切な意味を付与できるようにするためには fix の定義をもうちょっとうまく改修してあげなければならない。ここからすごく長い道のりが始まるのだ。

[1] 実は止まらないプログラムには「実行後の状態」なんて存在しないから、文に対応するのは部分関数というほうが正確だ。元の本では表記上も区別をしている。ここではしない。