Bounded combinatory logic
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Titel | Computer Science Logic 2012 - 26th International Workshop/21th Annual Conference of the EACSL, CSL 2012 |
Antal sider | 16 |
Publikationsdato | 1 dec. 2012 |
Sider | 243-258 |
ISBN (Trykt) | 9783939897422 |
DOI | |
Status | Udgivet - 1 dec. 2012 |
Eksternt udgivet | Ja |
Begivenhed | 26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL - Fontainebleau, Frankrig Varighed: 3 sep. 2012 → 6 sep. 2012 |
Konference
Konference | 26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL |
---|---|
Land | Frankrig |
By | Fontainebleau |
Periode | 03/09/2012 → 06/09/2012 |
Navn | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Vol/bind | 16 |
ISSN | 1868-8969 |
ID: 230702092