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:

xy-data is a list (x y). The corresponding predicate is cartesian:
(cartesian ?p ?q) means that ?q is the Cartesian equivalent of ?p.
rth-data is a list (r theta) where theta is in radians, measured counter-clockwise from the x axis. The corresponding predicate is polar.
rb-data is a list (range bearing) where bearing is in degrees, measured clockwise from north.
dd-data is a list (distance direction) where direction is a compass direction such as N, S, E, W, NE, etc.
lat-long is a list (latitude longitude) where the values are in floating degrees; negative longitude denotes west longitude.
UTM or Universal Transverse Mercator is a way of representing positions on Earth that locally maps locations to a flat, Cartesian x-y grid. UTM is a list (easting northing) where the values are in meters. northing is meters north of the equator and easting is meters east on a six-degree strip of longitude.
city is a symbol, such as austin.

Several operations and computations are defined:

(distance ?a ?b ?d) means that ?d is the distance between point ?a and point ?b.
(bearing ?a ?b ?d) means that ?d is the bearing from point ?a to point ?b.
(range-bearing ?a ?b ?d) means that ?d is the range and bearing from point ?a to point ?b.
(movefrom ?a ?b ?c) means that point ?c is the result of moving from point ?a by an amount ?b.

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:

(progn
  (<- (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.

Examine the rules and code in navrules.lsp and try the examples shown in comments.
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).
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.
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:

Use /p/bin/xgcl on a Linux machine.
Immediately after starting GCL, enter (setq si::*multiply-stacks* 50) to make the runtime stack 50 times (!) as large as normal.
If you get a stack overflow or segfault, restart Lisp and try again. It may be advisable to do each part of the assignment separately.