A Linear-logical Reconstruction of Intuitionistic Modal Logic S4

TL;DR

This paper develops a novel modal linear logic framework to accurately translate intuitionistic modal logic S4 into linear logic, addressing modality interactions and providing semantics via Geometry of Interaction.

Contribution

It introduces a modal linear logic that extends intuitionistic multiplicative exponential linear logic to incorporate S4 modalities, enabling a sound translation from IS4.

Findings

Established a sound translation from IS4 to modal linear logic.

Provided a Geometry of Interaction semantics for the modal lambda-calculus.

Resolved modality interaction issues in linear logic translation.

Abstract

We propose a "modal linear logic" to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.

Figures

Equations

$$\text{Formulae}\text{leavevmode}\text{leavevmode}A,B,C::=p\text{leavevmode}|\text{leavevmode}A⊸B\text{leavevmode}|\text{leavevmode}!A$$

$$\lceil p\rceil \stackrel{\mathrm{def}}{=}p,\lceil A\supset B\rceil \stackrel{\mathrm{def}}{=}(!\lceil A\rceil )⊸\lceil B\rceil$$

$$\lceil \Gamma \rceil$$

$$\text{Formulae}\text{leavevmode}\text{leavevmode}A,B,C::=p\text{leavevmode}|\text{leavevmode}A\supset B\text{leavevmode}|\text{leavevmode}\square A$$

$$A,B,C$$

$$M,N,L$$

$$|\text{leavevmode}\square M\text{leavevmode}|\text{leavevmode}\mathbf{let}\square x=M\mathbf{in}N$$

$$(\beta \supset )$$

$$(\beta \square )$$

$$A,B$$

$$\lceil -\rceil$$

$$\text{Formulae}\text{leavevmode}\text{leavevmode}A,B,C::=p\text{leavevmode}|\text{leavevmode}A⊸B\text{leavevmode}|\text{leavevmode}!A\text{leavevmode}|\text{leavevmode}\square \text{raise}0.86108pt\text{scalebox}0.7!A$$

$$\lceil p\rceil \stackrel{\mathrm{def}}{=}p,\lceil A\supset B\rceil \stackrel{\mathrm{def}}{=}(!\lceil A\rceil )⊸\lceil B\rceil ,\lceil \square A\rceil \stackrel{\mathrm{def}}{=}\square \text{raise}0.86108pt\text{scalebox}0.7!\lceil A\rceil$$

$$\lceil \Gamma \rceil$$

$$A,B,C$$

$$M,N,L$$

$$|\text{leavevmode}\mathbf{let}!x=M\mathbf{in}N\text{leavevmode}|\text{leavevmode}\mathbf{let}\square \text{raise}0.86108pt\text{scalebox}0.7!x=M\mathbf{in}N$$

$$(\beta ⊸)$$

$$(\beta !)$$

$$(\beta \square \text{raise}0.86108pt\text{scalebox}0.7!\text{leavevmode})$$

$$\lceil p\rceil$$

$$\lceil A\supset B\rceil$$

$$\lceil \square A\rceil$$

$$\lceil \Gamma \rceil$$

$$\mathcal{T}\lceil x\rceil$$

$$\mathcal{T}\lceil \lambda x:A.M\rceil$$

$$\mathcal{T}\lceil MN\rceil$$

$$\mathcal{T}\lceil \square M\rceil$$

$$\mathcal{T}\lceil \mathbf{let}\square x=M\mathbf{in}N\rceil$$

$$A,B,C$$

$$M,N,L$$

$$\mathrm{I}M$$

$$\mathrm{B}MNL$$

$$\mathrm{C}MNL$$

$${\mathrm{S}}^{\delta }MN(\delta L)$$

$${\mathrm{K}}^{\delta }M(\delta N)$$

$${\mathrm{W}}^{\delta }M(\delta N)$$

$${\mathrm{T}}^{\delta }(\delta M)$$

$${\mathrm{D}}^{\delta }(\delta M)(\delta N)$$

$$4^{\delta }(\delta M)$$

$$\mathrm{E}\square \text{raise}0.86108pt\text{scalebox}0.7!M$$

$$\text{Formulae}\text{leavevmode}\text{leavevmode}A,B,C$$

Full text

\NewEnvironrulefigure[2]

A Linear-logical Reconstruction of Intuitionistic Modal Logic S4

Yosuke Fukuda

  

Akira Yoshimizu

1 Introduction

Linear logic discovered by Girard [7] is, as he wrote, not an alternative logic but should be regarded as an “extension” of usual logics. Whereas usual logics such as classical logic and intuitionistic logic admit the structural rules of weakening and contraction, linear logic does not allow to use the rules freely, but it reintroduces them in a controlled manner by using the exponential modality ‘$!$’ (and its dual ‘$?$’). Usual logics are then reconstructed in terms of linear logic with the power of the exponential modalities, via the Girard translation.

In this paper, we aim to extend the framework of linear-logical reconstruction to the $(\Box,\supset)$-fragment of intuitionistic modal logic S4 ($\mathrm{IS4}$) by establishing what we call “modal linear logic” and an S4-version of Girard translation from $\mathrm{IS4}$ into it. However, the crux to give a faithful translation is that a naive combination of the $\Box$-modality and the $!$-modality causes an undesirable interaction between the inference rules of the two modalities. To solve the problem, we define the modal linear logic as an extension of intuitionistic multiplicative exponential linear logic with a modality ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’ (pronounced by “bangbox”) that integrates ‘$\Box$’ and ‘$!$’, and show that it admits a faithful translation from $\mathrm{IS4}$.

As an application, we consider a computational interpretation of the modal linear logic. A typed $\lambda$-calculus that we will define corresponds to a natural deduction for the modal linear logic through the Curry–Howard correspondence, and it can be seen as a reconstruction of the modal $\lambda$-calculus by Pfenning and Davies [18, 5] for the so-called staged computation. Thanks to our linear-logical reconstruction, we can further obtain a Geometry of Interaction Machine (GoIM) for the modal $\lambda$-calculus.

The remainder of this paper is organized as follows. In Section 2 we review some formalizations of linear logic and $\mathrm{IS4}$. In Section 3 we explain a linear-logical reconstruction of $\mathrm{IS4}$. First, we discuss how a naive combination of linear logic and modal logic fails to obtain a faithful translation. Then, we propose a modal linear logic with the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -modality that admits a faithful translation from $\mathrm{IS4}$. In Section 4 we give a computational interpretation of modal linear logic through a typed $\lambda$-calculus. In Section 5 we provide an axiomatization of modal linear logic by a Hilbert-style deductive system. In Section 6 we obtain a GoIM of our typed $\lambda$-calculus as an application of our linear-logical reconstruction. In Sections 7 and 8 we discuss related work and conclude our work, respectively.

2 Preliminaries

We recall several systems of linear logic and modal logic. In this paper, we consider the minimal setting to give an S4-version of Girard translation and its computational interpretation. Thus, every system we will use only contain an implication and a modality as operators.

2.1 Intuitionistic MELL and its Girard translation

{rulefigure}

fig:imellDefinition of $\mathrm{IMELL}$.

Syntactic category

$\displaystyle\text{Formulae}\leavevmode\nobreak\ \leavevmode\nobreak\ A,B,C::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\multimap\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}$

Inference rule

$\mathrm{Ax}$

$\mathit{A}\,\vdash\,\mathit{A}$

$\Gamma\,\vdash\,\mathit{A}$    $\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

$!\Gamma\,\vdash\,\mathit{A}$

$!\mathrm{R}$

$!\Gamma\,\vdash\,!\mathit{A}$

[TABLE]

{rulefigure}

fig:girard_translationDefinition of the Girard translation from intuitionistic logic.

$\lceil\mathit{A}\rceil$

$\displaystyle\hskip 15.00002pt\lceil\mathit{p}\rceil\overset{\mathrm{def}}{=}p,\hskip 35.00005pt\lceil\mathit{A}\supset\mathit{B}\rceil\overset{\mathrm{def}}{=}(!\lceil\mathit{A}\rceil)\multimap\lceil\mathit{B}\rceil$

$\lceil\Gamma\rceil$

$\displaystyle\hskip 15.00002pt\lceil\Gamma\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\{\lceil\mathit{A}\rceil\leavevmode\nobreak\ |\leavevmode\nobreak\ A\in\Gamma\}$

Figure LABEL:fig:imell shows the standard definition of the ($!$, $\multimap$)-fragment of intuitionistic multiplicative exponential linear logic, which we refer to as $\mathrm{IMELL}$. A formula is either a propositional variable, a linear implication, or an exponential modality. We let $p$ range over the set of propositional variables, and $A$, $B$, $C$ range over formulae. A context $\Gamma$ is defined to be a multiset of formulae, and hence the exchange rule is assumed as a meta-level operation. A judgment consists of a context and a formula, written as $\Gamma\,\vdash\,\mathit{A}$. As a convention, we often write $\Gamma\,\vdash\,\mathit{A}$ to mean that the judgment is derivable (and we assume similar conventions throughout this paper). The notation $!\Gamma$ in the rule $!\mathrm{R}$ denotes the multiset $\{!A\leavevmode\nobreak\ |\leavevmode\nobreak\ A\in\Gamma\}$.

Figure LABEL:fig:girard_translation defines the Girard translation111This is known to be the call-by-name Girard translation (cf. [12]) and we only follow this version in later discussions. However, we conjectured that our work can apply to other versions. from the $\supset$-fragment of intuitionistic propositional logic $\mathrm{IL}$. For an $\mathrm{IL}$-formula $A$, $\lceil\mathit{A}\rceil$ will be an $\mathrm{IMELL}$-formula; and $\lceil\Gamma\rceil$ a multiset of $\mathrm{IMELL}$-formulae. Then, we can show that the Girard translation from $\mathrm{IL}$ to $\mathrm{IMELL}$ is sound.

Theorem 2.1** (Soudness of the translation).**

If $\Gamma\,\vdash\,\mathit{A}$ in $\mathrm{IL}$, then $!\lceil\Gamma\rceil\,\vdash\,\lceil\mathit{A}\rceil$ in $\mathrm{IMELL}$.

2.2 Intuitionistic S4

