Augmenting Type Signatures for Program Synthesis

TL;DR

This paper proposes a method to enhance program synthesis by encoding additional property relations to better utilize type signatures, enabling the synthesis of complex programs with minimal primitives.

Contribution

It introduces a system of property relations that augment type signatures, improving search space reduction in program synthesis.

Findings

Successfully synthesized complex programs using minimal primitives.

Encoding property relations improves search efficiency.

Method applicable in novel synthesis contexts.

Abstract

Effective program synthesis requires a way to minimise the number of candidate programs being searched. A type signature, for example, places some small restrictions on the structure of potential candidates. We introduce and motivate a distilled program synthesis problem where a type signature is the only machine-readable information available, but does not sufficiently minimise the search space. To address this, we develop a system of property relations that can be used to flexibly encode and query information that was not previously available to the synthesiser. Our experience using these tools has been positive: by encoding simple properties and by using a minimal set of synthesis primitives, we have been able to synthesise complex programs in novel contexts