1997 Fiscal Year Annual Research Report
| Project/Area Number |
09640248
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
寶来 正子 東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)
|
|---|
| Keywords | 単純型理論 / ラムダ計算 / 単一化問題 / マッチング問題 / 帰納的関数 / 原始帰納法 |
|---|
| Research Abstract |
1.型理論における項の単一化問題については,その部分問題であるマッチング問題に焦点を当て,大学院学生と共に研究を行った.その結果,これまでに知られている,変数の型が4段以下のマッチング問題に対する結果を整理し,5段以上の高階のマッチング問題の特殊な場合について,解が存在するか否かと存在する場合はその解の一つを返すアルゴリズムを示すことが出来た.次年度以降は,この特殊な場合に対する我々の考え方を,より興味あるその他の場合に拡張することを目指したい.
2.型理論の表現力を帰納的関数論の立場から考察する問題については以下の成果を得た.(1)まずはじめに,自由代数の元に限らず,それを拡張した自由代数上の1階述語論理の項に対する関数に注目し,そのような関数のうちで単純型理論で表現可能なものを,帰納的関数論における原始帰納法の考え方を用いて特徴付ける結果を得た.(2)次に,この結果を用いて,自由代数上の関数に対する二つの表現定理を得た.なお,今回の研究の過程で,自由代数上の関数に対する表現力についてこれまで知られているZaioncの定理の証明に重大な誤りがあることに気付き,そのことを反例をもって示した.Zaiocの定理は証明が非常に煩雑であり,そのことがこのような誤りの原因となっていると思われるが,それに対して我々の表現定理の証明は,論理的に明解で見通しが非常に良いことが特徴的である.その見通しの良さは,我々が自由代数上の関数に取り組む前に,前述のように,まず視野をより広い世界に拡張し,そこでの議論を踏まえて行ったために得られたものであると考えられる.本研究の成果は,本年4月に開かれる国際学会で発表の予定である.
|
Research Products
(1 results)