We review a formalization of the $(\Box,\supset)$-fragment of intuitionistic propositional modal logic S4 ($\mathrm{IS4}$). In what follows, we use a sequent calculus for the logic, called $\mathrm{LJ}^{\Box}$. The calculus $\mathrm{LJ}^{\Box}$ used here is defined in a standard manner in the literature (e.g. it can be seen as the $\mathrm{IS4}$-fragment of G1s for classical modal logic S4 by Troelstra and Schwichtenberg [23]).

Figure LABEL:fig:ljbox shows the definition of $\mathrm{LJ}^{\Box}$. A formula is either a propositional variable, an intuitionistic implication, or a box modality. A context and a judgment are defined similarly in $\mathrm{IMELL}$. The notation $\Box\Gamma$ in the rule $\Box\mathrm{R}$ denotes the multiset $\{\Box\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ A\in\Gamma\}$.

{rulefigure}

fig:ljboxDefinition of $\mathrm{LJ}^{\Box}$.

Syntactic category

$\displaystyle\text{Formulae}\leavevmode\nobreak\ \leavevmode\nobreak\ A,B,C::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\supset\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ \Box\mathit{A}$

Inference rule

$\mathrm{Ax}$

$\mathit{A}\,\vdash\,\mathit{A}$

$\Gamma\,\vdash\,\mathit{A}$    $\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

$\Box\Gamma\,\vdash\,\mathit{A}$

$\Box\mathrm{R}$

$\Box\Gamma\,\vdash\,\Box\mathit{A}$

[TABLE]

Remark 2.2**.**

It is worth noting that the $!$-exponential in $\mathrm{IMELL}$ and the $\Box$-modality in $\mathrm{LJ}^{\Box}$ have similar structures. To see this, let us imagine the rules $\Box\mathrm{R}$ and $\Box\mathrm{L}$ replacing the symbol ‘$\Box$’ with ‘$!$’. The results will be exactly the same as $!\mathrm{R}$ and $!\mathrm{L}$. In fact, the $!$-exponential satisfies the S4 axiomata in $\mathrm{IMELL}$, which is the reason we also call it as a modality.

2.3 Typed $\lambda$-calculus of the intuitionistic S4

We review the modal $\lambda$-calculus developed by Pfenning and Davies [18, 5], which we call $\lambda^{\Box}$. The system $\lambda^{\Box}$ is essentially the same calculus as $\lambda^{\rightarrow\Box}_{e}$ in [5], although some syntax are changed to fit our notation in this paper. $\lambda^{\Box}$ is known to correspond to a natural deduction system for $\mathrm{IS4}$, as is shown in [18].

{rulefigure}

fig:lambdaboxDefinition of $\lambda^{\Box}$.

Syntactic category

Types $\displaystyle A,B,C$ $\displaystyle::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\supset\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ \Box\mathit{A}$

Terms $\displaystyle M,N,L$ $\displaystyle::=x\leavevmode\nobreak\ |\leavevmode\nobreak\ \lambda\mathit{x}:\mathit{A}.\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{M}\,\mathit{N}$

$\displaystyle\,|\leavevmode\nobreak\ \Box\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathbf{let}\,\Box\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$

Reduction rule

$\displaystyle(\beta\supset)\hskip 5.0pt$ $\displaystyle(\lambda\mathit{x}:\mathit{A}.\mathit{M})\,\mathit{N}$ $\displaystyle\leadsto\mathit{M}[\mathit{x}:=\mathit{N}]$

$\displaystyle(\beta\Box)\hskip 5.0pt$ $\displaystyle\mathbf{let}\,\Box\mathit{x}=\Box\mathit{N}\,\mathbf{in}\,\mathit{M}$ $\displaystyle\leadsto\mathit{M}[\mathit{x}:=\mathit{N}]$

[TABLE]

Figure LABEL:fig:lambdabox shows the definition of $\lambda^{\Box}$. The set of types corresponds to that of formulae of $\mathrm{IS4}$. We let $x$ range over the set of term variables, and $M,N,L$ range over the set of terms. The first three terms are as in the simply-typed $\lambda$-calculus. The terms $\Box\mathit{M}$ and $\mathbf{let}\,\Box\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$ is used to represent a constructor and a destructor for types $\Box\mathit{A}$, respectively. The variable $x$ in $\lambda\mathit{x}:\mathit{A}.\mathit{M}$ and $\mathbf{let}\,\Box\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$ is supposed to be bound in the usual sense and the scope of the biding is $M$ and $N$, respectively. The set of free (i.e., unbound) variables in $M$ is denoted by $\mathrm{FV}(M)$. We write the capture-avoiding substitution $\mathit{M}[\mathit{x}:=\mathit{N}]$ to denote the result of replacing $N$ for every free occurrence of $x$ in $M$.

A (type) context is defined to be the set of pairs of a term variable $x_{i}$ and a type $A_{i}$ such that all the variables are distinct, which is written as $x_{1}:A_{1},\cdots,x_{n}:A_{n}$ and is denoted by $\Gamma$, $\Delta$, $\Sigma$, etc. Then, a (type) judgment is defined, in the so-called dual-context style, to consists of two contexts, a term, and a type, written as $\Delta;\Gamma\,\vdash\,\mathit{M}:\mathit{A}$.

The intuition behind the judgment $\Delta;\Gamma\,\vdash\,\mathit{M}:\mathit{A}$ is that the context $\Delta$ is intended to implicitly represent assumptions for types of form $\Box\mathit{A}$, while the context $\Gamma$ is used to represent ordinary assumptions as in the simply-typed $\lambda$-calculus.

The typing rules are summarized as follows. $\mathrm{Ax}$, $\supset\!\mathrm{I}$, and $\supset\!\mathrm{E}$ are all standard, although they are defined in the dual-context style. $\Box\mathrm{Ax}$ is another variable rule, which can be seen as what to formalize the modal axiom T (i.e., $\vdash\,\Box\mathit{A}\supset\mathit{A}$) from the logical viewpoint. $\Box\mathrm{I}$ is a rule for the constructor of $\Box\mathit{A}$, which corresponds to the necessitation rule for the $\Box$-modality. Similarly, $\Box\mathrm{E}$ is for the destructor of $\Box\mathit{A}$, which corresponds to the elimination rule.

The reduction $\leadsto$ is defined to be the least compatible relation on terms generated by $(\beta\supset)$ and $(\beta\Box)$. The multistep reduction $\leadsto^{+}$ is defined to be the transitive closure of $\leadsto$.

3 Linear-logical reconstruction

3.1 Naive attempt at the linear-logical reconstruction

It is natural for a “linear-logical reconstruction” of $\mathrm{IS4}$ to define a system that has both properties of linear logic and modal logic, so as to be a target system for an S4-version of Girard translation. However, a naive combination of linear logic and modal logic is not suitable to establish a faithful translation.

Let us consider what happens if we adopt a naive system. The simplest way to define a target system for the S4-version of Girard translation is to make an extension of $\mathrm{IMELL}$ with the $\Box$-modality. Suppose that a deductive system $\mathrm{IMELL}^{\Box}$ is such a calculus, that is, the formulae of $\mathrm{IMELL}^{\Box}$ are defined by the following grammar:

[TABLE]

with the inference rules being those of $\mathrm{IMELL}$, along with the rules $\Box\mathrm{R}$ and $\Box\mathrm{L}$ of $\mathrm{LJ}^{\Box}$.

As in the case of Girard translation from $\mathrm{IL}$ to $\mathrm{IMELL}$, we have to establish the following theorem for some translation $\lceil-\rceil$:

If $\Gamma\,\vdash\,\mathit{A}$ is derivable in $\mathrm{LJ}^{\Box}$, then so is $!\lceil\Gamma\rceil\,\vdash\,\lceil\mathit{A}\rceil$ in $\mathrm{IMELL}^{\Box}$.

but, if we extend our previous translation $\lceil-\rceil$ from $\mathrm{IL}$ to $\mathrm{IMELL}$ with $\lceil\Box\mathit{A}\rceil\overset{\mathrm{def}}{=}\Box\lceil\mathit{A}\rceil$, we get stuck in the case of $\Box\mathrm{R}$. This is because we need to establish the inference $\Box^{\prime}$ in Figure 4, which means that we have to be able to obtain a derivation of form $!\lceil\Box\Gamma\rceil\,\vdash\,\Box\lceil\mathit{A}\rceil$ from that of $!\lceil\Box\Gamma\rceil\,\vdash\,\lceil\mathit{A}\rceil$ in $\mathrm{IMELL}^{\Box}$.

However, the inference $\Box^{\prime}$ is invalid in $\mathrm{IMELL}^{\Box}$ in general, because there exists a counterexample. First, the inference shown in Figure 4 is valid, and the judgment $\Box(\mathit{p}\supset\mathit{q}),\Box\mathit{p}\,\vdash\,\Box\mathit{q}$ is indeed derivable in $\mathrm{LJ}^{\Box}$. However, the corresponding inference via $\lceil-\rceil$ is invalid as Figure 4 shows. In the figure, the judgments correspond to those in Figure 4 via $\lceil-\rceil$, but the inference $\Box\mathrm{R}$ in Figure 4 is invalid in $\mathrm{IMELL}^{\Box}$ due to the side-condition of $\Box\mathrm{R}$. Even worse, we can see that the judgment $!\Box(!\mathit{p}\multimap\mathit{q}),!\Box\mathit{p}\,\vdash\,\Box\mathit{q}$ is itself underivable in $\mathrm{IMELL}^{\Box}$222Precisely speaking, this can be shown as a consequence of the cut-elimination theorem of $\mathrm{IMELL}^{\Box}$, and the theorem was shown in the authors’ previous work [6]..

Moreover, one may think the other cases that we extend the original translation $\lceil-\rceil$ from $\mathrm{IL}$ to $\mathrm{IMELL}$ with $\lceil\Box\mathit{A}\rceil\overset{\mathrm{def}}{=}\leavevmode\nobreak\ !\Box\lceil\mathit{A}\rceil$ or $\lceil\Box\mathit{A}\rceil\overset{\mathrm{def}}{=}\Box!\lceil\mathit{A}\rceil$ will work to obtain a faithful translation. However, the judgment $\Box\mathit{p}\,\vdash\,\Box\Box\mathit{p}$ will be a counter-example in either case.

All in all, the problem of the naive combination formulated as $\mathrm{IMELL}^{\Box}$ intuitively came from an undesirable interaction between the right rules of the two modalities:

