| 研究概要 |
本研究は紙・鉛筆部隊と計算機部隊という２部隊で遂行している．お互いの密な協力が不可欠であり，研究代表者と分担者全員およびその大学院生や研究協力者による研究打ち合わせを隔月で行った．打ち合わせでは，研究進展報告と進め方を議論してきた．他，紙・鉛筆部隊は，モダン符号の形式化に必要な，理論の再構築の準備として，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復号法の一時推定の正当化の言明の形式化を行った．その際，モダン符号の形式化に欠かせない特別な総和の形式化方法の提案ができた．次に、上記の言明の形式証明の記述を開始した．その際，ライブラリ化したタナーグラフと周辺事後確率の性質の利用ができた．情報理論と符号理論の形式化の向上（ビット列の性質に関する補題，線形符号の形式化の調整），タナーグラフの形式化，周辺事後確率の定義と性質の形式化，最大事後確率復号や最小距離復号や最尤復号の定義とその定義に関する定理の形式化など．これらを踏まえ，ハミング符号に関する様々な定理を形式化した．
|
