We are pleased to announce the Kananaskis-8 release of HOL 4.
The Define function for making function definitions now allows variables that appear as formal parameters to the new functions being defined to share names with existing constants.
This is based on the view that `f x = x + 1` should be the same as `f = λx. x + 1`.
In the latter, it was already permitted to use constant names in the position of the x, now it is permitted in the former as well.
There is one exception: if the formal name is the name of a constructor, then it has to be read as a constant rather than a bound name in order to allow ML-style pattern-matching.
So, the following now works:
> Define`x = (2,3)`;
Definition has been stored under "x_def"
val it = |- x = (2,3)
> Define`f x = x + 1`;
Definition has been stored under "f_def"
val it = |- ∀x. f x = x + 1
But, this next session fails:
> Hol_datatype`foo = X | Y`
<<HOL Message: Defined type: "foo">>
val it = () : unit
> Define`g X = X + 1`;
...<Type inference failure—exception raised>...
Thanks to Scott Owens for the feature suggestion.
Declaring an “enumerated” data type (one with nullary constructors only) with certain choices of constructor names could lead to unloadable theories. Thanks to Scott Owens for the bug report.
Calling delete_const on a constant that had been defined with Define could lead to unloadable theories.
Thanks to Magnus Myreen and Ramana Kumar for help in finding and fixing this bug.
If the Unicode trace was turned off in a user’s hol-config file (as per the FAQ), running the hol executable under Moscow ML resulted in lots of unnecessary warnings about “Unicode-ish” rules being added while the trace was off.
Thanks to Joseph Chan for the bug report.
The theory of sets has been extended with new PROD_IMAGE and PROD_SET constants, by analogy with existing SUM_IMAGE (also known as SIGMA) and SUM_SET.
The PROD_IMAGE constant is overloaded to PI and Π.
Thanks to Joseph Chan for this.
A new theory, real_sigmaTheory defining the sum over a finite set of real numbers. The REAL_SUM_IMAGE constant is overloaded to SIGMA.
A new probability theory providing an axiomatic formalization of probability theory including probability spaces, random variables, expectation and more.
The formalization is based on the formalization of measure theory and Lebesgue integration.
This work was done in the HVG group, Concordia and was built on top of the work of Coble in Cambridge.
In this formalization, functions as well as Lebesgue integrals are extended-real-valued. Among the main results of the formalization are the convergence theorems, the Radon Nikodym theorem and properties of the integral.
Details of the work can be found in
The probability theories replace the theories that used to be found in src/prob. (Minor incompatibility)
A small theory, gcdset defining a function gcdset that returns the greatest common divisor of any non-empty set of natural numbers (and returns 0 for the empty set for the sake of totality).
A theory, numposrep about positional representations for numbers, linking type :num (i.e., the natural numbers) to :num list. The conversion functions n2l and l2n are parameterised by the base to be used.
In addition, there is a theory ASCIInumbers, which builds on this base to define the conversion from lists of digits to lists of characters, using the ASCII encoding for the digits. This theory defines constants such as num_to_bin_string and num_from_dec_string.
These constants (and the theorems about them) were originally part of the existing theory bit, so theories and SML code referring to the constants and theorems may need to be adjusted to account for their new host theories. (Minor incompatibility)
A new proof-producing translator from HOL functions to MiniML:
examples/miniML/hol2miniml. Given an ML-like function in
the HOL logic, this tool generates a corresponding deeply embedded
MiniML program and automatically proves (w.r.t. an operational
semantics) that the generated MiniML program indeed computes exactly
the same value as the original HOL function. A description of this
tool can be found in:
A soundness proof of Jared Davis' ACl2-like Milawa theorem
prover: examples/theorem-prover. This examples directory
constructs a verified Lisp implementation in 64-bit x86 (including
verified garbage collection, parsing, printing, compilation) that is
able to host the Milawa theorem prover. Going further, we also verify
the soundness of Milawa's reflective kernel w.r.t. a formal definition
of the semantics of its logic. Part of this work is described in:
A development of the theory of ordinal numbers (in examples/set-theory/hol_sets, based on a quotient of well-orders.
Standard arithmetic operations (addition, multiplication and exponentiation) are defined, as well as the notion of supremum.
The theorem that all ordinals can be expressed in a unique polynomial form over all possible bases greater than 1 is also proved.
(When the base is ω, this gives the “Cantor Normal Form”.)
The example also shows the existence of the first uncountable ordinal (ω₁) if the underlying type (the α type parameter in α ordinal) is big enough.
The earlier ordinals theory (of Cantor Normal Form notation up to ε₀) is now in the same directory (moved from examples/ordinal) and is called ordinalNotation. (Minor incompatibility)
The syntax for case expressions has changed to be the same as in SML. This means that instead of
case n of
0 -> 1
|| SUC n -> n + 1
one should write
case n of
0 => 1
| SUC n => n + 1
Additionally, as an aid to uniformity, the first case may be preceded by a bar character. This makes the following valid HOL (it is not valid SML):
case n of
| 0 => 1
| SUC n => n + 1
The new syntax does not mix well with the vertical bars of the set comprehension syntax. If one has a case expression inside a set-comprehension, the parser will likely be confused unless the case expression is enclosed in parentheses. The pretty-printer will parenthesise all case-expressions inside set comprehensions.
The pretty-printer’s behaviour cannot be easily changed, but if one wishes to support source files using the old syntax, the following incantation can be used:
set_mapped_fixity {
tok = "||", fixity = Infixr 6,
term_name = GrammarSpecials.case_split_special
};
set_mapped_fixity {
tok = "->", fixity = Infixr 10,
term_name = GrammarSpecials.case_arrow_special
};
The problem with using this old syntax is that the || token is now also used for the bit-wise or operation on words.
If wordsLib is loaded, the parser will behave unpredictably unless the new syntax for bitwise or is removed.
This removal can be done with:
remove_termtok {tok = "||", term_name = "||"}
When this is done, or if wordsLib is not loaded in the first place, old-style case-expressions will be parsed correctly.