Type Inference by Coinductive Logic Programming
Type Inference by Coinductive Logic Programming
复制标题
通过共归纳逻辑编程进行类型推断
DOI：
10.1007/978-3-642-02444-3_1
复制
发表时间：
2009
影响因子：
2.6
通讯作者：
E. Zucca
中科院分区：
文献类型：
--
作者：
D. Ancona;Giovanni Lagorio;E. Zucca
我们提出了一种基于共同传感逻辑的基于约束类型推理的新方法。约束生成对应于转换为horn子句p的结合，而约束满意度是根据p的共同感应性赫布兰德模型来定义的。我们通过正式定义类似于对象轻量级Java的小型语言的翻译来说明方法，该语言可以省略字段和方法声明中的类型注释。
通过这种方式，我们获得了非常精确的类型推理，并为面向对象的程序的类型推理提供了新的见解。由于该方法是故意声明的，因此我们实际上定义了一类算法的正式规范，这对于研究人员来说可能是有用的路线图。
此外，尽管我们在这里考虑了一种特定的语言，但该方法通常可以用于提供各种编程语言的类型推断的抽象规范。
We propose a novel approach to constraint-based type inference based on coinductive logic. Constraint generation corresponds to translation into a conjunction of Horn clauses P , and constraint satisfaction is defined in terms of the coinductive Herbrand model of P . We illustrate the approach by formally defining this translation for a small object-oriented language similar to Featherweight Java, where type annotations in field and method declarations can be omitted.
In this way, we obtain a very precise type inference and provide new insights into the challenging problem of type inference for object-oriented programs. Since the approach is deliberately declarative, we define in fact a formal specification for a general class of algorithms, which can be a useful road map to researchers.
Furthermore, despite we consider here a particular language, the methodology could be used in general for providing abstract specifications of type inference for different kinds of programming languages.