On computational interpretations of the modal logic S4. I. Cut elimination

A language of constructions for minimal logic is the $\lambda$-calculus, where cut-elimination is encoded as $\beta$-reduction. We examine corresponding languages for the minimal version of the modal logic S4, with notions of reduction that encodes cut-elimination for the corresponding sequent system. It turns out that a natural interpretation of the latter constructions is a $\lambda$-calculus extended by an idealized version of Lisp\u27s \verb/eval/ and \verb/quote/ constructs. In this first part, we analyze how cut-elimination works in the standard sequent system for minimal S4, and where problems arise. Bierman and De Paiva\u27s proposal is a natural language of constructions for this logic, but their calculus lacks a few rules that are essential to eliminate all cuts. The ${\lambda_{\rm S4}}$-calculus, namelyBierman and De Paiva\u27s proposal extended with all needed rules, is confluent. There is a polynomial-time algorithm to compute principal typings of given terms, or answer that the given terms are not typable. The typed ${\lambda_{\rm S4}}$-calculus terminates, and normal forms are exactly constructions for cut-free proofs. Finally, modulo some notion $\sqeq$ of equivalence, there is a natural Curry-Howard style isomorphism between typed ${\lambda_{\rm S4}}$-terms and natural deduction proofs in minimal S4. However, the ${\lambda_{\rm S4}}$-calculus has a non-operational flavor, in that the extra rules include explicit garbage collection, contraction and exchange rules. We shall propose another language of constructions to repair this in Part II