id: 06109837 dt: a an: 06109837 au: Düdder, Boris; Martens, Moritz; Rehof, Jakob; Urzyczyn, Pawel ti: Bounded combinatory logic. so: Cégielski, Patrick (ed.) et al., Computer science logic (CSL’12). 26th international workshop, 21th annual conference of the EACSL, September 3‒6, 2012, Fontainebleau, France. Selected papers based on the presentations at the conference. Wadern: Schloss Dagstuhl ‒ Leibniz Zentrum für Informatik (ISBN 978-3-939897-42-2). LIPICS ‒ Leibniz International Proceedings in Informatics 16, 243-258, electronic only (2012). py: 2012 pu: Wadern: Schloss Dagstuhl ‒ Leibniz Zentrum für Informatik la: EN cc: ut: intersection types; inhabitation; composition synthesis ci: li: doi:10.4230/LIPIcs.CSL.2012.243 ab: Summary: 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 \$τ\$, 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 \$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. rv: