Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-05T11:42:44.942Z Has data issue: false hasContentIssue false

Transparent optimisation of rewriting combinators

Published online by Cambridge University Press:  01 March 1999

RICHARD J. BOULTON
Affiliation:
Division of Informatics, University of Edinburgh, 80 South Bridge, Edinburgh EH1 1HN, Scotland
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The LCF system was the first mechanical theorem prover to be user-programmable via a metalanguage, ML, from which the functional programming language Standard ML has been developed. Paulson has demonstrated how a modular rewriting engine can be implemented in LCF. This provides both clarity and flexibility. This paper shows that the same modular approach (using higher-order functions) allows transparent optimisation of the rewriting engine; performance can be improved while few, if any, changes are required to code written using these functions. The techniques described have been implemented in the HOL system, a descendant of LCF, and some are now in daily use. Comparative results are given. Some of the techniques described, in particular ones to avoid processing parts of a data structure that do not need to be changed, may be of more general use in functional programming and beyond.

Type
Research Article
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.