Menu
▾
▴
Re: [Hol-info] Abstract data types in HOL-Omega
|
From: Peter V. H. <pal...@tr...> - 2011-04-21 20:53:33
|
Dear Tom, Thank you so much for your kind words. I am very happy that you were pleased with my attempt to carry forward your work. If there is any further features you'd like to see added, any other ideas you had which you'd like implemented, please let me know. I'm still struck by your forward-looking vision from the perspective of 1993. In sincere gratitude, Peter 2011/4/21 Thomas Melham <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) > > -- "In Your majesty ride prosperously because of truth, humility, and righteousness; and Your right hand shall teach You awesome things." (Psalm 45:4) |
