Bootstrapping Inductive and Coinductive Types in HasCASL
We discuss the treatment of initial datatypes and final process types in the wide-spectrum language HasCASL. In particular, we present specifications that illustrate how datatypes and process types arise as bootstrapped concepts using HasCASL's type class mechanism, and we describe construction...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2008-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1166/pdf |
| _version_ | 1797268760796594176 |
|---|---|
| author | Lutz Schröder |
| author_facet | Lutz Schröder |
| author_sort | Lutz Schröder |
| collection | DOAJ |
| description | We discuss the treatment of initial datatypes and final process types in the
wide-spectrum language HasCASL. In particular, we present specifications that
illustrate how datatypes and process types arise as bootstrapped concepts using
HasCASL's type class mechanism, and we describe constructions of types of
finite and infinite trees that establish the conservativity of datatype and
process type declarations adhering to certain reasonable formats. The latter
amounts to modifying known constructions from HOL to avoid unique choice; in
categorical terminology, this means that we establish that quasitoposes with an
internal natural numbers object support initial algebras and final coalgebras
for a range of polynomial functors, thereby partially generalising
corresponding results from topos theory. Moreover, we present similar
constructions in categories of internal complete partial orders in
quasitoposes. |
| first_indexed | 2024-04-25T01:37:36Z |
| format | Article |
| id | doaj.art-52ef44084e4a42e4ae9ad6b22c00e73f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:36Z |
| publishDate | 2008-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-52ef44084e4a42e4ae9ad6b22c00e73f2024-03-08T08:57:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742008-12-01Volume 4, Issue 410.2168/LMCS-4(4:17)20081166Bootstrapping Inductive and Coinductive Types in HasCASLLutz Schröderhttps://orcid.org/0000-0002-3146-5906We discuss the treatment of initial datatypes and final process types in the wide-spectrum language HasCASL. In particular, we present specifications that illustrate how datatypes and process types arise as bootstrapped concepts using HasCASL's type class mechanism, and we describe constructions of types of finite and infinite trees that establish the conservativity of datatype and process type declarations adhering to certain reasonable formats. The latter amounts to modifying known constructions from HOL to avoid unique choice; in categorical terminology, this means that we establish that quasitoposes with an internal natural numbers object support initial algebras and final coalgebras for a range of polynomial functors, thereby partially generalising corresponding results from topos theory. Moreover, we present similar constructions in categories of internal complete partial orders in quasitoposes.https://lmcs.episciences.org/1166/pdfcomputer science - logic in computer sciencecomputer science - software engineeringd.2.1e.1f.3.1f.3.2f.4.1 |
| spellingShingle | Lutz Schröder Bootstrapping Inductive and Coinductive Types in HasCASL Logical Methods in Computer Science computer science - logic in computer science computer science - software engineering d.2.1 e.1 f.3.1 f.3.2 f.4.1 |
| title | Bootstrapping Inductive and Coinductive Types in HasCASL |
| title_full | Bootstrapping Inductive and Coinductive Types in HasCASL |
| title_fullStr | Bootstrapping Inductive and Coinductive Types in HasCASL |
| title_full_unstemmed | Bootstrapping Inductive and Coinductive Types in HasCASL |
| title_short | Bootstrapping Inductive and Coinductive Types in HasCASL |
| title_sort | bootstrapping inductive and coinductive types in hascasl |
| topic | computer science - logic in computer science computer science - software engineering d.2.1 e.1 f.3.1 f.3.2 f.4.1 |
| url | https://lmcs.episciences.org/1166/pdf |
| work_keys_str_mv | AT lutzschroder bootstrappinginductiveandcoinductivetypesinhascasl |