A Game Model for Proofs with Costs
Timo Lang Carlos Olarte Elaine Pimentel Christian Fermuller


Raven: Open Surgical Robotic Platforms
    [
    Received: date / Revised version: date
==========================================





We look at substructural calculi from a game semantic point of view,
guided by certain intuitions about resource conscious and, more
specifically, cost conscious reasoning. To this aim, we start with a
game, where player defends a claim corresponding to a (single-conclusion) sequent, while
player tries to refute that claim. Branching rules for additive
connectives are modeled by choices of , while branching for
multiplicative connectives leads to splitting the game into parallel
subgames, all of which have to be won by player to succeed. The game
comes into full swing by adding cost labels to assumptions, and a corresponding budget.
 Different proofs of the same end-sequent are interpreted as
more or less expensive strategies for to defend the corresponding claim.
This leads to a new kind
of labelled calculus, which can be seen as a fragment of  (subexponential linear logic).  
Finally, we generalize the
concept of costs in proofs by using a semiring
structure, illustrate our interpretation by examples and investigate
some proof-theoretical properties.


 



§ INTRODUCTION



Various kinds of game semantics have been introduced to characterize computational features of
substructural logics, in particular fragments and variants of linear logic () <cit.>. This line of research
can be traced back to the works of   Blass <cit.>, Abramsky and Jagadeesan <cit.>,
Hyland and Ong <cit.>, Lamarche <cit.>, Japaridze <cit.>, Melliès <cit.>, Delande et al. <cit.>,
among several others. 

Our particular view of game semantics is that it is not just a technical tool for characterizing provability in certain calculi,
but rather a playground for illuminating specific semantic intuitions underlying certain
proof systems. 
Specially, we aim at a better understanding of resource conscious reasoning, 
which is often cited as a motivation for substructural logics. 


In a first step, we characterize a version of linear logic (exponential-free affine inuitionistic linear logic 𝐚𝐈𝐌𝐀𝐋𝐋, or, equivalently, Full Lambek Calculus
with exchange and weakening ) by a game, where the difference between additive and multiplicative
connectives is modeled as sequential versus parallel continuation in game states that directly 
correspond to sequents.
 More precisely, every branching rule for a multiplicative connective
  corresponds to a game rule that splits the
current run of the game into two independent subgames. Player , who seeks to establish the
validity of a given sequent, has to win all the resulting subgames. In contrast,
a branching rule for an additive connective is modeled by a choice of player between
two possible succeeding game states,  corresponding to the  premises of the sequent rule in question. 
Note that this amounts to a deviation from the paradigm “formulas as games”, underlying
the game semantic tradition initiated by Blass <cit.>. Our games are, at least structurally,
closer to Lorenzen's game for intuitionistic logic <cit.>, where a state roughly corresponds to a situation
in which a proponent seeks to defend a particular statement against attacks from an opponent, who,
in general, has already granted a bunch of other statements.  This kind of semantics
for linear logic (but without the sequential/parallel distinction) was first explored in  <cit.>. 

As long as we only care about the existence of winning strategies, the distinction between sequential and
parallel subgames 
is
redundant.
However, our model not only highlights the
intended semantics, but it also has concrete effects once we introduce prices for
resources (represented by formulas) into the game. This is done via 
unary operators a and a, a∈^+, which share some characteristic features with subexponentials in   ( <cit.>). The intuition is that a formula aA is a single use resource with price a: By paying a, we can “unpack” aA to obtain the formula A, and aA is destroyed in the process. On the other hand, aA denotes a permanent resource: From aA we can obtain A as often as we want, each time paying the price a.
We lift our game to the extended language by enriching game states with a budget that is decreased whenever
a price is paid. Different strategies for proving the same endsequent can then be compared by the budget which they require to be run safely, i.e. without getting into debts.
This form of resource consciousness not only enhances the game, but it also translates
into a novel sequent system, where cost bounds for proofs are attached as labels to sequents. 

We observe that, up to this point, we only considered resources in assumptions. This is translated to sequents by restricting  negatively the occurrences of the modalities a and a. Thus a promotion rule is not present and the proof-theoretic properties of the proposed systems, such as cut-elimination, can be mimicked by the ones of 𝐚𝐈𝐌𝐀𝐋𝐋. 
We hence move towards two possible generalizations. First, we propose a  broader notion of cost and prices (for both the game and corresponding calculi) beyond the domain of the non-negative real numbers. For this, we organize the labels/prices in a semiring structure that enables for the instantiation of several interesting concrete examples, having the same game-theoretic characterization. Second, we discuss the quest of allowing modalities also in positive contexts, showing the limitations of such approach.

Organization and contributions.  Section <ref> defines the basic game for 𝐚𝐈𝐌𝐀𝐋𝐋 and establishes the correspondence between winning strategies and proofs. 
Section <ref> introduces the concept of prices and budgets into the game. 
The existence of cost-minimal strategies is shown in Section <ref> and cut-admissibility is discussed in Section <ref>. In Section <ref>, the concept of prices is generalized and several examples of our interpretation of costs in proofs are presented. 
In Section <ref>, the challenge of extending the semantics to full subexponential linear logic is discussed. Section <ref> concludes the paper.  


§ A GAME MODEL OF BRANCHING


Our starting point is a calculus for affine intuitionistic linear logic without exponentials (𝐚𝐈𝐌𝐀𝐋𝐋) <cit.>, whose calculus is also equivalent to , the Full Lambek calculus with exchange and weakening. We denote this calculus simply by for brevity. Formulas in are built from the grammar 


    A ::= p ||| A_1  A_2
    |   A_1  A_2 | A_1  A_2  | A_1 
     ⊕ A_2 .


where p stands for atomic propositions (variables); / are the false/true units;   denotes linear implication;  ⊗/ are the multiplicative/additive conjunctions; and ⊕ is the additive disjunction. 

We shall use A,B,C (resp. Γ,Δ) to range over formulas (resp. multisets of formulas).  The rules 
are in Fig. <ref>. Note that the cut rule is not included in our presentation of  and that weakening is present only implicitly, via the context Γ in the initial sequents. Furthermore, in rule I, p is a propositional variable.
We shall write ⊢_ S if the sequent S is provable in .



We shall  characterize proofs as winning strategies (w.s.) in a certain game. Usually, one can interpret bottom-up proof search in sequent systems as a  game, where  at any given state, player first 
chooses a formula of a sequent and, in the next step,  either moves to the premise sequent of the corresponding introduction rule (if the rule has
only one premise); or player chooses 
a premise sequent in which the game continues (if the rule has more than one premise).
Alternatively, 
rather than letting player choose the subgame,
one may stipulate that the game splits into independent subgames, all of
which player has to win. 
At first glance, these two approaches 
might seem  different. However, the difference is only of interpretation and it does not affect 
the (non-)existence of w.s.'s for . To see this, note that, by definition of a w.s.,
player has to be prepared to answer to every possible choice of her opponent . 
Therefore, it
does not matter whether we require to actually win every subgame 
or whether we image to play a single run
where she wins 
irrespectively of 's  choices. 
Hence, the two  interpretations are equivalent in terms of 's w.s.'s but 
they provide different viewpoints of branching sequent rules. Going more into detail, we can see that this equivalence holds as long as the parallel games are independent. We will break this independence later on by introducing a budget which is shared among parallel games (see Section <ref>).

The distinguishing feature of the game 
below is: 
branching
in additive rules is modeled as choices of , whereas in branching multiplicative rules,  splits the context into two disjoint parts,
which then form the corresponding contexts of two  subgames to
be played in parallel. Consequently, a state of the game is represented
by a multiset of sequents, each belonging to a separate subgame. 


is a game of two players, and . Game states (denoted by  G,H) are finite multisets of sequents.
proceeds in rounds, initiated by 's selection of a sequent S from the current game state. The successor state is determined according to rules that fit one of the  following schemes:


    [           (1)         G∪{S}                      G∪{S'}              ;           (2)         G∪{S}               G∪{S_1}∪{S_2}               ]


In (1), the subgame S changes to S'.
In (2), the subgame S splits into two subgames S_1 and S_2. Here is the complete description of a round: After has chosen a sequent S among the current game state, she chooses a principal formula in S and a matching rule instance r of such that S is the conclusion of that rule. Depending on r, the round proceeds as follows:


  * If r is a unary rule with premise S', then the game proceeds in the game state G∪{S'} (no interaction of is required).

  * Parallelism: If r is a binary rule with premises 
S_1,S_2
pertaining to a multiplicative connective, then the game proceeds in the game state G∪{S_1}∪{S_2} (again, no interaction of is required).

  * -choice: If r is a binary rule with premises S_1,S_2 pertaining to an additive connective, then chooses S'∈{S_1,S_2} and the game proceeds in the game state G∪{S'}.


A winning state (for ) is a game state consisting of initial sequents of  only, 
that is, sequents having one of the forms (Γ,p p), (Γ, A), (Γ). 



As an example of a round in , assume that the game starts with 
Δ A B. 
 might select A B as the principal formula. For the choice of a matching instance of the rule _R, she also has to choose a partition Δ=Δ_1∪Δ_2. The game then continues in the state
 {(Δ_1 A),(Δ_2 B)}. 

The following definitions are standard in game theory.

A play of on a game state H is a sequence H_1,H_2,…,H_n of game states, where H_1=H and each H_i+1 arises by playing one round on H_i.
 A strategy (for ) on a game state H is defined as a function telling how to move in any given state. 
 A strategy on H is a winning strategy (w.s.) if all plays following it eventually reach a winning state.
We shall write H if  has a w.s. on the game state H. 



Given w.s.'s π_1,…,π_n for sequents S_1,…,S_n, there is an obvious w.s. for the game state {S_1,…,S_n} which could be specified as “play according to π_i in the subgame S_i”. Not all w.s.'s for {S_1,…,S_n} need to arise in such a way though, since in principle it is allowed that moves in a subgame S_i depend on the moves in another subgame S_j. Nevertheless, since in the game  valid moves and the winning conditions in all subgames are independent, we can restrict to strategies of the former kind. This observation is encapsulated as follows. 


{S_1,…,S_n}    for all i≤ n, S_i

Strategies in a game can be pictured as trees of game states, and therefore strategies share a common form with proofs. In our case, game states are multisets of sequents. However, by virtue of the above lemma, we obtain a notation of winning strategies which uses single sequents as nodes, at least if the initial state of the game is a sequent.


Let S be a sequent. Then 
{S}  ⊢_ S.


(⇐) is a straightforward induction on the length of proofs. (⇒) is proved by induction on a w.s. (the maximal number of moves which can occur following it). We only present the case where Lemma <ref> comes into play.
Assume that the state is Δ_1,Δ_2 A B  and π tells  to choose the instance of _R with premises Δ_1 A and Δ_2 B. 
 By parallelism, the successor state is {(Δ_1 A),(Δ_2 B)}. Since π is a w.s., it must contain a substrategy π' for {(Δ_1 A),(Δ_2 B)}. By Lemma <ref>, we may assume that π' is of the form: 
“Use π_1 to play in the subgame Δ_1 A and π_2 to play in Δ_2 B” for some w.s.'s π_1,π_2 for Δ_1 A and Δ_2 B respectively. By induction, there are -proofs 
_1,_2  for the sequents Δ_1 A and Δ_2 B.  
Applying _R below 
_1 and _2, we obtain a -proof 
 of Δ_1,Δ_2 A B.
 


§ ADDING COSTS

To increase the expressiveness of our framework, we now augment assumptions with costs, where assumptions are formulas occurring negatively on sequents. Costs will be modeled—for now—by elements of ^+, the set of non-negative real numbers. Formally, we add the unary modal operators a and a
for each a∈^+ to our language and call the resulting formulas extended formulas. An extended formula aA can be considered as a single use resource with price a: By paying a, we can “unpack” aA to A (and aA is destroyed in the process). On the other hand, aA is a permanent resource: We can obtain as many copies of A from it as we want, each time paying the price a.
 
An extended sequent is a sequent built from extended formulas in which subformulas aA and aA occur only in negative polarity.

The notion of polarity  is the standard one: A subformula occurrence in the antecedent of a sequent is negative if it occurs in the scope of an even number (including 0) of contexts ([·] B), and otherwise it is positive. For occurrences of a subformula in the consequent, one replaces “even” by “odd”. For instance, ap ⊗ p', (bq q') q”cr r' is an  
extended sequent.
We denote by Γ a set of formulas  prefixed with a for some (not necessarily the same) a∈^+. We  introduce a game  
similarly as we did for  . The rules of  make reference to the calculus  of Fig. <ref>. It is obtained by interpreting all sequents as extended sequents, replacing the rules _R and _L as indicated in Fig. <ref> (for internalizing contraction) and adding the dereliction rules 

    [_L]Γ,aA CΓ,aA,A C    [_L]Γ,aA CΓ,A C

