Introduction to Program Synthesis

© Armando Solar-Lezama. 2018. All rights reserved.

Assignment 3

Submission deadline has been extended to Monday Nov 19 to account for schedule slippage.

Submission Instructions This assignment is due at 5pm on the date indicated in the class calendar. The starter code for the assignment can be found here (only for problem 2). In order to submit your code, pack your Assignment3.js, default.html and part2.sq, part1.sq files into a tar file and submit through stellar (same as last time).

Collaboration: You are allowed to collaborate with one other person for this assignment, but each of you is responsible for submitting your own solution. If you do collaborate with someone else, make sure to name your collaborator in your submission.

If you have any questions, please ask!

Problem 1 (35 pts)

Your goal is to use Synquid to synthesize some non-trivial functions. We suggest that you first study the tutorial examples in the interactive Synquid demo.

Your goal for this exercise is to develop a function that can serialize a binary search tree into a sorted list. Below are the definitions of the two main datastructures. The code block also includes some useful measures that will be helpful for the transformation. data BST a where Empty :: BST a Node :: x: a -> l: BST {a | _v < x} -> r: BST {a | x < _v} -> BST a data SortedList a where Nil :: SortedList a Cons:: x: a -> xs:SortedList { a | _v < x } -> SortedList a termination measure height :: BST a -> {Int | _v >= 0} where Empty -> 0 Node x l r -> 1 + if (height l) < (height r) then (height r) else (height l) measure keys :: BST a -> Set a where Empty -> [] Node x l r -> keys l + keys r + [x] measure vals :: SortedList a -> Set a where Nil -> [] Cons x xs -> vals xs + [x]

Part a)

Your goal for this part of the assignment is to synthesize a function transform: BST a -> SortedList a that takes in a BST defined as above, and outputs a SortedList containing the exact same values. You need to set up the synthesis problem so that Synquid synthesizes the transform function with the desired property. For this part, you are allowed to use a component merge that takes as input two sorted lists and produces a merged sorted list that contains all the elements in the two input lists. You do not have to synthesize merge, you are only providing its interface.

Part b)

For this part of the assignment, your goal is to synthesize a version of transform that does not use the merge function from earlier. Instead, you will have to synthesize a helper function helper:: BST a -> SortedList a -> SortedList a. The high-level intuition is that the helper function takes as the second input a partially constructed list SortedList a and produces its output by appending all the elements in the BST to the partially constructed list. Note that this imposes some strong constraints on the types of helper. For example, since all the elements in the BST will be appended to the SortedList, it is important that all the elements in the SortedList be less than all the elements in the BST.


Part b) is significantly harder than part a), but here are a few hints that will help you solve this.

You should submit your answers to this problem in two separate files named part1.sq and part2.sq.

Problem 2 (65 pts)

This problem is about quantitative synthesis. Your goal for this assignment is to extend the simple enumerative synthesizer from Assignment 1 with a probabilistic grammar for the expression language. Recall that the grammar from that original assignment was the grammar shown below. expr:= num(int n).....................// numeric constant num:int | flse()...........................// constant FALSE. Unfortunately ,we can't call it false | vr(string varname)...............// variable var:int | plus(expr left, expr right)......// arithmetic expressions plus and times | times(expr left, expr right).....// plus(int,int):int times(int, int):int | lt(expr left, expr right)........//less than operator lt(int, int):int | and(expr left, expr right).......// boolean operators and(bool,bool):bool | not(expr left)...................// not(bool):bool | ite(expr cond, expr tcase, expr fcase)...// if-then-else; ite(bool, int, int):int Your goal will be to write a synthesis procedure that takes as a parameter a probability function p(t1, pos, t2), which will provide the probability that a node of type t1 is a child in the position pos of a node of type t2. So for example, p(vr, 0, plus) is the probability that a plus node has a vr node as its first parameter (in the zero position). You can assume that nodes that don't type-check would have probability zero, so for example p(plus, 0, ite)=0.0. Also, $\forall i,m \sum_n p(n, i, m) = 1.0$. In other words, for any parent node m, for any position i that is valid for that parent, the sum of the probabilities of all child nodes n must add to $1.0$.

Your goal is to modify the basic bottom-up enumeration algorithm to ensure that it returns the correct expression with the highest probability.