Information Technology Reference
In-Depth Information
one of the major advantages of rippling. More details about critics, including
some hard examples which have been proved with their use, can be found in
[Ireland & Bundy, 1996] and in chapter 3 of [Bundy
et al
, 2005].
3.5
Miscellaneous
How Is Rippling Used to Choose Induction Rules? There is a one-level
look-ahead into the rippling process to see what induction rules would permit
rippling to take place. In particular, which wave-fronts placed around which
induction variables would match with corresponding wave-fronts in induction
rules. We call this ripple analysis. It is similar to the use of recursive defini-
tions to suggest induction rules, as pioneered by Boyer and Moore, but differs
in that all available wave-rules are used in ripple analysis, and not just recursive
definitions. More detail of ripple analysis can be found in [Bundy
, 1989], al-
though that paper is rather old now and is not a completely accurate description
of current rippling implementations. In particular, the term 'ripple analysis' was
not in use when that paper was written and it is misleadingly called 'recursion
analysis' there. A recent alternative approach is to postpone the choice of in-
duction rule by using meta-variables as place holders for the induction term and
then instantiating these meta-variables during rippling: thus tailoring the choice
of induction rule to fit the needs of rippling [Kraan
et al
et al
, 1996,Gow, 2004].
3.6 And Finally ...
Why Do You Use Orange Boxes to Represent Wave-Fronts? 2
The boxes form hollow squares, which help to display the outwards or inwards
movement of wave-fronts. In the days of hand-written transparencies, orange
was used because it is one of the few transparent overhead pen colours, allowing
the expression in the wave-front to show through 3 .
For more information about the research work outlined above, electronic
versions of some of the papers and information about down loading software, see
the web site of my research group at http://dream.dai.ed.ac.uk/.
References
[Basin & Walsh, 1993] Basin, David A. and Walsh, Toby. (1993). Difference unifica-
tion.InBajcsy,R.,(ed.), Proc. 13th Intern. Joint Conference on Artificial Intelli-
gence (IJCAI '93) , volume 1, pages 116-122, San Mateo, CA. Morgan Kaufmann.
Also available as Technical Report MPI-I-92-247, Max-Planck-Institut fur Infor-
matik.
[Basin & Walsh, 1996] Basin, David and Walsh, Toby. (1996). A calculus for and ter-
mination of rippling. Journal of Automated Reasoning , 16(1-2):147-180.
2 The boxes in Figs 1 and 2 are grey rather than orange because colour representation
is not possible in this topic.
3 Famously, Pete Madden coloured his wave-fronts red for a conference talk. The
underlying expressions were made invisible, ruining his presentation.
Search WWH ::




Custom Search