順序付き線形型に基づく 木構造処理プログラムから ストリーム処理プログラムへの変換

Presentation on theme: "順序付き線形型に基づく 木構造処理プログラムから ストリーム処理プログラムへの変換"— Presentation transcript:

1 順序付き線形型に基づく 木構造処理プログラムから ストリーム処理プログラムへの変換
末永 幸平 (東京大学) 児玉 紘一 (東京工業大学) 小林 直樹 (東京工業大学)

2 XML 処理の二つの手法 木構造処理 ストリーム処理 メモリ上に木を作って処理 例: DOM API, XDuce, CDuce
ストリームからデータを読みつつ処理 例: SAX

3 木構造処理 node leaf 2 3 node leaf 3 4 ここを記述 メモリ 二次記憶, ネットワーク <node> <leaf>2</leaf> <leaf>3</leaf> </node> <node> <leaf>3</leaf> <leaf>4</leaf> </node>

4 ストリーム処理 メモリ 二次記憶, ネットワーク ここを記述 <node> <leaf>2</leaf> <leaf>3</leaf> </node> <node> <leaf>3</leaf> <leaf>4</leaf> </node>

5 木構造処理とストリーム処理の比較 木構造処理 ストリーム処理 記述性 ○ × メモリ効率 良い点だけを取りたい

6 研究の目標 node leaf 2 3 node leaf 3 4 ここを記述 メモリ 二次記憶, ネットワーク <node> <leaf>2</leaf> <leaf>3</leaf> </node> <node> <leaf>3</leaf> <leaf>4</leaf> </node>

7 記述性を保ちつつ メモリ効率を向上させることが可能
研究の目標 node leaf 2 3 node leaf 3 4 記述性を保ちつつ メモリ効率を向上させることが可能 メモリ 二次記憶, ネットワーク <node> <leaf>2</leaf> <leaf>3</leaf> </node> ここに変換 <node> <leaf>3</leaf> <leaf>4</leaf> </node>

8 例) 要素全てに1を足した木を作る関数 木構造処理 ストリーム処理
fix f. λt. case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2) ストリーム処理 fix f. λt. case read() of leaf → write(leaf); write(read() + 1) | node → write(node); f (); f () 簡単な変換で済ませたい 例として、要素すべてに１を足した新しい木を作る関数をこの２つの言語を使って示します。 木構造処理を扱うソースプログラムでは入力木tに対してパターンマッチを行い、新しい木を作ります。 ストリーム処理を行うターゲットプログラムではread命令を用いてストリームから値をひとつ読み取り、 それにしたがってパターンマッチを行っています。 言語の詳しい説明は後で述べます。

9 変換できないプログラムの存在 例: 二分木の各ノードの左右を入れ替えるプログラム node leaf 2 3 1 node leaf 3 2

10 正しく変換するためには... プログラムが正しい順序で部分木にアクセスしなければならない 解決策: 順序付き線形型を使って制限
正しい順序: 左から右, 深さ優先順 解決策: 順序付き線形型を使って制限 型付け可能なプログラムは, 部分木に正しい順序でアクセスしていることを保証

11 今回の範囲 木構造処理とストリーム処理のための 関数型言語を定義 順序付き線形型を用いた型システムを定義
対象データを二分木に限定する ストリーム処理言語ではメモリ上に木を作らせない メモリ上に木を構築する拡張を後で行う 順序付き線形型を用いた型システムを定義 前者から後者への変換アルゴリズムを定義 アルゴリズムの正しさを証明

12 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

13 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

14 ソース言語とターゲット言語 ソース言語: 木構造処理 ターゲット言語: ストリーム処理 入力データを木として処理
λ計算 + 二分木操作プリミティブ ターゲット言語: ストリーム処理 入力ストリームからデータを読みつつ処理 λ計算 + ストリーム操作プリミティブ

15 ソース言語の syntax M (項) ::= i (整数) | x | λx.M | M1 M2 | M1 + M2 | fix f. M | leaf M | node M1 M | (case M of leaf x → M | node x1 x2 → M2)

16 プログラム例 各整数に 1 を加えた木を返す関数 fix f. λt case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2)

17 node (leaf 1) (leaf 2) は node; leaf; 1; leaf; 2 という
ターゲット言語の syntax e (項) ::= i | x | λx.e | () | e1　e2 | e1 + e2 | fix f. e | leaf | node | read e | write e | (case e of leaf → e | node → e2) node (leaf 1) (leaf 2) は node; leaf; 1; leaf; 2 という ストリームで表現 (閉じタグは考えない)

18 プログラム例 各整数に 1 を加えた木を出力する関数 fix f. λx (case read () of leaf → write leaf; write (read() + 1) | node → write node; f (); f ())

