Routing - the Euclidean bottleneck traveling salesman problem - FAQ

Purpose of exercise

• Practice writing equation-based programs
• Use engineering analysis to deal with numerical approximations
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Coach the ACL2 mechanical logic to verify software properties

Activities

• Define the following functions
• Package the functions you define as a book.
• DoubleCheck the properties stated below
• Use ACL2 to prove the properties
• Package the theorems as a book.

Requirements

1. Define a function insert-everywhere that, given a value x and a list xs, delivers a list xss whose elements are all like xs, but with x inserted among the elements. The list xss must contain one more element than xs, and for each index k, there must be a list in xss whose element of index k is x. (That is, the list xss must contain versions of xs with x in all possible positions.) The order of the lists in xss is is immaterial. For example, the value of (insert-everywhere 1 '(2 3)) could be ((1 2 3) (2 1 3) (2 3 1)), or it could be ((2 3 1) (2 1 3) (1 2 3)), or it could be other arrangements of the lists (1 2 3), (2 1 3), and (2 3 1).
2. Define a function that delivers the list of permutations of a given list. The order in which the list arranges the permutations is immaterial. For example, either the list ((1 2 3) (1 3 2) (2 1 3) (2 3 1) (3 1 2) (3 2 1)) or the list ((1 2 3) (2 1 3) (2 3 1) (1 3 2) (3 1 2) (3 2 1)) or any of many other arrangements would be suitable values for (permutations '(1 2 3)).
3. Define a function that finds an optimal route in the Euclidean bottleneck traveling salesman problem (as described in Wikipedia).
   Note 1: Include your max-min and permutations books in the code, and refer to their functions where you find them useful.
   Note 2: Since the bottleneck version of the problem seeks only minimize the longest segment in a route (not the length of the whole route), you can use squared Euclidean distance as a proxy for Euclidean distance. This is fortunate, since Euclidean distance is usually not a rational number.

Properties

1. State and prove a theorem about the relationship of the length of (insert-everywhere x xs) compared to the length of xs.
2. State and prove a theorem that says that x is an element of every list in (insert-everywhere x xs) [Hint: Define a predicate (member-all x xss) whose value is non-nil if and only if the formula (member-equal x xs) is non-nil for every element xs of xss.]
3. State and prove a theorem that says that every list in (insert-everywhere x xs) is a permutation of the list (cons x xs). [Hint: See the the definition of  perm, defined in Section 10.3 of the Computer-Aided Reasoning textbook]
4. Define a theorem that says that (permutations xs) is a true-list of true-lists, as long as xs is a true-list.