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

2001 年度 実績報告書

ポリモルフィズムの数学的構造

研究課題

研究課題/領域番号 12740057
研究機関東京大学

研究代表者

長谷川 立  東京大学, 大学院・数理科学研究科, 助教授 (20243107)

キーワード型付きラムダ計算 / ポリモルフィズム / パラメトリシティ / 線型論理
研究概要

線形パラメトリシティを公理としてもつ体系と,その実現可能性解釈の開発を試みた.Reynoldsは1980年代に,ポリモルフィックなプログラミング言語に対して,パラメトリシティと呼ばれる概念を提唱した.線形パラメトリシティは,二階線形論理に対してこの概念を適用しようという試みである.
パラメトリシティ原理を公理として仮定することの意味は,そこから再帰的データ型の存在が導かれることにある.1990年代に,高階の型付きラムダ計算に対するパラメトリシティ原理が盛んに研究されたのはこのような事情からであった.
しかし,型付きラムダ計算に対するパラメトリシティ原理は,不動点演算子の存在と矛盾する.不動点演算子は,再帰的プログラミングに対応し,現実のプログラミング言語には存在するべきものであるが,これと矛盾してしまうのは,ある意味パラメトリシティ原理のもつ大きな欠点といえよう.
われわれは,この原理を少し弱めた線形パラメトリシティ原理を考え,この矛盾を回避できることを主張した.具体的には,二階線形論理のモデルで,不動点演算子を持ち,さらに線形パラメトリシティと呼ぶにふさわしい性質を持つものを開発した.
さらに,このモデルの性質を調べ,それが満たす線形パラメトリシティ原理を体系化しようと試みている.現在まだ完成はしていないが,その体系は次のような性質を満たすはずであることは分かっている.再帰的なデータ型の存在が,線形パラメトリシティというやや弱い原理からでも導かれること.不動点演算子の存在とあわせることによって,負の位置にパラメータが現れるような,一般的な再帰的データ型の存在も導出できること.始代数と終代数の一致が導け,これによりhylomorphismと呼ばれるプログラム変換の技法が自由に適用できるようになることである.

  • 研究成果

    (1件)

すべて その他

すべて 文献書誌 (1件)

  • [文献書誌] R.Hasegawa: "Two applications of analytic functors"Theoretical Computer Science. 272. 113-175 (2002)

URL: 

公開日: 2003-04-03   更新日: 2016-04-21  

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

Powered by NII kakenhi