CS 378 Assignment 5: Program Synthesis by Deduction

Due: November 5, 2024.

Files:

navload.clj Function (navload) to load files
cs378.clj CS 378 functions
utmtrans.clj Functions for UTM translation
navfns.clj Navigation functions
unify.clj Unification and Backchaining, plus rules for navigation functions
nav.clj File with test cases for this assignment
navresult.txt Example results

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 function 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 symbolic knowledge about the functions in the program library.

For this assignment, we will use as our deduction engine a backchaining prover for first-order logic written in Clojure. A set of axioms for a library of navigation programs is contained in the file unify.clj .

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 r is a distance and theta is in radians, measured counter-clockwise from the x axis. The corresponding predicate is polar: (polar p q) means that q is the polar equivalent of p.
rb-data is a list (range bearing) where range is a distance and 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 of the center of a six-degree strip of longitude, plus 500000.
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. Usually you will make all the arguments of movefrom be constants (functions of no arguments), e.g., (movefrom (a) (b) (zzz)) says that point (zzz) is the result of moving from point (a) by an amount (b). Most constants in the logic forms correspond to input variables in the program.

A program is produced by the call:

(fnfor fn vars goal facts rules)

fn is the name of the desired function.
vars is a list of input variables.
goal is a predicate stating the goal of the program.
facts is a list of facts, such as input variable types.
rules is the set of navigation rules, navr .

fnfor calls the backchaining prover to infer a method of achieving the goal, then converts the proof into a Clojure function and calls eval to define it.

(def nav1 '( ((xy-data (a)))    ; type of input var a is xy-data
             ((rth-data (b)))   ; type of input var b is rth-data
             ))

(fnfor 'test1 '(a b) '(distance (a) (b) z) nav1 navr)
                     ; distance from a to b is z

In this example, the types of two input variables of the program, (a) and (b), are declared as facts. In the logic notation, the input variables such as b are written using parentheses, i.e. (b), which represent constants (functions of no variables) in logic. The two input variables are treated as constants for the logic form since they are inputs. The goal declares that z is the result if z is the distance between input variables (a) and (b). Proving the goal by backchaining results in the predicate

(distance (a) (b) (euclidist (a) (rth2xy (b))))

This is converted into the function:

(defn test1 [a b] (euclidist a (rth2xy b)))

This function can now be used on data:

user=> (test1  '(10 10) (list 30 (/ Math/PI 6)))

16.74469341998643

Several example program specifications are shown in the file nav.clj . The file unify.clj has rules that describe what the navigation library functions do; these functions are in the files navfns.clj and utmtrans.clj .

Assignment:

The file navload.clj has the function (navload) to load the necessary files. Edit this function as needed for your files.

The file nav.clj contains stubs for each program specification; use the input variable names as shown in the stubs.

Examine the rules and code in navfns.clj and try the examples test1 to test3 as shown in comments in nav.clj .
Fill in the stubs in the file nav.clj and turn in the completed file.
Make test4 to find the distance between two cities. Use the program to find the distance (in meters) from austin to dallas.
Make test5 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: test6. 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 test7 for problems of this type, then use it to solve the problem.
test8 should find the range and bearing from one city to another. Find the range and bearing from Austin to Waco and Austin to Dallas.