A Game Model for Proofs with Costs
Timo Lang, Carlos Olarte, Elaine Pimentel, Christian, Fermuller
TL;DR
This paper introduces a game-theoretic framework for resource-aware and cost-sensitive proof systems, modeling proofs as strategies with associated costs using labelled calculi and semiring structures.
Contribution
It develops a novel game semantics for substructural logics incorporating costs, leading to a new labelled calculus and generalizing proof costs via semirings.
Findings
Proofs are interpreted as costed strategies in a game setting.
A new labelled calculus for cost-aware proofs is introduced.
The framework is exemplified and some proof-theoretical properties are analyzed.
Abstract
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 I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I 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 I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
11institutetext: TU-Wien, Austria 22institutetext: Universidade Federal do Rio Grande do Norte, Brazil
A Game Model for Proofs with Costs
Timo Lang and Carlos Olarte and Elaine Pimentel
and Christian G. Fermüller Olarte and Pimentel are funded by CNPq, CAPES and the project FWF START Y544-N23. Lang is supported by FWF project W1255-N23.11222211
Abstract
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 SELL (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.
1 Introduction
Various kinds of game semantics have been introduced to characterize computational features of substructural logics, in particular fragments and variants of linear logic (LL) [11]. This line of research can be traced back to the works of Blass [5, 6], Abramsky and Jagadeesan [1], Hyland and Ong [12], Lamarche [14], Japaridze [13], Melliès [16], Delande et al. [8], 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 FLew) 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 [5]. Our games are, at least structurally, closer to Lorenzen’s game for intuitionistic logic [15], 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 [10].
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 and , , which share some characteristic features with subexponentials in LL (SELL [7, 18]). The intuition is that a formula is a single use resource with price : By paying , we can “unpack” to obtain the formula , and is destroyed in the process. On the other hand, denotes a permanent resource: From we can obtain as often as we want, each time paying the price . 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 and . 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 2 defines the basic game for and establishes the correspondence between winning strategies and proofs. Section 3 introduces the concept of prices and budgets into the game. The existence of cost-minimal strategies is shown in Section 3.1 and cut-admissibility is discussed in Section 3.2. In Section 4, the concept of prices is generalized and several examples of our interpretation of costs in proofs are presented. In Section 5, the challenge of extending the semantics to full subexponential linear logic is discussed. Section 6 concludes the paper.
2 A game model of branching
Our starting point is a calculus for affine intuitionistic linear logic without exponentials () [11], whose calculus is also equivalent to FLew, the Full Lambek calculus with exchange and weakening. We denote this calculus simply by for brevity. Formulas in are built from the grammar
[TABLE]
where 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 (resp. ) to range over formulas (resp. multisets of formulas). The rules are in Fig. 1. 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 , is a propositional variable. We shall write if the sequent 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 3).
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.
Definition 1 (The game )
is a game of two players, and . Game states (denoted by ) are finite multisets of sequents. proceeds in rounds, initiated by ’s selection of a sequent from the current game state. The successor state is determined according to rules that fit one of the following schemes:
[TABLE]
In (1), the subgame changes to . In (2), the subgame splits into two subgames and . Here is the complete description of a round: After has chosen a sequent among the current game state, she chooses a principal formula in and a matching rule instance of such that is the conclusion of that rule. Depending on , the round proceeds as follows:
If is a unary rule with premise , then the game proceeds in the game state (no interaction of is required). 2. 2.
Parallelism: If is a binary rule with premises pertaining to a multiplicative connective, then the game proceeds in the game state (again, no interaction of is required). 3. 3.
-choice: If is a binary rule with premises pertaining to an additive connective, then chooses and the game proceeds in the game state .
A winning state (for ) is a game state consisting of initial sequents of only, that is, sequents having one of the forms , , .
Example 1
As an example of a round in , assume that the game starts with . might select as the principal formula. For the choice of a matching instance of the rule , she also has to choose a partition . The game then continues in the state .
The following definitions are standard in game theory.
Definition 2 (Plays and strategies)
A play of on a game state is a sequence of game states, where and each arises by playing one round on . A strategy (for ) on a game state is defined as a function telling how to move in any given state. A strategy on is a winning strategy (w.s.) if all plays following it eventually reach a winning state. We shall write if has a w.s. on the game state .
Given w.s.’s for sequents , there is an obvious w.s. for the game state which could be specified as “play according to in the subgame ”. Not all w.s.’s for need to arise in such a way though, since in principle it is allowed that moves in a subgame depend on the moves in another subgame . 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.
Lemma 1 (Independence
)
\models_{\mathcal{G}_{\mathcal{C}}}\{S_{1},\ldots,S_{n}\}\quad\mbox{iff}\quad\text{for all i\leq n, }\models_{\mathcal{G}_{\mathcal{C}}}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.
Theorem 2.1 (Adequacy for )
Let be a sequent. Then .
Proof
() 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 1 comes into play. Assume that the state is and tells to choose the instance of with premises and . By parallelism, the successor state is . Since is a w.s., it must contain a substrategy for . By Lemma 1, we may assume that is of the form: “Use to play in the subgame and to play in ” for some w.s.’s for and respectively. By induction, there are -proofs for the sequents and . Applying below and , we obtain a -proof of .
3 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 and for each to our language and call the resulting formulas extended formulas. An extended formula can be considered as a single use resource with price : By paying , we can “unpack” to (and is destroyed in the process). On the other hand, is a permanent resource: We can obtain as many copies of from it as we want, each time paying the price .
Definition 3
An extended sequent is a sequent built from extended formulas in which subformulas and 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 [math]) of contexts , and otherwise it is positive. For occurrences of a subformula in the consequent, one replaces “even” by “odd”. For instance, is an extended sequent. We denote by a set of formulas prefixed with for some (not necessarily the same) . We introduce a game similarly as we did for . The rules of make reference to the calculus of Fig. 1. It is obtained by interpreting all sequents as extended sequents, replacing the rules and as indicated in Fig. 1 (for internalizing contraction) and adding the dereliction rules
[TABLE]
Note that there is no right rules for and in since they only appear in negative polarity.
Remark 1
can be naturally seen as a fragment of subexponential linear logic (SELL [7]). More specifically, let be a single conclusion calculus for SELL with weakening, and let be the subexponential signature where the set of unbounded subexponentials (that can be weakened and contracted at will) is , and is any partial order on in which, as standardly required in SELL, no bounded subexponential is above an unbounded one. We identify the subexponential with and with . 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 3.2. For some remarks on the system without the syntactic restriction, see Section 5.
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 and are invoked.
Definition 4 (The game )
is a game of two players, and . Game states are tuples , where is a finite multiset of extended sequents and is a “budget”. proceeds in rounds, initiated by ’s selection of an extended sequent from the current game state. The successor state is determined according to rules that fit one of the two following schemes:
[TABLE]
A round proceeds as follows: After has chosen an extended sequent among the current game state, she chooses a rule instance of such that is the conclusion of that rule. Depending on , the round proceeds as follows:
If is a unary rule different from with premise , then the game proceeds in the game state . 2. 2.
Budget decrease: If with premise and principal formula or , then the game proceeds in the game state . 3. 3.
Parallelism: If is a binary rule with premises pertaining to a multiplicative connective, then the game proceeds as . 4. 4.
-choice: If is a binary rule with premises pertaining to an additive connective, then chooses and the game proceeds in the game state .
A winning state (for ) is a game state such that all are initial sequents of and .
Plays and strategies are defined as in . We write if has a w.s. in the -game starting on . The intuitive reading of is: The budget suffices to win the game . From now on, we will just say “sequent” and “formula” instead of “extended sequent” and “extended formula”.
Example 2
Consider the state . In a first move, picks and she finds a partition of the premises not prefixed with and decides that goes to the right premise of . So by parallelism, the new state is . She now chooses to pick of the first component and, by budget decrease, her budget decreases and the next state is . Now picks leading to . Since both components are initial sequents and , 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 and whenever possible.) It is easy to see that a -proof of a sequent translates to a w.s. in for some sufficiently large budget . Taking these observations together, one can prove the following:
Theorem 3.1 (Weak adequacy for )
Let be a sequent. Then
**
The proof is similar to the one of Theorem 2.1. We call this theorem weak adequacy since information about the budget 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 where is an extended sequent and . The complete system is given in Fig. 2. Our aim is to prove that .
To this end, we need an analogue of Lemma 1 (independency of subgames in ) for . Note that crucially, the naive analogue
\models_{\mathcal{G}_{\mathcal{C}}(\mathbb{R}^{+})}(\{S_{1},\ldots,S_{n}\},b)\qquad\mbox{iff}\qquad\text{for all i\leq n, }\models_{\mathcal{G}_{\mathcal{C}}(\mathbb{R}^{+})}(\{S_{i}\},b)
does not hold: Having a w.s. in is not the same as having w.s.’s in all ’s, since the budget 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,
Lemma 2 (Quasi-independency of subgames in )
* *iff
* s.t. and for all , .*
Proof
The direction from right to left is obvious. For the other direction, assume that has a w.s. for . We may assume wlog that this strategy is composed of strategies for the subgames which are both independent from each other and from the budget. In each subgame , let be a strategy for which maximizes the cost (the total decrease of the budget) of playing against . Then . Furthermore, from player can compose a strategy such that when played against in the parallel game , the costs for sum up to . Since is a w.s. for , it must be the case that .
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 2 tells us that finding such a partition is always possible in principle (for an omnipotent player ). Now we can prove the desired correspondence.
Theorem 3.2 (strong adequacy for )
.
Proof
() By induction on the length of a proof of . We highlight two cases. Consider the following two possible ends for :
[TABLE]
In both cases, by induction, there are w.s.’s and for: (1) the game states and ; and (2) the game states and respectively. The needed w.s.’s for the game state and for the game state are:
(1): Choose the instance of as above. By -choice, the successor game state is either or . In any case, the budget in the successor state is greater or equal than both and , so can continue playing according to resp. .
(2): Choose the instance of as above. By parallelism, the successor state is . Use to play the subgame and to play in . By assumption on and , the total costs when playing both strategies in parallel cannot exceed .
( By induction on the length of a strategy . We present only the case where Lemma 2 is used. Assume that the state is and tells to choose the instance of with premises and . By parallelism, the successor state is . Since is a w.s., it must contain a substrategy for this state. By Lemma 2, we may assume that is composed of substrategies for the game states and where . By induction, there are -proofs for the sequents and . Applying and below and , we obtain a -proof of .
Let denote the labelled sequent corresponding to the sequent with label . Given a -proof of , we define the many-to-one onto skeleton function as the -proof of obtained by removing all labels and applications of from . Conversely, we define the one-to-one decoration function as the -proof of , obtained by assigning the label [math] to all initial sequents of and propagating the labels downwards according to the rules of . We define . Let be a proof of . It is easy to see that , that is, is the minimal label which can be attached to w.r.t. . In game theoretic terms, this means the following.
Theorem 3.3
Given a -proof of a sequent , is the smallest budget which suffices to win the game on when following the strategy corresponding to .
Example 3
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 , and the act of drawing a random sock by the labelled formula . The above question then becomes:
For which is the sequent provable?
The following proof shows that suffices:
where derivation is symmetric, and .
3.1 The spectrum of a provable sequent
Due to weakening on labels, many proofs in of labelled sequents of the form correspond to one skeleton proof in of the sequent . On the other hand, 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.
Definition 5
\texttt{spec}(S):=\{\texttt{cost}(\Xi)\mid\text{\Xi\mathcal{C}(\mathbb{R}^{+})S}\}.
For example, consists of the numbers and all combinations where are natural numbers and .
A subset is called discrete if, for every , there is an open interval such that . We can prove:
Theorem 3.4
For any sequent , is discrete and closed.
Proof
Let denote all real numbers appearing as or in , and let us denote by the set of all linear combinations of over , i.e., . By inspecting the rules of and since is not applied in , it is easy to see that , and hence . It suffices to show that each bounded monotone sequence in is eventually constant. We may assume wlog that all the ’s are nonzero. Now consider a sequence in , and assume that is an upper bound for it (a trivial lower bound is always [math]). Pick a number such that . It follows that for all we have . 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:
Corollary 1
If , then has a least element. In other words, there is a smallest such that .
Corollary 1 tells us that cost-optimal strategies for all provable sequents exist, but note that the proof is not constructive. Nevertheless, we may now define:
3.2 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 occur only negatively in sequents (Remark 1); consequently, there is no corresponding right rule (promotion) in . This has the effect that—even though (implicit) contraction on formulas is present in —the proof theory of is closer to than to .
inherits the admissibility of the following cut rule from
[TABLE]
Note that, appearing both in a positive and a negative context, the cut formula cannot contain any modal operator.
Now, let us extend cut admissibility to the labelled system . Assume that both and are provable in . Forgetting labels and , we can conclude, from cut-admissibility in , that . But then, is also provable in with, e.g., (see Cor. 1). Hence, stating cut-admissibility in strongly depends on the possibility of defining a computable function relating with the labels of the premises of the cut rule. We show that is the minimal such function.
Theorem 3.5
For , the following cut rule is admissible in :
[TABLE]
Moreover, whenever is admissible w.r.t. a given , then .
Proof
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 ):
For the minimality, let be distinct propositional variables. For any we have proofs of . Applying cut, we get . Now, is provable (without cut) only if . Hence if makes the cut rule admissible, .
One can easily show that also weakening in the antecedent is admissible in and does not lead to an increased label. Similarly, generalized axioms are admissible: Appearing both positively and negatively, does not contain modal operators, and hence .
Example 4
Consider a labelled transition system where is a set of states and is the transition relation on states. In , simply written as , is interpreted as the time needed for the transition to happen. We use distinct propositional variables to represent states. Moreover, the formula models the transition . We shall use to denote the set of such formulas. Given two sets of states , it is easy to see that the following sentences are equivalent:
From every state in , there is a state in reachable in time 2. 2.
Hence by Theorem 3.2, both are equivalent to
.
One common way to obtain (1) is by finding a set of intermediary states and a splitting of the time such that we can go from each state in to some state in in time , and from each state in to some state in in time . In terms of (3), this strategy corresponds to a cut: Assume we have proofs and of the sequents and . By cut admissibility (Theorem 3.5) we obtain the desired as the result of the “concatenation”of the paths encoded in with the paths encoded in .
4 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 is not the same as derelicting a formula marked with cost . 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. 2) 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 and commutative monoids; (S3) distributes over (i.e., ); and (S4) is absorbing for (i.e., ); is absorptive if it additionally satisfies (S5) ; in absorptive semirings, is idempotent, that is, . This allows for the definition of the following partial order: iff (and then, ); an absorptive semiring is idempotent whenever its operator is idempotent.
Absorptive semirings satisfy some additional properties [3]: (resp. ) is the bottom (resp. top) of ; ; coincides with the (least upper bound) operator; if then () is a total order; , 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. 2). On the other hand, is used to select which is the “best” value, in the sense that iff iff is “better” than (i.e., will replace in Fig. 2). Finally, we generalize (in Fig. 2) 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 and , in Fig. 2, the budget in the conclusion must be of the form . In the particular case of , we know that whenever . Hence, from a conclusion with budget we obtain a premise with decreased budget . In the general case, we guarantee that such splitting of the budget (also present in rules and ) is possible by requiring to be invertible in the following sense: is invertible if for all , the set is non-empty and admits a minimum. We then denote this minimum by . Observe that, in all our examples, if then the set is a singleton except when . In that case, and we set . In Remark 2 we explain and clarify this choice.
In what follows, will always denote an absorptive and invertible semiring.
Definition 6 (System )
Let be an absorptive and invertible semiring. The system is obtained from (Fig. 2) by replacing [math] with , with , with , and with . Similarly, we obtain as a generalization of (Fig. 1).
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.
Example 5 (Costs)
, where is the completion of with , reflects the meaning of costs in Section 3. If and (i.e., ), there is a unique way of splitting into , namely, (i.e., ). Alternatively, we may interpret the elements in as 2D areas. Then, a label in a sequent can be understood as the total area available to place some objects. Each time an object of size is placed (using or ) we observe, bottom-up, that the total area is decreased to .
Remark 2 (Meaning of and )
Consider the semiring above (where and ). If the label in the sequent is , regardless the value in an application of or , 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 . For instance, the sequent is provable in only if . The same sequent (removing the label ) is also provable in . Note that if we decree that (as in [3]), then the sequent above would not be provable for any .
Example 6 (Protected resources)
Let and define iff and iff . The intuition is that represents public information (and then not confidential) and represents secret information. Observe that no derivation of can apply on (since ). This means that only confidential (or protected) resources can be used in such a derivation. Alternatively, we can show that, if is provable then is also provable where is as but replacing any formula of the form with the constant (similarly for and ). is nothing less that the structure [4].
Example 7 (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 as the fact that, in order to produce , resources need to be used. As expected, once is produced, the resources can be released and freed to be used in other tasks. The idea is to know what is the least amount of resources s.t. some jobs can be all of them executed, sequentially if needed.
Consider where (if ). Let be atomic propositions representing tasks and let . Clearly, the sequents and are both provable if . Of course, if we start with more resources, , the sequent is still provable (rule ). Interestingly, from the point of view of costs, the difference between concurrent () and sequential choices () vanishes in this particular scenario, since is idempotent (and hence and coincide).
Example 8 (Transition systems revisited)
Consider the formulas of the shape and the sequent in Example 4. The interpretation there, of as the time needed to observe a transition from to , can be captured with the semiring (Example 5). As expected, according to (and then ), we prefer “faster” paths when there are different ways of going from to .
Another possible interpretation for is the probability of the different independent events (transitions) to happen. Hence, given a specific path from to , the possible values for must be less or equal to the product of the probabilities involved in that path. This behavior can be captured with the probabilistic semiring [4] .
For yet another example of , consider the typical probabilistic choice in process calculi: the process chooses with probability and with probability . Following the process-as-formulas interpretation [17, 9], relating process constructors with logical connectives and reductions with proof steps, the system offers a very natural interpretation of the process as the formula , that we can write as . For instance, if , then, the sequent (resp. ) is provable whenever (resp. ).
5 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., [18]). Let us call the system resulting from by adding the following labelled promotion rules
[TABLE]
where denotes all formulas in which are of the form or and ; and denotes all formulas in which are of the form where . These rules follow the standard formulation of the promotion rule in SELL: the promotion of requires all formulas of the context to be of the form where 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.
Theorem 5.1
There is no function such that the rule
[TABLE]
is admissible in .
Proof
Let be different propositional variables, and let denote the -fold multiplicative conjunction of a formula . The sequents
[TABLE]
are provable in for all natural numbers . The smallest label which makes their cut conclusion provable in is , which is not a function on the premise labels .
Note that Thm. 5.1 leaves open the possibility that cut is admissible w.r.t. a function which takes more information of the premises into account than just their labels. Please refer to the appendix for a more detailed discussion.
6 Concluding remarks and future work
We have introduced game semantics for fragments of (affine intuitionistic) linear logic with subexponentials (SELL [7, 18, 20]), culminating in labelled extensions of such systems so that is interpreted as: “Resource can be obtained from the resources with a budget ” or, alternatively, “The budget suffices to win the game ”. For achieving that, we proposed a new interpretation for the dereliction rule, opposing to the standard controls in the promotion rule: derelicting on means “paying to obtain (a copy of) ”. 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. 5, 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 [10], Thm. 5.1 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 [19].
Finally, we expect that the study of costs of proofs and cut-elimination in labelled fragments of SELL may indicate a relationship between labels and bounds of computation [2], as well as give a different approach to study the complexity of cut-elimination process, specially in the multiplicative-(sub)exponential fragment [21, 22].
Appendix 0.A Appendix
0.A.1 Cut elimination for
Consider the labelled sequent system built from (see Def. 6) by dropping the restriction on occurrences of modalities and adding the following labelled promotion rules (see Section 5)
[TABLE]
where denotes all formulas in which are of the form or and ; and denotes all formulas in which are of the form where . We shall explore different fragments and (admissible) cut-like rules that can be proposed for such a calculus. For concreteness, we consider the case (Example 5). 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 is an arbitrary formula (containing, possibly, positive and/or negative occurrences of the modalities or ).
Theorem 0.A.1 ( Rule)
The following rule is admissible in
[TABLE]
The proof follows the same steps of the cut-elimination proof for SELL, 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. 5.1 is the explosive combination of the use of tensor/implication and contraction, that is, SELL’s multiplicative-(sub)exponential fragment. Hence, limiting the occurrence of one or the other leads to more amenable results. For example, Thm. 3.5 can be straightforwardly extended for formulas not containing the modality (but may occur).
Theorem 0.A.2 (Linear cuts)
Let be a formula with no occurrences of . Then, the following rule is admissible in
[TABLE]
Moreover, if is provable using cutL, then there is a cut-free proof of with .
Proof
The cut-elimination procedure is rather standard. Let us present the case when the cut formula is :
[TABLE]
reduces to
[TABLE]
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 costs , then any use of must pay this “extra cost”. In order to keep track of this extra cost, we introduce the following notation.
Definition 7
Let be such that
. 2. 2.
(i.e., the ordering ignores the subindices). 3. 3.
iff .
For any formula , we define as the formula that substitutes any modality with .
Hence can be slightly modified so that sequent labels belong to , while modal labels belong to . Due to the ordering above, the promotion of has the same effect/constraints that the promotion of . However, the dereliction of the latter requires a greater budget ( instead of ). Moreover, the equivalence can be proven, each direction requiring a different budget. Finally, note that , that is, each element can be seen as the equivalence class of 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.
Lemma 3
If then with . More generally, if and then with .
The next definition restricts the appearance of unbounded modalities only under linear implication.
Definition 8 (-linear)
We say that is -linear if for all subformulas of the form in , does not have occurrences of .
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.
Theorem 0.A.3 (-linear cut)
The following rule is admissible
[TABLE]
Moreover, if is provable using , then there is a cut-free proof of with .
Proof
We will illustrate some cases.
- •
Note that: ; the promotion of , bottom-up, results in a context of formulas (that can be contracted at will); and the dereliction of decreases the budget in . Hence,
[TABLE]
reduces to
[TABLE]
where the “extra cost” disappears after the reduction.
- •
Note that . Here, let :
[TABLE]
reduces to
[TABLE]
It is worth noticing that in the first derivation, the cost is “charged” to (in the formula ) while in the second one, in a finer way, the cost is charged to and to .
- •
The case of implication explains the restriction we impose. Here :
[TABLE]
reduces to
[TABLE]
Note that the reduction above is correct since does not have occurrences of and then .
This kind of analysis seems to be related with flowgraphs in MELL [21, 22].
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Log. , 59(2):543–574, 1994.
- 2[2] Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL , 2(ICFP):94:1–94:30, 2018.
- 3[3] 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.
- 4[4] 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.
- 5[5] Andreas Blass. A game semantics for linear logic. Ann. Pure Appl. Logic , 56(1-3):183–220, 1992.
- 6[6] Andreas Blass. Some semantical aspects of linear logic. Logic Journal of the IGPL , 5(4):487–503, 1997.
- 7[7] 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.
- 8[8] Olivier Delande, Dale Miller, and Alexis Saurin. Proof and refutation in MALL as a game. Ann. Pure Appl. Logic , 161(5):654–672, 2010.