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

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

• 批准号: 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らの研究をふまえ、多相型の型付けをも制約系によって特徴づけするような、型体系を記述する一般的な枠組みを提案した。この枠組みの中では、適切な制約系とその制約解消器を与えれば自動的に型推論アルゴリズムが得られる。この枠組みのなかでは、多相型の型付けを表す汎用的な制約が導入され、この制約を解くことにより型推論を行うことができる。この汎用的型推論の枠組みにおいては、型推論はより柔軟な多相型の使用を可能にする。例えば、分散アプリケーションやトップダウンのプログラム開発など、必ずしも型の定義が先に得られないような場合でも、多相型を扱うことができるようになる。これらの結果を著した論文は、日本ソフトウェア学会学会誌に採録された。

类型推断是在执行前阶段捕获程序中隐藏的错误的重要技术。但是，传统的类型推理算法是对单个类型感兴趣的系统的，并且随着类型系统的富裕程度越复杂。特别是，需要一种描述包括多相类型的类型系统中多相类型的类型推断的方法。为了解决这个问题，Odersky，Sulzmann，Wher和其他人提出了一个基于约束系统的更通用的系统框架。但是，在HM（X）中，多相类型键入并未以约束系统为特征。在这项研究中，根据Odersky，Sulzmann和Wher的工作，我们提出了一个描述类型系统的一般框架，该框架还表征了由约束系统键入的多相类型。在此框架内，可以通过提供适当的约束系统及其约束解散设备来自动获得类型的推理算法。在此框架内，引入了代表多相类型键入的一般约束，可以通过求解这些约束来执行类型推理。在此一般类型推理框架中，类型推理允许使用更灵活的多相类型。例如，即使在不一定首先获得类型定义的情况下，例如在分布式应用程序或自上而下的程序开发中，也可以处理多相类型。撰写这些结果的论文是在日本软件学会杂志上收集的。

项目成果

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

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

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

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