Abstract
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 PSPACEcomplete 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 LinialPost theorem).
kbounded 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 kbounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in kbounded combinatory logic?
Our main result is that the problem is (k+2)EXPTIME complete for kbounded combinatory logic with intersection types, for every fixed k
(and hence nonelementary when k is a parameter). We also show that the problem is EXPTIMEcomplete 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.
BibTeX  Entry
@InProceedings{ddder_et_al:LIPIcs:2012:3676,
author = {Boris D{\"u}dder and Moritz Martens and Jakob Rehof and Pawel Urzyczyn},
title = {{Bounded Combinatory Logic}},
booktitle = {Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL},
pages = {243258},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897422},
ISSN = {18688969},
year = {2012},
volume = {16},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3676},
URN = {urn:nbn:de:0030drops36763},
doi = {10.4230/LIPIcs.CSL.2012.243},
annote = {Keywords: Intersection types, Inhabitation, Composition synthesis}
}
Keywords: 

Intersection types, Inhabitation, Composition synthesis 
Collection: 

Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL 
Issue Date: 

2012 
Date of publication: 

03.09.2012 