1991 Fiscal Year Annual Research Report
| Project/Area Number |
03640236
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
|
|---|
| 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月の日本数学会において(林晋氏と共同で)講演を行った。
|
-
[Publications] YASUGI,Mariko: "Syntactic properties of "hyper-terms"of transfinitely defined types (Abstract for Helsinki '90)" The Journal of Symbolic Logic. 56. 1150 (1991)
-
[Publications] Tsujii,Yoshiki: "Markov-self-similar sets" Hiroshima Mathematical Journal. 21. 491-519 (1991)
-
[Publications] HOSONO,Yuzo (E.Beretta): "Equilibrium of a phytoplankton in a laboratory controlled system" Survey on Mathematics for Industry.
-
[Publications] 八杉 満利子: "改訂増補 新数学事典(増補2.数学基礎論)" 大阪書籍株式会社, 5 (1991)
