Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-30T20:51:51.994Z Has data issue: false hasContentIssue false
  • English
  • Français

First-order unification by structural recursion

Published online by Cambridge University Press:  29 October 2003

CONOR MCBRIDE
CONOR MCBRIDE
Affiliation:
Department of Computer Science, University of Durham, South Road Durham, DH1 3LE, UK (e-mail: [email protected])
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.

First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve counting the number of unsolved variables and showing that this total decreases each time a substitution enlarges the terms. There are many such proofs in the literature (Manna & Waldinger, 1981; Paulson, 1985; Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999). This paper shows how a dependent type can relate terms to the set of variables over which they are constructed. As a consequence, first-order unification becomes a structurally recursive program, and a termination proof is no longer required. Both the program and its correctness proof have been checked using the proof assistant LEGO (Luo & Pollack, 1992; McBride, 1999).

Type
Article
Information
Journal of Functional Programming , Volume 13 , Issue 6 , November 2003 , pp. 1061 - 1075
Copyright
© 2003 Cambridge University Press
Supplementary material: Link

McBride Supplementary Material

/JFP/online/foubsr-website/index.html
Link
Submit a response

Discussions

No Discussions have been published for this article.