Why we can't have SML style datatype declarations in HOL

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

The type descriptions that define_type is capable of handling are noticeably more limited than those allowed by SML. In particular, define_type requires of a type description it is given that the type being defined should not occur within any compound type. While this restriction is more severe than is necessary for there to be a solution in HOL to the description, we show that some restriction on the nature of the compound types within which the type being defined may occur is necessary. Not all descriptions allowable in SML will have a solution in HOL. Moreover, owing to the nature of the basic principle of type definition in HOL, no purely syntactic non-ad hoc test of a recursive type description will be sufficient to allow us to extend define_type to compound types involving `safe' type constructors such as list while at the same time barring all descriptions for which no solution is possible. Any general extension to the define_type package that allows the types being defined to occur within compound types in the type description will need to take as additional arguments theorems about the type constructors used in the compound type that justify their being so used. Finally, we show that an extension to the case where all the type constructors used in compound types involving the types being defined are essentially recursive type constructors themselves; the type constructors must satisfy an `initiality' theorem of the form returned by define_type, which must be supplied as an argument to this extension of define_type.

Original languageEnglish (US)
Title of host publicationIFIP Transactions A
Subtitle of host publicationComputer Science and Technology
PublisherPubl by Elsevier Science Publishers B.V.
Pages561-568
Number of pages8
EditionA-20
ISBN (Print)0444898808
StatePublished - Dec 1 1993
Externally publishedYes
EventProceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications - HOL'92 - Leuven, Belg
Duration: Sep 21 1992Sep 24 1992

Other

OtherProceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications - HOL'92
CityLeuven, Belg
Period9/21/929/24/92

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Why we can't have SML style datatype declarations in HOL'. Together they form a unique fingerprint.

Cite this