Re: [Hol-info] Abstract data types in HOL-Omega

[Thomas M. <tom...@ba...>]

Dear Peter:

This is indeed a full achievement of my ambition to add a "type
specification" mechanism to HOL. Thank you and congratulations on a really
great addition to HOL, and a wonderful technical achievement. This is
beautiful work, Peter!

All best wishes,
Tom

On 18/04/2011 16:45, "Peter Vincent Homeier"
<pal...@tr...> wrote:

>One of the desires of system designers is to model their systems with
>the minimum of information, just what is necessary, and no more.
>
>If a new value can be described precisely, then it can be defined by
>using the HOL4 definitional principle "new_definition", which makes a
>new constant which is completely equal to a given expression.
>However, at times we may wish to intentionally not completely define a
>new constant, leaving some of its behavior unspecified.
>
>Thus in HOL4 the HD and TL operators on lists are defined on CONS
>values, but not on empty lists.  It's not that they yield an arbitrary
>value like NIL or 0 when applied to an empty list (such as is often
>done in ACL2, for example).  They are simply not defined on empty
>lists, and so one can deduce nothing more about ``HD ([]:num list)``
>than that it must be some value of the type ``:num``.
>
>This kind of incompleteness is supported by the HOL4 definitional
>principle "new_specification", which takes a theorem of the form
>
>|- ∃x y z. P
>
>and creates new constants a, b, and c with the same types as x, y, and
>z, where all that is known about a, b, and c is that they satisfy the
>property
>
>|- P[a, b, c / x, y, z].
>
>However, in HOL4, while there is a definitional principle supporting
>the definition of new types, "new_type_definition", there is not one
>for specifying new types incompletely.
>
>This is unfortunate, because it is very natural to describe an
>abstract data type as a type with an associated set of operations,
>where all that is known about that type are those constructors and
>operations, and the given algebraic relationships among them.
>
>The following example is taken from Tom Melham's paper:
>
>http://web.comlab.ox.ac.uk/oucl/work/tom.melham/pub/Melham-1994-HLE.pdf
>
>Consider the type of non-empty bit vectors, which is characterized
>algebraically as two constants t and f, and a associative binary
>operator c which concatenates two bit vectors together.  In addition,
>we wish this type to be "initial" in the sense of an initial algebra;
>that means that for any other type that also exhibits the same sort of
>two constants and an associative binary operator, there must be one
>and only one homomorphism from the bit vector type to this other type.
>
>(1)
>|- ∃:α.
>      ∃(t:α) (f:α) (c:α → α → α).
>         (∀b1 b2 b3. c b1 (c b2 b3) = c (c b1 b2) b3) /\
>         (∀β. ∀(x:β) (y:β) (op:β → β → β).
>            (∀a1 a2 a3. op a1 (op a2 a3) = op (op a1 a2) a3) ⇒
>            ∃!fn : α → β. (fn t = x) /\ fn f = y) /\
>                                 (∀b1 b2. fn (c b1 b2) = op (fn b1) (fn
>b2)))
>
>In Melham's article, he clearly describes how the "∀β." in the fourth
>line above is absolutely necessary in order for β to not be a free
>type variable when the time comes to create the constants
>corresponding to t, f, and c.
>
>The "∃:α." in the first line is a more straightforward way to express
>the existence of a type satisfying a property than Melham had
>available in his paper.
>
>Theorem (1) has been proven in HOL-Omega.  Using (1) and HOL-Omega's
>new definitional principle of type specification,
>"new_type_specification", we can create a new type called "vect" where
>all we know is its definitional axiom:
>
>(2)
>|- ∃(t:vect) (f:vect) (c:vect → vect → vect).
>         (∀b1 b2 b3. c b1 (c b2 b3) = c (c b1 b2) b3) /\
>         (∀β. ∀(x:β) (y:β) (op:β → β → β).
>            (∀a1 a2 a3. op a1 (op a2 a3) = op (op a1 a2) a3) ⇒
>            ∃!fn : vect → β. (fn t = x) /\ fn f = y) /\
>                                     (∀b1 b2. fn (c b1 b2) = op (fn
>b1) (fn b2)))
>
>Now from this theorem (2) we can use the existing term constant
>specification definitional principle, "new_specification", to actually
>create the constants t, f, and c, satisfying
>
>(3)
>|- (∀b1 b2 b3. c b1 (c b2 b3) = c (c b1 b2) b3) /\
>   (∀β. ∀(x:β) (y:β) (op:β → β → β).
>      (∀a1 a2 a3. op a1 (op a2 a3) = op (op a1 a2) a3) ⇒
>      ∃!fn : vect → β. (fn t = x) /\ fn f = y) /\
>                               (∀b1 b2. fn (c b1 b2) = op (fn b1) (fn
>b2)))
>
>The type specification rule now added to HOL-Omega may introduce
>multiple new types simultaneously:
>
>                      |- ∃:'a_1 ... 'a_n. Q
>        -------------------------------------------------
>          |- Q[newty_1, ..., newty_n / 'a_1, ..., 'a_n].
>
>The following ML function is used to make type specifications:
>
>       new_type_specification : string * string list * thm -> thm
>
>Evaluating
>
>       new_type_specification("name", ["tau_1", ..., "tau_n"],
>                              |- ∃:'a_1 ... 'a_n. Q['a_1, ..., 'a_n])
>
>simultaneously introduces new types named tau_1, ..., tau_n satisfying
>the property
>
>       |- Q[tau_1, ..., tau_n].
>
>This theorem is stored, with name "name", as a definition in the
>current theorey segment.
>
>A call to new_type_specification fails if:
>
>    (i) the theorem argument has a non-empty assumption list;
>   (ii) there are free variables or free type variables in the
>        theorem argument;
>  (iii) tau_1, ..., tau_n are not distinct names,
>   (iv) the kind of some taui does not contain all the kind variables
>        which occur in the term  ∃:'a_1 ... 'a_n. Q['a_1, ..., 'a_n].
>
>Examples of using new_type_specification are provided in
>examples/HolOmega/type_specScript.sml.
>
>This is all implemented in the current developer version of HOL-Omega,
>available by
>
>svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega
>
>Tom Melham was not able to finish implementing his dream, but 18 years
>after his paper, I hope HOL-Omega has given it a complete and full
>manifestation.  This is meant to honor his intricately beautiful and
>groundbreaking work of implementing the original HOL system with Mike
>Gordon in 1988, and his vision for the future of HOL even in 1993.
>
>All of this work has been beautifully and generously directed and
>undergirded and inspired by the Lord God Almighty.  Every good gift
>comes down from above.  If there is any value in this system, it is
>solely due to His wisdom and strength, as a pure gift from above, and
>I give Him all the credit.
>
>Soli Deo Gloria.
>
>Peter
>-- 
>"In Your majesty ride prosperously
>because of truth, humility, and righteousness;
>and Your right hand shall teach You awesome things." (Psalm 45:4)