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) ------------------------------------------------------------------------------ Benefiting from Server Virtualization: Beyond Initial Workload Consolidation -- Increasing the use of server virtualization is a top priority.Virtualization can reduce costs, simplify management, and improve application availability and disaster protection. Learn more about boosting the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