19 プログラム例 (比較) ソースプログラム ターゲットプログラム fix f.λt.(case t of
leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2)) ターゲットプログラム fix f.λt.(case read() of leaf → write(leaf);write(read()+1) | node → write(node);f ();f ()) それぞれ比較してみますと次のようになります。 大きな違いは入力木tの部分がread命令になっていること、 木の出力の部分がターゲット言語ではwriteを用いた逐次実行になっていることです。 このように２つのプログラムは似ているため、変換が行えそうであるということがわかると思います。

20 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

21 型システム 順序付き線形型を用いた ソース言語のための型システム 型付け可能なプログラムに対して以下を保証
各ノードを左から右, 深さ優先順に 丁度 1 度ずつアクセス 出力木をメモリに貯めない

22 入力木型 (Tree-) と 出力木型 (Tree+) を区別
型の syntax τ (型) ::= Int | τ1 → τ2 | Treed d (モード) ::= - (入力) | + (出力) 入力木型 (Tree-) と 出力木型 (Tree+) を区別 型は次のようになります。 整数の型Int、木の型Tree、およびτ１からτ２への関数です。 また、木の型には入力木型Tree-と出力木型Tree+が存在します。

23 二種類の型環境 (順序なし) 型環境 Γ 順序付き線形型環境 Δ
{ x1:τ1, x2:τ2, ..., xn:τn } (τi ≠ Treed) 変数の束縛の集合 順序が強制されない変数の型情報を保持 順序付き線形型環境 Δ x1:Tree-, x2:Tree-, ..., xn:Tree- 変数の束縛の列 「入力木が順番に一度ずつアクセスされる」 ことを表現

24 型判定 Γ | Δ ├ M : τ M 中の自由変数が型環境 Γ, Δ に従った型の値に 束縛されるとき, M の評価結果は型τの値となり,
評価中に Δ の順で入力木がアクセスされる

25 型判定の例 Γ = f : Tree- → Tree+ のとき Γ | x1 : Tree-, x2 : Tree- ├
node (f x1) (f x2) : Tree+ Γ | x1 : Tree-, x2 : Tree- ├ node (f x2) (f x1) : Tree+ 順序付き線形型環境についてです。 これがたとえばx1,x2,…,xnの順で構成されていたとき、x1からxnの順で丁度一回づつアクセスしなければならない、ということを意味します。 たとえばΓにfが入力木を受けとり出力木を返す関数という情報が入っていたとき 上の式は型付けできますが下の式は型付けできません。 なぜなら上の式は順序付線形型環境と同じ順でfx1,fx2の評価が行われていますが 下の式はfx2,fx1と、順序が違っているからです。 このように、下の式は木へのアクセス順序が正しくない、と判断され型付けできない、変換できない、ということになります。

26 型判定規則 (1/3) Γ|x:Tree ├ x:Tree Γ,x:τ | Ø ├ x:τ 順序付き型環境には余計なものは含まれない
(T-VAR1) Γ|x:Tree ├ x:Tree - - (T-VAR2) Γ,x:τ | Ø ├ x:τ 型判定規則をみてみます。 変数に関する判定規則は入力木型に関する規則T-VAR1と木以外に関するT-VAR2の２つです。 両者とも順序付き型環境に余計な物が含まれず、丁度一回読み込まれる、ということを保証します。 　　順序付き型環境には余計なものは含まれない = 入力木が丁度一回読み込まれる

27 型判定規則 (2/3) Γ|x:Tree ├M :τ Γ|Ø├ λx.M :Tree →τ Γ,x:τ1|Ø├M :τ2
- (T-ABS1) Γ|Ø├ λx.M :Tree →τ - Γ,x:τ1|Ø├M :τ2 (T-ABS2) Γ|Ø├ λx.M :τ1→τ2 λ抽象の型付け規則も同様に入力木の場合と木以外の場合の２つが存在します。 ここでも順序付き線形型環境には余計なものは含まれません。 適用は順序付き線形型環境をもちいます。 左からM1、M2の順序で評価されるため、順序付き線形型環境Δもその順で使われる必要がある。

28 型判定規則 (3/3) Γ|Δ1├M1 :Tree Γ|Δ2├M2 :Tree Γ|Δ1,Δ2├ node M1 M2 :Tree
+ + (T-NODE) Γ|Δ1,Δ2├ node M1 M2 :Tree + - Γ|Δ1├M :Tree Γ,x:Int|Δ2├M1 :τ Γ|x1:Tree ,x2:Tree ,Δ2├M2 :τ - - (T-CASE) Γ|Δ1,Δ2├ case M of leaf x → M1 |node x1 x2 → M2 :τ 次にリーフ、ノード、ケースに関する規則を見て見ます。 リーフは要素が整数であるとき型付け可能、 ノードは左の木から順序付き線形型環境が使われることが必要です。 またケースはまずMから評価を行うため、入力木Mに前半部分のΔ1が使われ、 M1、M2の評価にはΔ2が使われることになります。 リーフの場合は要素が整数であること、 ノードの場合はx1,x2が入力木であり、この順に用いることが順序付き型環境の中に入ります。

