Electronic Notes in Computer Science 1 (1995)On a Modal λ-Calculus for S4?F. PfenningDepartment of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213 [email protected]. C. WongDepartment of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213 [email protected] present λ→2, a concise formulation of a proof term calculus for the intuitionistic modal logicS4 that is well-suited for practical applications. We show that, with respect to provability, it isequivalent to other formulations in the literature, sketch a simple type checking algorithm, and provesubject reduction and the existence of canonical forms for well-typed terms. Applications include anew formulation of natural deduction for intuitionistic linear logic, modal logical frameworks, anda logical analysis of staged computation and binding-time analysis for functional languages [6].1 IntroductionModal operators familiar from traditional logic have received renewed attention in computerscience through their importance in linear logic. Typically, they are described axiomati-cally in the style of Hilbert or via sequent calculi. However, the Curry-Howard isomorphismbetween proofs and λ-terms is most poignant for natural deduction, so natural deduction for-mulations of modal and linear logics have also been the subject of research [20,1,5,3,4,22,13].?This work is supported by NSF Grant CCR-9303383 and the Advanced Research Projects Agencyunder ARPA Order No. 8313.c 1995 Elsevier Publishers B. V. and the author.F. Pfenning and H. C. WongAlthough most of the researchers in this area agree on the (potential) applications of modallogics, the works published to date seem to be primarily oriented toward proof theory andnot well suited for practical applications.Among the application areas of modal and linear logics are those of functional programmingand logical frameworks. In these settings, the simplicity of the language, a feasible typechecking procedure, the existence of canonical forms, and the property of type preservationare among the most desirable results. None of the work done to date, however, incorporatesthese results and characteristics.In this paper we present λ→2, a new, concise formulation of a term calculus equivalent, via aCurry-Howard isomorphism, to the intuitionistic modal logic S4, that is well-suited for typechecking. We show that, with respect to provability, it is equivalent to other formulations inthe literature and sketch a type checking algorithm. We then prove subject reduction and theexistence of a canonical form for every well-typed term. We omit a simpler and not so relevantstrong normalization result. A similar, but more verbose system motivated by proof-theoreticconsiderations has been given by Martini & Masini [13]. They investigate normalization andthe Church-Rosser property which is complementary to our own meta-theoretic study.A similar approach can be used beyond S4 to give an analogous formulation of intuitionisticlinear logic which is beyond the scope of this paper. A related system without weakeningand contraction has been analysed by Martini & Masini [14]. Our system can also serve asthe basis for a modal logical framework used for explanation-based generalization [7] and forbinding-time analysis of functional languages [6]. Another application to the combination ofhigher-order abstract syntax and induction in logical frameworks is the subject of currentresearch and sketched in slightly more detail in the conclusion.The remainder of this paper is structured as follows. Section 2 presents what we call anexplicit system, as given in [5,22], a formulation of a modal λ-calculus for S4 in which explicitsubstitutions in terms are used to enforce the global validity conditions associated with themodal2operator. In Section 3 we present our system λ→2, which immediately yields apractical procedure for type checking. In Section 4 we show that the two are equivalent withrespect to provability. In Section 5 we introduce a notion of approximate typing and showthat every approximately typed term can be converted to canonical form. We also provesubject reduction and type preservation for precise typing. In Section 6, we discuss relatedwork. In Section 7 we conclude with future work and brief discussions about concrete andpotential applications.2F. Pfenning and H. C. Wong2Modalλ-Calculus: An Explicit FormulationIn this section we present a formulation of a modal λ-calculus for intuitionistic S4, as it isgiven, for example, in [5]. We denote this system by λ→2e. We refer to it as explicit since itrequires substitutions to occur explicitly within terms in order to deal with the non-localvalidity conditions imposed by the modal operator. Much of the material in the subsequentsections will be concerned with a formulation where substitutions are no longer required.2.1 SyntaxTypes A ::= b | A1→ A2|2ATerms E ::= x | λx:A. E | E1E2| boxσ2ΓE | unbox EContexts Γ ::= ·|Γ,x:ASubstitutions σ ::= ·|σ, E/xBoxed Contexts2Γ ::= ·|2Γ,x:2AWe use b for base types and x for variables. We assume that any variable can be declaredat most once in a context Γ and defined at most once in a substutition σ. Bound variablesmay be renamed tacitly. We use A, B to range over types, E to range over terms, and Γ, ∆to range over contexts. We omit leading ·’s from contexts and substitutions for the sakeof brevity. We write [E0/x]E for the result of substituting E0for x in E, renaming boundvariables as necessary in order to avoid the capture of free variables in E0. Similarly, σEis the result of applying the substitution σ to E. We write idΓfor the identity substutionx1/x1,...,xn/xnon Γ = x1:A1,...,xn:An. The addition of types2A to the simply-typedλ-calculus introduces two new term constructs: box and unbox. box introduces objects oftype2A,andunbox is the corresponding elimination construct. The box construct requires asubstitution σ and a context2Γ whose role should become clear when we present the typingrules.2.2 Typing RulesThe problem of typing in the explicit system is well understood; we present here the systemin [5], using a slightly different notation. It is given by the following set of inference rules3F. Pfenning and H. C. Wongdefining the mutually recursive judgments for the typing of terms and substitutions.∆ `eE : A explicit term E has type A in context ∆∆ `eσ :Γ σis a valid substitution from terms over Γ to terms over ∆x:A in