Linearization via Rewriting (Long Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917967700164608 |
|---|---|
| author | Lago, Ugo Dal Olimpieri, Federico |
| author_facet | Lago, Ugo Dal Olimpieri, Federico |
| contents | We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_04408 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Linearization via Rewriting (Long Version) Lago, Ugo Dal Olimpieri, Federico Logic in Computer Science Programming Languages We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based. |
| title | Linearization via Rewriting (Long Version) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2503.04408 |