Writing HOL Terms and Types

The ML language is literally the HOL system's meta-language. We use it to manipulate and interact with the terms, types and theorems of higher-order logic. Ultimately this is done with ML functions and values, but a hugely significant part of the user's connection to the logic is via the system's parser and pretty-printer.

The parser allows the user to write terms and types in a pleasant textual form (rather than constructing them directly with the kernel's underlying ML API).¹ The pretty-printer shows the user terms, types and theorems in a pretty way. We believe it greatly helps the user experience to see $p \land q$ rather than something like

COMB (COMB (CONST ("bool", "/\",
                   TYPE("min", "fun",
                        [TYPE("min", "bool", []),
                         TYPE("min", "fun",
                              [TYPE("min", "bool", []),
                               TYPE("min", "bool", [])])])),
            VAR ("p", TYPE("min", "bool", []))),
      COMB (VAR ("q", TYPE("min", "bool", []))))

which is a much more accurate picture of what the term really looks like in memory.

HOL can use Unicode and ASCII

The fundamental logical connectives can usually be parsed and printed in two different ways, with an ASCII notation, or a generally prettier Unicode form. By default, the parser will accept either and the printer will choose to use the Unicode form. Thus

> [“p ∧ q”, ``p /\ q``];
val it = [“p ∧ q”, “p ∧ q”]: term list

> [“∀x:α. P x ⇒ ¬Q x”, “!x:'a. P x ⇒ ~Q x”];
val it = [“∀x. P x ⇒ ¬Q x”, “∀x. P x ⇒ ¬Q x”]: term list

It is possible to turn Unicode printing off and on by setting the PP.avoid_unicode trace:

> set_trace "PP.avoid_unicode" 1;
val it = (): unit
> “x ∈ A”;
<<HOL message: inventing new type variable names: 'a>>
val it = ``x IN A``: term

> set_trace "PP.avoid_unicode" 0;
val it = (): unit
> “x ∈ A”;
<<HOL message: inventing new type variable names: 'a>>
val it = “x ∈ A”: term

Table 3.1 lists a number of Unicode/ASCII pairs. Generation of Unicode code-points is up to the user's environment, but modes assisting this are available for emacs and vim. Note also that the encoding for both parsing and printing must be UTF8, which is again the user's responsibility.

Table: Unicode/ASCII equivalents in HOL syntax. Delimiters are the quotation marks that delimit whole terms or types, separating them from the ML level.

HOL looks like ML

One interesting (and also confusing for beginners) aspect of HOL is that its terms and types look like ML's. For example, the zip function in ML (from the previous chapter) might be characterised by the HOL term that can be written:

   zip (l1, l2) = if NULL l1 ∨ NULL l2 then []
                  else (HD l1, HD l2) :: zip (TL l1, TL l2)

Apart from the fact that some of the relevant constants have different names (NULL vs null for example), and apart from the use of logical disjunction ($\lor$) instead of orelse, the text is identical.

The following session shows the (rather involved) way in which this definition can be made,² allowing us to see the way the definition theorem is printed back. We can also ask the system to print the new constant's type:

> Definition zip_def:
    zip (l1, l2) = if NULL l1 ∨ NULL l2 then []
                   else (HD l1, HD l2) :: zip (TL l1, TL l2)
  Termination
    WF_REL_TAC ‘measure (LENGTH o FST)’ >> Cases_on ‘l1’ >> simp[]
  End
<<HOL message: inventing new type variable names: 'a, 'b>>
Equations stored under "zip_def".
Induction stored under "zip_ind".
val zip_def =
   ⊢ ∀l2 l1.
       zip (l1,l2) =
       if NULL l1 ∨ NULL l2 then [] else (HD l1,HD l2)::zip (TL l1,TL l2):
   thm

> type_of “zip”;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = “:α list # β list -> (α # β) list”: hol_type

Note how the pretty-printer is at liberty to make adjustments to the way the underlying term is rendered as a string: its placement of newline and space characters is not exactly the same as the user's.

HOL's language of types is also similar but slightly different to ML's: the # symbol is used for the pair type rather than *, and the printer uses Greek letters $\alpha$ and $\beta$ rather than 'a and 'b.

HOL vs ML Traps

Lists, sets and other types with syntax for enumerating elements use a semicolon rather than a comma to separate elements. Thus

> [1,2,3,4] (* ML *);
val it = [1, 2, 3, 4]: int list

> “[1;2;3;4] (* HOL *)”;
val it = “[1; 2; 3; 4]”: term
> type_of it;
val it = “:num list”: hol_type

ML has three distinct types $\tau_1 \texttt{*} \tau_2 \texttt{*} \tau_3$, $(\tau_1 \texttt{*} \tau_2) \texttt{*} \tau_3$, and $\tau_1 \texttt{*} (\tau_2 \texttt{*} \tau_3)$. One might see these as a flat triple, and two flavours of pair with a nested pair as one or other component. HOL cannot model the first of these, and the concrete syntax $\tau_1 \mathtt{\#} \tau_2 \mathtt{\#} \tau_3$ maps to $\tau_1 \mathtt{\#} (\tau_2 \mathtt{\#} \tau_3)$ (i.e., the infix # type operator is right-associative). One has to use parentheses to get the other association.

ML uses the op keyword to remove infix status from function forms. In HOL one can either “wrap” the operator in parentheses³ or precede it with a $-sign. Further, infixes in ML take pairs; in HOL they are curried:

> op+ (3,4) (* ML *);
val it = 7: int
> map op* [(1,2), (3,4)] (* ML *);
val it = [2, 12]: int list

> EVAL “(+) 3 4 < $* 3 4 (* HOL *)”;
val it = ⊢ 3 + 4 < 3 * 4 ⇔ T: thm
> EVAL “MAP (+) [1;2;3]”;
val it = ⊢ MAP $+ [1; 2; 3] = [$+ 1; $+ 2; $+ 3]: thm

ML insists that arguments of datatype constructors be tuples (“uncurried”), and that type arguments be provided to new types. HOL insists that type arguments be omitted, and allows either form of argument to constructors (though it's generally better practice to not use tuples). In ML:

> datatype 'a tree = Lf | Nd of ('a tree * 'a * 'a tree);
datatype 'a tree = Lf | Nd of 'a tree * 'a * 'a tree
> fun size Lf = 0 | size (Nd(l,_,r)) = 1 + size l + size r;
val size = fn: 'a tree -> int

In HOL:

> Datatype: tree = Lf | Nd tree α tree
  End
<<HOL message: Defined type: "tree">>

> type_of “Nd”;
<<HOL message: inventing new type variable names: 'a>>
val it = “:α tree -> α -> α tree -> α tree”: hol_type

> Definition size_def:
    (size Lf = 0) ∧ (size (Nd l _ r) = 1 + size l + size r)
  End
<<HOL message: inventing new type variable names: 'a>>
Definition has been stored under "size_def"
val size_def =
   ⊢ size Lf = 0 ∧ ∀l v0 r. size (Nd l v0 r) = 1 + size l + size r: thm

ML uses ~ as the unary negation operator on numeric types. HOL allows it in this role (as well as for boolean negation), but also allows - for numeric negation. First the ML behaviour:

> ~3;
val it = ~3: int
> -3;
Exception- (-) has infix status but was not preceded by op.
Type error in function application.
   Function: - : int * int -> int
   Argument: 3 : int
   Reason: Can't unify int to int * int (Incompatible types)
Fail "Static Errors" raised

In HOL:

> load "intLib";   ... output elided ...
> EVAL “~3 + 4”;
val it = ⊢ -3 + 4 = 1: thm
> EVAL “-3 * 4”;
val it = ⊢ -3 * 4 = -12: thm

1. Note that the user cannot write theorem values directly; this would break the prover's guarantee of soundness! ↩

2. The usual “HOL” way to define this function, with pattern-matching, wouldn't be so complicated. ↩

3. But watch out for the * operator; one can't wrap this in parentheses because the result then looks like comment syntax. ↩