Koichi Kodama (Tokyo Institute of Technology)

Presentation on theme: "Koichi Kodama (Tokyo Institute of Technology)"— Presentation transcript:

1 Translation of Tree-processing Programs into Stream-processing Programs based on Ordered Linear Type
Koichi Kodama (Tokyo Institute of Technology) Kohei Suenaga (University of Tokyo) Naoki Kobayashi (Tohoku University)

2 Two main methods of XML processing
Tree-processing Views XML documents as tree structures Manipulates tree structure of input data Trees are kept on memory in many implementations e.g., DOM API, XDuce, CDuce Stream-processing Views XML documents as stream of tokens Read/Write tokens from/to streams e.g., SAX 2019/4/4 The Second Asian Symposium on Programming Language and Systems

3 Tree-processing node leaf 3 4 node leaf 2 3 Programmers write here memory disk, network <node> <leaf>2</leaf> <leaf>3</leaf> </node> <node> <leaf>3</leaf> <leaf>4</leaf> </node> 2019/4/4 The Second Asian Symposium on Programming Language and Systems

4 Stream-processing memory Programmers write here disk, network <node> <leaf>2</leaf> <leaf>3</leaf> </node> <node> <leaf>3</leaf> <leaf>4</leaf> </node> 2019/4/4 The Second Asian Symposium on Programming Language and Systems

5 Example of programs in each style
Incrementing the value of each leaf Tree-processing fix f. λt case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2) Stream-processing fix f. λt case read() of leaf → write(leaf); write(read() + 1) | node → write(node); f (); f () 例として、要素すべてに１を足した新しい木を作る関数をこの２つの言語を使って示します。 木構造処理を扱うソースプログラムでは入力木tに対してパターンマッチを行い、新しい木を作ります。 ストリーム処理を行うターゲットプログラムではread命令を用いてストリームから値をひとつ読み取り、 それにしたがってパターンマッチを行っています。 言語の詳しい説明は後で述べます。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

6 Comparison of two styles
Tree-processing Stream-processing Readability, writability better worse Memory efficiency 2019/4/4 The Second Asian Symposium on Programming Language and Systems

7 The Second Asian Symposium on Programming Language and Systems
Our goal Taking the best of both world Readability and writability of tree-processing High memory efficiency of stream-processing Approach Automatic translation of tree-processing programs into stream-processing programs 2019/4/4 The Second Asian Symposium on Programming Language and Systems

8 The Second Asian Symposium on Programming Language and Systems
Key observation (1/2) In order for stream-processing to be effective, a program should access an input tree from left to right, in the depth-first order. fix f. λt case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x2) (f x1) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

9 The Second Asian Symposium on Programming Language and Systems
Key observation (2/2) If a program accesses an input tree in that order, then there is a simple, structure-preserving translation into an equivalent stream-processing program. 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 () 2019/4/4 The Second Asian Symposium on Programming Language and Systems

10 The Second Asian Symposium on Programming Language and Systems
Our solution Use the idea of ordered linear types [Polakow 2000] Guarantee “correct” access order by assigning ordered linear types to input trees 2019/4/4 The Second Asian Symposium on Programming Language and Systems

11 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

12 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

13 The Second Asian Symposium on Programming Language and Systems
Languages Source language Call-by-value λ-calculus + primitives for binary tree processing Target language Call-by-value λ-calculus + primitives for stream processing 2019/4/4 The Second Asian Symposium on Programming Language and Systems

14 The Second Asian Symposium on Programming Language and Systems
Source language M (terms) ::= i (integer) | M1 + M (addition) | x (variable) | λx.M (abstraction) | M1 M (application) | fix f. M (recursive function) | leaf M (leaf with an integer) | node M1 M (branch) | (case M of (case analysis) leaf x → M | node x1 x2 → M2) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

15 The Second Asian Symposium on Programming Language and Systems
Target language e (terms) ::= i (integer) | e1 + e (addition) | () (unit) | x (variable) |λx.e (abstraction) | e1 e (application) | fix f. e (recursive function) | leaf | node (tag) | read () | write e (stream manipulation) | (case e of (case analysis) leaf → e | node → e2) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

16 Representation of trees in each language
node Source language node (leaf 1) (leaf 2) Target language node; leaf; 1; leaf; 2 leaf 1 leaf 2 We do not consider closing tags because we only focus on binary trees for now 2019/4/4 The Second Asian Symposium on Programming Language and Systems

