Arrow Research search

Author name cluster

Moritz Martens

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
2 author rows

Possible papers

2

Highlights Conference 2013 Conference Abstract

Combinatory Logic synthesis and alternation

  • Boris Düdder
  • Moritz Martens
  • Jakob Rehof:

We discuss complexity theoretic results in the context of Combinatory Logic Synthesis which is a new approach to component-based synthesis using type inhabitation. The complexity theoretic reductions behind these results establish explicit and effective connections between combinatory logic inhabitation and automata theoretic models, in the form of alternating tree automata and alternating space bounded Turing machines. These computational models that are commonly found in automata theoretic approaches are related to synthesis based on logics within the MSO family of logics.

PDF Details

CSL Conference 2012 Conference Paper

Bounded Combinatory Logic

  • Boris Düdder
  • Moritz Martens
  • Jakob Rehof
  • Pawel Urzyczyn

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 tau, is there a combinatory term of type tau 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.

Details