• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2014 Fiscal Year Annual Research Report

モダン符号の形式化

Research Project

Project/Area Number 25289118
Research InstitutionChiba 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

H26年度の目標の一つ、sum-product復号の形式化に成功した。具体的には、「sum-product復号法の定義の形式化」、「木構造をもつタナーグラフ上のsum-product復号のもつMPM復号性定理の形式化」、「一時推定の正当化定理の形式化」、そして「行処理、列処理の正当化定理の形式化」ができた。
もう1つの目標である密度発展法の形式化については、まだ完成していない。その方向性として位置付けて研究した「空間結合符号のBEC上での通信路容量達成定理の証明の簡略化」は結果を得ている。
また、これまでに研究代表者と研究分担者で構築してきた情報理論・符号理論ライブラリを整理する過程において、可変長情報源符号化順定理と逆定理の形式化研究が成功した。
上記の研究成果の他、実績として、ワークショップ「TPP2014(Theorem proving and provers for reliable theory and implementations」を開催できた。主催は九州大大学IMIであり、本研究協力者の溝口氏が責任者となった。本科研費による開催のクレジットがワークショップのHPから確認できる。
そして、開催に伴い、形式化研究の世界トップ機関であるフランス国立情報学研究所(INRIA)の研究員Cyril Cohen氏を千葉大学に招へいし、また、TPPで招待講演を頂いた。千葉大学内で研究ミーティングを開催し、その後も、メール等で情報交換を行っている。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本年度の目標は大きく分けて2つあり、sum-product復号アルゴリズムの正当化、密度発展法の形式化であった。前者は無事に達成できた。後者はまだ達成できていない。
一方で本研究の成果を整理する過程から、情報源符号化定理に関する形式化が実行でき、予想外に進んだ。
最終年度に予定していた研究集会開催をH26年度中に実行できた。
全体的に考慮すると、おおむね順調と言える。

Strategy for Future Research Activity

密度発展法の形式化を中心に研究を進める。参考書籍としてModern Coding Theory (Cambridge Press, by Urbanke and Richardson)を予定している。書籍中の議論で数学的な記述と記法の再考が避けられないため、書籍中の3章の基礎的な事項から形式化に挑む必要がある。目標として、BEC版で通信路容量達成の定理まで遂行したい。
また、空間結合LDPC符号の定義の形式化も進める。そして、空間結合LDPC符号の通信路容量達成定理の形式化を目指す。

Causes of Carryover

全体予算170万円中の5万円未満であり、少額だったため、次年度と合わせて使用するほうが有意義に活用できると判断した。

Expenditure Plan for Carryover Budget

研究代表者・分担者・協力者で分けて配分する。一人当たり数千円程度であり、研究者の個別打ち合わせの旅費等に使用する。

  • Research Products

    (12 results)

All 2015 2014 Other

All Journal Article (3 results) (of which Peer Reviewed: 1 results) Presentation (7 results) Remarks (2 results)

  • [Journal Article] Formalization of Error-correcting Codes using SSReflect2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Journal Title

      MI Lecture Note 研究集会 高信頼な理論と実装のための定理証明および定理証明器 (TPP2014), 九州大学, December 3--5, 2014

      Volume: 61 Pages: 76-78

  • [Journal Article] On formalization of basic geometric topology2015

    • Author(s)
      Ken’ichi Kuga, Manabu Hagiwara
    • Journal Title

      MI Lecture Note 研究集会 高信頼な理論と実装のための定理証明および定理証明器 (TPP2014), 九州大学, December 3--5, 2014

      Volume: 61 Pages: 110-114

  • [Journal Article] Formalization of the Variable-Length Source Coding Theorem: Direct Part2014

    • Author(s)
      Ryosuke Obi, Manabu Hagiwara, and Reynald Affeldt
    • Journal Title

      Proceeding of International Symposium on Information Theory and its Applications

      Volume: 1 Pages: 201-205

    • Peer Reviewed
  • [Presentation] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      Marelle Project Seminar, INRIA
    • Place of Presentation
      Sophia Antipolis, France
    • Year and Date
      2015-03-31 – 2015-03-31
  • [Presentation] 可変長情報源符号化逆定理の形式化2014

    • Author(s)
      小尾良介, 萩原学, 山本光晴
    • Organizer
      SITA2014
    • Place of Presentation
      富山県宇奈月ニューオータニホテル
    • Year and Date
      2014-12-09 – 2014-12-12
  • [Presentation] 可変長情報源符号化定理の形式化の改良2014

    • Author(s)
      萩原学, 小尾良介
    • Organizer
      SITA2014
    • Place of Presentation
      富山県宇奈月ニューオータニホテル
    • Year and Date
      2014-12-09 – 2014-12-12
  • [Presentation] Formalization of Error-correcting Codes using SSReflect2014

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      研究集会「高信頼な理論と実装のための定理証明および定理証明器」
    • Place of Presentation
      九州大学
    • Year and Date
      2014-12-03 – 2014-12-05
  • [Presentation] Formalization of Error-correcting Codes using SSReflect2014

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      The 6th Coq Workshop
    • Place of Presentation
      Vienna, Austria
    • Year and Date
      2014-07-18 – 2014-07-18
  • [Presentation] Spatially-Coupled MacKay-Neal Codes with No Bit Nodes of Degree Two Achieve the Capacity of BEC2014

    • Author(s)
      Takuya Okazaki, Kenta Kasai
    • Organizer
      2014 IEEE International Symposium on Information Theory
    • Place of Presentation
      Honolulu, Hawaii
    • Year and Date
      2014-06-29 – 2014-07-04
  • [Presentation] Spatially-Coupled Precoded Rateless Codes with Bounded Degree Achieve the Capacity of BEC under BP decoding2014

    • Author(s)
      Kosuke Sakata, Kenta Kasai, Kohichi Sakaniwa
    • Organizer
      2014 IEEE International Symposium on Information Theory
    • Place of Presentation
      Honolulu, Hawaii
    • Year and Date
      2014-06-29 – 2014-07-04
  • [Remarks] Formalization of Shannon's Theorems

    • URL

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

  • [Remarks] TPP2014

    • URL

      http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html

URL: 

Published: 2016-06-01  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi