A Framework for Quantitative Program Synthesis

Herbert Wiklicky

We present a methodology which recasts program synthesis problems in a purely quantitative framework based on concepts in continuous (non-linear) rather than discrete optimisation. The first element of this is the representation of the semantics of deterministic (and probabilistic) programs as linear operators, or in the finite case simply as matrices. This allows us to identify (probabilistic) program sketches or, to be precise, their semantics as elements of an appropriately parameterised manifolds of such operators. The synthesis problem can then be interpreted in this setting as a non-linear, global optimisation problem. We illustrate this approach via a number of examples which involve functional as well as non-functional program properties.