Note that there is no right rules for  and  in  since they only appear in negative polarity.

 can be naturally seen as a fragment of subexponential linear logic ( <cit.>). More specifically, let  be a single conclusion calculus for with weakening, and let Σ=⟨,≼,𝒰⟩ be the subexponential signature  where the set of unbounded subexponentials (that can be weakened and contracted at will) is 𝒰={(a,𝔲) | a∈^+}, and
≼ is any partial order on  in which, as standardly required in ,  no bounded subexponential is above an unbounded one. 
We identify the subexponential !^(a,𝔟) with a and   !^(a,𝔲) with a. Then  is precisely the subsystem of  given by the syntactic restriction that subexponentials occur only in negative polarity. We will exploit this relation between  and  later in Section <ref>. For some remarks on the system without the syntactic restriction, see Section <ref>.

Let us return to the game now. The main difference between  and  is that game states in the latter will involve a budget (modeled as a real number) which will decrease whenever rules _L and _L are invoked. 





 is a game of two players, and . Game states are tuples (H,b), where H is a finite multiset of extended sequents and b∈ is a “budget”.
proceeds in rounds, initiated by 's selection of an extended sequent S from the current game state. The successor state is determined according to rules that fit one of the two following schemes:


    [               (1)         (G∪{S},b)                         (G∪{S'},b')                  ;               (2)         (G∪{S},b)                   (G∪{S^1}∪{S^2},b) ]


A round proceeds as follows: After has chosen an extended sequent S∈ H among the current game state, she chooses a rule  instance  r of  such that S is the conclusion of that rule. Depending on  r, the round proceeds as follows:


  * If r is a unary rule different from _L,_L with premise S', then the game proceeds in the game state (G∪{S'},b).

  * Budget decrease: If r∈{_L,_L} with premise S' and principal formula aA or aA, then the game proceeds in the game state (G∪{S'},b-a).

  * Parallelism: If r is a binary rule with premises S_1,S_2 pertaining to a multiplicative connective, then the game proceeds as (G∪{S_1}∪{S_2},b).

  * -choice: If r is a binary rule with premises S_1,S_2 pertaining to an additive connective, then chooses S'∈{S_1,S_2} and the game proceeds in the game state (G∪{S'},b).


