Finite Combinatory Logic with Intersection Types
Finite Combinatory Logic with Intersection Types
复制标题
具有交集类型的有限组合逻辑
DOI：
10.1007/978-3-642-21691-6_15
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
P. Urzyczyn
中科院分区：
文献类型：
--
作者：
J. Rehof;P. Urzyczyn
组合逻辑基于肯定前件和公理的示意性（多态）解释。在本文中，我们建议在公理不是示意性地解释而是“字面地”解释（对应于类型的单态解释）的限制下考虑表达组合逻辑。由此，我们得到了有限组合逻辑，它是严格有限公理化的，并且仅基于必然前件。我们证明了具有交集类型的有限组合逻辑的可证明性（居住）问题在有或没有子类型的情况下是 Exptime-complete 的。这个结果与一般情况形成对比，一般情况下，已知居住在等级 2 中是 Expspace-complete 的，而等级 3 及以上的居住是不可判定的。作为存在子类型的考虑因素的副产品，我们表明标准交集类型子类型位于 Ptime 中。从应用程序的角度来看，我们可以将交叉类型视为一种表达规范形式，我们的结果表明功能组合合成可以自动化。
Combinatory logic is based on modus ponens and a schematic (polymorphic) interpretation of axioms. In this paper we propose to consider expressive combinatory logics under the restriction that axioms are not interpreted schematically but "literally", corresponding to a monomorphic interpretation of types. We thereby arrive at finite combinatory logic, which is strictly finitely axiomatisable and based solely on modus ponens. We show that the provability (inhabitation) problem for finite combinatory logic with intersection types is Exptime-complete with or without subtyping. This result contrasts with the general case, where inhabitation is known to be Expspace-complete in rank 2 and undecidable for rank 3 and up. As a by-product of the considerations in the presence of subtyping, we show that standard intersection type subtyping is in Ptime. From an application standpoint, we can consider intersection types as an expressive specification formalism for which our results show that functional composition synthesis can be automated.