Coq上でのMonadic Total Parser Combinatorの実装

情報処理学会 Web Site

書誌事項

タイトル別名
  • Coq ジョウ デ ノ Monadic Total Parser Combinator ノ ジッソウ
  • Implementing Monadic Total Parser Combinator on Coq

この論文をさがす

説明

本論文では，必ず停止するパーザのみを構成できるようなパーザコンビネータライブラリ（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.

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