Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

Abstract

A system $\hat{\mathbf{I}}{»}_{\hat{I}}¸$ 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 $\hat{\mathbf{I}}{»}_{\hat{I}}¸$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\hat{\mathbf{I}}{»}_{\hat{I}}¸$ is controlled by a parameter $\hat{I}¸$ 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 some basic metatheory of $\hat{\mathbf{I}}{»}_{\hat{I}}¸$: (i) an Andrews-like characterization of its models in terms of combinatory logic is given, and this combinatory logic involves a $\mathsf{BCKW}$-like basis rather than an $\mathsf{SKI}$-like basis and (ii) semantic conservation and expressibility results relating $\hat{\mathbf{I}}{»}_{\hat{I}}¸$ to the maximal system $\hat{\mathbf{I}}{»}_{\ddot{I}}‰$ are proven. Similar results are proven for the relation between $\hat{\mathbf{I}}{»}_{\ddot{I}}‰$ and $\hat{\mathbf{I}}»$, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the semantics of the simply typed setting. In a companion paper this is extended to Church's simple theory of types. We further develop a partial correspondence between a pure combinatory logic centered on the $\mathsf{BCKW}$-like basis and the weak deductive system for $\hat{\mathbf{I}}{»}_{\ddot{I}}‰$ wherein ${\hat{I}}^2$-reduction is not allowed under a lambda abstract, and we use this to show partial deductive conservation between the maximal system $\hat{\mathbf{I}}{»}_{\ddot{I}}‰$ and the intermediary systems $\hat{\mathbf{I}}{»}_{\hat{I}}¸$.

Topics & keywords