2013 Fiscal Year Annual Research Report
| Project/Area Number |
25289118
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Chiba University |
|---|
Principal Investigator |
萩原 学 千葉大学, 理学(系)研究科(研究院), 准教授 (80415728)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
葛岡 成晃 和歌山大学, システム工学部, 講師 (60452538)
AFFELDT Reynald 独立行政法人産業技術総合研究所, その他部局等, 研究員 (40415641)
笠井 健太 東京工業大学, 理工学研究科, 准教授 (70431997)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 符号理論 / モダン符号 / 形式化 / 密度発展法 / ssreflect / Coq / 型理論 / 疎 |
|---|
| Research Abstract |
本研究は紙・鉛筆部隊と計算機部隊という２部隊で遂行している．お互いの密な協力が不可欠であり，研究代表者と分担者全員およびその大学院生や研究協力者による研究打ち合わせを隔月で行った．打ち合わせでは，研究進展報告と進め方を議論してきた．他，紙・鉛筆部隊は，モダン符号の形式化に必要な，理論の再構築の準備として，sum-product復号法の一時推定の正当化の言明の形式化の為の，紙上の証明を解説した．計算機部隊は，言語SSReflectの紹介，既存の情報理論の形式ライブラリのチュートリアルを行った．
紙・鉛筆部隊の成果：加法的ガウス雑音通信路に対するシャノン限界の公式に関して，情報理論における標準的な定義や証明手法について検討，形式化を進める上での難点を整理した．特に，可変長情報源符号化を検討した．更に，(dl=3,...,8,dr=2,dg=2)-MN符号のポテンシャル閾値がシャノン閾値と一致することを示し,閾値より小さい消失確率εに対して空間結合MN符号の密度発展式の不動点は0のみであることを示した.これらのことから,(dl = 3,...,8,dr = 2,dg =2,L,w)-空間結合MN符号がBECのシャノン限界を達成することを証明した．
計算機部隊の成果：LDPC符号に関して，まず，sum-product復号法の一時推定の正当化の言明の形式化を行った．その際，モダン符号の形式化に欠かせない特別な総和の形式化方法の提案ができた．次に、上記の言明の形式証明の記述を開始した．その際，ライブラリ化したタナーグラフと周辺事後確率の性質の利用ができた．情報理論と符号理論の形式化の向上（ビット列の性質に関する補題，線形符号の形式化の調整），タナーグラフの形式化，周辺事後確率の定義と性質の形式化，最大事後確率復号や最小距離復号や最尤復号の定義とその定義に関する定理の形式化など．これらを踏まえ，ハミング符号に関する様々な定理を形式化した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究背景の異なる五機関による共同研究の為，互いの理解を深めるのに長い時間がかかると予想された．蓋を開ければ，お互いが打ち解けるのに時間は係らず，互いの研究の用語がある程度理解できる状況が半年程度で築けた．順調な立ち上げとなった．
紙・鉛筆部隊による密度発展法関係の形式化は，想像以上に困難な課題であることが見えてきた．その為，非常に早く研究を進められることは，これからも無いだろう。本研究の提案時であらかじめ想定した通り、モダン符号の中でもML符号などの話題に制限して取り組む必要性を感じている．逆に，符号を適切に制限することで，提案書に記載した通りの進展が見込まれる．
|
| Strategy for Future Research Activity |
密度発展法の形式化へのモダン符号の応用に関する検討を進める．その他，具体的な符号の理解を深めるために，多端子情報符号化問題に対してモダン符号を応用することで，圧縮限界を達成する最適符号を構成できることの証明，および，その形式化のため検討を行う．
計算機部隊は，sum-product復号法の一次推定の正当化の証明を完成させる．次に書籍「符号理論～デジタルコミュニケーションにおける数学」の定理9.50「列処理および行処理の正当化」を形式化する．以上の結果を用いて，パリティ検査行列のタナーグラフが木構造を持つとき，sum-product復号アルゴリズムが周辺事後確率復号であるという証明の形式化が可能となる．その後，密度発展法の形式化へ進む．
これらを実行するために，Microsoft INRIAがFeit-Thompson定理の証明時に行ったのと同様，必要な補題の構造の図示が有効であると想像される．これを，今年度の上半期に完成させ，２部隊５機関の連携を円滑に進められるようにする．
|
| Expenditure Plans for the Next FY Research Funding |
研究代表者と研究分担者をあわせた５名のうち、４名に次年度使用額が生じた。そのうち３名は、その額は１万円未満であり、本年度中に使い切るよりも次年度に合わせたることで、研究費としてより活用できると判断した。
残りの１名に関して、学生が研究打ち合わせに同行する為の出張旅費として確保していた。実際は、都合が付かずに出張が発生できなかった為、次年度の打ち合わせの際に次年度へ残すこととした。
研究代表者と分担者に、次年度使用額の金額をそのまま配分する。
まず、４名の未使用額が１万円未満であることから、配分額の見直しに影響が少ないと考えた為である。
もう１名分は、上記の理由で述べた通り、該当する学生の旅費としてそのまま確保することとした。
|
Research Products
(10 results)
