K-frameworkの紹介 #1 - Aizu AdC 2015 / 20日目
おはようございます.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で用いられている項書換えの形式的な定義などは解説出来る気がしない(ボ!w)ので,この記事では実際に簡単な言語を定義して使用例を示したいと思います.
実行可能というのは?
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 frameworkのGitHub上のorganization
- ここからC言語,Java,WebAssembly(マジ?!),LLVM,JavaScriptなどのKでの意味論の定義のリポジトリにアクセスできます.やばい.
- K-MetaML
- ぼくの進捗です(大声).MetaMLのような言語を実装してみました.stagingやコード生成などのメタプログラミングもKで定義できてしまいました.
試してみる
プログラミング言語 Hammon Lisp の定義
複雑な言語は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の定義ができたらコンパイラになるんちゃうか?とか考えたりしています.
形式的な定義については教えて下さいお願いします,なんでもしますから!
〜おわり〜