Forskning ved Københavns Universitet - Københavns Universitet

Forside

Bounded combinatory logic

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfæ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.

OriginalsprogEngelsk
TitelComputer Science Logic 2012 - 26th International Workshop/21th Annual Conference of the EACSL, CSL 2012
Antal sider16
Publikationsdato1 dec. 2012
Sider243-258
ISBN (Trykt)9783939897422
DOI
StatusUdgivet - 1 dec. 2012
Begivenhed26th 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. 20126 sep. 2012

Konference

Konference26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL
LandFrankrig
ByFontainebleau
Periode03/09/201206/09/2012
NavnLeibniz International Proceedings in Informatics, LIPIcs
Vol/bind16
ISSN1868-8969

ID: 230702092