Co-operative research on theoretical foundations of computer programs

计算机程序理论基础合作研究

• 批准号: 05302011
• 负责人: TSUJI Takashi
• 金额: $ 7.17万
• 依托单位: Chiba University (1995)University of Tsukuba (1993-1994)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Co-operative Research (A)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 1995
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-05302011/
• 关键词: NU; logic; theory of programs; programming; graph theory; artificial inteligence; music information processing; ν-転換; 時制算術; プログラム検証; 人工知能

Owing to each of research fellows, good research results are established on subjects of this research project. Some of them are listed in the following.1.Logic : a formal derivation of the decidability of the theory SA,extending intuitionistic linear logic, the finite model property for BCK and BCIW,algebraic semantics for predicate logic, decidability and finite model property of substructural logics, a new formalization of Feferman's system, natural proofs in automated proving, validity verification of knowledge predicats.2.Theory of programs : locomorphism analytical equivalence theory, analysis of a real time problem in a software/hardware system in two ways using nu-conversion and by tense arithmetic, literal dependence net in concurrent logic programming environment, a typed lambda-calculus of proving-by-example, a transformation method for dynamic-sized tabulation, programming by example.3.Programming : biding time analysis for data type specialization, programming techniques for effective use of pipe-line and cache, efficiency of computing determinants by a fraction-free processor.4.Graph theory : graph decomposition with prescribed vertices, twist number of complete bipartite praphs.5.Artificial inteligence : a mathematical theory of machine discovery from facs, formalization of planar graphs, analysis methods and tools of expression in music performances.

由于每位研究员的努力，本研究项目的课题都取得了良好的研究成果。其中一些列在下面。逻辑学：SA理论的可判决性的形式化推导，扩展直觉线性逻辑，BCK和BCIW的有限模型性质，谓词逻辑的代数语义，子结构逻辑的可判决性和有限模型性质，Feferman系统的一种新形式化，自动证明中的自然证明，知识谓词的有效性验证。2 .程序理论：运动解析等价理论，软件/硬件系统实时问题的两种分析方法：非转换和时态算法，并发逻辑编程环境中的文字依赖网络，类型化的实例证明演算，动态大小表的转换方法，实例编程。编程：数据类型专门化的等待时间分析，有效使用流水线和缓存的编程技术，无分式处理器计算决定因素的效率。图论：规定顶点的图分解，完全二部图的捻数。人工智能：从面部发现机器的数学理论，平面图形的形式化，音乐表演中的分析方法和表达工具。

项目成果

Igarashi,S.,Mizutani,T.,Tsuji,T.and Hosono,C.: "On locomorphism in analytical equivalence theory" Logic,Language and Computation,Lecture notes in computer science. 792. 173-187 (1994)

Igarashi,S.、Mizutani,T.、Tsuji,T. 和 Hosono,C.：“论分析等价理论中的同态”逻辑、语言与计算、计算机科学讲义。

清野桂子,五十嵐滋,辻尚史: "音楽の演奏表情の図形的表現についての考察" 1994年度応用数学合同研究会報告集. 7-1-7-4 (1994)

Keiko Seino、Shigeru Igarashi、Naofumi Tsuji：“关于音乐表达的图形表示的考虑”1994年应用数学联合研究小组报告7-1-7-4（1994年）

Yasugi,M.and Hayashi,S.: "A functional system with transfinitely defined types" Lecture Notes in Computer Science. 792. 31-60 (1994)

Yasugi,M. 和 Hayashi,S.：“具有超限定义类型的功能系统”计算机科学讲义。

Igarashi,S.: "Experiments on Computerized Piano Accompaniment" Proceedings of International Computer Music Conference. 415-417 (1993)

Igarashi,S.：“计算机钢琴伴奏实验”国际计算机音乐会议论文集。

富田康治: "ハードウェア・ソフトウェアシステムのtense arithmeticによる解析" 応用数学合同研究集会報告集. 37-42 (1993)

Yasuharu Tomita：“硬件和软件系统的紧张算术分析”应用数学联合研究会议报告37-42（1993）。