Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory
Say you want to prove something about an infinite data-structure, such as a stream or an infinite tree, but you would rather not subject yourself to coinduction. The unique fixed-point principle is an easyto- use, calculational alternative. The proof technique rests on the fact that certain recursio...
| Autores principales: | , |
|---|---|
| Formato: | Conference item |
| Publicado: |
2011
|
| _version_ | 1826271863257432064 |
|---|---|
| author | Hinze, R James, D |
| author_facet | Hinze, R James, D |
| author_sort | Hinze, R |
| collection | OXFORD |
| description | Say you want to prove something about an infinite data-structure, such as a stream or an infinite tree, but you would rather not subject yourself to coinduction. The unique fixed-point principle is an easyto- use, calculational alternative. The proof technique rests on the fact that certain recursion equations have unique solutions; if two elements of a coinductive type satisfy the same equation of this kind, then they are equal. In this paper we precisely characterize the conditions that guarantee a unique solution. Significantly, we do so not with a syntactic criterion, but with a semantic one that stems from the categorical notion of naturality. Our development is based on distributive laws and bialgebras, and draws heavily on Turi and Plotkin's pioneering work on mathematical operational semantics. Along the way, we break down the design space in two dimensions, leading to a total of nine points. Each gives rise to varying degrees of expressiveness, and we will discuss three in depth. Furthermore, our development is generic in the syntax of equations and in the behaviour they encode-we are not caged in the world of streams. Copyright © 2011 ACM. |
| first_indexed | 2024-03-06T22:03:26Z |
| format | Conference item |
| id | oxford-uuid:4f5ef44e-1c6c-4b2f-a77e-c2d8c019f13a |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:03:26Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:4f5ef44e-1c6c-4b2f-a77e-c2d8c019f13a2022-03-26T16:06:40ZProving the Unique Fixed-Point Principle Correct An Adventure with Category TheoryConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4f5ef44e-1c6c-4b2f-a77e-c2d8c019f13aSymplectic Elements at Oxford2011Hinze, RJames, DSay you want to prove something about an infinite data-structure, such as a stream or an infinite tree, but you would rather not subject yourself to coinduction. The unique fixed-point principle is an easyto- use, calculational alternative. The proof technique rests on the fact that certain recursion equations have unique solutions; if two elements of a coinductive type satisfy the same equation of this kind, then they are equal. In this paper we precisely characterize the conditions that guarantee a unique solution. Significantly, we do so not with a syntactic criterion, but with a semantic one that stems from the categorical notion of naturality. Our development is based on distributive laws and bialgebras, and draws heavily on Turi and Plotkin's pioneering work on mathematical operational semantics. Along the way, we break down the design space in two dimensions, leading to a total of nine points. Each gives rise to varying degrees of expressiveness, and we will discuss three in depth. Furthermore, our development is generic in the syntax of equations and in the behaviour they encode-we are not caged in the world of streams. Copyright © 2011 ACM. |
| spellingShingle | Hinze, R James, D Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title | Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title_full | Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title_fullStr | Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title_full_unstemmed | Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title_short | Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory |
| title_sort | proving the unique fixed point principle correct an adventure with category theory |
| work_keys_str_mv | AT hinzer provingtheuniquefixedpointprinciplecorrectanadventurewithcategorytheory AT jamesd provingtheuniquefixedpointprinciplecorrectanadventurewithcategorytheory |