[TABLE]

Each of these rules has a side-condition: the conclusion $!A$ in $!\mathrm{R}$ must be derived from the modalized context $!\Gamma$, and similarly for $\Box\mathit{A}$ in $\Box\mathrm{R}$. This makes it hard to obtain a faithful S4-version of Girard translation for this naive extension.

3.2 Modal linear logic

We propose a modal linear logic to give a faithful S4-version of Girard translation from $\mathrm{IS4}$.

First of all, the problem we have identified essentially came from the fact that there is no relationship between ‘$!$’ and ‘$\Box$’, and hence the side-conditions of $!\mathrm{R}$ and $\Box\mathrm{R}$ do not hold when we intuitively expect them to hold. Thus, we introduce a modality, ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’ combining ‘$!$’ and ‘$\Box$’, to solve this problem.

{rulefigure}

fig:imellbangboxDefinition of \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Syntactic category

\displaystyle\text{Formulae}\leavevmode\nobreak\ \leavevmode\nobreak\ A,B,C::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\multimap\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}

Inference rule

$\mathrm{Ax}$

$\mathit{A}\,\vdash\,\mathit{A}$

$\Gamma\,\vdash\,\mathit{A}$    $\mathit{A},\Gamma^{\prime}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

[TABLE]

Our modal linear logic, which is called \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, is defined by a sequent calculus which is given in Figure LABEL:fig:imellbangbox. As we mentioned, the formulae are defined as an extension of those of $\mathrm{IMELL}$ with the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -modality. A point is that the $!$-modality is still there with the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality.

The \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality is defined so as to have properties of both ‘$!$’ and ‘$\Box$’, but ‘$!$’ still behaves similarly to $\mathrm{IMELL}$. Therefore, all the intuitions of the inference rules except $!\mathrm{R}$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{R} should be clear. The rules $!\mathrm{R}$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{R} reflect the “strength” between the modalities ‘$!$’ and ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’. Indeed, ‘$!$’ and ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\’ satisfy the S4 axiomata and ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\’ is stronger than ‘$!$’.

Example 3.1**.**

The following hold:

$\vdash\,!\mathit{A}\multimap\mathit{A}$* and \vdash\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap\mathit{A}* 2. 2.

$\vdash\,!(\mathit{A}\multimap\mathit{B})\multimap!\mathit{A}\multimap!\mathit{B}$* and \vdash\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}(\mathit{A}\multimap\mathit{B})\multimap\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{B}* 3. 3.

$\vdash\,!\mathit{A}\multimap!!\mathit{A}$* and \vdash\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\,\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}* 4. 4.

\vdash\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap!\mathit{A}* but \nvdash\,!\mathit{A}\multimap\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}*

Remark 3.2**.**

In Example 3.1, the first three represent the so-called S4 axiomata: T, K, and 4. The last one represents the strength of the two modalities. Actually, assuming the $!$-modality and the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality to satisfy the S4 axiomata and the “strength” axiom \vdash\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap!\mathit{A} is enough to characterize our modal linear logic (see Section 5 for more details).

The cut-elimination theorem for \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is shown similarly to the case of $\mathrm{IMELL}$, and hence \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is consistent. The addition of ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\’ causes no problems in the proof.

Definition 3.3** (Cut-degree and degree).**

For an application of $\mathrm{Cut}$ in a proof, its cut-degree is defined to be the number of logical connectives in the cut-formula. The degree of a proof is defined to be the maximal cut-degree of the proof (and [math] if there is no application of $\mathrm{Cut}$).

Theorem 3.4** (Cut-elimination).**

The rule $\mathrm{Cut}$ in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is admissible, i.e., if $\Gamma\,\vdash\,\mathit{A}$ is derivable, then there is a derivation of the same judgment without any applications of $\mathrm{Cut}$.

Proof 3.5**.**

We follow the proof for propositional linear logic by Lincoln et al. [9]. To show the admissibility of $\mathrm{Cut}$, we consider the admissibility of the following cut rules:

[TABLE]

where $(\mathit{C})^{n}$ denotes the multiset that has $n$ occurrences of $C$ and $n$ is assumed to be positive as a side-condition; and $\Gamma^{\prime}$ in $!\mathrm{Cut}$ (resp. in \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut}) is supposed to contain no formulae of form $!A$ (resp. \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}). The cut-degrees of $!\mathrm{Cut}$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut} are defined similarly to that of $\mathrm{Cut}$.

Then, all the three rules ($\mathrm{Cut}$, $!\mathrm{Cut}$, \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut}) are shown to be admissible by simultaneous induction on the lexicographic complexity $\langle\delta,h\rangle$, where $\delta$ is the degree of the assumed derivation and $h$ is its height. See the appendix for details of the proof.

Corollary 3.6** (Consistency).**

\mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,* is consistent, i.e., there exists an underivable judgment.*

{rulefigure}

fig:modal_girard_translationDefinition of the S4-version of Girard translation.

$\lceil\mathit{A}\rceil$

\displaystyle\hskip 3.99994pt\lceil\mathit{p}\rceil\overset{\mathrm{def}}{=}\mathit{p},\hskip 3.99994pt\lceil\mathit{A}\supset\mathit{B}\rceil\overset{\mathrm{def}}{=}(!\lceil\mathit{A}\rceil)\multimap\lceil\mathit{B}\rceil,\hskip 3.99994pt\lceil\Box\mathit{A}\rceil\overset{\mathrm{def}}{=}\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\lceil\mathit{A}\rceil

$\lceil\Gamma\rceil$

$\displaystyle\lceil\Gamma\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\{(x:\lceil\mathit{A}\rceil)\leavevmode\nobreak\ |\leavevmode\nobreak\ (x:A)\in\Gamma\}$

Then, we can define an S4-version of Girard translation as in Figure LABEL:fig:modal_girard_translation, and it can be justified by the following theorem, which is readily shown by induction on the derivation.

Theorem 3.7** (Soundness).**

If $\Box\Delta,\Gamma\,\vdash\,\mathit{A}$ in $\mathrm{LJ}^{\Box}$, then \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\lceil\Delta\rceil,!\lceil\Gamma\rceil\,\vdash\,\lceil\mathit{A}\rceil in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

4 Curry–Howard correspondence

In this section, we give a computational interpretation for our modal linear logic through the Curry–Howard correspondence and establish the corresponding S4-version of Girard translation for the modal linear logic in terms of typed $\lambda$-calculus.

4.1 Typed $\lambda$-calculus for the intuitionistic modal linear logic

We introduce \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, (pronounced by “lambda bangbox”) that is a typed $\lambda$-calculus corresponding to the modal linear logic under the Curry–Howard correspondence. The calculus \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, can be seen as an integration of $\lambda^{\Box}$ of Pfenning and Davies and the linear $\lambda$-calculus for dual intuitionistic linear logic of Barber [2]. The rules of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, are designed considering the “necessity” of modal logic and the “linearity” of linear logic, and formally defined as in Figure LABEL:fig:lambdabangbox.

{rulefigure}

fig:lambdabangboxDefinition of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Syntactic category

Types $\displaystyle A,B,C$ \displaystyle::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\multimap\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}

Terms $\displaystyle M,N,L$ \displaystyle::=x\leavevmode\nobreak\ |\leavevmode\nobreak\ \lambda\mathit{x}:\mathit{A}.\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{M}\,\mathit{N}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{M}

\displaystyle\,|\leavevmode\nobreak\ \mathbf{let}\,!\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}

Reduction rule

$\displaystyle(\beta\multimap)\hskip 5.0pt$ $\displaystyle(\lambda\mathit{x}:\mathit{A}.\mathit{M})\,\mathit{N}$ $\displaystyle\leadsto\mathit{M}[\mathit{x}:=\mathit{N}]$

$\displaystyle(\beta!)\hskip 5.0pt$ $\displaystyle\mathbf{let}\,!\mathit{x}=!\mathit{N}\,\mathbf{in}\,\mathit{M}$ $\displaystyle\leadsto\mathit{M}[\mathit{x}:=\mathit{N}]$

\displaystyle(\beta\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\ )\hskip 5.0pt \displaystyle\mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{N}\,\mathbf{in}\,\mathit{M} $\displaystyle\leadsto\mathit{M}[\mathit{x}:=\mathit{N}]$

[TABLE]

The structure of types are exactly the same as that of formulae in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. Terms are defined as an extension of the simply-typed $\lambda$-calculus with the following: the terms $!\mathit{M}$ and $\mathbf{let}\,!\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$, which are a constructor and a destructor for types $!A$, respectively; and the terms \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{M} and \mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}, which are those for types \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A} similarly. Note that the variable $x$ in $\mathbf{let}\,!\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$ and \mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N} is supposed to be bound.

A (type) context is defined by the same way as $\lambda^{\Box}$ and a (type) judgment consists of three contexts, a term and a type, written as $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$. These three contexts of a judgment $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ have the following intuitive meaning: (1) $\Delta$ implicitly represents a context for modalized types of form \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}; (2) $\Gamma$ implicitly represents a context for modalized types of form $\Box\mathit{A}$; (3) $\Sigma$ represents an ordinary context but its elements must be used linearly.

The intuitive meanings of the typing rules are as follows. Each of the first three rules is a variable rule depending on the context’s kind. It is allowed for the $\Delta$-part and the $\Gamma$-part to weaken the antecedent in these rules, but is not for the $\Sigma$-part since it must satisfy the linearity condition. The rules $\multimap\!\mathrm{I}$ and $\multimap\!\mathrm{E}$ are for the type $\multimap$, and again, the $\multimap\!\mathrm{E}$ is designed to satisfy the linearity. The remaining rules are for types $!\mathit{A}$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}.

The reduction $\leadsto$ is defined to be the least compatible relation on terms generated by $(\beta\multimap)$, $(\beta!)$, and (\beta\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\ ). The multistep reduction $\leadsto^{+}$ is defined as in the case of $\lambda^{\Box}$.

Then, we can show the subject reduction and the strong normalization of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, as follows.

Lemma 4.1** (Substitution).**

If $\Delta;\Gamma;\Sigma,\mathit{x}:\mathit{A}\,\vdash\,\mathit{M}:\mathit{B}$ and $\Delta;\Gamma;\Sigma^{\prime}\,\vdash\,\mathit{N}:\mathit{A}$, then $\Delta;\Gamma;\Sigma,\Sigma^{\prime}\,\vdash\,\mathit{M}[\mathit{x}:=\mathit{N}]:\mathit{B}$; 2. 2.

