Technical reports
A package for non-primitive recursive function definitions in HOL
Sten Agerholm
July 1995, 36 pages
DOI: 10.48456/tr-370
Abstract
This paper provides an approach to the problem of introducing non-primitive recursive function definitions in the HOL system. A recursive specification is translated into a domain theory version, where the recursive calls are treated as potentially non-terminating. Once we have proved termination, the original specification can be derived easity. Automated tools implemented in HOL88 are provided to support the definition of both partial recursive functions and total recursive functions which have well founded recursive specifications. There are constructions for building well-founded relations easily.
Full text
PDF (2.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-370, author = {Agerholm, Sten}, title = {{A package for non-primitive recursive function definitions in HOL}}, year = 1995, month = jul, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-370.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-370}, number = {UCAM-CL-TR-370} }