# 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.