日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

正規表現型を用いた解析表現文法への型付け
山口 大輔

倉光 君郎

本稿では，正規表現型を解析表現文法に型付けする方法について述べる．解析表現文法に型付けられた正規表現型は導出木の集合を表し，導出木の構造 (サブノードの数やノードの名前，順序) を記述することができる．解析表現文
法に型付けを行う目的は，解析表現文法をベースとしたパーサから出力される導出木の構造について型検査による検証を行うためである．我々は解析表現文法から導出木を出力するパーサへの関係を定義し，この関係に対し型が保存することを確認した．

In this paper, we describe a method of typing regular expression types into parsing expression grammar.
Regular expression types that is typed into parsing expression grammar represent a set of derived trees anddescribe the structure of the derived tree(i.e. the number of subnodes, the name of the node and the order).
The purpose of typing parsing expression grammar is to describe the structure of the derived tree outputtedfrom the parser based on the parsing expression grammar and to verify with type checking. We defined
relation from parsing expression grammar to parsers that output derived trees and confirmed that the typepreserves in this relation.

types) [5] を用いており，導出木の集合を定義するだ

1 はじめにけでなく，導出木の構造を記述することができる．本

解析表現文法 (parsing expression grammar, PEG)

稿では解析表現文法とパーサの導出木の二項関係に[3] は，2004 年に発表された形式文法である．解析表

対して，型が保存することを示した．これによって，現文法の意味論は，再帰下降パーサとして定義される．

解析表現文法が正規表現型で型付けされるとき，パー解析表現文法をベースとしたパーサを利用するプ

サの導出木の集合は正規表現型の表す構造を持つ導ログラマは，パーサの出力する導出木に対し操作を出木の集合に一致することがいえる．

行うプログラムを実装する必要がある．しかし，導本研究によって，任意の解析表現文法に対し型付け出木の構造 (例えば，ノードの数やノードの名前，順ができることが示された．また，パーサの導出木の序) はパーサの入力に依存するため，存在しないノー構造に対して型による仕様を記述することが可能とドへの参照によるエラーや意図しないノードへの参なり，パーサがこの仕様に適合するか否かを型検査に照といった実行時エラーを引き起こしやすいという問よって判定することが可能となった．

題がある．

以降の構成は次の通りである．2 節では，正規表現