17 The Second Asian Symposium on Programming Language and Systems
Example of programs Incrementing the value of each leaf Source language fix f. λt case t of leaf x → leaf (x + 1) | node x1 x2 → node (f x1) (f x2) Target language fix f. λt case read() of leaf → write(leaf); write(read() + 1) | node → write(node); f (); f () 例として、要素すべてに１を足した新しい木を作る関数をこの２つの言語を使って示します。 木構造処理を扱うソースプログラムでは入力木tに対してパターンマッチを行い、新しい木を作ります。 ストリーム処理を行うターゲットプログラムではread命令を用いてストリームから値をひとつ読み取り、 それにしたがってパターンマッチを行っています。 言語の詳しい説明は後で述べます。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

18 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

19 The Second Asian Symposium on Programming Language and Systems
Type system Utilizes ordered linear type Properties of well-typed programs: access each node of the input tree exactly once in left-to-right, depth-first order do not construct trees on memory 2019/4/4 The Second Asian Symposium on Programming Language and Systems

20 The Second Asian Symposium on Programming Language and Systems
Types τ (types) ::= Int (integer) | τ1→τ2 (function) | InTree (input tree) | OutTree (output tree) 型は次のようになります。 整数の型Int、木の型Tree、およびτ１からτ２への関数です。 また、木の型には入力木型Tree-と出力木型Tree+が存在します。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

21 The Second Asian Symposium on Programming Language and Systems
Type judgment Γ | Δ├ M :τ (Non-ordered) type environment: Γ { x1:τ1, x2:τ2, ..., xn:τn } (τi ∈ {InTree, OutTree} ) Set of bindings Ordered linear type environment: Δ x1:InTree, x2:InTree, ..., xn:InTree Sequence of bindings Represents that each of x1, x2, ..., xn is accessed exactly once in the order 2019/4/4 The Second Asian Symposium on Programming Language and Systems

22 Example of type judgment
Γ = f : InTree → OutTree Δ = x1 : InTree, x2 : InTree Γ | Δ├ node (f x1) (f x2) : OutTree Γ | Δ├ node (f x2) (f x1) : OutTree Γ | Δ├ node (f x1) (f x1) : OutTree 順序付き線形型環境についてです。 これがたとえばx1,x2,…,xnの順で構成されていたとき、x1からxnの順で丁度一回づつアクセスしなければならない、ということを意味します。 たとえばΓにfが入力木を受けとり出力木を返す関数という情報が入っていたとき 上の式は型付けできますが下の式は型付けできません。 なぜなら上の式は順序付線形型環境と同じ順でfx1,fx2の評価が行われていますが 下の式はfx2,fx1と、順序が違っているからです。 このように、下の式は木へのアクセス順序が正しくない、と判断され型付けできない、変換できない、ということになります。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

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

24 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

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