If $\Delta;\Gamma,\mathit{x}:\mathit{A};\Sigma\,\vdash\,\mathit{M}:\mathit{B}$ and $\Delta;\Gamma;\emptyset\,\vdash\,\mathit{N}:\mathit{A}$, then $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}[\mathit{x}:=\mathit{N}]:\mathit{B}$; 3. 3.

If $\Delta,\mathit{x}:\mathit{A};\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{B}$ and $\Delta;\emptyset;\emptyset\,\vdash\,\mathit{N}:\mathit{A}$, then $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}[\mathit{x}:=\mathit{N}]:\mathit{B}$.

Theorem 4.2** (Subject reduction).**

If $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ and $\mathit{M}\leadsto\mathit{N}$, then $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{N}:\mathit{A}$.

Proof 4.3**.**

By induction on the derivation of $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ together with Lemma 4.1.

Theorem 4.4** (Strong normalization).**

For well-typed term $M$, there are no infinite reduction sequences starting from $M$.

Proof 4.5**.**

By embedding to a typed $\lambda$-calculus of the $(!,\multimap)$-fragment of dual intuitionistic linear logic, named $\lambda^{!,\multimap}$, which is shown to be strongly normalizing by Ohta and Hasegawa [16].

The details are in the appendix, but the intuition is described as follows. First, for every well-typed term $M$, we define the term $(\mathit{M})^{\ddagger}$ by replacing the occurrences of \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{N} and \mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathit{N}\,\mathbf{in}\,\mathit{L} in $M$ with $!(\mathit{N})^{\ddagger}$ and $\mathbf{let}\,!\mathit{x}=(\mathit{N})^{\ddagger}\,\mathbf{in}\,(\mathit{L})^{\ddagger}$, respectively. Then, we can show that $(\mathit{M})^{\ddagger}$ is typable in $\lambda^{!,\multimap}$, because the structure of ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’ collapses to that of ‘$!$’, and that the embedding $(-)^{\ddagger}$ preserves reductions. Therefore, \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is strongly normalizing.

As we mentioned, we can view that \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is indeed a typed $\lambda$-calculus for the intuitionistic modal linear logic. A natural deduction that corresponds to \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is obtained as the “logical-part” of the calculus, and we can show that the natural deduction is equivalent to \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Definition 4.6** (Natural deduction).**

A natural deduction for modal linear logic, called \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, is defined to be one that is extracted from \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, by erasing term annotations.

Fact 1** (Curry–Howard correspondence).**

There is a one-to-one correspondence between \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, which preserves provability/typability and proof-normalizability/reducibility.

Lemma 4.7** (Judgmental reflection).**

The following hold in \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

$\Delta;\Gamma;\Sigma,!\mathit{A}\,\vdash\,\mathit{B}$* if and only if $\Delta;\Gamma,\mathit{A};\Sigma\,\vdash\,\mathit{B}$;* 2. 2.

\Delta;\Gamma;\Sigma,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\,\vdash\,\mathit{B}* if and only if $\Delta,\mathit{A};\Gamma;\Sigma\,\vdash\,\mathit{B}$.*

Theorem 4.8** (Equivalence).**

$\Delta;\Gamma;\Sigma\,\vdash\,\mathit{A}$* in \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, if and only if \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Delta,!\Gamma,\Sigma\,\vdash\,\mathit{A} in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.*

Proof 4.9**.**

By straightforward induction. Lemma 4.7 is used to show the if-part.

4.2 Embedding from the modal $\lambda$-calculus by Pfenning and Davies

We give a translation from Pfenning and Davies’ $\lambda^{\Box}$ to our \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. We also show that the translation preserves the reductions of $\lambda^{\Box}$, and thus it can be seen as the S4-version of Girard translation on the level of proofs through the Curry–Howard correspondence.

To give the translation, we introduce two meta $\lambda$-terms in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, to encode the function space $\supset$ of $\lambda^{\Box}$. The simulation of reduction of $(\lambda\mathit{x}:\mathit{A}.\mathit{M})\,\mathit{N}$ in $\lambda^{\Box}$ can be shown readily.

Definition 4.10**.**

Let $M$ and $N$ be terms such that $\Delta;\Gamma,\mathit{x}:\mathit{A};\Sigma\,\vdash\,\mathit{M}:\mathit{B}$ and $\Delta;\Gamma;\emptyset\,\vdash\,\mathit{N}:\mathit{A}$. Then, $\overline{\lambda}\mathit{x}:\mathit{A}.\mathit{M}$ and $\mathit{M}\overline{@}\mathit{N}$ are defined as the terms $\lambda\mathit{y}:!\mathit{A}.\mathbf{let}\,!\mathit{x}=\mathit{y}\,\mathbf{in}\,\mathit{M}$ and $\mathit{M}\,(!\mathit{N})$, respectively, where $y$ is chosen to be fresh, i.e., it is a variable satisfying $y\not\in(\mathrm{FV}(M)\cup\{x\})$.

Lemma 4.11** (Derivable full-function space).**

The following rules are derivable in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,:

[TABLE]

Moreover, it holds that $(\overline{\lambda}\mathit{x}:\mathit{A}.\mathit{M})\overline{@}\mathit{N}\leadsto^{+}\mathit{M}[\mathit{x}:=\mathit{N}]$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

{rulefigure}

fig:translationDefinitions of the S4-version of Girard translation in term of typed $\lambda$-calculus.

$\lceil\mathit{A}\rceil$

$\displaystyle\lceil\mathit{p}\rceil$ $\displaystyle\overset{\mathrm{def}}{=}p$

$\displaystyle\lceil\mathit{A}\supset\mathit{B}\rceil$ $\displaystyle\overset{\mathrm{def}}{=}!\lceil\mathit{A}\rceil\multimap\lceil\mathit{B}\rceil$

$\displaystyle\lceil\Box\mathit{A}\rceil$ \displaystyle\overset{\mathrm{def}}{=}\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\lceil\mathit{A}\rceil

$\lceil\Gamma\rceil$

$\displaystyle\hskip 3.00003pt\lceil\Gamma\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\{(x:\lceil\mathit{A}\rceil)\leavevmode\nobreak\ |\leavevmode\nobreak\ (x:A)\in\Gamma\}$

$\mathcal{T}\lceil\mathit{M}\rceil$

$\displaystyle\mathcal{T}\lceil\mathit{x}\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\mathit{x}$

$\displaystyle\mathcal{T}\lceil\lambda\mathit{x}:\mathit{A}.\mathit{M}\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\overline{\lambda}\mathit{x}:\lceil\mathit{A}\rceil.\mathcal{T}\lceil\mathit{M}\rceil$

$\displaystyle\mathcal{T}\lceil\mathit{M}\,\mathit{N}\rceil$ $\displaystyle\overset{\mathrm{def}}{=}\mathcal{T}\lceil\mathit{M}\rceil\overline{@}\mathcal{T}\lceil\mathit{N}\rceil$

$\displaystyle\mathcal{T}\lceil\Box\mathit{M}\rceil$ \displaystyle\overset{\mathrm{def}}{=}\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathcal{T}\lceil\mathit{M}\rceil

$\displaystyle\mathcal{T}\lceil\mathbf{let}\,\Box\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}\rceil$ \displaystyle\overset{\mathrm{def}}{=}\mathbf{let}\,\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{x}=\mathcal{T}\lceil\mathit{M}\rceil\,\mathbf{in}\,\mathcal{T}\lceil\mathit{N}\rceil

Together with the above meta $\lambda$-terms $\overline{\lambda}\mathit{x}:\mathit{A}.\mathit{M}$ and $\mathit{M}\overline{@}\mathit{N}$, we can define the translation from $\lambda^{\Box}$ into \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and show that it preserves typability and reducibility.

Definition 4.12** (Translation).**

The translation from $\lambda^{\Box}$ to \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is defined to be the triple of the type/context/term translations $\lceil\mathit{A}\rceil$, $\lceil\Gamma\rceil$, and $\mathcal{T}\lceil\mathit{M}\rceil$ defined in Figure LABEL:fig:translation.

Theorem 4.13** (Embedding).**

$\lambda^{\Box}$* can be embedded into \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, i.e., the following hold:*

If $\Delta;\Gamma\,\vdash\,\mathit{M}:\mathit{A}$ in $\lambda^{\Box}$, then $\lceil\Delta\rceil;\lceil\Gamma\rceil;\emptyset\,\vdash\,\mathcal{T}\lceil\mathit{M}\rceil:\lceil\mathit{A}\rceil$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. 2. 2.

If $\mathit{M}\leadsto\mathit{M^{\prime}}$ in $\lambda^{\Box}$, then $\mathcal{T}\lceil\mathit{M}\rceil\leadsto^{+}\mathcal{T}\lceil\mathit{M^{\prime}}\rceil$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Proof 4.14**.**

By induction on the derivation of $\Delta;\Gamma\,\vdash\,\mathit{M}:\mathit{A}$ and $\mathit{M}\leadsto\mathit{M^{\prime}}$ in $\lambda^{\Box}$, respectively.

From the logical point of view, Theorem 4.13.1 can be seen as another S4-version of Girard translation (in the style of natural deduction) that corresponds to Theorem 3.7; and Theorem 4.13.2 gives a justification that the S4-version of Girard translation is correct with respect to the level of proofs, i.e., it preserves proof-normalizations as well as provability.

5 Axiomatization of modal linear logic

{rulefigure}

fig:clbangboxDefinition of \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Syntactic category

Types $\displaystyle A,B,C$ \displaystyle::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\multimap\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}

Terms $\displaystyle M,N,L$ \displaystyle::=x\leavevmode\nobreak\ |\leavevmode\nobreak\ c\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{M}

[TABLE]

[TABLE]

We give an axiomatic characterization of the intuitionistic modal linear logic. To do so, we define a typed combinatory logic, called \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, which can be seen as a Hilbert-style deductive system of modal linear logic through the Curry–Howard correspondence. In this section, we only aim to provide the equivalence between \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and the Hilbert-style, while \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, satisfies several desirable properties, e.g., the subject reduction and the strong normalizability.