本稿では，型検査によってこのようなエラーが起型を用いた解析表現文法への型付けの直観を具体例をこらないを保証するために，解析表現文法への型付用いて説明する．3 節では，準備として解析表現文法けを行った．型は，正規表現型 (regular expressionと正規表現型について説明をし，導出木の記法の定義

Type System for Parsing Expression Grammar basedon Regular Expression Types
Daisuke Yamaguchi, Kimio Kuramitsu, 横浜国立大学大学院工学府, Graduate School of Engineering, Yokohama National University.

をする．4 節では，解析表現文法とパーサの導出木の二項関係を定義する．5 節では型付け規則を定義し，解析表現文法とパーサの導出木の二項関係に対し型が保存されることを示す．6 節では，関連研究をまとめる．最後に，7 節でまとめと今後の展望を述べる．

Prod

2 正規表現型の解析表現文法への型付けVal

正規表現型は，細谷らの XML 処理言語 [4] の基盤として，XML 文書への型付けを行うために定義されVal*1た．正規表現型はラベル付けられた型 (label[...])

図22

1*2 を入力した場合の導出木や正規表現にある記法 (*,|?など) によって XML 文
書の構造を表すことができる．我々は，XML 文書の構造は木構造であることに着目しパーサの導出木の3 準備構造を表す型として正規表現型を用いて正規表現型

3. 1 解析表現文法を解析表現文法に型付けする規則を定義した．

解析表現文法は，非終端記号の有限集合 NG ，終端正規表現型を解析表現文法に型付けする単純な例

記号の有限集合 Σ，導出規則の有限集合 PG ，開始表として，図 1 に定義される解析表現文法への型付け

現 es の 4 つ組 (NG , Σ, PG , es ) として定義される．

を考える． この解析表現文法は，1*2 や 1*2*5*8 のPG に属する導出規則は，非終端記号と解析表現の対応を表しており，A ← e という形式で記述される．

P rod←V al (* V al)∗ただし，A ∈ NG ，e は解析表現である．PG は，非V al←[0 − 9]終端記号から解析表現への写像とみることができる．

図1

単純な解析表現文法の例

ような乗算の式を認識するパーサに対応し，以下に定義される型 Prod が型付けされる．

type Prod = Prod[Val,(String,Val)*]type Val = Val[String]
型 Prod の表す導出木の構造は，ノードに Prod がラベルつけられており，子要素として型 Val が表す構造を持った導出木と，String，Val のそれぞれが表す構造を持った導出木の連接が 0 個以上結合することを

本稿では，PG の定義域を dom(PG ) で表す．本稿で扱う解析表現の構文は，図 3 に示す通りである．

e::=空文字εa(a ∈ Σ)

終端記号A(A ∈ NG )非終端記号ee

連接e/e

優先度付き選択e∗

0 回以上の繰り返し
否定先読み!e図3

解析表現の構文表している．型 Val が表す導出木の構造は，ノードがVal がラベル付けられており，子要素として String

解析表現の構文には，図 3 の他に便利なシンタックが表す構造を持った導出木が結合することを表してスシュガーが定義されている [3] が本稿ではそれらのいる．

説明は省略する．

図 1 のパーサに 1*2 を入力すると図 2 に示される導出木が得られる． この導出木の構造は，型 Prod の3. 2 解析表現文法の導出木表す導出木の構造に一致している．導出木の型付け規本稿で扱う導出木の記法について定義を行う．解析則は，型の表す導出木の構造に型付けされる導出木の表現文法 G = (NG , Σ, PG , es ) の導出木は，非終端記構造が一致することを反映している．

号の有限集合 NG と終端記号の有限集合 Σ の直積集合の上で定義される多分木である．ノードは非終端記号または終端記号列でラベル付けられている．

NG × Σ 上の導出木の集合を TNG ,Σ で表すとき，

導出木 t ∈ TNG ,Σ は次のように定義される．

t::=l[t](l ∈ NG ∪ Σ∗ )

::=T

ノード

()

empty

X型変数
ラベル

()
空の木
ノード l[t] は，NG 上の非終端記号または，終端記

L[T]T, T連接号列のラベル l が付けられており，導出木 t を子ノーT|T選択ドとして持つ．複数のサブノードをもつ場合は，導出T∗繰り返し

連接t, t

図4木の連接を表す演算子’,’ を用いる．ただし，演算子’,’は可換ではない．

正規表現型の構文というラベル型の縮約表記として扱い以降もこの表例として，図 2 の導出木をここで定義した記法で記を用いる．

表すと，4 解析表現文法とパーサの導出木の二項関係

Prod[Val[1],*,Val[2]]となる．ただし，1，*，2 はそれぞれ，1[()]，*[()]，

解析表現文法に型付けを行う目的に，パーサのイン2[()] の縮約表記である．以降もこの表記を用いる．

スタンスが出力する導出木の集合を型によって記述すProd で ラ ベ ル つ け ら れ た ノ ー ド の 子 ノ ーることがある．これが満たされるためには，解析表現

ド，Val[1],*,Val[3] は，最左木から Val[2] ，*，

文法とパーサの導出木への二項関係について型が保Val[3] という順で親ノードに結合することを表す．

存されることが重要である．これを示すため，本節でまた，演算子’,’ は可換でないほかに，次の等価関は解析表現文法の意味論を導出木を出力するパーサとして再定義を行う．

係が成り立つ．

t, ()≡t

我々は解析表現文法 G = (NG , Σ, PG , es ) の意味論(), t≡tを，対 (e, x) から対 (o, y) への二項関係 ⇓G で定義す

空の木 () は 0 個の導出木を表しており，演算子’,’ のる．ただし，e は解析表現，x は入力される非終端記単位元である．

号列を表す．y は読み残された非終端記号列を表す．

o は解析結果を表しており o ∈ TNG ,Σ ∪ {f } である．
3. 3 正規表現型

f は，構文解析が失敗しバックトラックすることを表

正規表現型 [5] は，型をプログラマが読み書きすす記号である．

るのに適した external form という形式と，部分型

本稿では，((e, x), (o, y)) ∈⇓G の表記を e ⇓xy o とのアルゴリズムの実装，証明に適した internal formする．e ⇓xy o は，解析表現 e は x を入力とし読み残という形式がある．本稿の解析表現文法への型付けされた記号列 y を伴って出力 o に写されると読む．には external form を用いるが，external form から

いま，t ∈ TNG ,Σ ， a, b, c ∈ Σ, x, y, z ∈ Σ∗ とすれinternal form への変換は translation 関数 [5] によって可能である．

ば，⇓G は図 5 の規則からなる最小の関係である．

Ford による意味論の定義 [3] に対し，解析表現文法ラベルの集合と型変数の加算無限集合を仮定するの意味論を導出木を出力する再帰下降パーサとしてとき，それぞれの元を L,X で表す．正規表現型 T の構定義したことによって，ε は，空の木 () を出力する

文は，図 4 の通り定義される．

パーサに写されるという違いがある (E-Empty)．そ型変数の束縛は，type X = T という形式で環境 Eれ以外に，終端記号 a は，ラベル a のノードに写されに保持される．E は，型変数から型への写像であり，る (E-Term1)，非終端記号 A は，ラベル A のノーdom(E) によって，E に定義されている型変数の集ドに写される (E-Nt)，否定先読み !e が失敗しない合を表す．

場合 (E-Not2) は，!e が空の木 () に写されるというString 型のような基底となる型は，String[()]違いがある．

ε ⇓xx ()(E-Empty)a ⇓axx a[()](E-Term1)

a ⇓bxx f(a ̸= b)A ∈ dom(PG )A ⇓xy A[t]e2 ⇓yx2 y t2

e1 ⇓xx12 xy 2 y t1

e1 e2 ⇓xy 1 x2 y t1 , t2
e1 ⇓xx fe1 e2 ⇓xx f
e1 ⇓xy 1 y t1e2 ⇓yy fe1 e2 ⇓xy 1 y f
e1 ⇓xyy t1
e1 /e2 ⇓xyy t1e1 ⇓xyxy fe2 ⇓xyy t2

e1 /e2 ⇓xyy t2
e1 ⇓xx fe2 ⇓xx f

e1 /e2 ⇓xx fe ⇓xx12 xy 2 y t1e∗e∗ ⇓xy 2 y tn

⇓xy 1 x2 y t1 , tn
e ⇓xx fe∗⇓xx ()e ⇓xyy t!e ⇓xy
xy f
e ⇓xy
x f!e ⇓xx ()図5

解析表現文法 G(E-Term2)

PG (A) ⇓xy t(E-Nt)

Alt1),(E-Alt2),(E-Rep1),(E-Rep2),(E-Not2) で定義される．

