The HOL theorem prover uses an ASCII approximation to standard logical notation. Before you begin, it is a good idea to see what normal logical terms look like in the HOL notation.
| HOL Notation | Meaning |
|---|---|
| T | true |
| F | false |
| ~t | not t |
| t1 \/ t2 | t1 or t2 |
| t1 /\ t2 | t1 and t2 |
| t1 ==> t2 | t1 implies t2 |
| t1 = t2 | t1 = t2 |
| \x1... xn. t[x1... xn] | map x1... xn to t[x1... xn] |
| !x1... xn. t[x1... xn] | t[x1... xn] holds for all x1... xn |
| ?x1... xn. t[x1... xn] | there exists an x1... xn such that t[x1... xn] holds |
| ?!x1... xn. t[x1... xn] | there exists precisely one x1... xn such that t[x1... xn] holds |
| @x. t[x] | an x such that t[x] holds (if there is one) |
| t1 => t2 | t3 | if t1 then t2 else t3 |
By now you should have set up your UNIX path variable and your Emacs environment to run ML (and HOL). If you haven't, then go back and complete the following exercises before proceeding further: Exercise 1: Getting Started with ML, and Exercise 2: Using ML with Emacs.
To start HOL first start Emacs and enter SML mode. This can be done by editing a file with the appropriate extension, something like `ex4.sml' would do. Then select the option `Moscow ML' from the `Process' submenu of the `SML' menu. You will then be prompted for the name of the Moscow ML interpretor. The default supplied is `mosml', but change that to `hol' before pressing Enter. You will then be prompted for any additional command line arguments, but you require none, so just hit Enter. A HOL process should now be started, you can change to the HOL buffer either by using the Buffers menu, or by typing C-C C-S as explained in Exercise 2: Using ML with Emacs. After a while the HOL buffer should contain the following text:
Moscow ML version 1.43 (April 1998)
Enter `quit();' to quit.
For HOL help, type: help "hol";
Loaded Hol Kernel.
HHH LL
HHH LL
HHH LL
HHH LL
HHH OOOO LL
HHHHHHH OO OO LL
HHHHHHH OO OO LLL
HHH OOOO LLLL
HHH LL LL
HHH LL LL
HHH LL LL
HHH LL LL98 [Athabasca 4]
[closing file "/.../hol98-Athabasca.4/std.prelude"]
HOL is just an ML interpreter with some extra types and functions already declared. Go ahead and enter a few simple ML expressions to convince yourself of this.
One of the types added to ML by HOL is
term, a type of terms in the HOL logic. One way to get a
value of type term is to type in a quotation that looks like
the term you want and call the HOL term parser on it. To enter a
term that is the conjunction of two booleans A and
B, just type the following:
- Term `A /\ B`; > val it = ``A /\ B`` : Term.term
Try using this method to enter some other, larger, terms for yourself.
All HOL terms are represented in ML by values of type
term. However, different terms are thought of as having
different types within the logic. For example, the term
T is an ML value of type term, but within
the logic with think of it as a boolean. A second type
hol_type has been added to ML to represent the logical
type of a term. The function function type_of will take
a HOL term and return its type. Try this out now on the term
T. What is the (ML) type of the function
type_of?
These two levels of typing can be confusing at first, but it is important to learn to distinguish between ML types and HOL types.
Sometimes when we enter a term, we may not give enough information for the HOL term parser to be able to determine the (HOL) type of it and all its subterms. For example, consider the interaction below:
- Term `A => B | C`; <<HOL message: inventing new type variable names: 'a.>> > val it = ``A => B | C`` : Term.termThe parser has been able to determine only that the term as a whole and the subterms B and C must share the same type, but not what type that is. (It has been able to establish that A must be boolean.) It has assigned the term, and the subterms B and B, the variable type 'a. All types with names beginning with ' are variable types in HOL. You can think of variable types in the same way you think of polymorphic types in a functional programming language.
We can add typing annotations when we enter a term if we would like it to be parsed to yield a term of a particular type rather than of a variable type. For example, if we also intend B and C to be booleans then we can annotate the term in any of the following ways to make sure they are parsed as such.
- Term `(A => B | C):bool`; > val it = ``A => B | C`` : Term.term - Term `A => B:bool | C`; > val it = ``A => B | C`` : Term.term - Term `A => B | C:bool`; > val it = ``A => B | C`` : Term.termNote: The type of booleans is about the only interesting primitive type that is defined in HOL at start up. Other types, like natural numbers, can be loaded in from libraries when they are needed.
ML allows a printing function to be associated with each type.
This function is called whenever ML needs to print a value of that
type. The function used to print values of type term is
called print_term. The global variable
Globals.show_types determines whether
print_term prints type information about terms or
not. Try setting this variable to true as follows:
- Globals.show_types := true; > val it = () : unitNow try entering a few more terms and see how they print out.
Feedback & Queries:
Jim.Grundy@anu.edu.au