Version Space Algebras are Acyclic Tree Automata

TL;DR

This paper demonstrates that version space algebras can be embedded into nondeterministic finite tree automata, revealing that tree automata are a more general framework for representing large program spaces efficiently.

Contribution

It provides a linear-time semantics-preserving embedding of version space algebras into nondeterministic finite tree automata, establishing a unifying theoretical foundation.

Findings

Version space algebras are a special case of nondeterministic finite tree automata.

Tree automata generalize recent approaches like e-graphs for program space representation.

The embedding preserves semantics and is computationally efficient.

Abstract

Version space algebras are ways of representing spaces of programs which can be combined using union, intersection, and cross-product/``join" operators. In their reified form as ASTs with explicit union and join nodes, they have the ability to compactly represent exponentially-large spaces of programs, owing to which they have become become the most popular approach to enumerative program synthesis since the introduction of FlashFill in 2010. We present a linear-time semantics-preserving constructive embedding from version space algebras into nondeterministic finite tree automata, showing that the former are but a special case of the latter. Combined with recent results finding a correspondence between e-graphs and minimal deterministic tree automata, this shows that tree automata are strict generalizations of all recent major approaches to efficiently representing large spaces of programs by sharing.