5 正規表現型の型付け
正規表現型は解析表現文法と，導出木に型付けられる．

(E-Seq1)

解析表現文法 G = (NG , Σ, PG , es ) が型 T で型付けられるとは，開始表現 es が型 T で型付けられること(E-Seq2)をいう．この型付け関係は Γ ⊢ es : T と表し，図 6 に定義される規則の集合からなる最小の関係と定義す(E-Seq3)

る． 図 6 の型付け規則は，補助的に非終端記号に型(E-Alt1)

Γ ⊢ ε : ()(T-Empty)Γ ⊢ a : String(T-Term)

Γ, A : X ⊢ PG (A) : TA

E(X) = A[TA ](E-Alt2)Γ⊢A:XΓ ⊢ e1 : T1

(E-Alt3)Γ ⊢ e 2 : T2

Γ ⊢ e1 e2 : T1 , T2Γ ⊢ e1 : T1

(E-Rep1)

Γ ⊢ e 2 : T2

Γ ⊢ e1 /e2 : T1 |T2
Γ⊢e:T(E-Rep2)Γ ⊢ e∗ : T∗⊢!e : ()

(E-Not1)(E-Not2)

二項関係 ⇓G= (NG , Σ, PG , es ) の パ ー

サ か ら 導 出 木 が 出 力 さ れ る 場 合 は ，ある 終 端 記 号 列 x が 与 え ら れ た と き ，esが (E-Empty),(E-Term1),(E-Nt),(E-Seq1),(E-図6(T-Nt)(T-Seq)(T-Alt)(T-Rep)(T-Not)解析表現の型付け規則

変数を割り当てる規則を定義した環境 Γ を用いる．Γ
は NG から型変数名の集合に 1 対 1 に対応付ける写像である．Γ の定義域を dom(Γ) と表し，A ∈ NG に割り当てられる型変数を Γ(A) と表す．
型変数は type X = T という形式で環境 E に束縛される．
簡単な例として解析表現文法の型付け導出を考え

Alt1),(E-Alt2),(E-Rep1),(E-Rep2),(E-Not2) のる．解析表現文法:

