|
LCF Examples in HOL
Sten Agerholm June 19, 1994 |
|
LCF Examples in HOL
Sten Agerholm June 19, 1994 |
Abstract:The LCF system provides a logic of fixed point theory and is useful to reason about nontermination, recursive definitions and infinite-valued types such as lazy lists. Because of continual presence of bottom elements, it is clumsy for reasoning about finite-valued types and strict functions. The HOL system provides set theory and supports reasoning about finite-valued types and total functions well. In this paper a number of examples are used to demonstrate that an extension of HOL with domain theory combines the benefits of both systems. The examples illustrate reasoning about infinite values and nonterminating functions and show how domain and set theoretic reasoning can be mixed to advantage. An example presents a proof of correctness of a recursive unification algorithm using well-founded induction.
IntroductionThe LCF system [GMW79, Pa87] is a theorem prover based on a version of Scott's Logic of Computable Functions (a first order logic of domain theory). It provides the concepts and techniques of fixed point theory to reason about nontermination and arbitrary recursive (computable) functions. For instance, it has been successfully applied to reason about infinite data structures and lazy evaluation [Pa84b]. On the other hand, the HOL system [GM93] supports set theoretic reasoning. It has no inbuilt notion of nontermination, all functions are total, and only primitive recursive definitions are supported. It has mainly been used for reasoning about finite data structures and terminating primitive recursive functions. In a way, extending HOL with domain theory as described in [Ag93, Ag94] corresponds to embedding the logic of the LCF system within HOL-this extension is called HOL-CPO in this paper. Thus, any proof conducted in LCF can be conducted in HOL-CPO as well, and axioms of LCF theories can be introduced as definitions, or derived from definitions, provided of course they are consistent extensions of LCF. This correspondence breaks for difficult recursive domains with infinite values. It is not easy to define such domains in HOL and LCF could just axiomatize the domains; still this has its theoretical difficulties in general, but has been automated in certain cases [Pa84a]. However, HOL-CPO is not just another LCF system. Ignoring the problems with recursive domains, we claim it is more powerful and usable than LCF since (1) it inherits
|
