Top > Search Research paper > (In Japanese)プログラムをときほぐす数学理論

(In Japanese)プログラムをときほぐす数学理論

Research report code R070000225
File No. R070000225
Posted date Apr 11, 2008
Researchers
  • (In Japanese)長谷川 真人
Affiliation
Report name (In Japanese)プログラムをときほぐす数学理論
Technology summary (In Japanese)現在用いられているプログラムおよびプログラムによって表現されたアルゴリズムは、一般に、とても複雑な構造をもっています。その構造は、多くの場合、プログラムの中で用いられるデータの構造、そしてプログラムの実行過程をつかさどる制御の構造の、巧妙な組み合わせから生みだされます。前者の、データ構造の特性を生かした効果的なアルゴリズム設計は、古くから計算機科学の中心的な話題のひとつでした。一方、プログラミング言語の制御構造の活用も、また古典的な問題ですが、高度な経験則や抽象的な思考を必要とするため、必ずしも広く深く理解されてきたとは言いがたいのが実情です。古くはgoto文のようなジャンプの使用の是非に関する議論が有名ですが、その一般化である継続(コンティニュエ一ション)、自己言及的なプログラミングを許す再帰、あるいはプログラムをデータとしてやりとりする高階のプログラムなど、いずれも表現力に富み、プログラムに明快な構造を与えうる高度な制御構造が、実際のプログラミングの現場では、むしろいたずらにプログラムをわかりにくくするものとして敬遠されたり、理論屋のおもちゃに過ぎないと揶揄されたりしているのが実情です。確かに、高度な制御構造は、習得に時間を要します。理解不足のまま用いれば、いともたやすく「スパゲッティプログラム」の出来上がりです。けれども、正しく用いれば、プログラムの開発・保守・改良に際し、大変有効な道具です。使わないのはもったいない。問題は、その「正しく使う」ための指針が、必ずしも誰にでもわかるかたちで与えられていないことです。これは、単に良い教科書がないとか良い先生がいないなどということではありません。実のところ、プログラムの制御構造の相互作用をきちんと解き明かした理論がまだないのです。個々の制御構造を取り出してきちんと調べたり解説した例は数多くありますが、現実のプログラミング言語でおきている、様々な制御構造がお互いに干渉しあって生じる現象は、まだ理論的に十分には解明されてはいないのです。本研究は、そのような、制御構造の間の関係を、プログラミング言語の基礎理論の最新の成果を駆使して、明らかにしようというものです。特に、継続、再帰、高階プログラム、そして多相型プログラムの関係に焦点を当て、プログラム間に成り立つ等式の理論を導きました。
Drawing

※Click image to enlarge.

R070000225_01SUM.gif R070000225_02SUM.gif
Research field
  • Theory of computation
  • System programmings in general
Published papers related (In Japanese)(1) M. Hasegawa, The Uniformity Principle on Traced Monoidal Categories. Publications of the Research Institute for Mathematical Sciences 40(3): 991-1014, September 2004.
(2) Y. Kakutani and M. Hasegawa, Parametrizations and Fixed-point Operators on Control Categories. Fundamenta Informaticae 65(1-2): 153-172, March 2005.
(3) M. Hasegawa, Classical Linear Logic of Implications. Mathematical Structures in Computer Science 15(2):323-342, April 2005.
(4) J.R.B. Cockett, M. Hasegawa and R.A.G. Seely, Coherence of the Double Involution on *-Autonomous Categories. To appear in Theory and Applications of Categories.
(5) Y. Kakutani and M. Hasegawa, Parametrizations and Fixed-point Operators on Control Categories. Proc. 6th International Conference on Typed Lambda Calculi and Applications (TLCA'03), Springer Lecture Notes in Computer Science 2701, pages 180-194, June 2003.
(6) Y. Kameyama and M. Hasegawa, A Sound and Complete Axiomatization of Delimited Continuations. Proc. 8th ACM SIGPLAN International Conference on Functional Programming (ICFP2003), pages 177-188, August 2003.
(7) M. Hasegawa, Semantics of Linear-Continuation Passing in Call-by-name. Proc. 7th International Symposium on Functional and Logic Programming (FLOPS2004), Springer Lecture Notes in Computer Science 2998, pages 229-243, April 2004.
(8) M. Hasegawa, Relational Parametricity and Control (Extended Abstract). Proc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS2005), pages 72-81, June 2005.
(9) 長谷川真人、Traces in Computer Science、トポロジーとコンピュータ研究集会、2002年11月
(10) 長谷川真人、Recursive Programs in the Abstract、第6回プログラミング及びプログラミング言語ワークショップ(PPL2004)、2004年3月
(11) M. Hasegawa, On a Complete Axiomatization of Delimited Continuations, Joint Queen Mary and Imperial College Theory Seminar, June 2004
(12) 長谷川真人、Geometry of Non-deterministic Interaction、第8回シンポジウム「代数・言語・計算」、2005年2月
Research project
  • Precursory Research for Embryonic Science and Technology.;Information and Systems
Information research report
  • (In Japanese)長谷川 真人. プログラムをときほぐす数学理論. 個人型研究さきがけタイプ研究報告会 先進情報システムとその構成に向けて 「機能と構成」領域 講演要旨集 第Ⅲ期研究者(研究期間2002-2005), 2005. p.17 - 24.

PAGE TOP