Algorithmic aspects of type-based program synthesis

Abstract

In the area of type-based program synthesis, the decision problem of inhabitation (given a type environment Gamma and a type tau, is there a term M such that M can be assigned the type tau in Gamma?) corresponds to existence of a program (term M) that satisfies the given specification (type tau) under additional assumptions (type environment Gamma).

Inhabitation in typed lambda-calculi can be seen as functional program synthesis from scratch. Complementarily, inhabitation in combinatory logic can be seen as domain-specific program synthesis. Further restrictions on inhabitant search, such as principality and relevance restrictions, yield inhabitants that are more closely tied to given specifications. Alternatively, dimension, rank, order, and arity restrictions provide means to control the complexity of inhabitant search.

This work provides an overview over following results in type-based program synthesis: PSpace-completeness of principal inhabitation in the simply typed lambda-calculus, undecidability of inhabitation in lambda-calculus with intersection types, undecidability of inhabitation in lambda-calculus with intersection types in bounded dimension, undecidability of inhabitation in subintuitionistic combinatory logic, (o+2)-ExpTime-completeness of inhabitation in combinatory logic with intersection types with instantiation of bounded order o, and ExpTime-hardness of intersection type unification.