Project Introduction
Rippling is ordinarily used to reason about expressions where
results are shared between functions via function nesting. However,
Prolog programmers will recognise another mode of
results sharing, that of shared existential variables between relations. In the following Prolog example, the variable
R, for example, is implicitly existentially quantified:
reverse([H|T], RL) :- reverse(T, R), append(R, H, RL).
This form of expression arises naturally in the analysis of logic programs. It may also be used when reasoning about electronic
circuits, where the existential variables represent the wires between logic gates and in relational proofs in mathematics.
Clearly, given the success of functional rippling, it would be nice to have its relational counterpart. In his 1996 PhD thesis,
Vincent Lombart created the basics of such a theory and was able to unify it with functional rippling.
Vincent wrote an experimental version of relational rippling in
Clam, that was then in use here at Edinburgh. However,
he never fully finished the implementation nor tested his theory extensively. Clam has now fallen out of use at Edinburgh,
replaced by the IsaPlanner system, developed by Lucas Dixon as part of
his 2005 PhD thesis. Whilst IsaPlanner has an existing implementation of functional rippling, no current implementation of
relational rippling yet exists.
Papers
Aims
In continuing this project, we wish to:
- Completely rewrite, from scratch, the IsaPlanner reasoning technique.
- Resolve the problem of the measure not being defined modulo associativity and commutativity of conjunction and existential
quantification, so as to make the measure suitable for implementation.
- Improve the identification of difference relations via a more sophisticated anaysis of the induction rule. If time
permits, a yet more sophisticated analysis of expressions may be implemented, fully automating the procedure.
- Automatically generate argument list data by co-opting the dynamic modality inference algorithm introduced by Lombart.
- Unify, within IsaPlanner, the dynamic functional and relational rippling heuristics.
- Test the heuristic in depth, using a case study of Mini-ML, a simple functional programming language.
Links
Papers and Introductory Background Reading
Results From initial Undergrad Project:
The project was originally a fourth year project, being carried out by Dominic Mulligan, an Artificial Intelligence and
Computer Science Honours Student. The project was supervised by
Alan Bundy,
Lucas Dixon and
Moa Johansson.
A relational rippling heuristic was successfully developed, a prototype system was created within
IsaPlanner and the
heuristic was tested on a small number of problems, by hand.
Due to time restrictions, a number of simplifying assumptions were made, and a number of things were left unimplemented. We now
wish to fully implement relational rippling, and also perform an in-depth investigation into the efficacy of the heuristic.
