おはようございます．Aizu Advent Calandar 20日目の @yutopp です．
前の人は @GUCC1_sp1ritu4l，次の人は @ishi_kuro です．
今回はK-frameworkというプログラミング言語の意味付けをサポートするフレームワークの紹介をしたいと思います．
日本語の資料がほとんど無い(英語もない)ので，どんどん使っていきましょう！！
間違えなど含んでいると思われます．ご指摘いただけると嬉しいです．
K-framework is 何
概要やチュートリアル，論文などは K-framework にて公開されています．
また，実装はGitHubの kframework/k 上で行われているようです．
何が出来るかというと，K-framework上で configuration と computation, rule を用いて，実行可能なプログラミング言語や型システム，解析ツールを定義できます．
加えて読みやすいドキュメントの自動生成もしてくれます．便利ですね．
C言語やJava，Scheme，LLVMなどの意味論が既にK上で与えられており，実用的なように見えます．
Kで用いられている項書換えの形式的な定義などは解説出来る気がしない(ボ！ｗ)ので，この記事では実際に簡単な言語を定義して使用例を示したいと思います．
実行可能というのは？
K-tools というものがあり，これを用いることでKで定義した意味論を実際に動かすことができます．
今回のサンプルを動かす場合は，GitHubの kframework/k から Version 3.6 のビルド済みパッケージ落としてくるか，私が作ったDocker imageを使うと楽に試せると思います．
ちなみにmasterはK-framework 4.0のSNAPSHOTになっており，挙動が不安定なため使用を見送りました．
言語はどう定義するのか？？
冒頭で述べたように，意味論に関しては configuration，computation, rule をK-framework上の記法に従って定義します．
加えて，syntax として言語の構文も定義し，それらを組み合わせて言語の定義とします．
動く仕組みと部品の説明
形式的ではないざっくりした説明ですが，
まず，K-frameworkは定義したsyntaxに従って文字列の入力をパースして構造に変換します．
次に，定義したruleに従ってconfigurationのマッチした構造を書き換えていき，それの繰り返しで入力の実行を行います．
configuration
configurationはcellと呼ばれる値の集まりです．
ざっくり説明すると，プログラムのコードやシンボルテーブル，データのストレージなどを保持しておくような所です．
computation
computationは計算の順序です．
という記号で区切られたデータ列で，左から右へと評価されます．
Kでは構文などの構造をcomputationに落として計算の順序のようなものを作ります．
rule
Kで定義したruleはK rulesと呼ばれ，これは項書換え規則に変換された後，それに従ってconfigurationが書き換えられていきます．
rulesは構造をcomputationに書き換えるstructural ruleと，実際に計算を進めるcomputational ruleに区別されます．
その他
Sort
型みたいなやつ．
Attributes
syntaxの項で指定できるもの．結合規則や評価順序などの指示を与えられます．
KResult
計算の最終状態のSortを指定します．
Run K Online - kweb というものがあり，実際のK-framework上で用いる記法や，意味論の定義の仕方などをステップごとに試すことが出来ます．
面白いな，と思ったものは
- SIMPLE言語 (場所:
tutorial/2_languages/1_simple)
- 並列計算もできる手続き言語のSIMPLE(震え声)言語．Static semantics(Typedと書かれた型付け規則)と，Dynamic semantics(実行時)の両方の定義があるので，静的型付けの言語の意味付けの参考になります．
- 型システムチュートリアル (場所:
tutorial/1_k/5_types)
- Brainf*ck (場所:
samples/bf/bf.k)
- Bfの意味論が定義されていた… 単純なので読みやすいです．
実際に作成された定義など
試してみる
複雑な言語はK-MetaMLで力尽きたので，ここではステップバイステップで簡単なLisp風言語を定義してみます！
この章を読んだ後に公式チュートリアルを読むとスラスラ理解できるようになっていれば嬉しいです．
K-frameworkにハマりすぎて研究室を破門されないように頑張っていきましょう！
全体のソースコードのリポジトリはここになります．動作確認はK-framework revision(a7673ca)で行いました．多分ver 3.6でも動くと思います．
全体の定義は上のリポジトリを見て頂いて，ここでは重要な点の説明をしていきます．
Step 1. 構文の定義
まず，構文の定義からいきます．ファイル名hammon-lisp.kの中に，HAMMON-LISP-SYNTAXというmoduleを作って，構文を定義していきます．
module HAMMON-LISP-SYNTAX
syntax Expr ::= SId | Int | "nil" | "t"
| "(" SList ")"
syntax SList ::= List{Expr, ""}
syntax SOp ::= "+" | "-" | "*"
| "="
syntax SId ::= Id | SOp
| "defun"
| "progn"
| "lambda"
| "if"
| "print"
endmodule
アトムとS式の構文の定義です．
syntaxキーワードを使って，構文を定義します．まんまBNFですね．多少拡張されており，attributeを加えたり，優先順位を変更できます．
Step 2. Configuration の定義と下準備
HAMMON-LISPというmoduleを作って，その中に本体の定義を書いていきます．
module HAMMON-LISP
imports HAMMON-LISP-SYNTAX
syntax KItem ::= "%t" | "%nil"
syntax KResult ::= Int | SId | "%t" | "%nil"
syntax KItem ::= "%toplevel"
configuration <k> %toplevel $PGM:SList </k>
<venv> .Map </venv>
<fenv> .Map </fenv>
<store> .Map </store>
<nextLoc> 0 </nextLoc>
<results> .List </results>
<out stream="stdout"> .List </out>
// rewrite parentheses to << >>
// it is needed to avoid confusion of K parsers...
syntax Expr ::= "<<" SList ">>"
rule ( E:SList ):Expr => << E >> [macro]
endmodule
まずimportsを用いて構文の定義を読み込みます．
KItem というのはKの構造の項みたいなもので，ここに加えた構文はどこでも使えるようになります．
KResult は計算の最終状態の形です．
configuration は configuration キーワードを用いてXMLで定義します．今回の定義のCell内訳は，
<k> : プログラム本体．$PGMの部分にパースされた構造が入ります．<venv> : 変数とLocationの対応を保存します．.Mapというのは空のマップ構造を指します．<fenv> : 関数とLocationの対応を保存します．<store> : Locationとデータの対応を保存します．<nextLoc> : LocationのFreshIdを保存します．<results> : おまけ．トップレベルのS式を評価したときの結果を保存します．デバッグ用．<out> : 標準出力です．
となります．変数と関数の名前空間は分割しました．
最後に，S式のカッコを<< >>に変換するマクロを定義しています．式の結合を変えるカッコとS式のカッコで，K-frameworkのパーサが混乱するようなので…
Step 3. Rules の定義
残るは書き換え規則をガンガン入れていくだけです！
Step 3.1 変数のルックアップ
// Variables
rule <k> X:Id => Val ... </k>
<venv> ... X |-> Loc ... </venv>
<store> ... Loc |-> Val </store>
このルールは以下のように読むと意味を汲みやすいです．
<k>の先頭にあるIdというSortを持った項をXと置いて，<venv>にXに対応するLocが存在して，<store>にLocに対応するValが存在したときに，Xと置いた項をValに書き換える
また，=> は左辺を右辺に書き換えることを示します．
... は0個以上の何かしらの値がある，ということを示します．
Step 3.2 値
// special value
rule <k> nil => %nil ... </k>
rule <k> << .SList >> => %nil ... </k>
rule <k> t => %t ... </k>
nilリテラルや空リスト，真偽値の変換を定義します．
Step 3.3 defun
// defun
syntax KItem ::= func(SId, SList, SList, Map, Map, Int)
syntax KItem ::= midDefunCheckParam(SList)
rule <k> << defun:SId Sym:SId << Params:SList >>:Expr Exprs:SList >> => midDefunCheckParam(Params) ~> Sym ... </k>
<venv> VEnv </venv>
<fenv> FEnv => FEnv[Sym <- N +Int 1] </fenv>
<store> Sto => Sto[ N +Int 1 <- func(Sym, Params, Exprs, VEnv, FEnv, N +Int 1)] </store>
<nextLoc> N => N +Int 1 </nextLoc>
rule midDefunCheckParam(P:Id Ps:SList) => midDefunCheckParam(Ps) [structural]
rule midDefunCheckParam(.SList) => .K [structural]
まず，funcという構造を定義しておきます．先頭から，関数名，パラメータ，関数本体，定義時の変数環境，定義時の関数環境，この関数のLocationを保持します．
このruleはdefun という構造が<k>の先頭にあったとき，それをmidDefunCheckParam(Params) ~> Sym という computation に書き換えます．
で区切られるcomputationは，K-frameworkの記法では~> で区切られます．これで，midDefunCheckParam(Params) が評価されてから Symが評価されることになります．
加えて，<fenv>と<store>，nextLocの値も書き換えます．
<fenv>を例に説明すると，まず現時点の<fenv>の内容をFEnvと置き，それにSymというキー を N +Int 1 という値に関連つけたものに書き換えます．
midDefunCheckParam は再帰的に，パラメータが全てIdというSortになっているかを確かめています．(パラメータに数字などを置かれると困りますからね…)
パラメータの名前の重複判定は省いてしまったので，気になる場合は追加してみてください．
Step 3.4 if
// if
syntax KItem ::= midCond(Expr, Expr)
rule <k> << if:SId Cond:Expr Then:Expr Else:Expr >> => Cond ~> midCond(Then, Else) ... </k>
[structural]
rule <k> CV:KResult ~> midCond(Then, Else) => Then ... </k>
when CV =/=K %nil
[structural]
rule <k> %nil ~> midCond(_, Else) => Else ... </k>
[structural]
みんな大好きifです．ここでは，まずifの条件式を最初にcomputationに乗せて評価させ，Then節かElse節は構造のまま保っておきます．
そして，条件式の結果によってThen節かElse節の構造をcomputationに乗せて評価させます．
これによって，Then節かElse節の片方のみが評価されます．
ruleにはwhen節を付けることができて，ここで細かいruleの切り替えを行えます．
Step 3.5 呼び出し
大物になってしまいました…
// ===
// call
// ===
syntax KItem ::= midFApply(SList) | midBeginApply(K, SList)
rule <k> << E:Expr Args:SList >> => E ~> midFApply(Args) ... </k>
when notBool isSpecialFormOrBuiltin(E)
[structural]
rule <k> Sym:Id ~> midFApply(Args) => midBeginApply(Func, Args) ... </k>
<fenv> ... Sym |-> Loc ... </fenv>
<store> ... Loc |-> Func ... </store>
[structural]
// (ref 1)
syntax KItem ::= midConv(SList, SList, Map, Map) | midEndApply(Map, Map)
rule <k> midBeginApply(func(Sym, Params, Body, FVEnv, FFEnv, N), Args) =>
midConv(Params, Args, FVEnv, FFEnv[Sym <- N])
~> << progn Body >>
~> midEndApply(VEnv, FEnv) ...
</k>
<venv> VEnv </venv>
<fenv> FEnv </fenv>
[structural]
// (ref 3)
rule <k> V:KResult ~> midEndApply(VEnv, FEnv) => V ... </k>
<venv> _ => VEnv </venv>
<fenv> _ => FEnv </fenv>
[structural]
// (ref 2.1)
syntax KItem ::= midBind(Id)
rule <k> midConv(P:Id Ps:SList, A:Expr As:SList, VEnv, FEnv) => A ~> midBind(P) ~> midConv(Ps, As, VEnv, FEnv) ... </k>
[structural]
rule <k> Val:Expr ~> midBind(P) ~> midConv(Ps, As, VEnv, FEnv) => midConv(Ps, As, VEnv[P <- N +Int 1], FEnv) ... </k>
<store> Sto => Sto[N +Int 1 <- Val] </store>
<nextLoc> N => N +Int 1 </nextLoc>
[structural]
// (ref 2.2)
rule <k> midConv(.SList, .SList, VEnv, FEnv) => .K ... </k>
<venv> _ => VEnv </venv>
<fenv> _ => FEnv </fenv>
[structural]
最初の3つのルールは今までの説明で読み取れると思います．今度は<venv>ではなく<fenv>から値を取ってきています．
面倒なのが残りのルールで，これは変数環境と関数環境をstatic scopeかつ再帰呼出し可能に設定しているところです(より効率よくできるかもしれません…)．
ざっくり説明すると，現在の変数/関数環境を保存した後(ref 1)に，呼び出す関数のパラメータと引数の対応を作りつつ(ref 2.1)新しい変数/関数環境に切り替えて(ref 2.2)関数本体をprognで包んで評価を行い(ref 1のcomputation)，評価が終わったら呼び出す前の変数/関数環境に戻す(ref 3)，という事をしています．
このあたりはK-frameworkのテクニックというよりは，この本の内容に近いです．
サンプルコード
これでコア部分の説明は終わりました．では，実際にどんなコードをHammon Lispで書けるのかというと，
(defun zoi (x y) 10)
(zoi 10 20)
(+ 10 20)
((lambda (x y) (+ x y)) 20 30)
(defun zero () 0)
(zero)
(if () 114 514)
(if nil 114 514)
(if (+ 10) 114 514)
(- 10 2)
(- 10 2 3)
(= 10 20)
(= 10 10)
(defun f1 (x)
(print (= x 0))
(if (= x 0) 100 200))
(f1 0)
(f1 1)
(defun fact (x)
(if (= x 0) 1 (* x (fact (- x 1)))))
(print (fact 4))
このくらいなら実行することができます．
コレを実行すると，最終状態のconfigurationの<results>Cellから
<results>
ListItem ( zoi )
ListItem ( 10 )
ListItem ( 30 )
ListItem ( 50 )
ListItem ( zero )
ListItem ( 0 )
ListItem ( 514 )
ListItem ( 514 )
ListItem ( 114 )
ListItem ( 8 )
ListItem ( 5 )
ListItem ( %nil )
ListItem ( %t )
ListItem ( f1 )
ListItem ( %t )
ListItem ( 100 )
ListItem ( %nil )
ListItem ( 200 )
ListItem ( fact )
ListItem ( 24 )
</results>
という結果が得られます．特に最後のfactではしっかり24という値が得られていますね！
まとめ
高級な言語の意味論を定義でき，形式的な検証を行うことの出来るK-frameworkくんの紹介でした．
LLVM-IRくんの意味も定義されていることだし，Translatorの定義ができたらコンパイラになるんちゃうか？とか考えたりしています．
形式的な定義については教えて下さいお願いします，なんでもしますから！
〜おわり〜