い ず れ か に よって 導 出 木 t に 写 さ れ る 場 合 に 限G=({V al, N um}

る ．こ れ ら の 規 則 が 成 り 立 つ と き の 終 端 記 号 列,{0}x の 集 合 を L(es ) と 表 す こ と に す れ ば ，解 析 表,{V al ← N um, N um ← 0}

現 文 法 G と そ の パ ー サ の 導 出 木 の 関 係 は ，入,V al)

力 さ れ る 終 端 記 号 列 を x ∈ L(es ) と し た と きが以下の型変数の束縛環境 E に束縛される正規表現の (E-Empty),(E-Term1),(E-Nt),(E-Seq1),(E-型 X で型付けされるとき，

type X = Val[Y]type Y = Num[String]

6 関連研究Γ = {V al : X, N um : Y} を導入することで型付け導出は図 7 のようになる．

解析表現文法は Ford による形式化以降盛んに研究がなされてきた．特に解析表現文法のパーサへの応用

解析表現文法についての型検査のアルゴリズムは，に関連して多くの研究が挙げられる [6] [7] [12] [11] [2] [9]．

図 6 に示す規則が構文主導であることから導出規則

解析表現文法理論的な背景の研究としては，これまでを下から上に辿ることで得られる．

明らかでなかった言語のクラスに関する研究などが挙次に，導出木 t に型 T が型付けられることを関係t : T で定義する．関係 t : T は図 8 に定義される規則の集合からなる最小の関係である．

げられる [8] [1] ．
しかし，我々の知る限りでは解析表現文法への型付けはこれまでなされなかった．我々は本稿で示した解(T-Sub1) は，型 String で型付けされる構文木の集合は，l を任意のラベルとするとき，型 l[()] で析表現文法への型付けは新しい着眼点であると考えている．

型付けされる構文木の集合を内包することを表す．

これまで，解析表現文法へ型付けがなされなかった(T-Sub2) は，型 () で型付けされる構文木は任意の理由は，解析表現文法の意味論は消費された文字列を型 T によって型付けされる構文木の集合に内包され出力するパーサとして定義されることから型付けを行ることを表す．これら 2 つの規則以外は，正規表現型

う動機が得られなかったためであると考えられる．多の型付け規則と同様である．

くの解析表現文法を用いたパーサジェネレータでは，解析表現文法を用いて構文を定義することができるが5. 1 型の保存

パーサの出力する導出木を含めた定義は行われない．

図 6,8 で定義された型付け規則は，4 節で定義されそのため，導出木の構築はアドホックな補強項によった解析表現文法と導出木の関係について保存する．て定義され，多くの場合それらはパーサホスト言語の定理 5.1 (保存). 解析表現文法 G = (NG , Σ, PG , es )型システムによって型付けがされる．

x∈L(es )について es ⇓yProoft かつ，es : T ならば，t : TL(e )es についての場合分けと，es ⇓y s t の一方，我々は解析表現文法の意味論を導出木を出力するパーサとして再定義を行った．これによって，解析表現文法を用いて導出木の定義を行うことが可能

導出規則に関する帰納法による．
自明でない場合は es = A ∈ NG の場合である．命となった．その結果，導出木を操作するプログラムを実装する上での難しさから解析表現文法への型付け

題の仮定は，(E-Nt) より，

A ⇓x∈L(A)
A[tA ]y(A1)を行う動機を得た．本研究で示した解析表現文法へのPG (A) ⇓x∈L(A)tAy(A1’)

型付けは，パーサの導出木の構造について型検査による検証を行うことを目的としており，本研究で定義さと，(T-Nt) より,

A:X(A2)れた型付け規則によって任意の解析表現文法への型付E(X) = A[TA ](A2’)

けが可能であることを示した．

が成り立つ．また，帰納法の仮定から，

PG (A) : TA(IH1)

tA : TA(IH2)

7 結び
本稿では，はじめに解析表現文法の意味論を導出木が成り立つ．(IH2) を (T-Node) に適用すれば，を出力するパーサとして再定義した．また，解析表現

A[tA ] : A[TA ](IH2’)

文法と導出木それぞれに正規表現型を型付けする規が成り立つ．(A2’),(IH2’) を (T-Var) に適用すれば，則を定義し，この型付けが解析表現文法とそのパー

A[tA ] : X となり成立する．

サから生成される導出木の二項関係関係で型が保存

(T-Term)
E(Y) = N um[String]Γ, V al : X, N um : Y ⊢ 0 : String(T-Nt)
Γ, V al : X ⊢ N um : Y(T-Nt)
Γ ⊢ V al : X

E(X) = V al[Y]図7

型付け導出の例

けのアルゴリズムを利用することはできない．解析表

t:T(T-Node)l[t] : l[T]t1 : T1

ルゴリズムについては今後の課題としたい．

t2 : T2(T-Seqt)
参 考 文 献t1 t2 : T1 , T2(T-Emptyt)() : ()
E(X) = T

t:T(T-Var)

t:Xt : T1
t : T1 |T2
t : T2t : T1 |T2
ti : T for each i(T-Or1)(T-Or2)(T-Rept)

t1 , . . . , tn : T∗t : l[()](T-Sub1)t : Stringt : ()(T-Sub2)t:T
図8

現文法に型付けられた正規表現型の部分型付けのア

導出木の型付け規則されることを示した．本稿で示した型付け規則によって，任意の解析表現文法に正規表現型を型付けできることが示された．また，パーサの導出木の構造に対して型による仕様を記述することが可能となり，パーサがこの仕様に適合するか否かを型検査によって判定することが可能となった．しかし，本稿で定義した解析表現文法への型付け規則は構文主導である反面，正規表現型の部分型関係に基づいた型付け規則を認めないため融通の利かないものとなった．正規表現型は部分型関係が定義されているが，これを決定するアルゴリズムは well-formed [5] である正規表現型を前提としている．本稿で示した規則によって解析表現文法に型付けを行った結果は必ずしも well-formed性を満たさないため，そのまま正規表現型の部分型付[ 1 ] Chida, N. and Kuramitsu, K.: Linear Parsing
Expression Grammars, Springer International Publishing, 2017, pp. 275–286.
[ 2 ] Ford, B.: Packrat Parsing:: Simple, Powerful,Lazy, Linear Time, Functional Pearl, Proceedings ofthe Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP ’02, New
York, NY, USA, ACM, 2002, pp. 36–47.
[ 3 ] Ford, B.: Parsing Expression Grammars: A
Recognition-based Syntactic Foundation, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’04, New York, NY, USA, ACM, 2004,
pp. 111–122.
[ 4 ] Hosoya, H. and Pierce, B. C.: XDuce: A
Statically Typed XML Processing Language, ACM
Trans. Internet Technol., Vol. 3, No. 2(2003),pp. 117–148.
[ 5 ] Hosoya, H., Vouillon, J., and Pierce, B. C.: Regular Expression Types for XML, ACM Trans. Program. Lang. Syst., Vol. 27, No. 1(2005), pp. 46–90.
[ 6 ] Koprowski, A. and Binsztok, H.: TRX: A Formally Verified Parser Interpreter, Proceedings of the19th European Conference on Programming Languages and Systems, ESOP’10, Berlin, Heidelberg,Springer-Verlag, 2010, pp. 345–365.
[ 7 ] Medeiros, S. and Ierusalimschy, R.: A Parsing
Machine for PEGs, Proceedings of the 2008 Symposium on Dynamic Languages, DLS ’08, New York,NY, USA, ACM, 2008, pp. 2:1–2:12.
[ 8 ] Medeiros, S., Mascarenhas, F., and Ierusalimschy, R.: From Regexes to Parsing Expression
Grammars, Sci. Comput. Program., Vol. 93(2014),
pp. 3–18.
[ 9 ] Parr, T., Harwell, S., and Fisher, K.: Adaptive
LL(*) Parsing: The Power of Dynamic Analysis,
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems
Languages &#38; Applications, OOPSLA ’14, New
York, NY, USA, ACM, 2014, pp. 579–598.
[10] Pierce, B.: Types and Programming Languages,MIT Press, 2002.
[11] Redziejowski, R. R.: Parsing Expression Grammar As a Primitive Recursive-Descent Parser withBacktracking, Fundam. Inf., Vol. 79, No. 3-4(2007),
pp. 513–524.
[12] Redziejowski, R. R.: Applying Classical Con-

cepts to Parsing Expression Grammar, Fundam.
Inf., Vol. 93, No. 1-3(2009), pp. 325–336.