Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918163416875008 |
|---|---|
| author | Walsh, Sean |
| author_facet | Walsh, Sean |
| contents | A system $\boldsymbolλ_θ$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the system $\boldsymbolλ_θ$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbolλ_θ$ is controlled by a parameter $θ$ which allows more options for state types and state variables than is present in Montague and Gallin. A main goal of the paper is to establish the basic metatheory of $\boldsymbolλ_θ$: (i) a completeness theorem is proven for $βη$-reduction, and (ii) an Andrews-like characterization of Henkin models in terms of combinatory logic is given; and this involves, with some necessity, a distanced version of $β$-reduction and a $\mathsf{BCKW}$-like basis rather than $\mathsf{SKI}$-like basis. Further, conservation of the maximal system $\boldsymbolλ_ω$ over $\boldsymbolλ_θ$ is proven, and expressibility of $\boldsymbolλ_ω$ in $\boldsymbolλ_θ$ is proven; thus these modal logics are highly expressive. Similar results are proven for the relation between $\boldsymbolλ_ω$ and $\boldsymbolλ$, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the simply-typed setting. In a companion paper this is extended to Church's simple theory of types. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_17463 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic Walsh, Sean Logic in Computer Science Logic 03B15, 03B40, 03B45 (Primary) 03B65, 68N18 (Secondary) F.4.1; F.3.1 A system $\boldsymbolλ_θ$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the system $\boldsymbolλ_θ$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbolλ_θ$ is controlled by a parameter $θ$ which allows more options for state types and state variables than is present in Montague and Gallin. A main goal of the paper is to establish the basic metatheory of $\boldsymbolλ_θ$: (i) a completeness theorem is proven for $βη$-reduction, and (ii) an Andrews-like characterization of Henkin models in terms of combinatory logic is given; and this involves, with some necessity, a distanced version of $β$-reduction and a $\mathsf{BCKW}$-like basis rather than $\mathsf{SKI}$-like basis. Further, conservation of the maximal system $\boldsymbolλ_ω$ over $\boldsymbolλ_θ$ is proven, and expressibility of $\boldsymbolλ_ω$ in $\boldsymbolλ_θ$ is proven; thus these modal logics are highly expressive. Similar results are proven for the relation between $\boldsymbolλ_ω$ and $\boldsymbolλ$, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the simply-typed setting. In a companion paper this is extended to Church's simple theory of types. |
| title | Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic |
| topic | Logic in Computer Science Logic 03B15, 03B40, 03B45 (Primary) 03B65, 68N18 (Secondary) F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2410.17463 |