A winning state (for ) is a game state (H,b) such that all S∈ H are initial sequents of  and b≥ 0.

Plays and strategies are defined as in . We write (H,b) if has a w.s. in the -game starting on (H,b). The intuitive reading of (H,b) is: The budget b suffices to win the game H. From now on, we will just say “sequent” and “formula” instead of “extended sequent” and “extended formula”.


Consider the state ({1p,3q p q},5). 
In a first move,  picks p q and she  finds a partition of the premises not prefixed with 
and decides that  3q goes to the right premise of _R. So by parallelism, the new state is
({(1p p),(1p,3q q)},5). 
She now chooses to pick 1p of the first component and, by budget decrease, her budget decreases  and the next  state is 
({(1p,p p),(1p,3q q)},4). 
Now picks 3q  leading to
({(1p,p p),(1p,q q)},1). 
Since both components are initial sequents and  budget ≥ 0, this is a winning state for .


Similarly to  , it is not necessary to consider all possible strategies in : For example, never needs to take the budget into account when deciding the next move. (A rule of thumb for could be: always play economical, i.e. avoid the rules _L and _L whenever possible.) It is easy to see that a -proof  of a sequent S translates to a w.s. in (S,b) for some sufficiently large budget b. Taking these observations together, one can prove the following:



Let S be a sequent. Then

∃ b(({S},b))    ⊢_ S

The proof is similar to the one of Theorem <ref>. We call this theorem weak adequacy since information about the budget b is lost in the proof theoretic representation. In other words, the game  is more expressive than the calculus .
To overcome this discrepancy, we now introduce a  labelled extension of  that we call . A -proof is build from labelled sequents Γ_b A where Γ A is an extended sequent and b∈^+. The complete system is given in Fig. <ref>. 
Our aim is to prove that
({Γ A},b)    ⊢_Γ_b A.

To this end, we need an analogue of Lemma <ref> (independency of subgames in ) for . Note that crucially, the naive analogue

({S_1,…,S_n},b)        for all i≤ n, ({S_i},b)

does not hold: Having a w.s. in ({S_1,…,S_n},b) is not the same as having w.s.'s in all ({S_i},b)'s, since the budget b is shared between the subgames in . 
However, one can prove that there are strategies in  which are independent up to a partition of the budget. More precisely, 




({S_1,…,S_n},b) 

∃ b_1,…,b_n≥ 0  s.t. ∑_i=1^n b_i≤ b  and for all i≤ n,  ({S_i},b_i).  

 The direction from right to left is obvious. For the other direction, assume that  has a w.s. π for ({S_1,…,S_n},b). We may assume wlog that this strategy is composed of strategies π_1,…,π_n for the subgames S_1,…,S_n which are both independent from each other and from the budget. In each subgame S_i, let τ_i be a strategy for  which maximizes the cost b_i (the total decrease of the budget) of playing π_i against τ_i. Then ({S_i},b_i). Furthermore, from τ_1,…,τ_n player can compose a strategy τ such that when played against π in the parallel game {S_1,…,S_n}, the costs for  sum up to ∑_i=1^n b_i. Since π is a w.s. for ({S_1,…,S_n},b), it must be the case that ∑_i=1^n b_i≤ b.


We emphasize that the game rules of  do not force to know a partition of the budget in order to play parallel subgames. Nevertheless, Lemma <ref> tells us that finding such a partition is always possible in principle (for an omnipotent player ).
Now we can  prove the desired correspondence.






({Γ A},b)    ⊢_Γ_b A. 


(⇐) By induction on the length of a proof 
 of Γ_b A. We highlight two cases.
Consider the  following two possible 
 ends for : 

    [(1)  ][_R]Γ_max{c,d} C DΓ_c C    Γ_d D    [(2)  ][_R]Δ_1,Δ_2_c+d C⊗ DΔ_1_c C    Δ_2_d D

In both cases, by induction, there are w.s.'s π_1 and π_2 for: (1) the game states ({Γ C},c) and ({Γ D},d);  
and (2) the game states 
({Δ_1 C},c) and ({Δ_2 D},d) respectively.
The needed w.s.'s π_ for the game state ({Γ C D},max{c,d}) and π_⊗ for the game state ({Δ_1,Δ_2 C⊗ D},c+d) are: 

 (1)π_: Choose the instance of _R as above. By 
-choice, the successor game state is either ({Γ C},max{c,d}) or ({Γ D},max{c,d}). In any case, the budget in the successor state is greater or equal than both c and d, so can continue playing according to π_1 resp.  π_2.
 (2)π_⊗: Choose the instance of _R as above. By parallelism, the successor  state is ({Δ_1 C,Δ_2 D},c+d). Use π_1 to play the subgame Δ_1 C and π_2 to play in Δ_2 D. By assumption on π_1 and π_2, the total costs when playing both strategies in parallel cannot exceed c+d.
