Tclのセマンティクスを定義してみる

自然意味論によってTclのセマンティクスを定義してみることにする．

Tclの構文

まず，抽象構文を以下のように定義する．

C ::= W W*
　　| C ; C
W ::= V | [ C ] | { C }
V ::= s | x | $x
s ∈ Str
x ∈ Var

sは文字列を表し，xは変数を表すメタ変数である．Tclが扱う対象はすべて文字列なので，本来なら変数も単なる文字列として扱った方がよいかもしれないが，混乱するので，ここでは区別して定義しておく．

評価関係

文献[B.Duba et.al,"Typing first-class continuations in ML", PoPL91.]を参考にして，ここでは
「環境E，継続計算KのもとでコマンドCを評価すると，文字列sが得られ，環境はE'となる」という評価関係を以下のように表す．

E;K |- C↓s,E'

環境E,継続計算Kは以下のように定義される．

E =
VE : Str→Loc
PE : Str→Proc
ST : Loc→Str

Proc ::= proc(x*, C)
K ::= stop | farg(W*,s*,K) | next(C,K) | retn(K)

環境Eは実際には値環境VE，手続き環境PE，記憶領域STの3つ組みである．

推論規則

E;K |- V↓s,E'

環境E,継続Kのもとで値Vを評価すると，文字列sと環境E'が得られる．

 E;s |- K↓s',E'
-----------------
 E;K |- s↓s',E

 E;"x" |- K↓s,E'
-----------------       変数xは文字列"x"とみなされる．
  E;K |- x↓s,E'

 E;E.ST(E.VE(x)) |- K↓s,E'
----------------------------
     E;K |- $x↓s,E'

E;K |- W↓s,E'

環境E,継続KのもとでワードWを評価すると，文字列sと環境E'が得られる．

  E;K |- "C"↓s,E'
--------------------
 E;K |- { C }↓s,E'

   E;K |- C↓s,E'
--------------------
 E;K |- [ C ]↓s,E'

E;K |- C↓s,E'

環境E,継続KのもとでコマンドCを評価すると，文字列sと環境E'が得られる．

 E;farg(W1...Wn,,K) |- W0↓s,E'
----------------------------------
    E;K |- W0 W1 ... Wn↓s,E'

 E;next(C2,K) |- C1↓s,E'
--------------------------
   E;K |- C1;C2↓s,E'

E;s |- K↓s',E'

環境E,値sのもとで継続Kを起動すると，文字列s'と環境E'が得られる．

E;s |- stop↓s,E

 E;farg(W*,s s*,K) |- W↓s',E'
---------------------------------
 E;s |- farg(W W*,s*,K)↓s',E'

    E;retn(K) |- s*↓s'
----------------------------
 E;s |- farg(,s*,K)↓s',E'

E;K |- s s*↓s',E'

環境E,継続Kのもとで，コマンドs s*を評価すると，文字列s'と環境E'が得られる．
規則はコマンドの種類によって異なるが，たとえばreturnコマンドの場合は以下のようになるだろう．

☆ returnコマンド

 E;stop |- "return" s↓s,E

      E.VE.pop;K |- s↓s',E'
-----------------------------------
 E;retn(K) |- "return" s↓s',E'

       E;K |- "return" s↓s'
-----------------------------------
 E;farg(W*,s*,K) |- "return" s↓s'

    E;K |- "return" s↓s'
-----------------------------
 E;next(C,K) |- "return" s↓s'

有向グラフを強連結成分に分解するアルゴリズム

CormenのIntroduction to Algorithmsには，グラフGと有向辺を逆にしたG_revに対してそれぞれDFSする方法が紹介されている．これは，わかりやすいアルゴリズムではあるのだけれど，逆グラフを求める必要があるのが玉にキズである．

一方，SedgewickのAlgorithms in C++には，逆グラフを求めないで1-passのDFSで求める手法が紹介されていた．こちらは連結成分を管理するためのスタックを別途使う必要があるが，逆グラフを求める必要がないのでうれしい．

そこで，OCamlで実装してみた．

module type DirectedGraphType =
  sig
    type t
    type node
    val all_nodes : t -> node list
    val adjacent_nodes : t -> node -> node list
  end

module type S =
  sig
    type t
    type node
    val decompose_scc : t -> node list list
  end

