Program Synthesis and Linear Operator Semantics

TL;DR

This paper introduces a novel approach to program synthesis and optimization by representing program semantics as linear operators, enabling compositional analysis and optimization of deterministic and probabilistic programs.

Contribution

It presents a new linear algebraic framework for program semantics, facilitating automatic generation and composition of program blocks for synthesis and optimization.

Findings

Representation of program semantics as matrices for deterministic and probabilistic programs

Automated generation of elementary block semantics

Application of abstract interpretation in a linear algebraic setting

Abstract

For deterministic and probabilistic programs we investigate the problem of program synthesis and program optimisation (with respect to non-functional properties) in the general setting of global optimisation. This approach is based on the representation of the semantics of programs and program fragments in terms of linear operators, i.e. as matrices. We exploit in particular the fact that we can automatically generate the representation of the semantics of elementary blocks. These can then can be used in order to compositionally assemble the semantics of a whole program, i.e. the generator of the corresponding Discrete Time Markov Chain (DTMC). We also utilise a generalised version of Abstract Interpretation suitable for this linear algebraic or functional analytical framework in order to formulate semantical constraints (invariants) and optimisation objectives (for example performance requirements).