The definition of \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is given in Figure LABEL:fig:clbangbox. The set of types has the same structure as that in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. A term is either a variable, a combinator, a necessitated term by ‘$!$’, or a necessitated term by ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’. The notions of (type) context and (type) judgment are defined similarly to those of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Every combinator $c$ has its type as defined in the list in the figure, and is denoted by $\mathrm{typeof}(c)$. Then, the typing rules are described as follows: $\mathrm{Ax}$ and $\mathrm{MP}$ are the standard rules, which logically correspond to an axiom rule of the set of axiomata, and modus ponens, respectively. The others are defined by the same way as in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

The reduction $\leadsto$ of combinators is defined to be the least compatible relation on terms generated by the reduction rules listed in the figure.

Remark 5.1**.**

\mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,* can be seen as an extension of linear combinatory algebra of Abramsky et al. [1] with the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality, or equivalently, a linear-logical reconstruction of Pfenning’s modally-typed combinatory logic [17]. The combinators $\mathrm{T}^{!}$, $\mathrm{D}^{!}$, $\mathrm{4}^{!}$ represent the S4 axiomata for the $!$-modality, and similarly, \mathrm{T}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}, \mathrm{D}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}, \mathrm{4}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, represent those for the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality. $\mathrm{E}$ is the only one combinator to characterize the strength between the two modalities.*

As we defined \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, from \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, we can define the Hilbert-style deductive system (with open assumptions) for the intuitionistic modal linear logic via \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Definition 5.2** (Hilbert-style).**

A Hilbert-style deductive system for modal linear logic, called \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, is defined to be one that is extracted from \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, by erasing term annotations.

Fact 2** (Curry–Howard correspondnece).**

There is a one-to-one correspondence between \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, which preserves provability/typability and proof-normalizability/reducibility.

The deduction theorem of \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, can be obtained as a consequence of the so-called bracket abstraction of \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, through Fact 2, which allows us to show the equivalence between \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. Therefore, the modal linear logic is indeed axiomatized by \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Theorem 5.3** (Deduction theorem).**

If $\Delta;\Gamma;\Sigma,\mathit{x}:\mathit{A}\,\vdash\,\mathit{M}:\mathit{B}$, then $\Delta;\Gamma;\Sigma\,\vdash\,(\lambda_{*}\mathit{x}.\mathit{M}):(\mathit{A}\multimap\mathit{B})$; 2. 2.

If $\Delta;\Gamma,\mathit{x}:\mathit{A};\Sigma\,\vdash\,\mathit{M}:\mathit{B}$, then $\Delta;\Gamma;\Sigma\,\vdash\,(\lambda^{!}_{*}\mathit{x}.\mathit{M}):(!\mathit{A}\multimap\mathit{B})$; 3. 3.

If $\Delta,\mathit{x}:\mathit{A};\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{B}$, then \Delta;\Gamma;\Sigma\,\vdash\,(\lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}_{*}\mathit{x}.\mathit{M}):(\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\multimap\mathit{B}).

where $(\lambda_{*}\mathit{x}.\mathit{M})$, $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$, (\lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}_{*}\mathit{x}.\mathit{M}) are bracket abstraction operations that take a variable $x$ and a \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-term $M$ and returns a \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-term, and the definitions are given in the appendix.

Proof 5.4**.**

By induction on the derivation. The proof is just a type-checking of the result of the bracket abstraction operations.

Theorem 5.5** (Equivalence).**

$\Delta;\Gamma;\Sigma\,\vdash\,\mathit{A}$* in \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, if and only if $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{A}$ in \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.*

Proof 5.6**.**

By straightforward induction. We use Theorem 5.3 and Fact 2 to show the if-part.

Corollary 5.7**.**

\mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, \mathrm{NJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, and \mathrm{HJ}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, are equivalent with respect to provability.

6 Geometry of Interaction Machine

In this section, we show a dynamic semantics, called context semantics, for the modal linear logic in the style of geometry of interaction machine [10, 11]. As in the usual linear logic, we first define a notion of proof net and then define the machine as a token-passing system over those proof nets. Thanks to the simplicity of our logic, the definitions are mostly straightforward extension of those for classical $\mathrm{MELL}$ ($\mathrm{CMELL}$).

6.1 Sequent calculus for classical modal linear logic

We define a sequent calculus of classical modal linear logic, called \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. The reason why we define it in the classical setting is for ease of defining the proof nets in the latter part.

{rulefigure}

fig:cmellbangboxDefinition of \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Syntactic category

$\displaystyle\text{Formulae}\leavevmode\nobreak\ \leavevmode\nobreak\ A,B,C$ \displaystyle::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{p}^{\bot}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\otimes\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\parr\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ ?\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}\mathit{A}

Inference rule

$\mathrm{Ax}$

$\vdash\,\mathit{A}^{\bot},\mathit{A}$

[TABLE]

Figure LABEL:fig:cmellbangbox shows the definition of \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. The set of formulae are defined as an extension of $\mathrm{CMELL}$-formulae with the two modalities ‘\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} ’ and ‘\mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}} ’. A dual formula of $A$, written $\mathit{A}^{\bot}$, is defined by the standard dual formulae in $\mathrm{CMELL}$ along with (\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{A})^{\bot}\overset{\mathrm{def}}{=}\mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}(\mathit{A}^{\bot}) and (\mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}\mathit{A})^{\bot}\overset{\mathrm{def}}{=}\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}(\mathit{A}^{\bot}). Here, the \mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}\leavevmode\nobreak\-modality is the dual of the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality by definition, and it can be seen as an integration of the $?$-modality and the $\Diamond$-modality. The linear implication $\mathit{A}\multimap\mathit{B}$ is defined as $\mathit{A}^{\bot}\parr\mathit{B}$ as usual. The inference rules are defined as a simple extension of \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, to the classical setting in the style of “one-sided” sequent.

Then, the cut-elimination theorem for \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, can be shown similarly to the case of \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, and we can see that there exists a trivial embedding from \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, to \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Theorem 6.1** (Cut-elimination).**

The rule $\mathrm{Cut}$ in \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is admissible.

Theorem 6.2** (Embedding).**

If $\Gamma\,\vdash\,\mathit{A}$ in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, then $\vdash\,\Gamma^{\bot},\mathit{A}$ in \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

6.2 Proof-nets formalization

First, we define proof structures for \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. The proof nets are then defined to be those proof structures satisfying a condition called correctness criterion. Intuitively, a proof net corresponds to an (equivalence class of) proof in \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Definition 6.3**.**

A node is one of the graph-theoretic node shown in Figure 5 equipped with \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, types on the edges. They are all directed from top to bottom: for example, the $\mathsf{\parr}$ node has two incoming edges and one outgoing edge. A $!$-node (resp. \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -node) has one outgoing edge typed by $!A$ (resp. \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}A) and arbitrarily many (possibly zero) outgoing edges typed by $?A_{i}$ and \mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}B_{i} (resp. \mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}A_{i}).

A proof structure is a finite directed graph that satisfies the following conditions:

• •

each edge is with a type that matches the types specified by the nodes (in Figure 5) it is connected to;

• •

some edges may not be connected to any node (called dangling edges). Those dangling edges and also the types on those edges are called the conclusions of the structure;

• •

the graph is associated with a total map from all the $!$-nodes and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -nodes in it to proof structures called the contents of the $!$/\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}* -nodes. The map satisfies that the types of the conclusions of a $!$-node (resp. \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -node) coincide with the conclusions of its content.*

Remark 6.4**.**

Formally, a $!$-node (resp. a \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -node) and its content are distinctive objects and they are not connected as a directed graph. Though, it is convenient to depict them as if the $!$-node (resp. \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} -node) represents a “box” filled with its content, as shown at the bottom-right of Figure 5. We also depict multiple edges by an edge with a diagonal line. In what follows, we adopt this “box” notation and multiple edges notation without explicit note.

Definition 6.5**.**

Given a proof structure $S$, a switching path is an undirected path on $S$ (meaning that the path is allowed to traverse an edge forward or backward) satisfying that on each $\parr$ node, $?c$ node, and \mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}c node, the path uses at most one of the premises, and that the path uses any edge at most once.

Definition 6.6**.**

The correctness criterion is the following condition: given a proof structure $S$, switching paths of $S$ and all contents of $!$-nodes, \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-nodes in $S$ are all acyclic and connected. A proof structure satisfying the correctness criterion is called a proof net.

