Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-24T02:31:12.612Z Has data issue: false hasContentIssue false
  • English
  • Français

Transparent optimisation of rewriting combinators

Published online by Cambridge University Press:  01 March 1999

RICHARD J. BOULTON
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
Information
Journal of Functional Programming , Volume 9 , Issue 2 , March 1999 , pp. 113 - 146
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.