制約に基づく汎用型推論モジュールの研究

基于约束的通用推理模块研究

• 批准号: 12780216
• 负责人: 西村 進
• 金额: $ 1.66万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2001
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12780216/
• 关键词: 型推論; 多相型; 制約解消; 制約

型推論は、プログラム中に潜むエラーを実行前の段階で捕捉するための重要な技術である。しかし、従来の型推論のアルゴリズムは、対象とする個々の型体系に対して与えられ、しかもそれは型体系がより豊かになればなるほど複雑になる傾向にあった。とくに、多相型を含む型体系において、多相型の型推論を一般的に記述する方法が求められていた。このような問題を解決するため、Odersky, Sulzmann, Wherらは、制約系をベースとしたより一般的な型体系の枠組みであるHM(X)を提案した。しかしながら、HM(X)では、多相型の型付けは制約系によっては特徴づけられていなかった。本研究では、Odersky, Sulzmann, Wherらの研究をふまえ、多相型の型付けをも制約系によって特徴づけするような、型体系を記述する一般的な枠組みを提案した。この枠組みの中では、適切な制約系とその制約解消器を与えれば自動的に型推論アルゴリズムが得られる。この枠組みのなかでは、多相型の型付けを表す汎用的な制約が導入され、この制約を解くことにより型推論を行うことができる。この汎用的型推論の枠組みにおいては、型推論はより柔軟な多相型の使用を可能にする。例えば、分散アプリケーションやトップダウンのプログラム開発など、必ずしも型の定義が先に得られないような場合でも、多相型を扱うことができるようになる。これらの結果を著した論文は、日本ソフトウェア学会学会誌に採録された。

Type inference: The key technology of the stage before the implementation The type of inference is based on the tendency of the type system to be complex. However, in a multi-phase system including multi-phase systems, there is a need for a general method to describe multi-phase type inferences. Odersky, Sulzmann, Wher, Constraint System, General Type System, HM(X) The characteristic of HM(X) is that it is a polyphase type and a constraint system. In this study, Odersky, Sulzmann, Wher, the study of polyphase type control systems, characteristics, and general type control systems are described. In this case, the appropriate constraint system and the constraint canceller are automatically inferred. This is a combination of polyphase and polyphase type constraints. These constraints are generally used in the introduction of polyphase type constraints. This general type inference is based on the possibility of using soft multiphase models. For example, in case of dispersion, dispersion. The results of this paper were recorded in the Journal of the Japanese Society of Science and Technology.

项目成果

西村進: "制約によるパラメータ多相型推論"コンピュータソフトウェア. (発表予定).

Susumu Nishimura：“基于约束的参数多态推理”计算机软件（待提交）。

西村 進: "制約によるパラメータ多相型推論"コンピュータソフトウェア. 18・2. 20-39 (2001)

Susumu Nishimura：“基于约束的参数多态推理”计算机软件18・2。