TY - GEN
T1 - Bounded combinatory logic
AU - Düdder, Boris
AU - Martens, Moritz
AU - Rehof, Jakob
AU - Urzyczyn, Paweł
PY - 2012/12/1
Y1 - 2012/12/1
N2 - 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). Bounded combinatory logic (BCLk) 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 BCLk: Given an arbitrary set of typed combinators and a type τ, is there a combinatory term of type τ in k-bounded combinatory logic? Our main result is that the problem is (k + 2)-EXPTIME complete for BCLk 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.
AB - 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). Bounded combinatory logic (BCLk) 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 BCLk: Given an arbitrary set of typed combinators and a type τ, is there a combinatory term of type τ in k-bounded combinatory logic? Our main result is that the problem is (k + 2)-EXPTIME complete for BCLk 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.
KW - Composition synthesis
KW - Inhabitation
KW - Intersection types
UR - http://www.scopus.com/inward/record.url?scp=84880198028&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2012.243
DO - 10.4230/LIPIcs.CSL.2012.243
M3 - Article in proceedings
AN - SCOPUS:84880198028
SN - 9783939897422
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 243
EP - 258
BT - Computer Science Logic 2012 - 26th International Workshop/21th Annual Conference of the EACSL, CSL 2012
T2 - 26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL
Y2 - 3 September 2012 through 6 September 2012
ER -