|
The HOL-Omega or HOLω system presents a more powerful version of the widely used HOL4 theorem prover. This system implements a new logic,
which is an extension of the existing higher order logic of the HOL4 system. The logic is extended to three levels, adding
kinds to the existing levels of types and terms. New types include type operator variables and universal types as in System
F. Impredicativity is avoided through the stratification of types by ranks according to the depth of universal types. The
HOL-Omega system is a merging of HOL4, HOL2P by Völker, and major aspects of System Fω from chapter 30 of Types and Programming Languages by Pierce. Like HOL4, HOL-Omega is constructed according to the
design principles of the LCF approach, for the highest degree of soundness.
Paper
The HOL-Omega system is described in the paper The HOL-Omega Logic (pdf) by Homeier, P.V., in Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics
(TPHOLs) 2009, LNCS vol. 5674, pp. 244-259. The paper presents the abstract syntax and semantics for the ranks, kinds, types,
and terms of the logic, as well as the new fundamental axioms and rules of inference. It also provides examples illustrating
the need for an expanded logic.
Despite the value of higher order logic, it has been recognized that there are some useful concepts beyond the power of higher
order logic to state. An example is the practical device of monads. Monads are particularly useful in modeling, for example,
realistic computations involving state or exceptions, as a shallow embedding in a logic which itself is strictly functional,
without state or exceptions. The paper presents examples of using the HOL-Omega system to model monads and prove theorems
about their general properties, as well as concepts from category theory such as functors and natural transformations.
Downloads
hol-omega-kananaskis-5.tar.gz (7.92 MB)
Please
be aware that the PDF documents above are the same as those for the
HOL4 Kananaskis-5 system. They are provided here as a convenience, but
do not as yet contain any new information about the new HOL-Omega
features.
Implementation
The release version of the HOL-Omega implementation may be downloaded either from this website by the link above,
or from the official SourceForge website here. The current development version may be downloaded from SourceForge by the Subversion command
svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega
Installation instructions are in the top directory. HOL-Omega may be built using either the standard or the experimental
kernel, and either Moscow ML or Poly/ML, by the same process as for HOL4. This implementation is still in development but
is currently useful. It provides a practical workbench for developments in the HOL-Omega logic, integrated in a natural and
consistent manner with the existing HOL4 tools and libraries that have been refined and extended over many years. Examples
using the new features of HOL-Omega may be found in the directory examples/HolOmega.
The implementation was designed with particular concern for backwards compatibility with HOL4. This was almost entirely
achieved, which was possible only because the fundamental data types representing types and terms were originally encapsulated.
This meant that the underlying representation could be changed without affecting the abstract view of types and terms by
the rest of the system. Virtually all existing HOL4 code will build correctly, including the extensive libraries. The simplifiers
have been upgraded, including higher-order matching of the new types and terms and automatic type beta-reduction. Algebraic
types with higher kinds and ranks may be constructed using the familiar Hol_datatype tool. Not all of the tools
will work as expected on the new terms and types, as the revision process is ongoing, but they will function identically on
the classic terms and types. So nothing of HOL4's existing power has been lost.
|
