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:
(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 programIn 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.
Note: This version of Prolog has a tendency to create stack overflows and segfaults. The following are recommendations for this assignment: