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: