文章基本信息

标题：Bounded Combinatory Logic
本地全文：下载
作者：Boris D{\"u}dder ; Moritz Martens ; Jakob Rehof 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2012
卷号：16
页码：243-258
DOI：10.4230/LIPIcs.CSL.2012.243
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem). k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic? Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k (and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k. Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.
关键词：Intersection types; Inhabitation; Composition synthesis