As a counterpart of cut-elimination process in \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, the notion of reduction is defined for proof structures (and hence for proof nets): this intuition is made precise by Lemma 6.9 where $(-)^{\bullet}$ is the translation from \mathrm{CMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, to proof nets, whose definition is omitted here since it is defined analogously to that of $\mathrm{CMELL}$ and $\mathrm{CMELL}$ proof net. The lemmata below are naturally obtained by extending the case for $\mathrm{CMELL}$ since the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality has mostly the same logical structure as the $!$-modality.

Definition 6.7**.**

Reductions* of proof structures are local graph reductions defined by the set of rules depicted in Figure 6.*

Lemma 6.8**.**

Let $S\to S^{\prime}$ be a reduction between proof structures. If $S$ is a proof net (i.e., satisfies the correctness criterion), so is $S^{\prime}$.

Lemma 6.9**.**

Let $\Pi$ be a proof of \vdash\,\mathrel{\Diamond\raise 0.86108pt\hbox{\scalebox{0.6}{?}}}\Delta^{\bot},?\Gamma^{\bot},\Sigma^{\bot},\mathit{A} and suppose that $\Pi$ reduces to another proof $\Pi^{\prime}$. Then there is a sequence of reductions $(\Pi)^{\bullet}\to^{*}(\Pi^{\prime})^{\bullet}$ between the proof nets.

6.3 Computational interpretation

Definition 6.10**.**

A context is a triple $(\mathcal{M},\mathcal{B},\mathcal{N})$ where $\mathcal{M},\mathcal{B},\mathcal{N}$ are generated by the following grammar:

$\mathcal{M}::=\varepsilon\leavevmode\nobreak\ |\leavevmode\nobreak\ l.\mathcal{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ r.\mathcal{M}\quad\mathcal{B}::=\varepsilon\leavevmode\nobreak\ |\leavevmode\nobreak\ L.\mathcal{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ R.\mathcal{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ \langle\mathcal{B},\mathcal{B}\rangle\leavevmode\nobreak\ |\leavevmode\nobreak\ \star\quad\mathcal{N}::=\varepsilon\leavevmode\nobreak\ |\leavevmode\nobreak\ L^{\prime}.\,\mathcal{N}\leavevmode\nobreak\ |\leavevmode\nobreak\ R^{\prime}.\,\mathcal{N}\leavevmode\nobreak\ |\leavevmode\nobreak\ \langle\mathcal{N},\mathcal{N}\rangle\leavevmode\nobreak\ |\leavevmode\nobreak\ \star$* *

The intuition of a context is an intermediate state while “evaluating” the proof net (and, by translating into a proof net, a term in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,). The geometry of interaction machine calculates the semantic value of a net by traversing the net from a conclusion to another; to traverse the net in a “right way” (more precisely, in a way invariant under net reduction), the context accumulates the information about the path that is already passed. Then, how the net is traversed is defined by the notion of path over a proof net as we define below.

Definition 6.11**.**

The extended dynamic algebra $\Lambda^{\Box*}$ is a single-sorted $\Sigma$ algebra that contains $0,1,p,q,r,r^{\prime},s,s^{\prime},t,t^{\prime},d,d^{\prime}\colon\Sigma$ as constants, has an associative operator $\cdot\colon\Sigma\times\Sigma\to\Sigma$ and operators $(-)^{*}\colon\Sigma\to\Sigma$, ${!}\colon\Sigma\to\Sigma$, {\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}{}}\colon\Sigma\to\Sigma, equipped with a formal sum $+$, and satisfies the equations below. Hereafter, we write $xy$ for $x\cdot y$ where $x$ and $y$ are metavariables over $\Sigma$.

[TABLE]

Remark 6.12**.**

The equations in the definition above are mostly the same as the standard dynamic algebra $\Lambda^{*}$ [10, 11] except those equations concerning the symbols with ′ and the operator \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}{}, and their structures are analogous to those for $!$ operator. This again reflects the fact that the logical structure of rules for \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}{} is analogous to that of $!$.

Definition 6.13**.**

A label is an element of $\Lambda^{\Box*}$ that is associated to edges of proof structures as in Figure 7. Let $S$ be a proof structure and $T_{S}$ be the set of edge traversals in the structure. $S$ is associated with a function $w\colon T_{S}\to\Lambda^{\Box*}$ defined by $w(e)=l$ (resp. $l^{*}$) if $e$ is a forward (resp. backward) traversal of an edge $e$ and $l$ is the label of the edge; $w(e_{1}e_{2})=w(e_{1})w(e_{2})$.

Definition 6.14**.**

A walk over a proof structure $S$ is an element of $\Lambda^{\Box*}$ that is obtained by concatenating labels along a graph-theoretic path over $S$ such that the graph-theoretic path does not traverse an edge forward (resp. backward) immediately after the same edge backward (resp. forward); and does not traverse a premise of one of $\otimes,\parr,c$ node and another premise of the same node immediately after that. A path is a walk that is not proved to be equal to [math]. A path is called maximal if it starts and finishes at a conclusion.

The intuition of the notion of path is that a path is a “correct way” of traversing a proof net, in the sense that any path is preserved before and after a reduction. All the other walks that are not paths will be broken, which is represented by the constant [math] of $\Lambda^{\Box*}$. Then, we obtain a context semantics from paths in the following way.

Definition 6.15**.**

Given a monomial path $a$, its action $\llbracket a\rrbracket:\Sigma\rightharpoonup\Sigma$ on contexts is defined as follows. We define $\llbracket 1\rrbracket$ as the identity mapping on contexts. There is no definition of $\llbracket 0\rrbracket$. The $\llbracket f^{*}\rrbracket$ is the inverse translation, i.e., $\llbracket f\rrbracket^{-1}$. The transformer of the composition of $a$ and $b$ is defined as $\llbracket ab\rrbracket(m)\overset{\mathrm{def}}{=}\llbracket a\rrbracket(\llbracket b\rrbracket(m))$. For the other labels, the interpretation are defined as follows where exponential morphisms $!$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\, are defined by the meta-level pattern matchings:

[TABLE]

[TABLE]

Given a path $a$, its action $\llbracket a\rrbracket:\Sigma\rightharpoonup\mathbb{M}(\Sigma)$ is defined by the rules above (regarding the codomain as a multiset) and $\llbracket a+b\rrbracket(m)=(\llbracket a\rrbracket(m))\uplus(\llbracket b\rrbracket(m))$ where $\uplus$ is the multiset sum.

Remark 6.16**.**

In Mackie’s work [10], the multiset in the codomain is not used since the main interest of his work is on terms of a base type: in that setting any proof net corresponding to a term has an execution formula that is monomial. In general, this style of context semantics is slightly degenerated compared to Girard’s original version and its successors because the information of “current position” is dropped from the definition of contexts.

Definition 6.17**.**

Let $S$ be a closed proof net and $\chi$ be the set of maximal paths between conclusions of $S$. The execution formula is defined by $\mathcal{EX}(S)=\Sigma_{\phi\in\chi}\phi$ where the RHS is the sum of all paths in $\chi$. The context semantics of $S$ is defined to be $\llbracket\mathcal{EX}(S)\rrbracket\colon\Sigma\rightharpoonup\mathbb{M}(\Sigma)$.

Definition 6.18**.**

Let $M$ be a closed well-typed term in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. The context semantics of $M$ is defined to be $\llbracket(M)^{\dagger}\rrbracket$, where $(-)^{\dagger}$ is a straightforward translation from \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-terms to proof nets, defined by constructing proof nets from \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-derivations as in Figure 8.

Lemma 6.19**.**

Let $S$ be a closed proof net and $S^{\prime}$ be its normal form. Then $\llbracket S\rrbracket=\llbracket S^{\prime}\rrbracket$.

The lemma is proved through two auxiliary lemmata below.

Lemma 6.20**.**

Let $\phi$ be a path from a conclusion of a closed net $S$ ending at a node $a$. Let $(\mathcal{M}^{\prime},\mathcal{B}^{\prime},\mathcal{N}^{\prime})=\llbracket\phi\rrbracket(\mathcal{M},\varepsilon,\varepsilon)$. The height of $\mathcal{B}^{\prime}$ (resp. $\mathcal{N}^{\prime}$) matches with the number of exponential (resp. necessitation) boxes containing the node $a$.

Proof 6.21**.**

By spectating the rules of actions above: the height of stacks only changes at doors of a box.

Lemma 6.22**.**

Let $\phi$ be a path inside a box of a closed net $S$. $\llbracket\phi\rrbracket(\mathcal{M},\sigma.\mathcal{B},\tau.\mathcal{N})$ is in the form $(\mathcal{M}^{\prime},\sigma^{\prime}.\mathcal{B},\tau.\mathcal{N})$.

Proof 6.23**.**

Again, by spectating the rules of actions.

Theorem 6.24**.**

If a closed term $M$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is typable and $\mathit{M}\leadsto\mathit{M^{\prime}}$, then $\llbracket(M)^{\dagger}\rrbracket=\llbracket(M^{\prime})^{\dagger}\rrbracket$.

Remark 6.25**.**

This notion of context semantics inherently captures the “dynamics” of computation, and indeed Mackie exploited [10, 11] the character to implement a compiler, in the level of machine code, for PCF. In this paper we do not cover such a concrete compiler, but the definition of $\llbracket-\rrbracket$ can be seen as “context transformers” of virtual machine that is mathematically rigorous enough to model the computation of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, (and hence of $\lambda^{\Box}$).

7 Related work

7.1 Linear-logical reconstruction of modal logic

The work on translations from modal logic to linear logic goes back to Martini and Masini [13]. They proposed a translation from classical S4 ($\mathrm{CS4}$) to full propositional linear logic by means of the Grisin–Ono translation. However, their work only discusses provability.

The most similar work to ours is a “linear analysis” of $\mathrm{CS4}$ by Schellinx [20], in which Girard translation from $\mathrm{CS4}$ with respect to proofs is proposed. He uses a bi-colored linear logic, a subsystem of multicolored linear logic by Danos et al. [4], called 2-LL, for a target calculus of the translation. It has two pairs of exponentials $\langle\underset{0}{!},\underset{0}{?}\rangle$ and $\langle\underset{1}{!},\underset{1}{?}\rangle$, called subexponentials following the terminology by Nigam and Miller [14], with the following rules:

[TABLE]

These rules have, while they are defined in the classical setting, essentially the same structure to what we defined as $!\mathrm{R}$ and \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{R} for \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, respectively.

To mention the difference between the results of Schellinx and ours, his work has investigated only in terms of proof theory. Neither a typed $\lambda$-calculus nor a Geometry of Interaction interpretation was given. However, even so, he already gave a reduction-preserving Girard translation for the sequent calculi of $\mathrm{CS4}$ and 2-LL, and his linear decoration (cf. [20, 4]) allows us to obtain the cut-elimination theorem for $\mathrm{CS4}$ as a corollary of that of 2-LL. Thus, it should be interesting to investigate a relationship between his work and ours.

Furthermore, there also exist two uniform logical frameworks that can encode various logics including $\mathrm{IS4}$ and $\mathrm{CS4}$. One is the work by Nigam et al. [15] which based on Nigam and Miller’s linear-logical framework with subexponentials and on the notion of focusing by Andreoli. The other work is adjoint logic by Pruiksma et al. [19] which based on, again, subexponentials, and the so-called LNL model for intuitionistic linear logic by Benton. While our present work is still far from the two works, it seems fruitful to take our discussion into their frameworks to give linear-logical computational interpretations for various logics.

7.2 Computation of modal logic and its relation to metaprogramming

Computational interpretations of modal logic have been considered not only for intuitionistic S4 but also for various logics, including the modal logics $\mathrm{K}$, $\mathrm{T}$, $\mathrm{K4}$, and $\mathrm{GL}$, and a few constructive temporal logics (cf. the survey by Kavvos in [8]). This field of modal logics is known to be connected to “metaprogramming” in the theory of programming languages and has been substantially studied. One of the studies is (multi-)staged computation (cf. [22]), which is a programming paradigm that supports Lisp-like quasi-quote, unquote, and eval. The work of $\lambda^{\Box}$ by Davies and Pfenning [5] is actually one of logical investigations of it.

Furthermore, the multi-stage programming is not a mere theory but has “real” implementations such as MetaML [22] and MetaOCaml (cf. a survey in [3]) in the style of functional programming languages. Some core calculi of these implementations are formalized as type systems (e.g. [21, 3]) and investigated from the logical point of view (e.g. [24]).

8 Conclusion

We have presented a linear-logical reconstruction of the intuitionistic modal logic S4, by establishing the modal linear logic with the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality and the S4-version of Girard translation from $\mathrm{IS4}$. The translation from $\mathrm{IS4}$ to the modal linear logic is shown to be correct with respect to the level of proofs, through the Curry–Howard correspondence.

While the proof-level Girard translation for modal logic is already proposed by Schellinx, our typed $\lambda$-calculus \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, and its Geometry of Interaction Machine (GoIM) are novel. Also, the significance of our formalization is its simplicity. All we need to establish the linear-logical reconstruction of modal logic is the \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\leavevmode\nobreak\-modality, an integration of $!$-modality and $\Box$-modality, that gives the structure of modal logic into linear logic. Thanks to the simplicity, our $\lambda$-calculus and the GoIM can be obtained as simple extensions of existing works.

As a further direction, we plan to enrich our framework to cover other modal logics such as $\mathrm{K}$, $\mathrm{T}$, and $\mathrm{K4}$, following the work of contextual modal calculi by Kavvos [8]. Moreover, reinvestigating of the modal-logical foundation for multi-stage programming by Tsukada and Igarashi [24] via our methods and extending Mackie’s GoIM for PCF [11] to the modal-logical setting seem to be interesting from the viewpoint of programming languages.

Lastly, we have also left a semantical study for modal linear logic with respect to the validity. At the present stage, we think that we could give a sound-and-complete characterization of modal linear logic by an integration of Kripke semantics of modal logic and phase semantics of linear logic, but details will be studied in a future paper.

Appendix A Appendix

A.1 Cut-elimination theorem for the intuitionistic modal linear logic

In this section, we give a complete proof of the cut-elimination theorem of \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

Theorem A.1** (Cut-elimination).**

The rule $\mathrm{Cut}$ in \mathrm{IMELL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, is admissible, i.e., if $\Gamma\,\vdash\,\mathit{A}$ is derivable, then there is a derivation of the same judgment without any applications of $\mathrm{Cut}$.

Proof A.2**.**

As we mentioned in the body, we will show the following rules are admissible.

[TABLE]

The admissibility of $\mathrm{Cut}$, $!\mathrm{Cut}$, \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut} are shown by simultaneous induction on the derivation of $\Gamma\,\vdash\,\mathit{A}$ with the lexicographic complexity $\langle\delta,h\rangle$, where $\delta$ is the degree of the assumed derivation and $h$ is its height. Therefore, it is enough to show that for every application of cuts, one of the following hold: (1) it can be reduced to a cut with a smaller cut-degree; (2) it can be reduced to a cut with a smaller height; (3) it can be eliminated immediately.

In what follows, we will explain the admissibility of each cut rule separately although the actual proofs are done simultaneously.

• •

The admissibility of $\mathrm{Cut}$. We show that every application of the rule $\mathrm{Cut}$ whose cut-degree is maximal is eliminable. Thus, consider an application of $\mathrm{Cut}$ in the derivation:

$\Pi_{0}$

$\Gamma\,\vdash\,\mathit{A}$

     

$\Pi_{1}$

$\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

---

such that its cut-degree is maximal and its height is minimal (comparing to the other applications whose cut-degree is maximal). The proof proceeds by case analysis on $\Pi_{0}$.

• –

$\Pi_{0}$* ends with $\mathrm{Cut}$. In this case the derivation is as follows:*

$\vdots$

$\Gamma_{{\mathrm{0}}}\,\vdash\,\mathit{C}$

     

$\vdots$

$\Gamma_{{\mathrm{1}}},\mathit{C}\,\vdash\,\mathit{A}$

$\mathrm{Cut}$

$\Gamma_{{\mathrm{0}}},\Gamma_{{\mathrm{1}}}\,\vdash\,\mathit{A}$

     

$\Pi_{1}$

$\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma_{{\mathrm{0}}},\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{B}$

---

Since the bottom application of $\mathrm{Cut}$ was chosen to have the maximal cut-degree and the minimum height, the cut-degree of the above is less than that of the bottom. Therefore, the derivation can be translated to the following:

$\vdots$

$\Gamma_{{\mathrm{0}}}\,\vdash\,\mathit{C}$

     

$\vdots$

$\Gamma_{{\mathrm{1}}},\mathit{C}\,\vdash\,\mathit{A}$

     

$\Pi_{1}$

$\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}$

