• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2015 年度 実績報告書

モダン符号の形式化

研究課題

研究課題/領域番号 25289118
研究機関千葉大学

研究代表者

萩原 学  千葉大学, 理学(系)研究科(研究院), 准教授 (80415728)

研究分担者 Affeldt Reynald  国立研究開発法人産業技術総合研究所, 情報技 術研究部門, 主任研究員 (40415641)
葛岡 成晃  和歌山大学, システム工学部, 准教授 (60452538)
笠井 健太  東京工業大学, 理工学研究科, 准教授 (70431997)
J Garrigue  名古屋大学, 多元数理科学研究科, 准教授 (80273530)
研究期間 (年度) 2013-04-01 – 2016-03-31
キーワード符号理論 / 形式化 / LDPC符号 / 空間結合LDPC符号 / モダン符号理論 / マスデジタリゼーション
研究実績の概要

本研究の主テーマであるLDPC符号の通信路容量に関連する事項の形式化に関して、主に次の3つの成果を得た。
1.二元消失通信路および二元消失対称通信路に関する定義の形式化およびそれらの通信路容量と導出補題の形式化を行った。この結果は infotheo ライブラリの追加パッケージ itEXT4CapOfChans としてオンライン公開している。
2.LDPC符号の標準的な復号アルゴリズムである Sum-Productアルゴリズムの形式化を行った。それに付随する概念を形式化するために書籍 Modern Coding Theory を参照し、 Tree Ensemble ・ Computation Graph Ensemble ・ LDPC Ensemble の概念を形式化した。
3.2元消失通信路上のメッセージ伝達法の停止性を証明し、Stopping setの形式化も完成させた。
その他にも上の形式化を実行するうえで、周辺理論の形式化等の成果が得られる。主な結果として、4.ユークリッドアルゴリズムを含むリード・ソロモン符号を形式化、5.定理証明支援系 Coq/SSReflect に関する教科書のドラフト(約190ページ)執筆、6.関係代数の形式化のためのライブラリの完成、7.万能代数の形式化の基礎となる議論、8.Wang タイル関数の形式化と証明、9.共変幾何代数の形式的定式化と計算アルゴリズムの考察、などが挙げられる。

現在までの達成度 (段落)

27年度が最終年度であるため、記入しない。

今後の研究の推進方策

27年度が最終年度であるため、記入しない。

次年度使用額が生じた理由

27年度が最終年度であるため、記入しない。

次年度使用額の使用計画

27年度が最終年度であるため、記入しない。

  • 研究成果

    (24件)

すべて 2016 2015 その他

