Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 7 Dec 1994 18:51:36 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA26642; Wed, 7 Dec 1994 11:41:04 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA26629; Wed, 7 Dec 1994 11:40:49 -0700 Received: from skua.cl.cam.ac.uk (user sa10004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 7 Dec 1994 18:36:21 +0000 To: info-hol@leopard.cs.byu.edu Subject: Thesis available. Date: Wed, 07 Dec 1994 18:36:16 +0000 From: Sten Agerholm Message-Id: <"swan.cl.cam.:263440:941207183634"@cl.cam.ac.uk> Hi all, My thesis is now available: Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. December 1994. PhD thesis. 233 pp. A summary is provided below. It is being printed in the BRICS Report series as RS-94-44 and can be obtained on the Web/Ftp or as a hard copy. Please let me know if you would like a hard copy. Best wishes, -sTen --------------<><><>------------- HTML abstract: http://www.daimi.aau.dk/BRICS/RS/94/44/BRICS-RS-94-44/BRICS-RS-94-44.html which has a link to: http://www.daimi.aau.dk/BRICS/RS/94/44/BRICS-RS-94-44.ps.gz FTP (anonymous): file://ftp.daimi.aau.dk/pub/BRICS/RS/94/44/BRICS-RS-94-44.ps.gz Summary: Domain theory is the mathematical theory underlying denotational semantics. This thesis presents a formalization of domain theory in the Higher Order Logic (HOL) theorem proving system along with a mechanization of proof functions and other tools to support reasoning about the denotations of functional programs. By providing a fixed point operator for functions on certain domains which have a special undefined (bottom) element, this extension of HOL supports the definition of recursive functions which are not also primitive recursive. Thus, it provides an approach to the long-standing and important problem of defining non-primitive recursive functions in the HOL system. Our philosophy is that there must be a direct correspondence between elements of complete partial orders (domains) and elements of HOL types, in order to allow the reuse of higher order logic and proof infrastructure already available in the HOL system. Hence, we are able to mix domain theoretic reasoning with reasoning in the set theoretic HOL world to advantage, exploiting HOL types and tools directly. Moreover, by mixing domain and set theoretic reasoning, we are able to eliminate almost all reasoning about the bottom element of complete partial orders that makes the LCF theorem prover, which supports a first order logic of domain theory, difficult and tedious to use. A thorough comparison with LCF is provided. The advantages of combining the best of the domain and set theoretic worlds in the same system are demonstrated in a larger example, showing the correctness of a unification algorithm. A major part of the proof is conducted in the set theoretic setting of higher order logic, and only at a late stage of the proof domain theory is introduced to give a recursive definition of the algorithm, which is not primitive recursive. Furthermore, a total well-founded recursive unification function can be defined easily in pure HOL by proving that the unification algorithm (defined in domain theory) always terminates; this proof is conducted by a non-trivial well-founded induction. In such applications, where non-primitive recursive HOL functions are defined via domain theory and a proof of termination, domain theory constructs only appear temporarily.