Abstract clones for abstract syntax
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2021
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917627476049920 |
|---|---|
| author | Arkor, Nathanael McDermott, Dylan |
| author_facet | Arkor, Nathanael McDermott, Dylan |
| contents | We give a formal treatment of simple type theories, such as the simply-typed $λ$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $λ$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $β$- and $η$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2105_00969 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Abstract clones for abstract syntax Arkor, Nathanael McDermott, Dylan Logic in Computer Science Programming Languages F.3.2; F.4.1 We give a formal treatment of simple type theories, such as the simply-typed $λ$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $λ$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $β$- and $η$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax. |
| title | Abstract clones for abstract syntax |
| topic | Logic in Computer Science Programming Languages F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2105.00969 |