(⇒) By induction on the length of a strategy π
. We present only the case where Lemma <ref> is used. 
Assume that the state is ({Δ_1,Δ_2 C D},b)  and π tells  to choose the instance of _R with premises Δ_1 C and Δ_2 D. 
 By parallelism, the successor state is ({Δ_1 C,Δ_2 D},b). Since π is a w.s., it must contain a substrategy π' for this state. By Lemma <ref>, we may assume that π' is composed of substrategies π_1,π_2 for the game states ({Δ_1 C},c) and ({Δ_2 D},d) where c+d≤ b. By induction, there are -proofs 
_1,_2  for the sequents Δ_1_c C and Δ_2_d D.  
Applying _R and w_ℓ below _1 and _2, we obtain a -proof  of Δ_1,Δ_2_b C D.



Let S_b denote the labelled sequent corresponding to the sequent S with label b. Given
Π a -proof of S_b, we define the many-to-one onto skeleton function 𝒮𝒦(Π) as the -proof  of S obtained by removing all labels and applications of w_ℓ from Π.  Conversely, 
we define the one-to-one decoration function 𝒟() as the -proof Π^ℓ of S_a, obtained by assigning the label 0 to all initial sequents 
of  and propagating the labels downwards according to the rules of . 
We define :=a. Let Λ∈𝒮𝒦^-1() be a proof of S_c. It is easy to see that a≤ c, that is,  is the minimal label which can be attached to S w.r.t. .
In game theoretic terms, this means the following.

Given a -proof  of a sequent S,  is the smallest budget which suffices to win the game  on S when following the strategy corresponding to .




Consider the following well-known riddle:

You have white and black socks in a drawer in a completely dark room. How many socks do you have to take out blindly to be sure of having a matching pair? 

We can model the matching pair by the disjunction (w w)⊕(b b), and the act of drawing a random sock by the labelled formula 1(w⊕ b). The above question then becomes:

For which n is the sequent 1(w⊕ b)_n (w w)⊕(b b)   provable?

The following proof shows that n=3 suffices: 


!
=[3×_L]G_3 F[⊕_L]G, w⊕ b, w⊕ b, w⊕ b_0 F[⊕_L]G, w, w⊕ b, w⊕ b_0 F[⊕_R]G, w, w, w⊕ b_0 F=[⊗_R, I]G, w, w, w⊕ b_0 w w   [⊕_L]G, w, b, w⊕ b_0 F[⊕_R]G, w, b, w_0 F=[⊗_R,I]G, w, b, w_0 (w w)   [⊕_R]G, w, b, b_0 F=[⊗_R,I]G, w, b, b_0 b b



where derivation  is symmetric, F=(w w)⊕(b b) and G=1(w⊕ b). 


  


 §.§ The spectrum of a provable sequent



Due to weakening on labels, many proofs in  of labelled sequents of the form S_b correspond to one skeleton proof in  of the sequent S. On the other hand, S may have, itself, many proofs in , each of them having a cost, uniquely determined by the decoration 𝒟. In this section we will consider the spectrum of such costs and prove the existence of a minimal one.

S:={| is a -proof of S}.

For example, 1p,0.8p,0.8p p⊗ p consists of the numbers {1.6,1.8,2.6} and all combinations n+k· 0.8 where n,k are natural numbers and n≥ 2,k≤ 2.

A subset X⊆ is called 
discrete if, for every x∈ X, there is an open interval I⊆ such that I∩ X={x}.
We can prove:


For any sequent S, S⊆^+ is discrete and closed.


Let a_1,…,a_n denote all real numbers appearing as a or a in S, and let us denote by Ω(a_1,…,a_n) the set of all linear combinations of a_1,…,a_n over ℕ, i.e., 
Ω(a_1,…,a_n):={k_1· a_1+…+k_n· a_n| k_1,…,k_n∈ℕ}. 
By inspecting the rules of  and since w_ℓ is not applied in 𝒟(), it is easy to see that ∈Ω(a_1,…,a_n),
and hence
S⊆Ω(a_1,…,a_n). 
It suffices to show that each bounded monotone sequence in Ω(a_1,…,a_n) is eventually constant. We may assume wlog that all the a_i's are nonzero. Now consider a sequence
 (k^i_1· a_1+…+k^i_n· a_n)_i≥ 1 
in Ω(a_1,…,a_n), and assume that B is an upper bound for it (a trivial lower bound is always 0). Pick a number K such that K·min{a_1,…,a_n}>B. It follows that for all i,j we have k^i_j< K. In particular, there are only finitely many different terms in the sequence, from which our claim follows.

Since any bounded below, closed set in  has an minimum, we obtain:

If ⊢_Γ A, then Γ A has a least element. In other words, there is a smallest b such that ⊢_Γ_b A.

Corollary <ref> tells us that cost-optimal strategies for all provable sequents exist, but note that the proof is not constructive.
Nevertheless, we may now define:

S:=min(S)   ⊢_ S
∞ 


 §.§ Cut admissibility



So far, the  results about our game semantics  did not depend essentially on the chosen calculus . We now want to relate 
proof-theoretic properties of  and  to the game semantics. Recall that  can be seen as a fragment of , arising from the syntactic restriction that the modal operators a,a occur only negatively in sequents (Remark <ref>); consequently, there is no corresponding right rule (promotion) in . This has the effect that—even though (implicit) contraction on formulas aA is present in —the proof theory of  is closer to 𝐚𝐈𝐌𝐀𝐋𝐋 than to .

 inherits the admissibility of the following cut rule from 

    [cut]Γ,Δ_1,Δ_2 CΓ,Δ_1 A    Γ,Δ_2,A C
 
Note that, appearing both in a positive and a negative context, the cut formula A cannot contain any modal operator. 

Now, let us extend cut admissibility to the labelled system .
Assume that both
Γ,Δ_1_a A and Γ,Δ_2,A_b C are provable in . Forgetting  labels a and b, we can conclude, from cut-admissibility in , that ⊢_Γ,Δ_1,Δ_2 C. But then, Γ,Δ_1,Δ_2_c C is also provable in  with, , 
c=Γ,Δ_1,Δ_2 C (see Cor. <ref>).
Hence, stating cut-admissibility in  strongly depends on the possibility of defining a  computable function f relating c with the labels of the premises of the cut rule. 
We show that f(a,b)=a+b is the minimal such function.

For f(a,b)=a+b, the following cut rule is admissible in :

    [cut_ℓ]Γ,Δ_1,Δ_2_f(a,b) CΓ,Δ_1_a A    Γ,Δ_2,A_b C

Moreover, whenever cut_ℓ is admissible w.r.t. a given f', then a+b≤ f'(a,b).


For cut admissibility, one can follow the standard cut reduction strategy of 𝐚𝐈𝐌𝐀𝐋𝐋 and observe that it is compatible with the proposed labelling of the cut rule. Consider for instance  the following reduction (note that max{a+c,a+d}=a+max{c,d}):


