Intrinsically Correct Sorting in Cubical Agda
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915058858065920 |
|---|---|
| author | Alexandru, Cass Choudhury, Vikraman Rot, Jurriaan van der Weide, Niels |
| author_facet | Alexandru, Cass Choudhury, Vikraman Rot, Jurriaan van der Weide, Niels |
| contents | The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort.
We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_08362 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Intrinsically Correct Sorting in Cubical Agda Alexandru, Cass Choudhury, Vikraman Rot, Jurriaan van der Weide, Niels Logic in Computer Science Combinatorics Category Theory F.3.1; F.3.2 The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law. |
| title | Intrinsically Correct Sorting in Cubical Agda |
| topic | Logic in Computer Science Combinatorics Category Theory F.3.1; F.3.2 |
| url | https://arxiv.org/abs/2412.08362 |