29 型付け例 Γ|Ø├ f : Tree- →Tree+ Γ|x1:Tree-├ x1 : Tree+
Γ|x1:Tree-├ f x1 : Tree+ 　 Γ|x2:Tree-├ f x2 : Tree+ Γ|t:Tree-├ t :Tree- Γx:Int|Ø├ leaf (x+1) :Tree+ Γ|x1:Tree-,x2:Tree-├ node (f x1) (f x2) :Tree+ Γ|t:Tree-├case t of leaf x => leaf (x + 1) | node x1 x2 => node (f x1) (f x2) :Tree+ Γ|Ø├λt.(case t of leaf x => leaf (x + 1) | node x1 x2 => node (f x1) (f x2)) :Tree- → Tree+ これらの型判定規則を用いて先ほどの例を型付けを行います。 下から説明では省きましたがfixの規則、アブストラクションの規則を行い、 ケースの規則を行います。 これをみますと、まずtの型付けに、Δの前半部分が使われます。 ここでは前半部分をt:Tree-、後半部分を空にしています。 またノードでは新しくx1,x2の情報がこの順で順序つき線形型環境に入っています。 この上をみると、fx1,fx2の評価にそれぞれこの環境の前半部分、後半部分が使われています。 このように全体を通してうまく型付けできていることがわかります。 Ø|Ø├ fix f.λt.(case t of leaf x => leaf (x + 1) | node x1 x2 => node (f x1) (f x2)) :Tree- → Tree+ (ただしΓ= f:Tree- → Tree+とする)

30 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

31 変換アルゴリズム A(x) = x A(i) = i A(λx.M) = λx.A(M) A(M1M2) = A(M1)A(M2)
A(fix f.M) = fix f.A(M) A(leaf M) = write(leaf);write(A(M)) A(node M1 M2) -> write(node);A(M1);A(M2) A(case M of leaf x => M1| node x1 x2 => M2) = (case A(M);read() of leaf => let x=read() in A(M1) | node => [()/x1,()/x2]A(M2)) 変換アルゴリズムＡの定義は次のようになります。 上の黒の部分は構造に従って分解しているだけです。 赤い部分ですが leafではまずwriteを用いてタグを書き出し、残りを変換したものの書き出しを行うことになります。 nodeでは同じようにまずタグの書き出しを行い、M1,M2の順で変換したものを逐次実行するものに変わります。 caseですが、入力木Mを受け取る部分がMの変換とread命令の逐次実行に殻っています。 またM1の中には要素の整数となるxが含まれるため、これをread命令に変えて入力ストリームから整数を読み取ります。 ノードの場合はM2に含まれる入力木x1,x2をユニットに変えています。 これは残りの木は後でcaseを用いて読み込むためです。 残りの木は後で読み込むためx1,x2はユニットになる

32 変換例 A(fix f.λt.(case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2))) = fix f.λt.(case t;read() of leaf => let x = read() in (write(leaf);write(x + 1)) | node => write(node);f ();f ()) 変換の様子を見てみますと次のようになります。 tが変換で得られたそのまま変数のtとreadの逐次実行に変わっています。 また後ろでは木の書き出しがwriteのシーケンスになっています。 代入をした最終的な形はこのようになります。 このように、ソースプログラムからターゲットプログラムへ変換がきちんと行われています。

33 変換の正しさ 型付け可能なプログラムは, 変換によって 意味が変わらない
型検査を通れば, 変換によって必ず ストリーム処理のプログラムを得ることが出来る

34 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

35 どのような拡張が必要か 型システムによる制限の緩和 一般の XML への対応 入力木のスキップ 何度もアクセスできる木
子要素の数は一般に 2 より大 タグの種類の増加 ストリーム処理で閉じタグも考える必要 今回は この部分を紹介

36 拡張の方法 ターゲット言語 型システム 入力木をスキップするプリミティブを導入 メモリ上に木を構築するプリミティブを導入
メモリ上の木へのパターンマッチを導入 型システム “何度も使える木” の型 (MTree) を導入 入力木スキップ, MTreeに関する規則を導入 型判定と変換アルゴリズムを融合 変換に型情報を利用するので

37 ターゲット言語への変更 e (項) ::= i | x | λx.e | () | e1　e2 | e1 + e2 | fix f. e | leaf | node | read e | write e | skip e | memtree e | (case e of leaf → e1 | node → e2) | (mcase e of leaf x → e | node x1 x2 → e2)