module Make(Graph: DirectedGraphType) =
  struct
    type t = Graph.t
    type node = Graph.node

    (*
     * decompose_scc: t -> node list list
     * 
     * -- decompose to strongly connected components(SCC)
     * -- from directed graph
     * 
     * ref. Algorithms in C++ by R. Sedgewick
     *)
    let decompose_scc g =
      let stack = Stack.create() in
      let all_nodes = Graph.all_nodes g in
      let node_num = List.length all_nodes in
      let values = Hashtbl.create node_num in
      let index = ref 0 in
      let results = ref  in
      let rec visit n =
        incr index;
        let min = ref !index in
          Hashtbl.add values n !index;
          Stack.push n stack;
          List.iter (
            fun t ->
              let m =
                if Hashtbl.mem values t then Hashtbl.find values t else visit t
              in
                if m < !min then min := m
          ) (Graph.adjacent_nodes g n);
          if !min == Hashtbl.find values n then
            (let rec loop ns =
              let m = Stack.pop stack in
                Hashtbl.replace values m (node_num + 1);
                if m != n then loop (m::ns) else (m::ns)
             in
               results := (loop )::!results);
          !min
      in
        List.iter
          (fun n -> if not (Hashtbl.mem values n) then ignore (visit n))
          all_nodes;
        !results
  end

基本的には参考書通りの実装だが，汎用的に使いたいのでファンクタとして定義している．

DSからCPSの関数を呼び出す方法

CPSからDS(Direct Style)の関数を呼び出すのは，以下のように何の問題もなくできる．

fun f_cps(k, x) =
  let t = g_ds(x) in
    ...
    (k t) // リターン

ではその逆はどうか？
DSの関数は，現在の継続を明示的にパラメータとして渡されていないので，呼び出したいCPS関数に渡してやる継続をどうにかしてひねり出す必要がある．
で，以下のように代入演算子を使えば，そのようなことができる．（と思う）

fun f_cps(k, x) =
  ... (k r)
