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'