1995 Fiscal Year Annual Research Report
| Project/Area Number |
06680342
|
|---|
| Research Institution | University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
|
|---|
| Keywords | 型理論 / 型付きλ計算 / 制約 / 算術制約 / 機械学習 / 帰納推論 / 定理証明 / ユーザ・インタフェース |
|---|
| Research Abstract |
(1)算術制約の入った型理論の実装:前年度に引き続き、算術制約の入った型理論を、研究代表者が従来から開発している型理論をベースにした証明開発環境上に実装した。この証明開発環境の特徴の一つとして、関数が暗黙の引数を持てるということがある。本年度は、暗黙の引数を利用した算術制約の実装を行った。具体的には、(Below n)と書かれるnより小さい自然数の型を導入し、自然数からBelow型への埋め込みを、Πi:Nat.Πj|Nat.Below(j+(i+1))を型として持つ関数として定義した。この関数はiとjという二つの引数を持つが、jは暗黙の引数である。すると、算術制約を解くことによって、この埋め込み関数が正しく適用されているかどうかを判定することができる。
(2)一般化機能の実現:上記の証明開発環境上で作られた証明テキストの一部を指定し、その中で解消すべき算術制約に基づいて自然数定数を変数に一般化することにより、数学的帰納法の帰納ステップを求める機能の実現を試みた。(本機能はまだ完成していない。)
(3)iteration annotationに関する考察:本研究では、上記のような一般化機能を、証明テキスト中に挿入され繰り返し指摘するためのannotation(iteration annotation)によって呼び出せるようにする方針であった。本年度は、繰り返しを指定するためのインタフェースとして、iteration annotationに関する一般的な考察も行った。
(4)自動証明機能との融合:本研究では、主として、型理論のもとで書かれた証明の一般化について考察したが、その最後の段階で、tacticやresolutionなどの自動証明機能を利用して作られた証明の一般化に関して考察した。
|
-
[Publications] 萩谷昌己,白取知樹: "「計算=編集」パラダイムにおける例によるプログラミング" コンピュータ・ソフトウェア. (掲載予定). (1996)
-
[Publications] 萩尾昌己,渡辺洋,北村敏子: "導出法と帰納的証明の融合について" 情報処理学会,プログラミング研究会. (掲載予定). (1996)
-
[Publications] Masami Hagiya,Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium on Visual Languages. 275-283 (1995)
-
[Publications] M.Yamamoto,S.Nishizaki,M.Hagiya,Y.Toda: "Formalization of Planar Graphs" High-Order Logic Theorem Proving and Its Applications,Lecture Notes in Computer Science,Springer-Verlag. 971. 369-384 (1995)
-
[Publications] 山本光晴,萩谷昌己,白取知樹,西崎真也: "図的対象を扱う証明チェッカのための視覚化ツール" インタラクティブシステムとソフトウェアIII,レクチャーノート/ソフトウェア学,近代科学社. 12. 85-92 (1995)
-
[Publications] Masami Hagiya,Kouhei Iino: "Binding Time Analysis for Data Type Specialization" Fuji International Workshop on Functional and Logic Programming,World Scientific. 254-269 (1995)
