# Project suggestions from Michael Norrish

If you're interested in doing these, I'm likely to be happy to supervise you. However, some of these ideas are pretty tentative and may not be feasible in the time available. Please don't assume that these are sure to work. On the other hand, if you're keen, we can talk it through and try to make sure that we come up with something reasonable.

## Simple declarative theorem-proving

When specifying systems formally, a significant error-finding benefit can accrue simply from writing everything down in an expressive logic, and getting it all to type-check. Actual formal verification of important properties can almost be relegated to the role of ``nice work if you can get it''.

The HOL system currently doesn't allow for this model of work very well. Part of the reason for this is that script files for HOL inter-mingle ML (which is the theorem-prover's implementation language) and embedded bits of logic. We would like to check the logic without having to be able to parse (and execute) ML as well.

Therefore, the aim of this project is to design a simple file format in which users could write ``ML-less HOL'', and to then implement at least two tools for manipulating this format. The first tool would be the type-checker. It would make sure that the definitions and other logical material in the file actually made sense at the level of types. The second tool would do all this and also produce a genuine HOL theory, using the various facilities already present in HOL.

If this all went well, there would be ample opportunity to extend this project so that it also included a declarative proof (as opposed to just definition) element.

## Smart(er) matching

In interactive theorem-proving systems such as HOL, a lot of work is typically done by fairly simple-minded rewriting with equalities. For example, if we know that
`FACT(SUC n) = (SUC n) * FACT(n)`

(i.e., that the factorial of a number greater than zero is equal to that number multiplied by the factorial of the number one less), then we can rewrite a term such as `FACT(SUC 6)` to ```SUC 6 * FACT(6)```. However, at this point, the rewriter can't make any more progress, because it doesn't recognise 6 as an instance of `SUC n` for some variable n. (The representation of the numeral 6 is not just a chain of `SUC`s applied to 0; this representation would be very inefficient.) In order to be able to make progress, we need to prove that there exists a number m such that 6 = `SUC` m.

Similarly, if we know that

f (2m) = g(m)

for some functions f and g, then we would have to prove that a number was even before we could apply the rewrite. Note also that this procedure would ideally work with more than just numerals. If we have as context that x > 10, then we could do quite a bit of rewriting with x!, maybe all the way to

x! = x * (x - 1) * (x - 2) * ... * (x - 10) * (x - 11)!

A project to investigate this idea would probably proceed by first implementing a simple rewriting system over arithmetic terms. This system would then need to be extended with access to an arithmetic decision procedure that could figure out the various supporting theorems. I can provide one of these. If you can find your own arithmetic decision procedure, this project could be done in any language. My d.p. is in SML, and you would almost certainly have to write the rest of the project in SML too.

Alternatively, and for extra kudos, the whole project could be done in HOL. Here the basic rewriting system is already provided, but there would be quite a bit (probably even, a lot) of hard work involved in learning the HOL system.

## Comparison of arithmetic decision procedures

This project idea is due to Larry Paulson and is described here (it's the second one on the page). You might also try to implement another procedure, due to Cooper, that I can explain.

## Word unification

Given an equation involving variables and characters, where variables can range over strings of any length, and the only operation is string concatenation, is there any satisfying assignment of strings to variables to make the two sides of the equation equal? E.g., given the equation
aXb = aaY
where X and Y are variables, one satisfying assignment is X = a and Y = b. But X = aa and Y = ab also works. In fact, there are an infinite number of unifiers, all of the form X = aZ, Y = Zb, where Z can be anything at all (including the empty string, as in the first solution above). There is a horrendously complicated algorithm for solving these problems. Your task would be to understand it, and then implement it.

## AC unification

Explanation to come.

Michael Norrish <Michael.Norrish@cl.cam.ac.uk>