fun g_ds(y) =
   ...
   let r = 0 in
     f_cps((fun (r') = r := r'), y)
     ...

以下のようにラッパ関数を作っておくと便利だ．

// CPS版の関数fをDS版に引き戻すラッパ関数
fun f_ds(x) =
  let r = 0 in
    f_cps((fun (r') = r := r'), x);
    r

ちょっとインチキっぽいけどcall/cc(letcc)を使っても実装できる．

fun f_ds(x) =
  letcc c in f_cps(c, x)

あるいは，return E to fnameのようにネストした関数内部から一気に戻れるようなreturn構文を導入して，

fun f_ds(x) =
  f_cps((fun (r) = return r to f_ds), x)

とかも良さそう．

トランポリンの代わりにgotoを使う

値としてのラベル

GCCはいろいろな独自拡張があるけど，その1つにラベルの指すアドレスを値として取得する機能がある．

void *address = &&label;
...
label:
...
goto *address;

のように&&演算子をラベル名の前に付けると，そのラベルのアドレスを取り出すことができ，通常の値と同様に変数に格納することもできるのだ．もちろんgotoを使って格納したアドレスへジャンプすることも可能である．

トランポリンの代わりにgotoを用いる

ここでいうトランポリンとは，以下に示すように次に実行すべき関数のアドレスを戻り値で返し，大元の実行ループでは返されたアドレス値を次々とコールしていくようなスタイルのことを指す．

void *f();
void *g();
int x;

void *f() {
  x++; return g;
}

void *g() {
  x--; return f;
}

int main() {
  void *(*r)() = f;
  for (;;) r = r();
  return 0;
}

残念ながらトランポリンスタイルは，無駄に関数のcall-returnを繰り返しているので効率が悪い．そこで，さきほどの値としてのラベルを使って無駄な関数callをなくす．

void *f;
void *g;
int x;

void f_module(int n) {
  f = &&l_f;
  if (n) return; // 無条件にreturnすると，以降の処理がデットコードとなり削除されてしまう
l_f:{ x++; goto *g; }
}

void g_module(int n) {
  g = &&l_g;
  if (n) return;
l_g:{ x--; goto *f; }
}

int main() {
  f_module(1);
  g_module(1);
  goto *f;
  return 0;
}

CPS変換まとめ

CPS変換の手法にもいろいろある．

前提として，λ式は以下のような構文で定義されているとする．
M, N ::= x | λx.M | M N

CPS(継続渡し形式)とは，計算が行われる順序を明示するために，ある式の計算結果を，残りの計算を表す継続（途中結果を受け取り，残りの計算を行う関数として表現できる）に次々と渡していくようなスタイルのλ式である．
上で定義したλ式では，計算はλ適用(M N)しかないので，CPSは適用の順序を明示的に示すようなλ式のスタイルということになる．

たとえば，(h ((g x) y))というλ式は，左から右へのcall-by-valueの評価戦略では，計算順序は以下のようになる．
(g x)を計算し，その結果t1とする．
(t1 y)を計算し，その結果をt2とする．
(h t2)を計算し，その結果を最終的な計算結果rとする．
以上の計算の流れをCPSで表すと，
((g x) λt1.((t1 y) λt2.((h t2) λr.r)
という感じになる．

PlotkinのCPS変換

まずは，PlotkinのCPS変換を以下に示す．

C[[x]]     = λk.k x                               - (a)
C[[λx.M]] = λk.k(λx.C[[M]])                     - (b)
C[[M N]]   = λk.C[[M]](λm.C[[N]](λn.(m n) k))   - (c)

上の変換で何をやっているかというと，あらゆるλ式を，「継続kをもらって，その式自身の評価結果をkに渡す」という形式に変換している．たとえば，xやλx.Mは値なのでこれ以上評価できないので，変換結果は単に受け取った継続kにそれ自身をそのまま渡す，という形式に変換される．((a)と(b))

問題は(c)のλ適用(M N)の変換である．
そもそも，(M N)の計算の順序は次のようになる．
(1) 部分式Mを評価し，その結果をmとする．
(2) 部分式Nを評価し，その結果をnとする．
(3) (m n)の評価結果を残りの継続に渡す．

(1)について考えると，部分式MのCPS変換結果C［［M］］は，継続を受け取ってMを評価し，その結果を継続に渡すような関数に変換されているので，次のような形で表せるだろう．
C［［M］］ (λm.(2)から先の計算)
同様に(2)について考えると，
C［［N］］(λn.(3)から先の計算)
となる．(3)は，それ以降の継続をkとすると
(m n) (λr.k r)
となる．以上をまとめると，
C［［M N］］ = λk.C［［M］］(λm.C［［N］］(λn.(m n) (λr.k r)))
となる．上記のλr.k rの部分はη簡約によりkとなるので，結局(c)のようになる．

問題点

残念なことに，Plotkin方式の変換では，出力されるλ式がえらく冗長になってしまう．たとえば，
λf.λx.λy.((f y) x)
は，
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λk.(k x) λn.((m n) k))))))
のような長いλ式に変換されてしまう．この式をよくみると，部分的に簡約可能な式があることに気がつく．
たとえば，以下のように簡約していける．
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λk.(k x) λn.((m n) k))))))
=>
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λn.((m n) k)　x)))))
=>...
λk.(k λf.λk.(k λx.λk.(k λy.λk.((f y) λm.((m x) k)))))

このように，変換後に改めてリダクションしてもいいけど，どうせなら一発でコンパクトな式へ変換したい．要するにone-passで簡約化されたCPS式を出力してくれるような変換があると，いろいろな意味でありがたい．次に説明するDanvyのCPS変換はそういった変換の一つである．

DanvyのCPS変換

C[[x]]     = Λк.кx
C[[λx.M]] = Λк.к(λx.λk.C[[M]](Λm.k m))
C[[M N]]   = Λк.C[[M]](Λm.C[[N]](Λn.(m n) (λa.кa))))

ここでは，CPS変換時に簡約化されるラムダ抽象を，通常のラムダ式と区別するために，大文字のΛで表記してある．

上で示したDanvyのCPS変換は，CPSのλ式を出力するのではなく，кを受け取るとCPSに変換されたλ式を出力する変換関数を出力する．кは何かというと，実はλ式を受け取ると，それを穴の空いたλ式に埋めたものを返すバックパッチ関数である．PlotkinとDanvyのCPS変換をともに関数とみたてて，その型を考えると，両者の違いがはっきりする．

C［［］］_plotkin : lambda -> lambda
C［［］］_danvy : lambda -> (lambda -> lambda) -> lambda

DanvyのCPS変換の導出

ここでは，PlotkinのCPS変換から出発して，Danvyの変換を導出していく．

戦略としては，CPS変換時に導入されるλ抽象（λkやλm,λn）のうち，常に簡約可能なものは変換時に簡約し，除去してしまえばよい．たとえば，...(λk.(k M) K)...のような部分は常に...(K M)...に簡約化できる．問題は，どうやったらそのような部分を特定するかである．

