2015 Fiscal Year Annual Research Report
| Project/Area Number |
25289118
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
萩原 学 千葉大学, 理学(系)研究科(研究院), 准教授 (80415728)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技 術研究部門, 主任研究員 (40415641)
葛岡 成晃 和歌山大学, システム工学部, 准教授 (60452538)
笠井 健太 東京工業大学, 理工学研究科, 准教授 (70431997)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 符号理論 / 形式化 / ＬＤＰＣ符号 / 空間結合ＬＤＰＣ符号 / モダン符号理論 / マスデジタリゼーション |
|---|
| Outline of Annual Research Achievements |
本研究の主テーマであるLDPC符号の通信路容量に関連する事項の形式化に関して、主に次の３つの成果を得た。
１．二元消失通信路および二元消失対称通信路に関する定義の形式化およびそれらの通信路容量と導出補題の形式化を行った。この結果は infotheo ライブラリの追加パッケージ itEXT4CapOfChans としてオンライン公開している。
２．LDPC符号の標準的な復号アルゴリズムである Sum-Productアルゴリズムの形式化を行った。それに付随する概念を形式化するために書籍 Modern Coding Theory を参照し、 Tree Ensemble ・ Computation Graph Ensemble ・ LDPC Ensemble の概念を形式化した。
３．2元消失通信路上のメッセージ伝達法の停止性を証明し、Stopping setの形式化も完成させた。
その他にも上の形式化を実行するうえで、周辺理論の形式化等の成果が得られる。主な結果として、４．ユークリッドアルゴリズムを含むリード・ソロモン符号を形式化、５．定理証明支援系 Coq/SSReflect に関する教科書のドラフト（約190ページ）執筆、６．関係代数の形式化のためのライブラリの完成、７．万能代数の形式化の基礎となる議論、８．Wang タイル関数の形式化と証明、９．共変幾何代数の形式的定式化と計算アルゴリズムの考察、などが挙げられる。
|
| Research Progress Status |
27年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
27年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
27年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
27年度が最終年度であるため、記入しない。
|
