Logic programs as types for logic programs
Logic programs as types for logic programs
复制标题
逻辑程序作为逻辑程序的类型
DOI：
10.1109/lics.1991.151654
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
Eyal Yardeni
中科院分区：
文献类型：
--
作者：
Thom W. Frühwirth;E. Shapiro;Moshe Y. Vardi;Eyal Yardeni
考虑逻辑程序的乐观型系统。在这样的系统中，类型是对程序谓词成功集的保守近似。提出了使用逻辑程序来描述类型。这种方法统一了描述类型系统的外延方法和操作方法，比以往的方法更简单、更自然。重点是使用一元谓词程序来描述类型。确定了一类合适的一元谓词程序，并证明了它的代价足以表达几种类型概念。通过与双向自动机的类比和与交替算法的对应，得到了类型推理和类型检查的复杂性刻画。这一特征通过使用逻辑程序来表示类型而变得容易。
Optimistic type systems for logic programs are considered. In such systems types are conservative approximations to the success set of the program predicates. The use of logic programs to describe types is proposed. It is argued that this approach unifies the denotational and operational approaches to descriptive type systems and is simpler and more natural than previous approaches. The focus is on the use of unary-predicate programs to describe the types. A proper class of unary-predicate programs is identified, and it is shown that it is expensive enough to express several notions of types. An analogy with two-way automata and a correspondence with alternating algorithms are used to obtain a complexity characterization of type inference and type checking. This characterization is facilitated by the use of logic programs to represent types.<<ETX>>