PV2 ⊧ Synducegenerates equivalent recursive functions when migrating from one data structure to another

Application domain/field

• Program synthesis
• Recursive functions
• Recursive data types
• Bounded model checking

Type of tool

Synthesis tool

Expected input

• Input reference (recursive) function, this precisely describes the functionality
• Recursion skeleton, i.e. traversal plan over the new recursive data type
• Representation function, a mapping that converts an instance of the old data type to the new data type

Format:

One of the following:

• a syntax for pattern-matching recursion schemes (PRMS) (.pmrs file)
• OCaml (.ml file)

Expected output

Recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton.

Internals

The context that they consider is one where you have two data types A and B. You have implemented a recursive function for A, and now want to implement this for B. Synduce uses bounded model checking to check the validity of a synthesis solution. Uses Z3 and CVC4.

Comments

License: MIT