著者

上里 友弥

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.5, no.2, pp.1-15, 2012-03-30

---

本論文では,必ず停止するパーザのみを構成できるようなパーザコンビネータライブラリ(total parser combinator library)の実装手法について述べる.構成されるパーザが必ず停止することの保証は,定理証明支援系のCoqによって行う.Coqは,停止する関数だけを許すプログラミング言語としても使うことができるので,Coq上で定義することができればよい.パーザおよびパーザコンビネータはmonadicに実装したい.しかし一般に,monadicな実装においては証明の段階で逐一定義を展開していかなければならず,無駄が多いという問題がある.一方,この問題に対しては,Swierstraの提案したHoare state monadが有効である.そこで,我々はパーザをmonadicに実装する手段として,Hoare state monadを一般化したHoare state monad transformerを新たに提案する.このHoare state monad transformerを用いたことで,従来のmonadicな実装をもとにしながらも,停止性を比較的容易に証明することができた.

著者

上里 友弥

出版者

情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.5, no.2, pp.1-15, 2012-03-30

---

本論文では,必ず停止するパーザのみを構成できるようなパーザコンビネータライブラリ(total parser combinator library)の実装手法について述べる.構成されるパーザが必ず停止することの保証は,定理証明支援系のCoqによって行う.Coqは,停止する関数だけを許すプログラミング言語としても使うことができるので,Coq上で定義することができればよい.パーザおよびパーザコンビネータはmonadicに実装したい.しかし一般に,monadicな実装においては証明の段階で逐一定義を展開していかなければならず,無駄が多いという問題がある.一方,この問題に対しては,Swierstraの提案したHoare state monadが有効である.そこで,我々はパーザをmonadicに実装する手段として,Hoare state monadを一般化したHoare state monad transformerを新たに提案する.このHoare state monad transformerを用いたことで,従来のmonadicな実装をもとにしながらも,停止性を比較的容易に証明することができた.We have implemented a total parser combinator library that can constitute only a parser that terminates for all inputs. The termination is guaranteed by using the Coq proof assistant as a programming language that allows only terminating functions. If a parser is implemented with the library on the Coq, then termination of it is really guaranteed. It is desirable to implement parsers and parser combinators in the monadic style. However, when a program is implemented in the monadic style, it is usually necessary to unfold the definition of monads in the process of proving, and the unfolding makes the proofs rather cumbersome. To overcome this problem, we generalize Hoare state monads of Swierstra to Hoare state monad transformers. By using Hoare state monad transformers, we maintain the monadic style implementation, and also it is relatively easy to prove the termination of constructed parsers.

著者

上里 友弥 南出 靖彦

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.7, no.4, pp.8-20, 2014-08-29

---

本論では,言語が決定性文脈自由言語(DCFL)ではないことを証明するための,決定性プッシュダウンオートマトン(DPDA)に基づく手法を提案する.提案する手法は,計算中でのスタックの高さを特徴付けるもので,以下のようなスタックの変化に対する直感を形式的に扱うことができる:言語{anbncn | n ≧ 1}が何らかのDPDAで受理できたとすると,aの個数とbの個数を比較した結果として,anbnの部分を読み終わった段階のスタックはほとんど空になっているはずである.このとき,続く文字列cnを検査することができない.したがって,この言語はDCFLではない.具体的には,十分に長い繰返し文字列を消費した結果のスタックの内容には繰返し構造があることを示し,繰返し文字列を消費した結果のスタックが一般化順序機械と呼ばれる機械で定義可能であることを示した.この結果を用いて,上の例のようにaの個数とbの個数を比較するためには,スタックがほとんど空にならなければならないことを形式化して示した.