26 Translation algorithm (2/2)
A(leaf M) = write(leaf);write(A(M)) A(node M1 M2) = write(node);A(M1);A(M2) A(case M of leaf x → M | 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はユニットになる 2019/4/4 The Second Asian Symposium on Programming Language and Systems

27 Correctness of the translation
If φ | x : InTree├ M : OutTree 　　　(M, {x=V}) * W iff (A(M), <V>, ) * ( ( ), , <W>) input stream output stream 2019/4/4 The Second Asian Symposium on Programming Language and Systems

28 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

29 The Second Asian Symposium on Programming Language and Systems
Extensions Introduce buffering of trees Introduce primitives for buffered tree construction and destruction Extend typing rules and translation algorithm for those primitives As we stated, a good point of stream-processing is that it does not construct trees on memory. But among programs that need buffering, there are many programs that need only partial buffering of input trees. So introducing buffering can improve expressive power of our framework. -- With these primitives, we can use buffering by explicitly write buffered trees. But being conscious of buffering is sometimes troublesome. So we provide source-to-source translation algorithm next. 2019/4/4 The Second Asian Symposium on Programming Language and Systems

30 The Second Asian Symposium on Programming Language and Systems
Source language M (terms) ::= ... | mleaf M (buffered leaf) | mnode M1 M (buffered branch) | (mcase M of (case analysis mleaf x → M for buffered tree) | mnode x1 x2 → M2) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

31 The Second Asian Symposium on Programming Language and Systems
Target language e (terms) ::= ... | mleaf M (buffered leaf) | mnode M1 M (buffered branch) | (mcase M of (case analysis mleaf x → M for buffered tree) | mnode x1 x2 → M2) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

32 Types τ (types) ::= ... | MTree Type of buffered trees
(kept in non-ordered environment) 型は次のようになります。 整数の型Int、木の型Tree、およびτ１からτ２への関数です。 また、木の型には入力木型Tree-と出力木型Tree+が存在します。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

33 Example of type judgment
Γ = f : MTree → OutTree Γ’ = g : InTree → OutTree Γ, x : MTree | φ├ node (f x) (f x) : OutTree Γ’ | x : InTree ├ node (g x) (g x) : OutTree 順序付き線形型環境についてです。 これがたとえばx1,x2,…,xnの順で構成されていたとき、x1からxnの順で丁度一回づつアクセスしなければならない、ということを意味します。 たとえばΓにfが入力木を受けとり出力木を返す関数という情報が入っていたとき 上の式は型付けできますが下の式は型付けできません。 なぜなら上の式は順序付線形型環境と同じ順でfx1,fx2の評価が行われていますが 下の式はfx2,fx1と、順序が違っているからです。 このように、下の式は木へのアクセス順序が正しくない、と判断され型付けできない、変換できない、ということになります。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

34 The Second Asian Symposium on Programming Language and Systems
Typing rules Γ|Δ1├M : MTree Γ,x:Int|Δ2├M1 :τ Γ, x1:MTree ,x2:MTree | Δ2├M2 :τ Γ|Δ1,Δ2├ mcase M of mleaf x → M1 |mnode x1 x2 → M2 :τ (T-MCASE) 次にリーフ、ノード、ケースに関する規則を見て見ます。 リーフは要素が整数であるとき型付け可能、 ノードは左の木から順序付き線形型環境が使われることが必要です。 またケースはまずMから評価を行うため、入力木Mに前半部分のΔ1が使われ、 M1、M2の評価にはΔ2が使われることになります。 リーフの場合は要素が整数であること、 ノードの場合はx1,x2が入力木であり、この順に用いることが順序付き型環境の中に入ります。 2019/4/4 The Second Asian Symposium on Programming Language and Systems

35 Translation algorithm
A(mleaf M) = mleaf A(M) A(mnode M1 M2) = mnode A(M1) A(M2) A(mcase M of mleaf x → M | mnode x1 x2 → M2) = (mcase A(M) of leaf x → 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はユニットになる 2019/4/4 The Second Asian Symposium on Programming Language and Systems

36 The Second Asian Symposium on Programming Language and Systems
Example of programs fix s2m. λt. case t of leaf x → mleaf x | node x1 x2 → mnode (s2m x1) (s2m x2) fix m2s. λt. mcase t of mleaf x → leaf x | mnode x1 x2 → node (m2s x1) (m2s x2) 2019/4/4 The Second Asian Symposium on Programming Language and Systems

37 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

38 The Second Asian Symposium on Programming Language and Systems
Related work Attribute grammar based approach [Nakano et al. 2004] Translates tree-processing attribute grammars into stream-processing attribute grammars Pros: need not be conscious which part of stream to be buffered Cons: cannot specify evaluation order Introduction of side-effect may be problematic 2019/4/4 The Second Asian Symposium on Programming Language and Systems

39 The Second Asian Symposium on Programming Language and Systems
Related work Deforestation [Wadler 1988] Remove intermediate trees from programs Put syntactic restrictions (treelessness) on programs Variables have to occur only once Only variables can be passed to functions Do not require order restrictions Translated programs may not suitable for stream-processing 2019/4/4 The Second Asian Symposium on Programming Language and Systems

40 The Second Asian Symposium on Programming Language and Systems
Related work Ordered linear logic [Polakow 2000] Formalizes ordered linear logic Type system for memory allocation and data layout [Petersen et al. 2003] Uses ordered linear type to express spatial order on memory 2019/4/4 The Second Asian Symposium on Programming Language and Systems

41 The Second Asian Symposium on Programming Language and Systems
Outline Syntax of languages Type system Translation algorithm Extension Related work Conclusion 2019/4/4 The Second Asian Symposium on Programming Language and Systems

42 The Second Asian Symposium on Programming Language and Systems
Conclusion Proposed a method of translating tree-processing programs to stream-processing ones utilizing ordered linear type 2019/4/4 The Second Asian Symposium on Programming Language and Systems

43 The Second Asian Symposium on Programming Language and Systems
Future work Providing automatic insertion of buffering primitives Extension to general XML documents Dealing with rose trees Considering closing tags 2019/4/4 The Second Asian Symposium on Programming Language and Systems

44 Fin