.7![cut_ℓ]Γ,Δ_1,Δ_2_a+max{c,d} C DΓ,Δ_1_a A    [_R]Γ,Δ_2,A_max{c,d} C DΓ,Δ_2,A_c C    Γ,Δ_2,A_d D

⇝



.95!
[_R]Γ,Δ_1,Δ_2_max{a+c,a+d} C D[cut_ℓ]Γ,Δ_1,Δ_2_a+c CΓ,Δ_1,_a A    Γ,Δ_2,A_c C
		   [cut_ℓ]Γ,Δ_1,Δ_2_a+d DΓ,Δ_1,_a A    Γ,Δ_2,A_d D




For the minimality, let p,q be distinct propositional variables. For any a,b∈^+ we have proofs of apap  and   p,bqbp q.  Applying cut, we get ap,bqc p q. Now, ap,bqc p q is provable (without cut) only if a+b≤ c. Hence if f makes the cut rule admissible, a+b≤ f(a,b).



One can easily show that also  weakening in the antecedent is admissible in  and does not lead to an increased label. Similarly, generalized axioms Γ,A_0 A are admissible: Appearing both positively and negatively, A does not contain modal operators, and hence Γ,A A=A A=0.
 
Consider a labelled transition system (T,)
where T is a set of states and ⊆ T ×× T is the transition relation on states. In (t_i,a_i,t_i')∈, simply written as t_i a_it_i',   a_i is interpreted as the time needed for the transition to happen. 
We  use distinct propositional variables to 
represent states. Moreover, 
the  formula a_i(t_i t_i')  models the transition t_i a_it_i'. We shall use Δ_ to denote the set of such formulas. 
Given two sets of states S_start,S_end⊆ T, it is easy to see that the following sentences are equivalent:


  * From every state in S_start, there is a state in S_end reachable in time ≤ a

  * ({Δ_, ⊕ S_start⊕ S_end},a)

Hence by Theorem <ref>, both are equivalent to


  * ⊢_Δ_, ⊕ S_start_a ⊕ S_end.


One common way to obtain (1) is by finding a set of intermediary states S_i and a splitting of the time a_1+a_2= a such that we can go from each state in S_start to some state in S_i in time a_1, and from each state in S_i to some state in S_end in time a_2. In terms of (3), this strategy corresponds to a cut: Assume we have proofs Ξ_1 and Ξ_2 of the sequents Δ_, ⊕ S_start_a_1⊕ S_i and Δ_, ⊕ S_i_a_2⊕ S_end. By cut admissibility (Theorem <ref>) we obtain the desired Δ_, ⊕ S_start_a_1+a_2⊕ S_end as the result of the “concatenation”of the paths encoded in Ξ_1 with the paths encoded in Ξ_2.
 





§ ALTERNATIVE COST STRUCTURES



We have used non-negative real numbers  for representing costs and budgets, together with   basic operations  for accumulating (+)  and comparing (≥) them. 
This allowed us  to give 
a more interesting perspective of resource  consumption in linear logic: we know that the cost of using  a formula  marked with  cost 3 is not the  same  as  derelicting a formula marked with  cost 7. 
A natural question that arises is whether it is possible to consider other systems 
governing the way we understand costs and budgets. In this section, we consider sequent systems  in which the real numbers of  (see Fig. <ref>) are replaced by elements of a semiring . As we shall see, the structure of  determines the  behavior of the system and the interpretation of costs and budgets. 








A commutative semiring is a tuple = ⟨,, , ,⟩ satisfying:
 (S1)  is a set and ,∈;
 (S2)   and  are binary operators that make the triples ⟨ A,  , _⟩ and 
  ⟨ A,  , ⊤_⟩ commutative monoids;
  (S3)   ×_  distributes over  (i.e., a  (b  c ) = (a b)  (a  c));
  and (S4) _ is  absorbing  for  (i.e., a  _ = _);  
  is absorptive if it additionally satisfies (S5)
 a  (a  b) = a; in absorptive semirings,  is idempotent, that is, a a=a. This allows for the definition of the following partial order:  a  b 
  iff a b = b
  (and then,  a  b  a);
    an absorptive semiring  is idempotent whenever its  operator is idempotent.


Absorptive semirings satisfy some additional properties <cit.>: 
   (resp. ) is the bottom (resp. top) of ; 
 a  =; 
  coincides with the  (least upper bound) operator;
 if a b ∈{a,b}, ∀ a,b∈ then (,) is a total order; 
  a  b (a,b), where  is the greatest lower bound operator;
  if    is idempotent, then  distributes over  and   coincides with .


We  identify  costs as elements of .
We can naturally 
consider  (resp. ) 
as
the “best” (resp. “worst”) cost.
Dually,    (resp. ) is the “worst” (resp. “best”) budget. 
Also, we expect the accumulating operator to be commutative and associative (S2). 
Moreover, 
accumulating costs gives rise to a “worse” cost (S5). Hence, the ×_ operator is used to combine costs (+, on ^+,  in Fig.  <ref>).
On the other hand,    +_ is used to select which is the “best” value,   in the sense that a b = a iff b  a iff a is “better” than b (i.e.,  ≼_ will replace  ≥ in Fig.  <ref>). 
Finally, we generalize   max (in Fig.  <ref>) 
as .
 As mentioned above,  in the case of idempotent semirings,  coincides with the  while in the non-idempotent  case accumulating costs often gives a “worse” result than the .

Note that the rules a_L and  a_L,  in Fig. <ref>,
the budget c in the conclusion must be of the form a+b. In the particular case of ^+, 
we know that 
b = c -a whenever c ≥ a. Hence,  from a conclusion with   budget c  we obtain a premise with decreased budget c-a.  
In the general case,
we guarantee that such splitting of the budget (also present in rules  ⊗_R and _L)  is possible  
by requiring  to be invertible in the following sense:
 is 
invertible if for all b a, the set  (b,a)= {x ∈| a  x =b} is non-empty and admits a minimum. We then denote this minimum by b  a.
Observe that,  in all our examples, if b  a then the set (b,a)   is a singleton except when a=b=. In that case,   (b,a) = and   we set =.
In Remark <ref> we explain and clarify this choice.


In what follows,   will always denote an absorptive and invertible 
semiring. 






 
 


 





 

Let =⟨,,, ,⟩ be an absorptive and invertible semiring. 
The system  is obtained from  (Fig. <ref>) by replacing 0 with , + with ×_, max with _, and ≥ with ≼_. Similarly, we obtain   
as a generalization of  (Fig. <ref>). 

Just as  can be seen as a fragment of , the system  is a fragment of , i.e. affine subexponential linear logic with subexponentials taken from the set 𝒦×{𝔲,𝔟}. We omit the (rather straightforward) formulation of the corresponding game semantics.




Next we present some instances of 
and their intended behavior.


[Costs]
 _c = ⟨, min_, +_, ∞, 0  ⟩, where  is the completion of  with ∞, reflects  the meaning of costs   in Section <ref>. If a,b≠∞ and b ≥ a (i.e., b ≼_ a), 
 there is a  unique way of splitting b
 into a + b', namely, b' = b -a (i.e., b' = b ÷_ a).
Alternatively,  we may interpret the elements in _c as 2D areas. Then, a label b≠∞ in a sequent  can be understood as the total area available to place some objects. Each time an object of size a is placed (using a_L or a_L)  we observe, bottom-up,   that  the  total area is decreased to b- a. 

   
  Consider the semiring   _c above (where = ∞ and = 0). 
If the  label in the sequent is b=, regardless the value a in an application of a_L or  a_L,
the premise will be labelled with ∞. This is because, according to our definition, ÷ =. This makes sense since we select the most “generous” budget to continue the derivation. Of course, smaller suitable budgets  are also allowed due to  rule w_ℓ. 
For instance, the sequent p, (p  q) _b q
is provable in   only if b=. The same sequent (removing the label b) is also provable in . 
Note that if we decree that  ÷ = (as in  <cit.>),
then the sequent above would not be provable for any b.  




[Protected resources]
Let _c/p=⟨{,}, +, ×, , ⟩
and define a+b = iff a = b = and a × b = iff 
a=b=. 
The intuition is that 
 F represents public  information  (and then not confidential) and  
F represents secret information. 
Observe that no derivation of Γ, F _ G can apply _L on F (since ⋠). 
 This means that only confidential (or protected) resources can be used in such a derivation. 
	Alternatively, we can show that, if  Γ G is provable then 
  Γ'  G' is also provable where Γ' is as Γ but replacing any formula of the form 
	F with the constant  (similarly for G and F). 
_c/p  is nothing less that the structure
S_c = ⟨{,}, ∨,∧,,⟩ <cit.>.


[Maximum amount of resources] Consider 
now the situation where labels in sequents  represents a certain amount of computational resources, e.g., RAM, 
	available to process a series of tasks. Moreover, 
	let us interpret cF as the fact that, 
	  in order to  produce  F, c resources need to be used.
	As expected, once F is produced, the c resources can be released and  freed to be used in other tasks. The idea is to know what is the least amount of resources b s.t. some  jobs Γ   can be all of them executed, sequentially if needed. 
	  
     Consider    _max = ⟨, min, max, ∞, 0  ⟩ 
where  b ÷ a = b (if b ≥ a). Let t_1, t_2 be atomic propositions representing tasks and let Γ = {at_1, ct_2}. Clearly, 
the sequents Γ_b t_1 ⊗ t_2
and Γ_b t_1  t_2
are both provable if 
b =max(a,c). Of course, if we start with more resources, e.g., b=a+c, the sequent is still provable (rule w_ℓ). 
     Interestingly, from the point of view of costs, the difference between concurrent  (⊗) and 
     sequential choices () vanishes in this particular scenario, since _max is idempotent (and hence  and  coincide). 


[Transition systems revisited]
Consider the 
formulas of the shape a_i(t_i t_i')
and the sequent Δ_, t_b t'
in  Example <ref>. 
The interpretation there, of   b  as the time needed to observe a transition from t to t',  can be captured with the semiring 
_c (Example <ref>). As expected, according to  (and then ), we prefer “faster” paths when there are different ways of going from t to t'. 

 Another possible interpretation for b  is the probability of the different independent events (transitions) to happen. Hence, given a specific path from t to t', the possible values for   b must be less or equal to the product of the probabilities a_i involved in that path. 
 This behavior can be captured with the probabilistic semiring <cit.> 
_p = ⟨  [0,1], max, ×, 0 ,1  ⟩. 

For yet another example of _p, consider the typical probabilistic choice in process calculi: the process P +_α Q   chooses P with probability α and Q with probability 1-α. Following the process-as-formulas interpretation 
<cit.>, relating  process constructors with logical connectives and reductions with proof steps, the system   offers a very natural interpretation of the process P +_α Q as the formula
	(αP)  (1- αQ), that we can write as P _α Q. For instance, if Γ = {t_1 _α t_2, t_1  t_3, t_2 t_4}, 
	then, 
	the sequent  Γ_b t_3 
	(resp.  Γ_b t_4) is  provable
	whenever α≥ b (resp. 1- α≥ b). 




 

 





















 


§ MODALITIES IN POSITIVE CONTEXTS



We have considered modalities appearing only in negative polarity. 
In this section, we show some problems and limitations
that arise when trying to extend the labelled sequent approach to consider also positive occurrences of modalities 
as in the full system of subexponential linear logic (see e.g., <cit.>).
Let us call 
the system resulting from   by 
adding the following labelled promotion rules

    Γ_b a AΓ^a_b A    Γ_b a AΓ^a_b A

where Γ^a denotes all formulas in Γ which are of the form c B or c B  and a ≥ c; and 
Γ^a 
denotes all formulas in Γ which are of the form c B where a ≥ c. These rules follow the standard formulation of the promotion rule in  : the promotion of !^aA requires all formulas of the context to be of the form !^cB
where a ≼ c  and ≼ is the underlying  preorder on the subexponential signature. 


The following result shows that it is not possible to define a labelled cut rule for where the label of the conclusion depends exclusively on the labels of the premises.
 There is no function f:^+×^+→^+ such that the rule

    [cut]Γ,Δ_1,Δ_2_f(a,b) CΓ,Δ_1_a A    Γ,Δ_2,A_b C

is admissible in .


Let p,q be different propositional variables, and let A^ n denote the n-fold multiplicative conjunction of a formula A. The sequents

    1/kp_a1/kp^⊗ (k· a)    and    1/kp^⊗ (k· a)_b p^⊗(k· k· a· b)

are provable in  for all natural numbers a,b,k. The smallest label f which makes their cut conclusion
1/kp_f p^⊗(k· k· a· b) 
provable in  is k· a· b, which is not a function on the premise labels a,b.

Note that Thm. <ref> leaves open the possibility that cut is admissible w.r.t. a function f which takes more information of the premises into account than just their labels. Please refer to the appendix   for a more detailed discussion. 


§ CONCLUDING REMARKS AND FUTURE WORK


We have introduced game semantics for fragments of (affine intuitionistic) linear logic with subexponentials ( <cit.>), culminating in labelled extensions of such systems so that
Γ_b A is interpreted as: “Resource A can be obtained from the resources Γ with a budget b” or, alternatively, “The budget b suffices to win the game Γ A”.  For achieving that, we proposed a new interpretation for the dereliction rule, opposing to the standard controls in the promotion rule:  derelicting on aB,aB means “paying a to obtain (a copy of) B”. Hence our games and systems offer a neater  control of the resources appearing negatively on sequents. 

There are several ways of extending and continuing this work. First of all, as signalized in Sec. <ref>, the quest of extending the cost conscious reasoning to modalities occurring positively in sequents is not trivial. Despite the obvious game interpretation of promotion that could be given in the style of <cit.>, Thm. <ref> shows that this would not be followed with a proof theoretical notion of cut-elimination, due to the impossibility of defining a functional notion of the cut-label. In the appendix we discuss some possible paths to trail in this direction. On the other side, a philosophical discussion on the need of compositionally of dialogue games driven by a cut rule can also be done <cit.>. 

Finally, we expect that the study of costs of proofs and cut-elimination in labelled fragments of  may indicate a relationship between labels and bounds of computation <cit.>, as well as give a different approach to study the complexity of cut-elimination process, specially in the multiplicative-(sub)exponential fragment <cit.>.





 

10

DBLP:journals/jsyml/AbramskyJ94
Samson Abramsky and Radha Jagadeesan.
Games and full completeness for multiplicative linear logic.
J. Symb. Log., 59(2):543–574, 1994.

DBLP:journals/pacmpl/AccattoliGK18
Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner.
Tight typings and split bounds.
PACMPL, 2(ICFP):94:1–94:30, 2018.

DBLP:conf/ecai/BistarelliG06
Stefano Bistarelli and Fabio Gadducci.
Enhancing constraints manipulation in semiring-based formalisms.
In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo
  Traverso, editors, ECAI 2006, 17th European Conference on Artificial
  Intelligence, Including Prestigious Applications of Intelligent Systems
  (PAIS 2006), Proceedings, volume 141 of Frontiers in Artificial
  Intelligence and Applications, pages 63–67. IOS Press, 2006.

DBLP:journals/constraints/BistarelliMRSVF99
Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Thomas Schiex, Gérard
  Verfaillie, and Hélène Fargier.
Semiring-based csps and valued csps: Frameworks, properties, and
  comparison.
Constraints, 4(3):199–240, 1999.

DBLP:journals/apal/Blass92
Andreas Blass.
A game semantics for linear logic.
Ann. Pure Appl. Logic, 56(1-3):183–220, 1992.

DBLP:journals/igpl/Blass97
Andreas Blass.
Some semantical aspects of linear logic.
Logic Journal of the IGPL, 5(4):487–503, 1997.

danos93kgc
Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx.
The structure of exponentials: Uncovering the dynamics of linear
  logic proofs.
In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors,
  Kurt Gödel Colloquium, volume 713 of Lecture Notes in Computer
  Science, pages 159–171. Springer, 1993.

DBLP:journals/apal/DelandeMS10
Olivier Delande, Dale Miller, and Alexis Saurin.
Proof and refutation in MALL as a game.
Ann. Pure Appl. Logic, 161(5):654–672, 2010.

DBLP:journals/mscs/DengSC16
Yuxin Deng, Robert J. Simmons, and Iliano Cervesato.
Relating reasoning methodologies in linear logic and process algebra.
Mathematical Structures in Computer Science, 26(5):868–906,
  2016.

DBLP:conf/tableaux/FermullerL17
Christian G. Fermüller and Timo Lang.
Interpreting sequent calculi as client-server games.
In Renate A. Schmidt and Cláudia Nalon, editors, Automated
  Reasoning with Analytic Tableaux and Related Methods - 26th International
  Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017,
  Proceedings, volume 10501 of Lecture Notes in Computer Science, pages
  98–113. Springer, 2017.

girard87tcs
Jean-Yves Girard.
Linear logic.
Theor. Comput. Sci., 50:1–102, 1987.

Hyland93fairgames
J.M.E. Hyland and C. h. L. Ong.
Fair games and full completeness for multiplicative linear logic
  without the mix-rule, 1993.

DBLP:journals/apal/Japaridze97
Giorgi Japaridze.
A constructive game semantics for the language of linear logic.
Ann. Pure Appl. Logic, 85(2):87–156, 1997.

DBLP:conf/lics/Lamarche95
François Lamarche.
Games semantics for full propositional linear logic.
In Proceedings, 10th Annual IEEE Symposium on Logic in
  Computer Science, San Diego, California, USA, June 26-29, 1995, pages
  464–473. IEEE Computer Society, 1995.

Lorenzen1960-LORLUA
Paul Lorenzen.
Logik und agon.
Atti Del XII Congresso Internazionale di Filosofia, 4:187–194,
  1960.

DBLP:conf/lics/Mellies05
Paul-André Melliès.
Asynchronous games 4: A fully complete model of propositional
  linear logic.
In 20th IEEE Symposium on Logic in Computer Science (LICS
  2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 386–395.
  IEEE Computer Society, 2005.

DBLP:conf/elp/Miller92
Dale Miller.
The pi-calculus as a theory in linear logic: Preliminary results.
In Evelina Lamma and Paola Mello, editors, Extensions of Logic
  Programming, Third International Workshop, ELP'92, Bologna, Italy, February
  26-28, 1992, Proceedings, volume 660 of Lecture Notes in Computer
  Science, pages 242–264. Springer, 1992.

nigam09ppdp
Vivek Nigam and Dale Miller.
Algorithmic specifications in linear logic with subexponentials.
In António Porto and Francisco Javier López-Fraguas, editors,
  PPDP, pages 129–140. ACM, 2009.

dutilh18
Catarina Dutilh Novaes and Rohan French.
Paradoxes and structural rules from a dialogue perspective.
Philosophical Issues, 28:129–158, 2018.

DBLP:journals/tplp/PimentelON14
Elaine Pimentel, Carlos Olarte, and Vivek Nigam.
A proof theoretic study of soft concurrent constraint programming.
TPLP, 14(4-5):649–663, 2014.

DBLP:journals/tcs/Strassburger03
Lutz Straßburger.
MELL in the calculus of structures.
Theor. Comput. Sci., 309(1-3):213–285, 2003.

DBLP:journals/tocl/StrassburgerG11
Lutz Straßburger and Alessio Guglielmi.
A system of interaction and structure IV: the exponentials and
  decomposition.
ACM Trans. Comput. Log., 12(4):23:1–23:39, 2011.






§ APPENDIX




 §.§ Cut elimination for 

Consider the labelled sequent system  built from 
 (see Def. <ref>) by dropping the restriction on occurrences  of modalities and  adding the following 
  labelled promotion rules
(see Section <ref>)

    Γ_b a AΓ^a_b A    Γ_b a AΓ^a_b A

where Γ^a denotes all formulas in Γ which are of the form c B or c B  and a ≼_ c; and 
Γ^a 
denotes all formulas in Γ which are of the form c B where a ≼_ c.
 We shall explore 
different fragments and (admissible) cut-like rules that can be proposed for such a calculus. For concreteness, we 
consider the case = _c (Example <ref>). But note, however, the discussion below applies for any absorptive, invertible semiring . 

We start by observing that the inclusion of “worse costs”  (∞ in the reals,  in the semiring) entails a trivial labelling 
that makes cut admissible. In the following theorem,  the cut formula F is an arbitrary formula (containing, possibly, positive and/or negative occurrences of 
the modalities a or a). 


The following rule is admissible in 

    [cut_∞]Γ,Δ_1,Δ_2 ∞ CΓ,Δ_1 a F   Γ,Δ_2, F b C


The proof follows the same steps of the cut-elimination proof for , 
using natural extensions of invertibility and permutability of rules to the labelled case.

It is worth noticing that the sole responsible for the impossibility result of Thm. <ref> is the explosive combination of the use of tensor/implication and contraction, that is, 's multiplicative-(sub)exponential fragment. Hence, limiting the occurrence of one or the other leads to more amenable results.
For example, Thm. <ref> can be straightforwardly 
extended for 
formulas not containing the modality a (but a may occur). 


Let F be a formula with no occurrences of 
a. Then, the following rule is admissible in 

    [cutL]Γ,Δ_1,Δ_2 a + b CΓ,Δ_1 aF   Γ,Δ_2, F bC

Moreover, if Γa C is provable using cutL, then there is a cut-free proof of 
Γa'C with a ≥ a'.


The cut-elimination procedure is rather standard. Let us present the case when the cut formula is cF: 

    [cutL]Γ,Δ_1,Δ_2a+b+c CΓ,Δ_1 acF(Γ,Δ_1)^ca F   Γ,Δ_2, cF b+c CΓ,Δ_2, F b C

reduces to

    [cutL]Γ,Δ_1, Δ_2a+b C(Γ,Δ_1)^ca F   Γ,Δ_2, F b C


Still, forcing cut formulas to be linear seems to be a very severe restriction
to impose. A better approach is given by keeping an exact track of the use of contraction in the cut-elimination process.  
The idea is that, if proving F costs a, then any use of F  
must pay this “extra cost”. In order to keep track of this extra cost, we introduce the following notation.


Let ={a_b| a,b∈} be such that 


  * a_b+_ c_d=a+b+c+d.

  * a_b ≥_ a_c (i.e., the ordering ≥_ ignores the subindices).

  * a_b >_ c_d iff a>c.

For any formula F∈, we define [F]_c as the formula that substitutes any 
modality a_b with a_b+c.

Hence  can be slightly modified so that sequent labels belong to  , while modal labels belong to . Due to the ordering above, the promotion of a_0 
has the same effect/constraints that the promotion of a_b. However, the dereliction of the latter requires a greater budget (a+b instead of a). Moreover, the equivalence a_bF ≡a_cF can be proven, each direction requiring a different budget.
Finally, note that _0={a_0| a∈}≃, that is, each element a∈ can be seen as the equivalence class of a_0 in × modulo .
We will abuse the notation and continue representing the resulting system by , also unchanging the representation of sequents. 


The following lemma has a straightforward proof.

If Γ, [F]_c bG then 
Γ, F b'G
with b ≥ b'. More generally,  if Γ, [F]_c bC and c ≥ c' then
Γ, [F]_c'b'C with b ≥ b'. 

The next definition restricts the appearance of unbounded modalities 
only under linear implication.

We say that F is  -linear if for all subformulas of the form A  B in F, A does not have occurrences 
of a. 

The following result presents the admissibility of an extended form of the cut rule, where the budget information from the left premise is passed to the cut-formula in the right premise. Observe that the label
of the conclusion is now a function of the labels of the premises. Moreover, the cut-reduction is label preserving, meaning that the budget monotonically decreases in the cut-elimination process.

The following rule is admissible

    [cut_LL]Γ,Δ_1,Δ_2 a + b CΓ,Δ_1 aF   Γ,Δ_2, [F]_a bC

Moreover, if Γa C is provable using cut_LL, then there is a cut-free proof of 
Γa'C with a≥ a'.



We will illustrate some cases. 

 
  * Note that: [a_bF]_c = a_b+c[F]_c;  the promotion of a_bF, bottom-up, results in a context of 
  formulas (that can be contracted at will);
 and   the dereliction of a_b[F]_c decreases the budget in a + b. Hence, 
  
    Γ,Δ_1,Δ_2 a + b + 2c+dCΓ,Δ_1 ca_bF(Γ)^a_bcF   Γ, Δ_2, a_b+c[F]_c a+b+c+dCΓ, Δ_2, [F]_c, a_b+c[F]_c dC

reduces to

    Γ,Δ_1,Δ_2 2c+dC(Γ)^a_bcF   Γ,Δ_2, [F]_cc+dCΓca_bF   Γ,a_b+c[F]_c, Δ_2, [F]_cdC

where the  “extra cost” a_b disappears after the reduction. 
 
  * Note that [F⊗ G]_c = [F]_c⊗ [G]_c. Here, let c = c_1 + c_2: 
 
    Γ,Δ_1,Δ_2 b+cCΓ,Δ_1 c F ⊗ GΓ,Δ_1' c_1F   Γ,Δ_1”c_2G      Γ,Δ_2, [F ⊗ G]_cbCΓ,Δ_2, [F]_c, [G]_c bC

 reduces to

    Γ,Δ_1,Δ_2 b  +cCΓ,Δ_1' c_1 F   Γ,Δ_1 ”,Δ_2, [F]_c_1b+c_2CΓ,Δ_1”c_2 G   Γ,Δ_2,[F]_c_1, [G]_c_2bC

 It is worth noticing that in the first derivation, the cost c=c_1 + c_2 is “charged” to  F⊗ G 
(in the formula [F ⊗ G]_c)
while in the second one, in a  finer way, the cost c_1 is charged to F and c_2 to G. 
 
  * The case of implication explains the restriction we impose. Here b = b_1 + b_2:
 
    Γ,Δ_1,Δ_2 c + bC Γ,Δ_1 c F GΓ,Δ_1,F  c G      Γ,Δ_2, [F  G]_c b C Γ,Δ_2' b_1[F]_c   Γ,Δ_2”, [G]_cb_2 C

 reduces to 
 
    Γ,Δ_1,Δ_2 c + b CΓ,Δ_2' b_1 F   Γ,Δ_1,Δ_2”, [F]_b_1c + b_2CΓ,Δ_1, [F]_b_1c G   Γ,Δ_2”, [G]_cb_2 C

Note that the reduction above is correct since F does not have 
occurrences of a and then  [F]_c = [F]_b_1=F. 


This kind of analysis seems to be related with flowgraphs in  <cit.>. 

 

