1<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN"> 2<html> 3<head> 4<meta http-equiv="content-type" 5 content="text/html ; charset=UTF-8"> 6<title>Release Notes for Kananaskis-8 version of HOL 4</title> 7<style type="text/css"> 8<!-- 9 body {color: #333333; background: #FFFFFF; 10 margin-left: 1em; margin-right: 1em } 11 code, pre {color: #006400; font-weight: bold; font-family: "Andale Mono", "Lucida Console", monospace; } 12 div.footer { font-size: small; display: flex; justify-content: space-between; } 13--> 14</style> 15 16</head> 17 18<body> 19<h1>Notes on HOL 4, Kananaskis-8 release</h1> 20 21<p>We are pleased to announce the Kananaskis-8 release of HOL 4.</p> 22 23<h2 id="contents">Contents</h2> 24<ul> 25 <li> <a href="#new-features">New features</a> </li> 26 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 27 <li> <a href="#new-theories">New theories</a> </li> 28 <li> <a href="#new-tools">New tools</a> </li> 29 <li> <a href="#new-examples">New examples</a> </li> 30 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 31</ul> 32 33<h2 id="new-features">New features:</h2> 34 35<ul> 36<li><p>The <code>Define</code> 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. 37This is based on the view that <code>`f x = x + 1`</code> should be the same as <code>`f = ��x. x + 1`</code>. 38In the latter, it was already permitted to use constant names in the position of the <code>x</code>, now it is permitted in the former as well. 39There 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. 40So, the following now works: 41<pre> 42 > Define`x = (2,3)`; 43 Definition has been stored under "x_def" 44 val it = |- x = (2,3) 45 46 > Define`f x = x + 1`; 47 Definition has been stored under "f_def" 48 val it = |- ���x. f x = x + 1 49</pre> 50<p>But, this next session fails: 51<pre> 52 > Hol_datatype`foo = X | Y` 53 <<HOL Message: Defined type: "foo">> 54 val it = () : unit 55 56 > Define`g X = X + 1`; 57 ...<i><Type inference failure—exception raised></i>... 58</pre> 59<p>Thanks to Scott Owens for the <a href="http://github.com/mn200/HOL/issues/17">feature suggestion</a>. 60 61</ul> 62 63<h2 id="bugs-fixed">Bugs fixed:</h2> 64 65<ul> 66<li><p> Declaring an ���enumerated��� data type (one with nullary constructors only) with certain choices of constructor names could lead to unloadable theories. 67Thanks to Scott Owens for the <a href="https://github.com/mn200/HOL/issues/78">bug report</a>. 68 69<li><p> Calling <code>delete_const</code> on a constant that had been defined with <code>Define</code> could lead to unloadable theories. 70Thanks to Magnus Myreen and Ramana Kumar for help in finding and fixing <a href="http://github.com/mn200/HOL/issues/73">this bug</a>. 71 72<li><p> If the Unicode trace was turned off in a user���s <code>hol-config</code> file (as per the <a href="http://hol.sourceforge.net/faq.html#turn-off-unicode">FAQ</a>), running the <code>hol</code> executable under Moscow ML resulted in lots of unnecessary warnings about ���Unicode-ish��� rules being added while the trace was off. 73Thanks to Joseph Chan for the bug report. 74 75</ul> 76 77<h2 id="new-theories">New theories:</h2> 78 79<ul> 80<li> <p>The theory of sets has been extended with new <code>PROD_IMAGE</code> and <code>PROD_SET</code> constants, by analogy with existing <code>SUM_IMAGE</code> (also known as <code>SIGMA</code>) and <code>SUM_SET</code>. 81The <code>PROD_IMAGE</code> constant is overloaded to <code>PI</code> and <code>��</code>. 82Thanks to Joseph Chan for this. 83 84<li> <p> A new theory, <code>real_sigmaTheory</code> defining the sum over a finite set of real numbers. The <code>REAL_SUM_IMAGE</code> constant is overloaded to <code>SIGMA</code>. 85 86<li> <p>A new <code>probability</code> theory providing an axiomatic formalization of probability theory including probability spaces, random variables, expectation and more. 87The formalization is based on the formalization of measure theory and Lebesgue integration. 88This work was done in the HVG group, Concordia and was built on top of the work of Coble in Cambridge. 89In 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. 90Details of the work can be found in 91<ol> 92<li> T. Mhamdi, O. Hasan, and S. Tahar: <cite>On the Formalization of the Lebesgue Integration Theory in HOL</cite>, ITP 2010; and 93<li> T. Mhamdi, O. Hasan, and S. Tahar: <cite>Formalization of Entropy Measures in HOL</cite>, ITP 2011. 94</ol> 95<p>The <code>probability</code> theories replace the theories that used to be found in <code>src/prob</code>. (<b>Minor incompatibility</b>) 96 97<li> <p> A small theory, <code>gcdset</code> defining a function <code>gcdset</code> 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). 98 99<li> <p> A theory, <code>numposrep</code> about positional representations for numbers, linking type <code>:num</code> (<em>i.e.,</em> the natural numbers) to <code>:num list</code>. The conversion functions <code>n2l</code> and <code>l2n</code> are parameterised by the base to be used. 100 101<p> In addition, there is a theory <code>ASCIInumbers</code>, 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 <code>num_to_bin_string</code> and <code>num_from_dec_string</code>. 102 103<p>These constants (and the theorems about them) were originally part of the existing theory <code>bit</code>, so theories and SML code referring to the constants and theorems may need to be adjusted to account for their new host theories. (<b>Minor incompatibility</b>) 104 105</ul> 106 107<h2 id="new-tools">New tools:</h2> 108 109<ul> 110<li><p>A new proof-producing translator from HOL functions to MiniML: 111<code>examples/miniML/hol2miniml</code>. Given an ML-like function in 112the HOL logic, this tool generates a corresponding deeply embedded 113MiniML program and automatically proves (w.r.t. an operational 114semantics) that the generated MiniML program indeed computes exactly 115the same value as the original HOL function. A description of this 116tool can be found in: 117<ol> 118<li> Myreen and Owens: <cite>Proof-Producing Synthesis of ML from Higher-Order Logic</cite>, ICFP 2012. 119</ol> 120 121</ul> 122 123<h2 id="new-examples">New examples:</h2> 124 125<ul> 126<li><p>A soundness proof of Jared Davis' ACl2-like Milawa theorem 127prover: <code>examples/theorem-prover</code>. This examples directory 128constructs a verified Lisp implementation in 64-bit x86 (including 129verified garbage collection, parsing, printing, compilation) that is 130able to host the Milawa theorem prover. Going further, we also verify 131the soundness of Milawa's reflective kernel w.r.t. a formal definition 132of the semantics of its logic. Part of this work is described in: 133<ol> 134<li> Myreen and Davis: <cite>A verified runtime for a verified theorem prover</cite>, ITP 2011. 135</ol> 136 137<li><p>A development of the theory of ordinal numbers (in <code>examples/set-theory/hol_sets</code>, based on a quotient of well-orders. 138Standard arithmetic operations (addition, multiplication and exponentiation) are defined, as well as the notion of supremum. 139The theorem that all ordinals can be expressed in a unique polynomial form over all possible bases greater than 1 is also proved. 140(When the base is <code>��</code>, this gives the ���Cantor Normal Form���.) 141 142<p>The example also shows the existence of the first uncountable ordinal (<code>�����</code>) if the underlying type (the <code>��</code> type parameter in <code>�� ordinal</code>) is big enough. 143 144<p>The earlier ordinals theory (of Cantor Normal Form notation up to <code>�����</code>) is now in the same directory (moved from <code>examples/ordinal</code>) and is called <code>ordinalNotation</code>. (<b>Minor incompatibility</b>) 145</ul> 146 147<h2 id="incompatibilities">Incompatibilities:</h2> 148 149<ul> 150 151<li><p>The syntax for <code>case</code> expressions has changed to be the same as in SML. This means that instead of 152<pre> 153 case n of 154 0 -> 1 155 || SUC n -> n + 1 156</pre> 157<p>one should write 158<pre> 159 case n of 160 0 => 1 161 | SUC n => n + 1 162</pre> 163<p>Additionally, as an aid to uniformity, the first case may be preceded by a bar character. 164This makes the following valid HOL (it is not valid SML): 165<pre> 166 case n of 167 | 0 => 1 168 | SUC n => n + 1 169</pre> 170 171<p>The new syntax does not mix well with the vertical bars of the set comprehension syntax. 172If one has a case expression inside a set-comprehension, the parser will likely be confused unless the case expression is enclosed in parentheses. 173The pretty-printer will parenthesise all case-expressions inside set comprehensions. 174 175<p>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: 176<pre> 177 set_mapped_fixity { 178 tok = "||", fixity = Infixr 6, 179 term_name = GrammarSpecials.case_split_special 180 }; 181 set_mapped_fixity { 182 tok = "->", fixity = Infixr 10, 183 term_name = GrammarSpecials.case_arrow_special 184 }; 185</pre> 186<p>The problem with using this old syntax is that the <code>||</code> token is now also used for the bit-wise or operation on words. 187If <code>wordsLib</code> is loaded, the parser will behave unpredictably unless the new syntax for bitwise or is removed. 188This removal can be done with: 189<pre> 190 remove_termtok {tok = "||", term_name = "||"} 191</pre> 192<p>When this is done, or if <code>wordsLib</code> is not loaded in the first place, old-style case-expressions will be parsed correctly. 193</ul> 194 195<hr> 196<div class="footer"> 197<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-8</a></em></p> 198<p>(<a href="kananaskis-7.release.html">Release notes for previous version</a>)</p> 199 200</body> </html> 201