Bootstrapping Inductive and Coinductive Types in HasCASL

摘要

We discuss the treatment of initial datatypes and final process types in thewide-spectrum language HasCASL. In particular, we present specifications thatillustrate how datatypes and process types arise as bootstrapped concepts usingHasCASL's type class mechanism, and we describe constructions of types offinite and infinite trees that establish the conservativity of datatype andprocess type declarations adhering to certain reasonable formats. The latteramounts to modifying known constructions from HOL to avoid unique choice; incategorical terminology, this means that we establish that quasitoposes with aninternal natural numbers object support initial algebras and final coalgebrasfor a range of polynomial functors, thereby partially generalisingcorresponding results from topos theory. Moreover, we present similarconstructions in categories of internal complete partial orders inquasitoposes.