A Package for Non-primitive Recursive Function Definitions in HOL.

Front Cover
University of Cambridge, Computer Laboratory, 1995 - Logic, Symbolic and mathematical - 36 pages
0 Reviews
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 easily. 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."

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.


Wellfounded Recursive Functions

2 other sections not shown

Common terms and phrases

Bibliographic information