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

2014 年度 実施状況報告書

Haskellコアの意味論-先端的ソフトウェア検証基盤へ向けて

研究課題

研究課題/領域番号 25540002
研究機関群馬大学

研究代表者

浜名 誠  群馬大学, 大学院理工学府, 助教 (90334135)

研究分担者 勝股 審也  京都大学, 数理解析研究所, 助教 (30378963)
研究期間 (年度) 2013-04-01 – 2016-03-31
キーワードプログラム理論 / 関数プログラム / プログラム意味論 / Haskell
研究実績の概要

本年度は、コアHaskellの代数理論の定式化について次の二点に取り組んだ。
- seq 機構の公理化の研究。Haskellには正格評価を導入するseq演算子が存在するため、その代数理論は単純なcall-by-name の理論ではない。評価順序を公理化するための複数の方策を検討し、seqのcase文による表現が適切であることが分かった。またGHCの実装を解析し、中間言語において取られているアプローチとマッチする方法でもあることも判明した。
- 再帰メカニズムの代数的公理化。再帰演算子の定式化のために、Conway演算子と commutative identity という特殊な公理を用い、イテレーション理論として定式化する事でドメイン理論のような順序構造を必要としない、純粋な代数理論として再帰演算子を公理化することができることがわかった。
また本年度は、日本ソフトウェア科学会プログラミング論研究会のPPL'15ワークショップにてプログラム委員長を務め、最新のプログラミング言語研究の結果、関数型プログラミングの動向を幅広く調査した。これをコアHaskellのさらなる機構の意味論のために用いる。

現在までの達成度 (区分)
現在までの達成度 (区分)

3: やや遅れている

理由

再帰演算子の公理化をドメイン理論を用いずに完全な代数理論によって与えることができた。Haskellの副作用のための代数エフェクトの理論については、来年度に探求したい。

今後の研究の推進方策

今後は、再帰とcase式の機構の組合わせの検討をする。その代数理論からHaskellコアの圏を明らかにする。副作用の機構のためには、特にイテレーション理論をトレイス付きプレモノイダル圏について拡張して考察する必要があると考えている。

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

研究課題に必要な技術に関する国際会議が日本で開催されたため調査を、海外出張ではなく国内出張とした。そのため旅費に余裕が生まれ、未使用分が生じた。

次年度使用額の使用計画

次年度の研究打合せと、成果発表旅費に用いる。

  • 研究成果

    (2件)

すべて 2015

すべて 学会発表 (2件)

  • [学会発表] モナド、代数理論と計算効果2015

    • 著者名/発表者名
      勝股 審也
    • 学会等名
      第17回プログラミングおよびプログラミング言語ワークショップ PPL 2015
    • 発表場所
      道後プリンスホテル
    • 年月日
      2015-03-04 – 2015-03-04
  • [学会発表] Sound and Complete Equational Axiomatisation of Cyclic Semi-structured Data2015

    • 著者名/発表者名
      浜名誠
    • 学会等名
      メタプログラムに対する論理学的アプローチ
    • 発表場所
      東北大学 電気通信研究所
    • 年月日
      2015-02-24 – 2015-02-24

URL: 

公開日: 2016-06-03  

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

Powered by NII kakenhi