| Project/Area Number |
03640236
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
|
|---|
| Project Period (FY) |
1991
|
| Project Status |
Completed (Fiscal Year 1991)
|
| Budget Amount *help |
¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 1991: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | 構成的数学の体形 / 超限帰納法 / 汎関数の体系 / 超限的型理論 / バ-帰納法 / 正規化 |
|---|
| Research Abstract |
0.TRDBと略記される構成的数字の体系(一階算術HAにVf,transfinite recursionで定義される速語H、bar inductionを加えたもの)と、transfinitely defined typesを持つ.bar recursionをベ-スにした汎関数の体系TRMの相互関係を明らかにし、TRDBのformulaをtype,proofをtermと考えたときのTRDBの計算性の意味を明確にすることが目標であった。その目標はすべて達成され、現在論文作製中である。龍谷大学の林晋氏との共同研究である。なお他に広い意味の研究協力者たちもあり、その成果も発表論文の項目に記す。以下研究内容を詳細する。
1.TRMのtypeの集合論的モデルを構成。(typeのdegrllに関する超限帰納法による。また、それがtermの構成と整合的であることを示した。
2.TRMの有限のtypeのtermの特徴づけ。
3.TRDBをCurryーHoward型の写像でTRMに写し、TRDBの正規化がTRMの正規化に写されること、および、過去に行った、modified realizability interpretationと同じtermが得られることを示した。なお、このTRDBは、前年度までの体系よりは一般化されているが、それでも同様の結果が得られることが分った。
4.既存の還元法による無予盾性証明との関連は、還元のプロセスをtermの還元と考えて、証明図のdegreeに関する超限帰納法とbar inductionによってTRMへの埋め込みを考える。この点はまだ研究続行中である。
なお中間報告の意味でLogic Colloquium '90(Helsinki)に演題を出し、また平成3年4月の日本数学会において(林晋氏と共同で)講演を行った。
|
