The HOLOmega 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 HOLOmega 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,
HOLOmega is constructed according to the design principles of the LCF approach, for the highest degree of soundness.
Briefing
HOLOmega is generally described in a briefing (PDF, 21 pages, 12 MB).
Tutorial
Here is the tutorial for HOLOmega (PDF, 928 KB). This tutorial is the best way to learn
about the HOLOmega system. It explains both the core features of classic HOL and the new features of HOLOmega,
along with many examples that demonstrate applications of the system. Alternatively, as a short introduction to HOLOmega, there is a brief teaser for the tutorial (PDF, 202 KB), containing examples that demonstrate
in a light way the essential new features of the logic.
Paper
The HOLOmega system is more deeply described in the paper The HOLOmega 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. 244259. The paper provides examples illustrating and motivating the need for
an expanded logic. It 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. 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 HOLOmega 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 HOLOmega system differs from that described
in the 2009 paper in one major 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  k_{1}
⇒ k_{2} 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. When deciding if a function term can be properly applied to its argument,
the type of the argument must be ≤ the type expected
by the function, where some difference in ranks is acceptable. As an important innovation, the comparison of types for inequality
(≤) depends on whether or not
they are classified as humble types. Humble types are types that do not change how
they interact with other types as they are promoted to higher rank. In other words, their semantics do not change if their
rank is increased. Humble types are defined and described further in an upcoming paper being submitted to ITP 2013.
This
change has had no effect on the examples in the 2009 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 HOLOmega kernel.
For more details, see here.
Downloads
The current development version of HOLOmega 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 HOLOmega may be checked out into a fresh subdirectory
called holomega by the following Git command: git clone b HOLOmega git://github.com/mn200/HOL.git holomega To check out a fresh copy of HOLOmega 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 HOLOmega git@github.com:mn200/HOL.git holomega To become an HOL developer and have write access to the github repository, please contact Michael Norrish of NICTA. The development version is significantly improved over the 2009 release version, and new users are
encouraged to use it.
Installation and Implementation
The HOLOmega theorem prover installs in exactly the same way as the HOL4
theorem prover. Helpful instructions for building HOL4 or HOLOmega may be found here. Installation instructions are also found in the file INSTALL
in the top directory of the downloaded software. HOLOmega
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 HOLOmega 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 HOLOmega 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 HOLOmega 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 higherorder matching of the new types and terms and automatic type
betareduction. 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.
