型理論とその機械学習への応用

1994 年度 実績報告書

• 研究課題/領域番号: 06680342
• 研究機関: 東京大学
• 研究代表者: 萩谷 昌己 東京大学, 大学院・理学系研究科, 助教授 (30156252)
• 研究分担者: 原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
• キーワード: 型理論 / 型付きλ計算 / 制約 / 算術制約 / 機械学習 / 帰納推論 / 定理証明

研究概要

[制約の入った型理論に関する理論的考察]ここで研究した制約付きの型理論は、型付きλ計算のconv則を等式理論を用いて拡張することによって得られるものである。制約付き型理論は、拡張されたconv則を暗黙の引数の機能と組み合わせることによって、より大きな記述力を得ることができる。さらに、通常の書き換え規則と組み合わせて、条件付の書き換え規則を自然に表現することができる。以上のような型理論に対する拡張に関し、特に型の保存性などの性質について考察した。
[算術制約の入った型理論の実装]上述の枠組を多少修正した後、制約付き型理論の一例として、算術制約付きの型理論を、研究代表者が従来から開発している型理論をベースにした証明開発環境上に実装した。算術制約の解消には、SUP-INF法を簡略化した証明系を用いることにより十分な速度を得ることができた。
[上記の型理論における一般化機能の実現に関する検討]従来から提案していた一般化手続きは、全体として非決定的で計算量も大きいものである。そこで、一般化手続きを二つの部分に分割して実装する方法について検討した。一つは、証明の中の繰り返しを認識して証明の中にiterationを表すannotationを挿入する部分で、もう一つは、iteration annotationに従って帰納的な証明を合成する部分である。
iteration annoationは、帰納的なプログラムや帰納的な証明を、例を用いて簡潔に表現する手段(ユーザ・インターフェース)と考えることができ、後者の部分だけでも証明開発環境にとって有用である。今年度は、その実現方法について検討し大まかな見通しを立てることができた。来年度は、今年度の成果に従って、iteration annotationに基づく一般化機能を実際の証明開発環境の上に実装し、その評価と検討を行う。

研究成果

• [文献書誌] Masami Hagiya: "A Typed lambda-Calculus for Priving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)
• [文献書誌] 萩谷昌己: "制約付き型理論の実現" 関数プログラミングII,JSSST'94,レクチャーノート/ソフトウェア学,近代科学社,. 63-77 (1994)
• [文献書誌] Wei-Ngan Chin,Masami Hagiya: "Tupling and Lambda Abstraction yield Dynamic-Sized Tabulation" Acta Informatica. (発表予定). (1995)
• [文献書誌] Masami Hagiya: "On Reduction and Projection in Type Theory with Inductive Definitions" 12th International Conference on Automated Deduction,Workshop 1B:Proof Search in Type-Theoretic Languages. 31-38 (1994)
• [文献書誌] Masanori Arita,MasamiHagiya,Tomoki Shiratori: "GEISHA System:An Environment for Simulating Protein Interaction" Genome Informatics Workshop. V. 80-89 (1994)
• [文献書誌] Masami Hagiya,Yozo Toda: "On Implicit Arguments(TR-95-1)" Department Information Science,University of Tokyo, 31 (1995)