Research on group type theory and its functorial semantic models in category logic.
This paper explores the introduction of group structures within type theory, drawing from the algebraic theory proposed by Roy L. Crole. We define types with group structures and demonstrate that models of these types in categories with finite products can be interpreted as group objects. Each equat...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Public Library of Science (PLoS)
2025-01-01
|
| Series: | PLoS ONE |
| Online Access: | https://doi.org/10.1371/journal.pone.0326301 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849419080580202496 |
|---|---|
| author | Jian-Gang Tang Yimamujiang Aishan Ji-Yu Liu Jia-Yin Peng |
| author_facet | Jian-Gang Tang Yimamujiang Aishan Ji-Yu Liu Jia-Yin Peng |
| author_sort | Jian-Gang Tang |
| collection | DOAJ |
| description | This paper explores the introduction of group structures within type theory, drawing from the algebraic theory proposed by Roy L. Crole. We define types with group structures and demonstrate that models of these types in categories with finite products can be interpreted as group objects. Each equation within the context of group theory types corresponds to a commutative diagram, representing the axioms of groups, inspired by Lawvere's functorial semantics. Moreover, we clarify the role of control equations associated with fundamental properties of groups, such as operations and identities. By formalizing a type referred to as "Group Type," which involves integrating group operations and the equations they satisfy into an algebraic type, we incorporate the algebraic structure of a specific group into this type. This Group Type represents a concrete algebraic structure. In practical applications, the introduction of group structures into types is anticipated to optimize algorithms and data structures, leveraging the algebraic properties of groups to enhance computational efficiency. Furthermore, our exploration is not limited to mathematical conversions; it is also envisioned to extend to the application in various type systems, providing support for future research in formal verification and program analysis in computer science. |
| format | Article |
| id | doaj-art-e6f3093196594346aab61e7163fb20e6 |
| institution | Kabale University |
| issn | 1932-6203 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | Public Library of Science (PLoS) |
| record_format | Article |
| series | PLoS ONE |
| spelling | doaj-art-e6f3093196594346aab61e7163fb20e62025-08-20T03:32:15ZengPublic Library of Science (PLoS)PLoS ONE1932-62032025-01-01206e032630110.1371/journal.pone.0326301Research on group type theory and its functorial semantic models in category logic.Jian-Gang TangYimamujiang AishanJi-Yu LiuJia-Yin PengThis paper explores the introduction of group structures within type theory, drawing from the algebraic theory proposed by Roy L. Crole. We define types with group structures and demonstrate that models of these types in categories with finite products can be interpreted as group objects. Each equation within the context of group theory types corresponds to a commutative diagram, representing the axioms of groups, inspired by Lawvere's functorial semantics. Moreover, we clarify the role of control equations associated with fundamental properties of groups, such as operations and identities. By formalizing a type referred to as "Group Type," which involves integrating group operations and the equations they satisfy into an algebraic type, we incorporate the algebraic structure of a specific group into this type. This Group Type represents a concrete algebraic structure. In practical applications, the introduction of group structures into types is anticipated to optimize algorithms and data structures, leveraging the algebraic properties of groups to enhance computational efficiency. Furthermore, our exploration is not limited to mathematical conversions; it is also envisioned to extend to the application in various type systems, providing support for future research in formal verification and program analysis in computer science.https://doi.org/10.1371/journal.pone.0326301 |
| spellingShingle | Jian-Gang Tang Yimamujiang Aishan Ji-Yu Liu Jia-Yin Peng Research on group type theory and its functorial semantic models in category logic. PLoS ONE |
| title | Research on group type theory and its functorial semantic models in category logic. |
| title_full | Research on group type theory and its functorial semantic models in category logic. |
| title_fullStr | Research on group type theory and its functorial semantic models in category logic. |
| title_full_unstemmed | Research on group type theory and its functorial semantic models in category logic. |
| title_short | Research on group type theory and its functorial semantic models in category logic. |
| title_sort | research on group type theory and its functorial semantic models in category logic |
| url | https://doi.org/10.1371/journal.pone.0326301 |
| work_keys_str_mv | AT jiangangtang researchongrouptypetheoryanditsfunctorialsemanticmodelsincategorylogic AT yimamujiangaishan researchongrouptypetheoryanditsfunctorialsemanticmodelsincategorylogic AT jiyuliu researchongrouptypetheoryanditsfunctorialsemanticmodelsincategorylogic AT jiayinpeng researchongrouptypetheoryanditsfunctorialsemanticmodelsincategorylogic |