Open AccessLCF Examples in HOL
Author(s) -
Sten Agerholm
Publication year - 1994
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v1i18.21649
Subject(s) - hol , correctness , unification , computer science , domain (mathematical analysis) , set (abstract data type) , theoretical computer science , mathematics , proof assistant , fixed point , algorithm , programming language , mathematical analysis , geometry , mathematical proof
The LCF system provides a logic of fixed point theory and is useful to reason about non-termination, arbitrary recursive definitions and infinite types as lazy lists. It is unsuitable for reasoning about finite types and strict functions. The HOL system provides set theory and supports reasoning about finite 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 non-terminating functions and show how mixing domain and set theoretic reasoning eases reasoning about finite LCF types and strict functions. An example presents a proof of the correctness and termination of a recursive unification algorithm using well-founded induction.