著者

上里 友弥

雑誌

情報処理学会論文誌プログラミング(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な実装をもとにしながらも,停止性を比較的容易に証明することができた.