すべて 国際共同研究 (1件) 雑誌論文 (7件) (うち国際共著 2件、 査読あり 4件、 オープンアクセス 3件、 謝辞記載あり 5件) 学会発表 (12件) (うち国際学会 9件、 招待講演 3件) 備考 (3件) 学会・シンポジウム開催 (1件)

  • [国際共同研究] University of Hawaii(米国)

    • 国名
      米国
    • 外国機関名
      University of Hawaii
  • [雑誌論文] A short proof for the multi-deletion error correction property of Helberg codes2016

    • 著者名/発表者名
      Manabu Hagiwara
    • 雑誌名

      IEICE Communication Express

      巻: 2 ページ: 49 - 51

    • DOI

      http://doi.org/10.1587/comex.2015XBL0182

    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Uniqueness of Buston Hadamard matrices of small degrees2015

    • 著者名/発表者名
      M.Hirasaka, K.Kim, Y.Mizoguchi
    • 雑誌名

      Journal of Discrete Algorithms

      巻: 34 ページ: 70 - 77

    • DOI

      http://www.sciencedirect.com/science/article/pii/S1570866715000623

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] A Property of Random Walks on a Cycle Graph2015

    • 著者名/発表者名
      Y.Ikeda, Y.Fukai, Y.Mizoguchi
    • 雑誌名

      Pacific Journal of Mathematics for Industry

      巻: 7 ページ: 3:01 - 3:27

    • DOI

      http://link.springer.com/article/10.1186/s40736-015-0015-3/fulltext.html

    • 査読あり / オープンアクセス
  • [雑誌論文] 順序のある代数系上の挿入削除誤り訂正符号2015

    • 著者名/発表者名
      萩原学
    • 雑誌名

      情報理論とその応用シンポジウム予稿集

      巻: 1 ページ: 469 - 474

    • 謝辞記載あり
  • [雑誌論文] Coq/SSReflectによる二元消失通信路の通信路容量の形式化2015

    • 著者名/発表者名
      中野恭輔、萩原学
    • 雑誌名

      情報理論とその応用シンポジウム予稿集

      巻: 1 ページ: 752 - 757

    • 謝辞記載あり
  • [雑誌論文] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 雑誌名

      Springer LNCS

      巻: 9236 ページ: 17 - 33

    • DOI

      10.1007/978-3-319-22102-1_2

    • 査読あり / 国際共著 / 謝辞記載あり
  • [雑誌論文] Variable-Length Coding for Mixed Sources with Side Information Allowing Decoding Errors2015

    • 著者名/発表者名
      Shigeaki Kuzuoka
    • 雑誌名

      第9回シャノン理論ワークショップ予稿集

      巻: 1 ページ: 51 - 58

    • 謝辞記載あり
  • [学会発表] A Mathematica module for Conformal Geometric Algebra and Origami Folding2016

    • 著者名/発表者名
      M.Kondo, T.Matsuo, Y.Mizoguchi, H.Ochiai,
    • 学会等名
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • 発表場所
      お茶の水女子大学(東京都・文京区)
    • 年月日
      2016-03-28 – 2016-03-31
    • 国際学会
  • [学会発表] Workshop on Formalization of Applied Mathematical Systems2016

    • 著者名/発表者名
      T.Matsushima, Y.Mizoguchi, A.D.Jourdan
    • 学会等名
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • 発表場所
      お茶の水女子大学(東京都・文京区)
    • 年月日
      2016-03-28 – 2016-03-31
    • 国際学会
  • [学会発表] 二元消失通信路のシャノン限界形式化とその形式的証明について2015

    • 著者名/発表者名
      中野恭輔
    • 学会等名
      平成27年度情報理論特別講演会
    • 発表場所
      休暇村紀州加太(和歌山県・和歌山市)
    • 年月日
      2015-12-18 – 2015-12-19
  • [学会発表] 多重挿入/削除誤り訂正符号の順序付代数による構成とその表現2015

    • 著者名/発表者名
      萩原学
    • 学会等名
      琉球大学理学部セミナー
    • 発表場所
      琉球大学(沖縄県・中頭郡)
    • 年月日
      2015-12-04 – 2015-12-04
    • 招待講演
  • [学会発表] 多重挿入/削除誤り訂正符号の構成と表現2015

    • 著者名/発表者名
      萩原学
    • 学会等名
      実験計画法と符号および関連する組合せ構造
    • 発表場所
      箱根水明荘(神奈川県・足柄下郡)
    • 年月日
      2015-12-01 – 2015-12-03
    • 招待講演
  • [学会発表] Certification of a sum-product algorithm for LDPC on a BSC2015

    • 著者名/発表者名
      Jacques Garrigue
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25 – 2015-10-03
    • 国際学会
  • [学会発表] A Coq Library for the Theory of Realational Calculus2015

    • 著者名/発表者名
      Y.Mizoguchi
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25 – 2015-10-02
    • 国際学会 / 招待講演
  • [学会発表] Formalization of the Channel Capacity of Binary Erasure Channel in Coq/SSReflect2015

    • 著者名/発表者名
      Kyosuke Nakano
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25 – 2015-10-02
    • 国際学会
  • [学会発表] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25 – 2015-10-02
    • 国際学会
  • [学会発表] Wang Tiles Modeling of Wall Patterns2015

    • 著者名/発表者名
      A.D.Jourdan, Y.Mizoguchi and M.Salvati
    • 学会等名
      Mathematical Progress in Expressive Image Systems (MEIS2015)
    • 発表場所
      九州大学(福岡県福岡市)
    • 年月日
      2015-09-25 – 2015-09-25
    • 国際学会
  • [学会発表] GADTs and exhaustiveness: looking for the impossible2015

    • 著者名/発表者名
      Jacques Garrigue, Jacques Le Normand
    • 学会等名
      ML Family Workshop
    • 発表場所
      Vancouver (カナダ)
    • 年月日
      2015-09-03 – 2015-09-03
    • 国際学会
  • [学会発表] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      The 6th conference on Interactive Theorem Proving
    • 発表場所
      Nanjing (中国)
    • 年月日
      2015-08-24 – 2015-08-27
    • 国際学会
  • [備考] infotheoライブラリ

    • URL

      http://manau.jp/research/infotheo/

  • [備考] 雅利賀 惹玖のホームページ

    • URL

      http://www.math.nagoya-u.ac.jp/~garrigue/home-j.html

  • [備考] Linear ECCs in Coq

    • URL

      https://staff.aist.go.jp/reynald.affeldt/ecc/

  • [学会・シンポジウム開催] Workshop on Formalization of Applied Mathematical Systems2015

    • 発表場所
      University of Hawaii
    • 年月日
      2015-09-25 – 2015-10-02

URL: 

公開日: 2017-01-06   更新日: 2022-01-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi