Synthesis of string transformations.
String transformations are one of the main targets of program synthesis.
Gulwani showed they could be synthesized from input-output examples [1]} and introduced the idea of using a DSL to aid synthesis.
Optician extended the DSL-based idea to synthesizing lenses [2]}, [3]}, which are programs that transform between two formats.
Optician supports not only examples but also input-output types.
While DSL-based approaches provide good performance, they are also monolithic as they rely on the structure of the DSL to search efficiently.
astra does not rely on a DSL and can synthesize string transformations from complex specifications that cannot be handled by DSL-based tools.
Moreover, transducers allow applying verification techniques to the synthesized programs (e.g., checking whether two solutions are equivalent).
One limitation of transducers is that they do not have `memory', and consequently astra cannot be used for data-transformation tasks where this is required—e.g., mapping the string Firstname Lastname to Lastname, Firstname—something Optician can do.
We remark that there exist transducer models with such capabilities [4]} and our work lays the foundations to handle complex models in the future.