I.H.

$\Gamma_{{\mathrm{1}}},\mathit{C},\Gamma^{\prime}\,\vdash\,\mathit{B}$

I.H.

$\Gamma_{{\mathrm{0}}},\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{B}$

---

• –

$\Pi_{0}$* ends with $\multimap\!\mathrm{R}$. In this case, the derivation is as follows:*

$\vdots$

$\Gamma,\mathit{A_{{\mathrm{0}}}}\,\vdash\,\mathit{A_{{\mathrm{1}}}}$

$\multimap\!\mathrm{R}$

$\Gamma\,\vdash\,\mathit{A_{{\mathrm{0}}}}\multimap\mathit{A_{{\mathrm{1}}}}$

     

$\Pi_{1}$

$\Gamma^{\prime},\mathit{A_{{\mathrm{0}}}}\multimap\mathit{A_{{\mathrm{1}}}}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

---

for some $A_{0}$ and $A_{1}$ such that $A\equiv\mathit{A_{{\mathrm{0}}}}\multimap\mathit{A_{{\mathrm{1}}}}$. If the last step in $\Pi_{1}$ is $\mathrm{Ax}$, then the result is obtained as $\Pi_{0}$. If the last step in $\Pi_{1}$ is $\multimap\!\mathrm{L}$, the derivation is as follows:

$\vdots$

$\Gamma,\mathit{A_{{\mathrm{0}}}}\,\vdash\,\mathit{A_{{\mathrm{1}}}}$

$\multimap\!\mathrm{R}$

$\Gamma\,\vdash\,\mathit{A_{{\mathrm{0}}}}\multimap\mathit{A_{{\mathrm{1}}}}$

     

$\vdots$

$\Gamma^{\prime}\,\vdash\,\mathit{A_{{\mathrm{0}}}}$

     

$\vdots$

$\Gamma^{\prime\prime},\mathit{A_{{\mathrm{1}}}}\,\vdash\,\mathit{B}$

$\multimap\!\mathrm{L}$

$\Gamma^{\prime},\Gamma^{\prime\prime},\mathit{A_{{\mathrm{0}}}}\multimap\mathit{A_{{\mathrm{1}}}}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma,\Gamma^{\prime},\Gamma^{\prime\prime}\,\vdash\,\mathit{B}$

---

which is translated to the following:

$\vdots$

$\Gamma^{\prime}\,\vdash\,\mathit{A_{{\mathrm{0}}}}$

     

$\vdots$

$\Gamma,\mathit{A_{{\mathrm{0}}}}\,\vdash\,\mathit{A_{{\mathrm{1}}}}$

I.H.

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{A_{{\mathrm{1}}}}$

     

$\vdots$

$\Gamma^{\prime\prime},\mathit{A_{{\mathrm{1}}}}\,\vdash\,\mathit{B}$

I.H.

$\Gamma,\Gamma^{\prime},\Gamma^{\prime\prime}\,\vdash\,\mathit{B}$

---

since the cut-degrees of $A_{0}$ and $A_{1}$ are less than that of $A$. The other cases can be shown by simple commutative conversions.

• –

$\Pi_{0}$* ends with $!\mathrm{R}$. This case is dealt as a special case of the case $!\mathrm{R}$ in $!\mathrm{Cut}$.*

• –

$\Pi_{0}$* ends with \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{R}. This case is dealt as a special case of the case \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{R} in \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut}.*

• –

$\Pi_{0}$* ends with the other rules. Easy.*

• •

The admissibility of $!\mathrm{Cut}$. As in the case of $\mathrm{Cut}$, consider an application of $!\mathrm{Cut}$:

$\Pi_{0}$

$\Gamma\,\vdash\,!\mathit{A}$

     

$\Pi_{1}$

$\Gamma^{\prime},(!\mathit{A})^{n}\,\vdash\,\mathit{B}$

$!\mathrm{Cut}$

$\Gamma,\Gamma^{\prime}\,\vdash\,\mathit{B}$

---

such that its cut-degree is maximal and its height is minimal. By case analysis on $\Pi_{0}$.

• –

$\Pi_{0}$* ends with $\mathrm{Ax}$. In this case the cut-elimination is done as follows:*

[TABLE]

• –

$\Pi_{0}$* ends with $!\mathrm{R}$. In this case the derivation is as follows:*

$\vdots$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,\mathit{A}

$!\mathrm{R}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

     

$\Pi_{1}$

$\Gamma^{\prime},(!\mathit{A})^{n}\,\vdash\,\mathit{B}$

$!\mathrm{Cut}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{B}

---

Due to the side-condition of $!\mathrm{R}$, we have to do case analysis on $\Pi_{1}$ further as follows.

$\Pi_{1}$* ends with $\mathrm{Cut}$. In this case the derivation is as follows:*

$\Pi_{0}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

     

$\vdots$

$\Gamma^{\prime},(!\mathit{A})^{k}\,\vdash\,\mathit{C}$

     

$\vdots$

$\Gamma^{\prime\prime},(!\mathit{A})^{l},\mathit{C}\,\vdash\,\mathit{B}$

$\mathrm{Cut}$

$\Gamma^{\prime},\Gamma^{\prime\prime},(!\mathit{A})^{n}\,\vdash\,\mathit{B}$

$!\mathrm{Cut}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime},\Gamma^{\prime\prime}\,\vdash\,\mathit{B}

---

where $n=k+l$. We only deal with the case of $k>0$ and $l>0$, and the other cases are easy. Then, the derivation can be translated to the following:

$\Pi_{0}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

   

$\vdots$

$\Gamma^{\prime},(!\mathit{A})^{k}\,\vdash\,\mathit{C}$

I.H.

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{C}

   

$\Pi_{0}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

   

$\vdots$