Plotkinの変換等式をよく見ると，変換結果は常にλk.Mの形をしていることがわかる．したがって，変換等式の右辺に現れるC［［...］］が，λ適用の左側に位置していれば（すなわち(C［［...］］X)のようになっていれば），変換時に簡約可能である．このことを念頭において，再びPlotkinの変換等式を見てみると，残念ながら以下の等式はそうなっていない．

C［［λx.M］］ = λk.k(λx.C［［M］］)　　　　　- (b)

そこで，この等式を，意味を保ったまま，C［［M］］の位置がλ適用の側にくるように変形する．以下のようにη変換すればよい．

C［［λx.M］］ = λk.k(λx.λk.C［［M］］k)　　　　　- (b')

この時点で，変換等式の右辺で導入されたλk，λm，λnをそれぞれΛк，Λm，Λnに置きかえてみると，以下のようになる．(λxはもともとのλ式に存在するので，Λxに置き換えずにそのままにしておく)

C[[x]]     = Λк.к x                              - (a')
C[[λx.M]] = Λк.к(λx.λk.C[[M]] k)              - (b'')
C[[M N]]   = Λк.C[[M]](Λm.C[[N]](Λn.(m n) к))  - (c')

改めて，上の変換等式をみてみると，すべてのC［［M］］の位置はめでたくΛ適用の左側に来るようになった．これで変換時にΛ簡約ができるようになったかというと，まだいくつか問題が残っていることに気がつく．

まず，C［［M］］の引数に注意すると，(c')ではΛ式が引数になっているが，(b'')では引数がkになっている．kはλ式における単なる変数なので，このままでは，変換時，кに適用する時に失敗してしまう．そこで，再びη変換を使って，(b'')を以下のように変形してやる．

C「「λx.M］］ = Λк.к(λx.λk.C［［M］］(Λm.k m)) - (b''')

残る問題はкの出現位置だ．(a')と(b''')では，кは（変換時の）Λ適用の左に位置しているが，(c')は（変換後のλ式における）λ適用の右の位置に来ている．そこで，(c')を変形してΛ適用の左側にくるようにしよう．例によってη変換すればよい．

C［［M N］］ = Λк.C［［M］］(Λm.C［［N］］(Λn.(m n) (λa.кa))) - (c'')

以上，DanvyのCPS変換を導出することができた．

η-redex(末尾呼び出し)の除去

先ほど示したDanvyのCPS変換では，変換後にη-redexが残ってしまうことがある．たとえば，以下の例．
C［［λf.(f a)］］（Λm.m）=λf.λk.(f x)(λa.k a)

このように余計なη-redexが残ってしまうのは，λx.(M N)のような形のλ式を変換した場合である．したがって，以下のような変換規則を追加し，あらかじめη簡約しておけばよい．

C[[λx.(M N)]] = Λк.к(λx.λk.C[[M]](Λm.C[[N]](Λn.(m n) k)))

Sabry&WadlerのCPS変換

DanvyのCPS変換関数は，one-passではあったが，その型（lambda->(lambda->lambda)->lambda）を見ればわかるように高階（higher-order）関数であった．1階(first-order)の関数として，すなわち関数自身を引数に取ったり，関数を値として返したりせずに，同様の変換を実現できないだろうか？

以下に示すSabry&Wadlerの変換はそのような要求を満たす変換方式である．

// V, Wはxかλx.Mの形をしたλ式
C[[V]]K = K T[[V]]
C[[V W]]K = (T[[V]] T[[W]]) K
C[[V N]]K = C[[N]](λn.C[[V n]]K)
C[[M N]]K = C[[M]](λm.C[[m N]]K)
// 補助関数T[[]]を定義
T[[x]] = x
T[[λx.M]] = λx.λk.C[[M]]k

C［［］］_sabry : lambda * lambda -> lambdaであり，確かに1階の関数になっている．

SabryのCPS変換の導出

ここでも，PlotkinのCPS変換から出発して，Sabryの変換を導出していくことにする．基本的な方針は，Danvyでやったのと同じで，β-redexが導入されないような変換を検討していく．このとき，高階関数が入り込まないように注意する．

まずは，以下の変換規則を出発点にする．

C[[x]]     = λk.k x                               - (a)
C[[λx.M]] = λk.k(λx.λk.C[[M]] k)               - (b')
C[[M N]]   = λk.C[[M]](λm.C[[N]](λn.(m n) k))   - (c)

C［［...］］は常にλk.Mの形に変換され，かつ，変換規則の右辺に現れるC［［］］は常にλ適用の左に位置するので，このλkは変換時にβ簡約できる．ΛKを用いて以下のように変形できる．

C[[x]]      = ΛK.K x 
C[[λx.M]]  = ΛK.K (λx.λk.C[[M]] k)
C[[M N]]    = ΛK.C[[M]](λm.C[[N]](λn.(m n) K))

このまま進めていってもよいのだが，C［［］］］をアンカリー化してやると，以下のように書きなおせる．

C[[x]]K      = K x 
C[[λx.M]]K  = K (λx.λk.C[[M]] k)
C[[M N]]K    = C[[M]](λm.C[[N]](λn.(m n) K))

上記の変換規則には，まだ余計なβ-redexが導入される可能性が残っている．λmとλnの部分である．たとえば，C［［x N］］k = (λm.C［［N］］(λn.(m n) k)) xとなるが，これは，C［［N］］(λn.(x n) k)にβ簡約できる．要するに，(M N)の形によって変換規則を場合分けしてやれば，このようなβ-redexを取り除くことができる．
まず，場合分けがややこしくならないように，以下のように補助変換規則T［［］］を導入して，変換規則を書きかえる．

C[[V]]K      = K T[[V]] // Vはxからλx.Mの形
C[[M N]]K    = C[[M]](λm.C[[N]](λn.(m n) K))

T[[x]]      = x 
T[[λx.M]]  = λx.λk.C[[M]] k

まず，C［［V W］］の場合を考える．変換規則にしたがって変形していくと，
C［［V W］］K
　= C［［V］］
= (λm.C［［W］］(λn.(m n) K)) T［［V］］
= (λm.(λn.(m n) K) T［［W］］) T［［V］］
となる．これは，β簡約できるので，結局，

C[[V W]]K = (T[[V]] T[[W]]) K　-- (*)

という規則になる．次に，C［［V N］］の場合である．
C［［V N］］K
　= C［［V］］
= (λm.C［［N］］(λn.(m n) K)) T［［V］］
→C［［N］］(λn.(T［［V］］n) K)
となるので，結局，

C[[V N]]K = C[[N]](λn.(T[[V]] n) K)  -- (**)

という規則が得られる．さらに，上記の規則において，nは単なる変数（値）なので，さきほどの変換規則(*)を左向きに適用することで，以下が得られる．

C[[V N]]K = C[[N]](λn.C[[V n]] K)

最後に，C［［M N］］K=C［［M］］(λm.C［［N］］(λn.(m n) K))という最も一般的なケースであるが，これも，変換規則(**)を左向きに適用することで以下が得られることに気がつく．
C［［M］］(λm.C［［m N］］K)
したがって，最終的には以下の変換規則が得られる．

C[[M N]]K = C[[M]](λm.C[[m N]] K)

以上，SabryのCPS変換も導出することができた．

参考文献

• "Representing Control: A Study of the CPS Transformation (1992)", Oliver Danvy, Andrzej Filinski
• "A Reflection on Call-by-Value (1996)", Amr Sabry, Philip Wadler
• "A first-order one-pass CPS transformation (2003)", Olivier Danvy, Lasse R. Nielsen
• "Essentials of Programming Languages -- 2nd ed. (2001)", Daniel P. Friedman, Mitchell Wand, Christopher T. Haynes

Committed-Choice型の言語

KL1とかGHC、FlengはCommitted-Choice型の言語と呼ばれている。
並行論理型言語の一種なのだが、どうして、Committed-Choiceと呼ばれるのかが
やっとわかった。

  そこで KL1 では, どの公理を選ぶかを決めたら決して後戻りしない方針をとった. 

  そのかわり, どの公理を選ぶかの条件となる部分を「ガード」として分離し, その

  条件を正確に判断できる情報が集まるまでは選択を待つことによって, 誤った選択

  をしないようにしたわけである. このような方針をとる論理型プログラム言語は, 

  自らの選択に賭けるというニュアンスから committed choice 型の並列論理型言語

  などと呼ばれることもある. 

つまり、Prologのようにバックトラックしないで、ガードによって、選択(Choice)を
決めて突き進む（Commit）するから、Committed-Choiceなのね。