Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909887083053056 |
|---|---|
| author | Cerda, Rémy |
| author_facet | Cerda, Rémy |
| contents | Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in {0,1}) and of capture-avoiding substitution on alpha-equivalence classes of such terms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_02595 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi Cerda, Rémy Logic in Computer Science Programming Languages F.3.3; F.4.1; D.3.3 Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in {0,1}) and of capture-avoiding substitution on alpha-equivalence classes of such terms. |
| title | Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi |
| topic | Logic in Computer Science Programming Languages F.3.3; F.4.1; D.3.3 |
| url | https://arxiv.org/abs/2511.02595 |