|
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.
Briefing
HOL-Omega is generally described in a briefing (PDF, 21 pages, 12 MB).
Paper
The HOL-Omega system is more deeply 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. The
current implementation of the HOL-Omega system differs from that described in the paper in one important respect. Previously,
ranks were attributes of types, as also were kinds. In the current version, ranks are attributes of kinds, and a type's
rank is the rank of its kind. The grammar of kinds and types is now as follows: Kinds: k ::= ty
: r | κ : r | k1 ⇒ k2 Types: σ
::= α : k | τ : k | σarg σopr
| λα.σ | ∀α.σ | ∃α.σ The
parser will accept type annotations of terms (``t : σ``), kind annotations of types (``σ : k``),
and rank annotations of kinds (``k : r``). Rank annotations of types (``σ :≤ r``) are also still accepted. This change has had no effect on the
examples in the paper or in the example source files in the distribution.
Bounty
There is a $100.00 bounty available for new soundness bugs discovered in the HOL-Omega kernel.
For more details, see here.
Downloads
The current development version of HOL-Omega is the best version to use. This is available by using the Git
version control system. Git
is freely available from here and competently described in the book ProGit by Scott Chacon. A fresh copy of HOL-Omega may be checked out into a fresh subdirectory called hol-omega by the following Git command: git clone -b HOL-Omega
git://github.com/mn200/HOL.git hol-omega To
check out a fresh copy of HOL-Omega that one could edit and write back to the github repository, one would set up a SSH key
with github (see here) and then do: git clone -b HOL-Omega git@github.com:mn200/HOL.git hol-omega To become an HOL developer and have write access to the github repository, please contact Michael Norrish of NICTA. If Git is for some reason
unavailable, for now an older version of HOL-Omega may be downloaded from SourceForge by the Subversion command
svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-OmegaThe development version is significantly improved over the 2009 release
version, and new users are encouraged to use it. However, the 2009 release version of the HOL-Omega implementation is
also available, and may be downloaded directly from this website by the link below.
hol-omega-kananaskis-5.tar.gz (7.92 MB)
Installation and Implementation
The HOL-Omega theorem prover installs in exactly the same way as the HOL4
theorem prover. Helpful instructions for building HOL4 or HOL-Omega may be found here. Installation instructions are also found in the file INSTALL in the top directory of the downloaded
software. HOL-Omega may be built using either the standard or the experimental kernel, and either Moscow ML
or Poly/ML, by exactly the same process as for HOL4. Please be aware that building the HOL-Omega system usually takes a few
hours, depending on the speed of the computer. The current implementation
is still in development but is already 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 subdirectory examples/HolOmega. Jeremy Dawson of the Australian National University has contributed an advanced exploration
of generalized monads and other category theory topics in examples/HolOmega/interim.
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.
|
