Synthesis with Asymptotic Resource Bounds

TL;DR

This paper introduces a novel synthesis method that automatically generates recursive programs satisfying both functional specifications and asymptotic resource bounds using a type system and big-O notation.

Contribution

It presents a new synthesis approach that handles asymptotic resource bounds with a type system, enabling the synthesis of complex divide-and-conquer algorithms.

Findings

Successfully synthesized complex divide-and-conquer programs

Handles asymptotic resource bounds using big-O notation

Outperforms prior solvers in complexity of programs synthesized

Abstract

We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity O(nlog(n)). Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, SynPlexity, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.