38 型の拡張 τ (型) ::= Int | τ1 → τ2 | Treed | MTree
型は次のようになります。 整数の型Int、木の型Tree、およびτ１からτ２への関数です。 また、木の型には入力木型Tree-と出力木型Tree+が存在します。

39 新しい型判定 型判定にプログラム変換を含めて書く Γ | Δ ├ M : τ  e 変換に型情報が必要になるので
評価中に Δ の順で入力木がアクセスされ, M を変換すると ターゲット言語の項 e になる

40 Γ | x:Tree-, Δ ├ M :τ  let x = memtree () in e
型判定規則への変更 (一部のみ) Γ | x:Tree-, Δ ├ M :τ  let x = memtree () in e Γ, x:MTree | Δ ├ M :τ  e (T-MEMTREE) Γ | Δ ├ M : τ  e (T-SKIP) Γ | x:Tree-, Δ├ M : τ  let x = skip () in e

41 発表の流れ 対象言語の syntax 型システム 変換アルゴリズムとその正しさ 拡張に向けて 関連研究 まとめ

42 関連研究 属性文法を用いたXMLストリーム処理器の自動導出（中野 ’03） XMLストリーム処理のための言語XP++ (戸沢，萩谷 ’03)
長所: ストリームの一部をメモリに確保できる 短所: 副作用を伴う処理の記述が難しい XMLストリーム処理のための言語XP++ (戸沢，萩谷 ’03) 長所: 型検査に基づいたノード補完 短所: ストリーム処理を意識するが必要 ＸＭＬの処理に対しての研究はこのようなものがあります。 中野は、属性文法を用いて木変換を記述し、それにパーズアンパーズを行う文法と合成する方法で ＸＭＬストリーム処理器の自動導出をめざしています。 この研究の利点は、木を一部メモリ上にためておけることがあげられます。 我々の型システムでは、現時点ではその強い制限から木をメモリにためておくことを許していません。 コレに対する我々の研究の利点は、型の制限はあるがプログラム自体は関数型言語で記述できるため、 プログラマへの負担が少ない、ということがあげられます。また、副作用をともなう処理は属性文法で記述できないため、 この点においても優れていると考えられます。 戸沢、萩谷らの研究は、我々の研究とは違いストリーム処理の記述を簡単に行うことをめざしています。 ストリーム処理を行う言語XP++ではDTDに基づいた型検査を行い生成する文書の妥当性を静的に保証しています。 また、型検査に基づいてノード補完ができる点が優れています。 しかしストリーム操作をユーザが記述するため我々の手法より記述がやや困難であると考えられます。

43 関連研究 Ordered Linear Logic and applications. (Polakow ’01)
A type theory for memory allocation and data layout. (Petersen et al. ’03) メモリ上のデータ配置の正しさを保証 本研究で用いた順序付き線形型はpolakowの順序付き線形理論に基づいています。 これを利用した研究としてはPetersenらの、メモリ割り当てとデータ配置の正しさを保証する型システムが存在します。

44 まとめ 二分木を扱う木構造処理プログラムを ストリーム処理プログラムへ変換する手法を提案
変換可能かを判定するため、順序付き線形型を用いた型システムを考案 変換の正しさを証明 我々は二分木を扱う木構造処理プログラムをストリーム処理プログラムへと自動変換するシステムを確立しました。 また、プログラムがストリームの順序で木にアクセスしているかどうかを調べるため、順序付き線形型を用いた型システムを考案しました。 また、変換で等価なプログラムが得られることを保証しました。

45 Fin

46 例) 要素全てに1を足した木を作る関数 木構造処理 ストリーム処理
let rec f t = match t with Leaf x → Leaf (x + 1) | Node x1 x2 → Node (f x1) (f x2) ストリーム処理 let rec f () = match read () of Leaf → write Leaf; write (read() + 1) | Node → write Node; f (); f () 例として、要素すべてに１を足した新しい木を作る関数をこの２つの言語を使って示します。 木構造処理を扱うソースプログラムでは入力木tに対してパターンマッチを行い、新しい木を作ります。 ストリーム処理を行うターゲットプログラムではread命令を用いてストリームから値をひとつ読み取り、 それにしたがってパターンマッチを行っています。 言語の詳しい説明は後で述べます。

47 Γ | x:Tree-, Δ ├ M :τ  let x = memtree () in e
型判定規則への変更 (一部のみ) Γ | x:Tree-, Δ ├ M :τ  let x = memtree () in e Γ, x:MTree | Δ ├ M :τ  e (T-MEMTREE) Γ | Δ1├ M : MTree  e Γ, x:Int | Δ2├ M1:τ  e1 Γ, x1:MTree, x2:MTree | Δ2 ├ M2 :τ  e2 Γ | Δ1, Δ2├ case M of leaf x → M1 | node x1 x2 → M2 :τ  mcase e of leaf x → e1 | node x1 x2 → e2 (T-MCASE)