CS 394P: Program Synthesis by Deduction

Due: May 4, 2005.

The purpose of this assignment is to experiment with deductive synthesis of programs that consist of calls to subroutines from a library, similar to the programs synthesized by Amphion (Stickel et al.).

Axioms are written that describe what each library subroutine does. Programs are specified by stating a set of facts, such as the types of inputs, then stating the goal of the program. Proof of the goal results in a series of subroutine calls that compute the goal from the inputs; the proof can then be converted into a program. Deduction converts the specification of what the program should do into a plan for how to do it; the axioms represent codified knowledge about the procedures in the program library.

For this assignment, we will use as our deduction engine a version of Prolog written in Lisp, as described by Paul Graham in his book On Lisp. This Prolog is obtained by loading the file onlisp.lisp, then loading onlispfix.lisp . A set of axioms for a library of navigation programs is contained in the file navrules.lsp . The file onlispex.lisp contains some examples from the book that illustrate how the Prolog works.

For our application domain, we will use the domain of navigation on a plane (including local areas on Earth), which can be considered to be a simpler version of the Amphion astronomical navigation domain. There are many different ways of specifying positions and movements on the plane; library subroutines are provided to convert representations, model movements, and calculate distances and directions. Deductive synthesis allows us to produce programs that work with a variety of data forms.

The data formats that we will use include:

Several operations and computations are defined:

A program is produced by stating facts (such as the types of variables), stating the goal of the program, and calling do-program. do-program calls the prover to infer a method of achieving the goal, then converts the result into a Lisp function and defines it. For example:

  (<- (xy-data 'a))                      ; type of input var a
  (<- (rth-data 'b))                     ; type of input var b
  (<- (program1 ?d) (distance 'a 'b ?d)) ; program1 is distance from a to b
  (do-program 'program1 '(a b)) )        ; do it and make the program
In this example, the types of two input variables of the program, a and b, are declared first. The next axiom declares that ?d is the result for program1 if ?d is the distance between a and b. The final line calls do-program, which will call the prover to derive a way of accomplishing the goal, then convert the result into a program. The arguments of do-program are the program name and the argument list for the program. Several example program specifications are shown in the file navrules.lsp .

Assignment: Be sure to use different variable names for each program so that the type of a variable is not declared to be two different types.

  1. Examine the rules and code in navrules.lsp and try the examples shown in comments.
  2. Make a program to find the distance between a range-bearing point and a distance-direction point. Use the program to find the distance between (10 60) and (12 NE).
  3. A trip starts at a city and travels a specified distance-direction. Find the bearing from the resulting position to another city. Use the program to find the bearing to San Antonio after starting at Austin and traveling 70000 meters W.
  4. A helicopter starts at Austin and flies 80000 meters at bearing 20 to pick up a clue; then it flies 100000 meters NW and picks up a treasure. Find the range and bearing to take the treasure to Dallas. Make a program for problems of this type, then use it to solve the problem.

Note: This version of Prolog has a tendency to create stack overflows and segfaults. The following are recommendations for this assignment: