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

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:

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