論理の階層的構造と超限的型理論

逻辑的层次结构和超限类型理论

• 批准号: 06640338
• 负责人: 八杉 満利子
• 金额: $ 0.7万
• 依托单位: Kyoto Sangyo University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1994
• 资助国家: 日本
• 起止时间: 1994 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-06640338/
• 关键词: 型; 項; 構成的体系; 正規性; 型のモデル

当研究の主目的は、当申請者が提案した構成的解析学の体系(TRDB)と、その計算性を実現する超限的型理論(TRM)の諸関係の解明である。平成6年度の課題として、TRMの超限的型の集合論的意味付け、TRMのTRDBへの翻訳、TRDBからTRMへの写像と、その反対の写像の合成が恒等写像ではないことの証明、およびその意味の解明、などを提案し、予定通りの結果を得た。詳しくは、下記のとおりである。集合論の内包公理や帰納的集合の定義を使って、型の自然なモデルをつくる:型を論理式へ(とくに超限的型を超限帰納法で述語記号へ)写し、汎関数を証明図へ(とくにbar関数をbar帰納法へ)写す:TRDBとTRMの間の写像がたがいに逆写像になっていなくても、ある種の性質が保存されことを示す、など。さらにこのような体系と実際の数学との関連の考察のために、幾何学、整数論、解析学、などの専門家の協力をえた。とくに、構成的体系において微分積分法を展開することにより、区間解析の理論的基礎づけを与える端緒を得た。構成的世界では、有限の情報で数学を組み立てるので、関数の諸性質などは、区間上で決定される。見かけ上ふつうの微分積分法を展開しているような設定にして、そこからの情報は区間上でのみ得られるようにする。これらの成果は、証明論研究会(数理解析研究所短期共同研究集会)、Workshop on Constructivity,Computability,and Language(京都産業大学計算機科学研究所主催)などでも、発表した。

When the main purpose of the study is to clarify the relationship between the analytical system (TRDB) and the computational implementation of the application, the transfinite type theory (TRM) In 2006, the topic of TRM transfinite form set theory, TRM TRDB translation, TRM translation, TRDB translation, TRDB translation Details: ,. Set theory contains axioms and contains definitions of sets, types and natural expressions: types and logical expressions (transfinite types and transfinite expressions), universal relations and proofs (bar relations and bar expressions), TRDB and TRM, intermediate relations and inverse relations. A study of the relations between mathematics and reality, geometry, integer theory, analysis, and cooperation among families. The basic theory of interval analysis The composition of the world, finite information, mathematics, the establishment of, the nature of the number, interval, decision The differential integral method is used to set the information interval. The results of the Workshop on Constructivity,Computability,and Language, Kyoto Sangyo University, were presented at the Seminar on Proof Theory (Institute of Mathematical Analysis Short-term Joint Research Conference).

项目成果

正岡弘照: "Harmonic dimension of covering surfaces" Kodai Math.J.17. 351-359 (1994)

Hiroteru Masaoka：“覆盖表面的谐波维数”Kodai Math.J.17 (1994)。

村瀬 篤: "shintani function and its application to automorphic L-functions for classical groups:1" Math.Ann.299. 17-56 (1994)

Atsushi Murase：“shintani 函数及其在经典群自守 L 函数中的应用：1”Math.Ann.299 (1994)。

八杉満利子: "Interpretations of transfinite recursion and parametric abstraction in types" Words,Languages and Combinatorics(World Scientific). II. 452-464 (1994)

安杉真理子：“超限递归和类型中的参数抽象的解释”Words、Languages and Combinatorics（世界科学）II 452-464。

水原 亮: "Left symmetric algebras over a read reducitve Lie algebra" Acta Hum.et Sci.Univ.Sangyo kyot.(to appear).

Ryo Mizuhara：“在读还原李代数上的左对称代数”Acta Hum.et Sci.Univ.Sangyo kyot。（待发表）。

八杉満利子: "A functional system with transfinitely defined types" LNCS. 792. 31-60 (1994)

Mariko Yasugi：“具有超限定义类型的功能系统”LNCS. 792. 31-60 (1994)。