著者

村田 康佑 江本 健斗

雑誌

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

巻号頁・発行日

vol.11, no.4, pp.1-12, 2018-12-14

---

数学定理やプログラムの性質の形式的証明では,自然数上の不等式についての証明が頻出する.しかし,定理証明支援系Coqでの不等式の形式的証明は,非形式的証明とは異なる記法で記述されるため,数学的な直観がそのまま使えないことも多い.たとえば,非形式的証明では,不等式L ≤ Rを証明するために,しばしばL = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = Rのように項を不等号で「鎖状」につなげて示す宣言的な記法が用いられる.こうした記法は数学の教科書等でよく馴染んだ記法であり,直観的に理解・記述することが可能である.一方,Coqにはそうした宣言的な記法は標準では用意されていないため,証明の理解・記述が困難になっている.本論文では,Coq上で,自然数上の不等式変形を,非形式的証明のように「鎖状」に記述する手法を提案する.本手法の特徴は,タクティックライブラリによって「鎖状」記法が実現されることにあり,それゆえ,提案記法はライブラリをモジュールとして読み込むだけで既存記法とあわせて使うことができる.また,このタクティックライブラリを用いて,Ackermann関数の性質についての不等式の証明を試みる.その結果,標準的な数学の教科書と近い記法で形式的証明を記述できることを確認する.

著者

松崎 公紀 江本 健斗

雑誌

情報処理

巻号頁・発行日

vol.56, no.5, pp.482-488, 2015-04-15

---

BSP (Bulk Synchronous Parallel) モデルは,L.G.Valiant (2010年ACM Turing賞)によって1990年に提案されたモデルであり,抽象並列計算機モデルと並列計算モデルとを与えるものである.近年,Google Pregelなど,BSPの計算モデルに倣った大規模グラフ処理フレームワークが提案され,BSPモデルにも注目が寄せられている.本解説では,BSPの提案に至った歴史やBSPの計算モデルについて説明するとともに,BSPに基づく実際の並列プログラミングについて,コードを交えて紹介する.

著者

松崎 公紀 江本 健斗 劉 雨

出版者

情報処理学会

雑誌

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

巻号頁・発行日

vol.4, no.4, pp.1-11, 2011-09-22

---

正規表現は広く用いられており,文章が正規表現にマッチするかどうかの問合せ (クエリ) を効率的に実行することは重要である.これまで,正規表現マッチングを高速に行う逐次的な手法について多くの研究がある.正規表現マッチングを並列に行う方法についても研究があるが,その多くは,複数の文章に対するクエリの並列実行や,複数のクエリの並列実行というような自明な並列実行について扱うものである.一方で,巨大な 1 つの文章に対して 1 つのクエリを行う場合には,正規表現マッチングそのものを並列化する必要が発生する.本稿では,正規表現マッチングを並列化する手法について議論を行う.また,本稿で提案する正規表現の並列マッチングの計算効率を評価するため,Hadoop を用いて実験を行いその結果を報告する.Hadoop は,大規模分散データに対して効率的に処理を行うことができる MapReduce フレームワークのオープンソース実装である.Regular expressions are now widely used and efficient implementation of regular expression matching is an important issue for efficient manipulation of data. There have been many studies for efficient implementation of regular expression matching. There have also been studies on parallel implementations of regular expression matching, but these implementations exploit parallelism only in executing a single query on multiple documents or in executing multiple queries on a single document. In this paper, we discuss a technique to parallelize a regular expression query itself. In other words, with this technique we can execute a regular expression query on a single document in parallel. We evaluate efficiency of regular expression matchings parallelized by the proposed method on the Hadoop; the Hadoop is an open-source implementation of the MapReduce framework that enables efficient processing of large-scale data.