Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910664682897408 |
|---|---|
| author | Stassen, Philipp Jan Andries Møgelberg, Rasmus Ejlers Zwart, Maaike Aguirre, Alejandro Birkedal, Lars |
| author_facet | Stassen, Philipp Jan Andries Møgelberg, Rasmus Ejlers Zwart, Maaike Aguirre, Alejandro Birkedal, Lars |
| contents | Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics, as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_04455 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Modelling Recursion and Probabilistic Choice in Guarded Type Theory Stassen, Philipp Jan Andries Møgelberg, Rasmus Ejlers Zwart, Maaike Aguirre, Alejandro Birkedal, Lars Programming Languages Logic in Computer Science F.3.1; F.3.2 Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics, as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence. |
| title | Modelling Recursion and Probabilistic Choice in Guarded Type Theory |
| topic | Programming Languages Logic in Computer Science F.3.1; F.3.2 |
| url | https://arxiv.org/abs/2408.04455 |