MRG home page · Research · Publications · Projects · Software · People

Relational Rippling

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:

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.

Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.