Department of Computer Science and Technology

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}
}