A Package for Non-primitive Recursive Function Definitions in HOL.
University of Cambridge, Computer Laboratory, 1995 - Logic, Symbolic and mathematical - 36 pages
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."
What people are saying - Write a review
We haven't found any reviews in the usual places.
A-abstraction ACK_DEF ACK(PRE Ackermann function admiss argument automation backbone binary relation bottom element conditional style constant construction cont f(frel,frel cont(\g contain g continuity prover continuous functions cpo frel defined dest_Comb2 dest_Var example f rel f_def f_fun fix G fixed point definition fixed point induction fixed point operator fixed point property frel f g frel g f function extension g(APPEND GEN_TAC higher order logic instantiating Intermediate theorems is_Const is_Failure is_Var islub R X lemma2 less-than ordering let-term lifted range type lookup lrel lrel(ext(\u ML name wf new_wfrec_definition non-primitive recursive function non-trivial package Park induction partial function partial recursive function pointwise ordering primitive recursive proof obligations prove_thm QSORT Quicksort recursive call recursive definition recursive function definitions recursive specification Section structural induction subgoals t,dest_Combl term list termination properties theorems and tools theory file tl t2 unification algorithm UNIFY(dest_Combl unifyR well-founded induction well-founded recursive function well-founded relation wf_ack wf_less xs,y xs.y