Coq上でのMonadic Total Parser Combinatorの実装

• Item type: Trans(1)
• 公開日: 2012-03-30
• タイトル: Coq上でのMonadic Total Parser Combinatorの実装
• タイトル / 言語: en
• タイトル: Implementing Monadic Total Parser Combinator on Coq
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 筑波大学情報学群情報科学類
• 著者所属(英): en
• 著者所属(英): College of Information Science, University of Tsukuba
• 著者名: 上里, 友弥
• 著者名(英): Yuya, Uezato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，必ず停止するパーザのみを構成できるようなパーザコンビネータライブラリ（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な実装をもとにしながらも，停止性を比較的容易に証明することができた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 5, 号 2, p. 1-15, 発行日 2012-03-30
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会