|
Abstract : |
Abstract. In this paper we describe the construction in hol of the inductive type of arbitrarily branching labeled trees. Such a type is characterized by an initiality theorem similar to that for finitely branching labeled trees. We discuss how to use this type to extend the system of simple recursive type specifications automatically definable in hol to ones including a limited class of functional arguments. The work discussed here is a part of a larger project to expand the recursive types package of hol which is nearing completion. All work described in this paper has been completed. 1 A Broader Class of Recursive Type Definitions The work described in this paper forms the foundation of a project to expand the class of recursive type specifications for which hol is capable of automatically defining the types specified and proving the initiality theorem, which acts as an axiomatization for the defined types. The full class of specifications the project aims to handle are those BNF-style specification of the form, |