$\Gamma^{\prime\prime},(!\mathit{A})^{l},\mathit{C}\,\vdash\,\mathit{B}$

I.H.

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime\prime},\mathit{C}\,\vdash\,\mathit{B}

I.H.

(\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}})^{2},(!\Gamma_{{\mathrm{1}}})^{2},\Gamma^{\prime},\Gamma^{\prime\prime}\,\vdash\,\mathit{B}

!\mathrm{C},\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{C}

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime},\Gamma^{\prime\prime}\,\vdash\,\mathit{B}

---

since the cut-degree of $!\mathrm{Cut}$ is less than that of $\mathrm{Cut}$ from the assumption.

• *

$\Pi_{1}$* ends with $!\mathrm{L}$. If the formula introduced by $!\mathrm{L}$ is not the cut-formula, then it is easy. For the other case, the derivation is as follows:*

$\vdots$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,\mathit{A}

$!\mathrm{R}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

     

$\vdots$

$\Gamma^{\prime},(!\mathit{A})^{n-1},\mathit{A}\,\vdash\,\mathit{B}$

$!\mathrm{L}$

$\Gamma^{\prime},(!\mathit{A})^{n}\,\vdash\,\mathit{B}$

$!\mathrm{Cut}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{B}

---

which is translated to the following:

$\vdots$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,\mathit{A}

     

$\Pi_{0}$

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}}\,\vdash\,!\mathit{A}

     

$\vdots$

$\Gamma^{\prime},(!\mathit{A})^{n-1},\mathit{A}\,\vdash\,\mathit{B}$

I.H.

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime},\mathit{A}\,\vdash\,\mathit{B}

I.H.

(\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}})^{2},(!\Gamma_{{\mathrm{1}}})^{2},\Gamma^{\prime}\,\vdash\,\mathit{B}

!\mathrm{C},\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{C}

\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\Gamma_{{\mathrm{0}}},!\Gamma_{{\mathrm{1}}},\Gamma^{\prime}\,\vdash\,\mathit{B}

---

$\Pi_{1}$* ends with $!\mathrm{C}$. If the formula introduced by $!\mathrm{C}$ is not the cut-formula, then it is easy. For the other case, the cut-elimination is done as follows:*

[TABLE]

Note that the whole proof has not been proceeding by induction on $n$, and hence the number of occurrences of $!A$ does not matter in this case.

• *

$\Pi_{1}$* ends with the other rules. Easy.*

• –

$\Pi_{0}$* ends with the other rules. Easy.*

• •

The admissibility of \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathrm{Cut}. Similar to the case of $!\mathrm{Cut}$.

A.2 Strong normalizability of the typed $\lambda$-calculus for modal linear logic

We complete the proof of the strong normalization theorem for \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. As we mentioned, this is done by an embedding to a typed $\lambda$-calculus for the $(!,\multimap)$-fragment of dual intuitionistic linear logic, studied by Ohta and Hasegawa [16], and shown to be strongly normalizing.

{rulefigure}

fig:lambdabanglimpDefinition of $\lambda^{!,\multimap}$ (some syntax are changed to fit the present paper’s notation).

Syntactic category

Types $\displaystyle A,B,C$ $\displaystyle::=p\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{A}\multimap\mathit{B}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{A}$

Terms $\displaystyle M,N,L$ $\displaystyle::=x\leavevmode\nobreak\ |\leavevmode\nobreak\ \lambda\mathit{x}:\mathit{A}.\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathit{M}\,\mathit{N}\leavevmode\nobreak\ |\leavevmode\nobreak\ !\mathit{M}\leavevmode\nobreak\ |\leavevmode\nobreak\ \mathbf{let}\,!\mathit{x}=\mathit{M}\,\mathbf{in}\,\mathit{N}$

[TABLE]

[TABLE]

The calculus of Ohta and Hasegawa, named $\lambda^{!,\multimap}$ here, is given in Figure LABEL:fig:lambdabanglimp. The syntax and the typing rules can be read in the same way as (the ($!$, $\multimap$)-fragment of) \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. There are somewhat many reduction rules in contrast to those of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, but these are due to the purpose of Ohta and Hasegawa to consider $\eta$-rules and commutative conversions. The different sets of reduction rules do not cause any problems to prove the strong normalizability of \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,.

{rulefigure}

fig:embeddingDefinition of the embeddings $(\mathit{A})^{\ddagger}$, $(\Gamma)^{\ddagger}$, and $(\mathit{M})^{\ddagger}$.

[TABLE]

Definition A.3** (Embedding).**

An embedding from \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, to $\lambda^{!,\multimap}$ is defined to be the triple of the translations $(\mathit{A})^{\ddagger}$, $(\Gamma)^{\ddagger}$, and $(\mathit{M})^{\ddagger}$ given in Figure LABEL:fig:embedding.

Lemma A.4** (Preservation of typing and reduction).**

If $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, then $(\Delta,\Gamma)^{\ddagger};(\Sigma)^{\ddagger}\,\vdash\,(\mathit{M})^{\ddagger}:(\mathit{A})^{\ddagger}$ in $\lambda^{!,\multimap}$. 2. 2.

If $\mathit{M}\leadsto\mathit{N}$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, then $(\mathit{M})^{\ddagger}\leadsto(\mathit{N})^{\ddagger}$ in $\lambda^{!,\multimap}$.

Proof A.5**.**

By induction on $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ and $\mathit{M}\leadsto\mathit{N}$, respectively.

Theorem A.6** (Strong normalization).**

In \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, there are no infinite reduction sequences starting from $M$ for all well-typed term $M$.

Proof A.7**.**

Suppose that there exists an infinite reduction sequence starting from $M$ in \lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,. Then, the term $(\mathit{M})^{\ddagger}$ is well-typed in $\lambda^{!,\multimap}$ and yields an infinite reduction sequence in $\lambda^{!,\multimap}$ by Lemma A.4. However, this contradicts the strong normalizability of $\lambda^{!,\multimap}$.

A.3 Bracket abstraction algorithm

We show the definition of bracket abstraction operators in this section.

{rulefigure}

fig:bracket_abstractionDefinitions of $(\lambda_{*}\mathit{x}.\mathit{M})$, $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$, and (\lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}_{*}\mathit{x}.\mathit{M}) for bracket abstraction.

$\lambda_{*}\mathit{x}.\mathit{M}$

$\displaystyle\lambda_{*}\mathit{x}.\mathit{x}$ $\displaystyle\overset{\mathrm{def}}{=}$ $\displaystyle\leavevmode\nobreak\ \mathrm{I}$

$\displaystyle\lambda_{*}\mathit{x}.(\mathit{M}\,\mathit{N})$ $\displaystyle\overset{\mathrm{def}}{=}$ $\displaystyle\leavevmode\nobreak\ \mathrm{C}\,(\lambda_{*}\mathit{x}.\mathit{M})\,\mathit{N}$ if $x\in\mathrm{FV}(M)$

$\displaystyle\lambda_{*}\mathit{x}.(\mathit{M}\,\mathit{N})$ $\displaystyle\overset{\mathrm{def}}{=}$ $\displaystyle\leavevmode\nobreak\ \mathrm{B}\,\mathit{M}\,(\lambda_{*}\mathit{x}.\mathit{N})$ if $x\in\mathrm{FV}(N)$

[TABLE]

where $(a),(b),(c),(d)$ means the conditions $(x\not\in\mathrm{FV}(M))$, $(x\in\mathrm{FV}(M)\text{ and }x\not\in\mathrm{FV}(N))$, $(x\not\in\mathrm{FV}(M)\text{ and }x\in\mathrm{FV}(N))$, $(x\in\mathrm{FV}(M)\text{ and }x\in\mathrm{FV}(N))$, respectively.

Definition A.8** (Bracket abstraction).**

Let $M$ be a term $M$ of \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\, such that $\Delta;\Gamma;\Sigma\,\vdash\,\mathit{M}:\mathit{A}$ and $x\in\mathrm{FV}(M)$ for some $\Delta,\Gamma,\Sigma,A$ and $x$. Then, the bracket abstraction of $M$ with respect to $x$ is defined to be either one of the following, depending the variable kind of $x$:

[TABLE]

*where each one of $(\lambda_{*}\mathit{x}.\mathit{M})$, $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$, and (\lambda^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}_{*}\mathit{x}.\mathit{M}) is the meta-level bracket abstraction operation given in Figure LABEL:fig:bracket_abstraction, which takes the pair of $x$ and $M$, and yields a \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-term. *

Remark A.9**.**

As in the case of standard bracket abstraction algorithm, the intuition behind the operations $(\lambda_{*}\mathit{x}.\mathit{M})$, $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$, and $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$ is that they are defined so as to mimic the $\lambda$-abstraction operation in the framework of combinatory logic. For instance, the denotation of $(\lambda_{*}\mathit{x}.\mathit{M})$ is a \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-term that represents a function with the parameter $x$, that is, it is a term that satisfies that $(\lambda_{*}\mathit{x}.\mathit{M})\,\mathit{N}\leadsto^{+}\mathit{M}[\mathit{x}:=\mathit{N}]$ in \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,, for all \mathrm{CL}^{\mathrel{\Box\raise 0.60275pt\hbox{\scalebox{0.5}{!}}}\hskip 0.24503pt}\,-terms $N$.

Remark A.10**.**

There are no definitions for some cases in $(\lambda_{*}\mathit{x}.\mathit{M})$ and $(\lambda^{!}_{*}\mathit{x}.\mathit{M})$, e.g, the case that $(\lambda_{*}\mathit{x}.(\mathit{M}\,\mathit{N}))$ such that $x\in\mathrm{FV}(M)$ and $x\in\mathrm{FV}(N)$, and the case that (\lambda^{!}_{*}\mathit{x}.(\mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}}\mathit{M})). This is because that these are actually unnecessary due to the linearity condition and the side condition of the rule \mathrel{\Box\raise 0.86108pt\hbox{\scalebox{0.7}{!}}} . Moreover, the well-definedness of the bracket abstraction operations can be shown by induction on $M$, and in reality, the proof of the deduction theorem can be seen as what justifies it. The intentions that $(\lambda_{*}\mathit{x}.\mathit{M})\,\mathit{N}\leadsto^{+}\mathit{M}[\mathit{x}:=\mathit{N}]$, etc. can also be shown by easy calculation.