Linear Logic Proof Games and Optimization (Extended Abstract)

Patrick D. Lincoln^{∗}  John C. Mitchell^{†}  Andre Scedrov^{‡}

1 Introduction

Perhaps the most surprising recent development in complexity theory is the discovery that the class np can be characterized using a form of randomized proof checker that only examines a constant number of bits of the “proof” that a string is in a language [6, 5, 31, 3, 4]. More specifically, writing |x| for the length of a string x, a language L in the class np of languages recognizable in nondeterministic polynomial time is traditionally given by a polynomial p and a polynomialtime predicate P such that a string x is in L iff there is some string y satisfying P (x, y), where |y| ≤ p(|x|). Intuitively, we can think of a string y as a possible proof that x ∈ L, with the predicate P some kind of proof checker that distinguishes good proofs from bad ones. A string x is therefore in a language L ∈ np if there is a short proof that x ∈ L, and not in L otherwise. The surprising discovery is that the deterministic proof checker that reads the entire input and proof can be replaced by a probabilistic verifier that on input x and possible proof y, where y is presented in a certain way, flips at most O(log |x|) coins and reads at most a constant number of bits of x and y. Obviously, a probabilistic verifier that does not read the whole proof will sometimes make mistakes. However, the surprising and essentially non-intuitive mathematical fact is that for each language L in np, it is possible to find a polynomial q and verifier V flipping a logarithmic number of coins and reading a constant number of bits such that, for any x ∈ L, there exists y with |y| ≤ q(|x|) and with V (x, y) accepting with probability 1 and, for x ∉ L, there is no y with |y| ≤ q(|x|) and with V (x, y) accepting with probability ≥ 1/4. This idea can also be extended to pspace [10, 9], using a game that alternates between two players instead of a proof presented by a “single player.”

Since the construction of reliable probabilistic verifiers is not very intuitive, it might help to consider some analogies. One is a parallel between probabilistic verifiers and a judge on a thesis review panel. In the traditional presentation of np, a thesis is reviewed by a very careful judge who listens to every word and tries to find a flaw, rejecting if one flaw is found. In the probabilistic version, a thesis is reviewed by a busy and distracted, but intelligent professor who has several other things on her mind. Instead of listening to every word, her thoughts randomly drift away from the presentation and back. However, when she listens to the presentation, she analyzes the argument carefully. The theorem says, intuitively, that it is possible for such a person to distinguish reliably good theses from bad ones. An important aspect of this claim is that in replacing a thorough, attentive judge with a probabilistic one, we can ask the student to present the thesis according to any guidelines we choose. In particular, we can ask that parts of the thesis be repeated often, in various ways (perhaps like one of those interminable Faulkner passages). To draw another analogy, we could ask for a presentation that resembles a play of the game sometimes called “My father went to New York,” which goes,

∗ lincoln@csl.sri.com SRI International Computer Science Laboratory, Menlo Park CA 94025 USA. Work supported under NSF Grant CCR-9224858 and ONR Grant N00014-95-C-0168.

† mitchell@cs.stanford.edu WWW: http://theory.stanford.edu/people/jcm/home.html Department of Computer Science, Stanford University, Stanford, CA 94305-9045 USA. Partially supported by NSF.

‡ scedrov@cis.upenn.edu WWW: http://www.cis.upenn.edu/~scedrov Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395 USA. Partially supported by NSF Grant CCR-94-00907, by ONR Grant N00014-92-J-1916, and by a Centennial Research Fellowship from the American Mathematical Society.

1. my father went to New York and he took a suitcase,

2. my father went to New York and he took a suitcase and a tie,

3. my father went to New York and he took a suitcase and a tie and a pair of socks,

4. my father went to New York and he took a suitcase and a tie and a pair of socks and one of those golf shirts with an alligator,

and so on.

The probabilistic verifier characterization of np may be used to show that a number of optimization problems are hard to approximate in the sense that computing an approximation would also solve every known recognition problem in np. For instance, the size of the largest clique in a graph is np-hard to approximate up to any constant factor. See [4, 27] for an overview. Let us also mention recent work [18] that obtains several np lower bounds for approximation problems by traditional complexity-theoretic techniques.

The probabilistic verifier characterization of pspace is given in [10, 9]. A traditional characterization of pspace is that a language L is given by a polynomial p and a polynomial-time predicate P on strings, with a string x in L iff ∃y_{1}∀y_{2}∃y_{3} … ∀y_{p(|x|)}P (xy_{1}y_{2}y_{3} … y_{p(|x|)}), where each y_{i} may be taken to be a single bit {0, 1} or, alternatively, a string of length polynomial in |x|. In [10], it is shown that one can replace the deterministic polynomial-time predicate P by a probabilistic one that flips a logarithmic number of coins and reads a constant number of bits of the concatenation of strings xy_{1}y_{2}y_{3} … y_{p(|x|)} , when y_{i} ’s are presented in a certain way. This result is strengthened in [9] to a characterization that also allows the universally-quantified choices (y_{2}, y_{4}, … above) to be chosen randomly. This is most easily understood using games. In the traditional characterization, pspace is the class of languages characterized by games that alternate between players ∃ (proponent) and ∀ (opponent), with the outcome determined by a polynomial-time verifier (or referee) that looks at all the moves and decides the winner. In the first probabilistic characterization, the play proceeds in the same way, but verifier (referee) flips coins to decide how to review the game, looks at a constant number of moves (not depending on the length of the game) and chooses a winner. In the second probabilistic characterization, one keeps this form of probabilistic verifier, but replaces the ∀ player (which may need to make clever moves in order to win) by a simple opponent ¶ who moves purely randomly. Formulas that begin with a string of ∃, ¶ quantifiers followed by a list of disjunctive clauses may be called stochastic formulas. Among the other possible variations one must mention “interactive proof systems” or ip [7, 16, 25, 30, 27, 26], which provided an important technical source for the more recent work mentioned above. A relevant result of [9], quoted as Theorem 5.3 in this paper, is that it is pspace-hard to approximate the expected number of clauses in a stochastic formula that player ∃ can satisfy when playing optimally against a random opponent ¶.

After several expository sections that discuss this material in more detail, in Section 6 we develop several variations of the linear logic proof game discussed in [22]. These games are played on linear logic formulas, and their moves are actually instances of inference rules of linear logic [14, 15, 21]. Linear logic is a natural choice in this regard because of its intrinsic ability to reflect computational resources [15, 28, 29].

In our context, there are two players, called proponent and opponent, and a separate verifier. Proponent’s goal is to play a sequence of moves that constitute a formal proof of an input formula, consisting of axioms and matching inference rules. Opponent tries to force the direction of proponent’s evidence in a way that makes it impossible for proponent to obtain a formal proof. Each version of the game has a numeric score that reflects the number of certain preferred axioms used in a complete or partial formal proof.

Our main results can be explained as representations of complexity-theoretic games in the linear logic proof game, with the new complexity results obtained as corollaries of the complexity properties of games from the literature, such as those mentioned above. More specifically, the game representations we consider in Section 7 are defined in a move-by-move fashion; that is, they preserve proponent’s moves, opponent’s moves, proponent’s strategies, as well as proponent’s optimal strategies (that is, optimal with respect to the score).

In this way, one transfers to the linear logic proof game the complexity lower bounds for the approximation of the expected score when proponent plays optimally. In the case of the pspacecomplete multiplicative-additive fragment of propositional linear logic [21], it is shown in Section 7.1 that it is as hard to compute an approximation of the optimal score as it is to determine proponent’s optimal strategy. One way to explain this intuitively and informally is that provability in linear logic is not only globally hard, but also locally hard. In other words, the linear logic proof game shares with many other intricate games such as chess the feature that choosing the best next move is just as hard as developing a complete winning strategy.

Our results have analogs for the np-complete extended multiplicative fragment mll ⊤ where opponent is absent. This is discussed in [24].

2 Stochastic quantified boolean formulas and games

We consider boolean matrices in conjunctive normal form. Prenex boolean formulas are defined as usual, but we allow the “random” quantifier ¶ in addition to ∃ and ∀. A formula is a k − CNF if every clause in its matrix has exactly k literals. For the purposes of establishing a succinct terminology, we say a formula is classical if it is closed and all of the quantifiers are ∀ or ∃, existential if it is closed and all of the quantifiers are ∃, and stochastic if it is closed and all of the quantifiers are ¶ or ∃. It is possible to consider formulas that contain other combinations of quantifiers (such as ∀ and ¶), but we will not need these other classes of formulas.

A classical formula is either valid or invalid, according to the usual interpretation. One way of understanding the value of a classical formula that will be useful in comparing classical and stochastic formulas is through a very simple game with two players called “∀” and “∃”. For a formula Q_{0}x_{0}Q_{1}x_{1} … Q_{n}x_{n}M, the play follows the quantifier order Q_{0}, Q_{1}, …, Q_{n} from left to right, with each player selecting a truth value (true or false, or, equivalently, 1 or 0) for each variable identified with that player. Informally, the goal of player “∃” is to choose values for the existentially-quantified variables so that the matrix is true. Player “∀” tries to do the opposite, choosing values for the universally-quantified variables that will make the formula false.

It is easy to see that, for any classical formula, if both players continue until the quantifier prefix is exhausted, player “∃” has the ability to win against any possible “∀” opponent precisely if the formula is valid. When player “∃” has a way of winning, regardless of how player “∀” plays, we say player “∃” has a winning strategy, and similarly for player “∀.” More formally, a strategy is a function from positions (which may be represented by the sequence of moves made so far in the game) to moves. A strategy is a winning strategy for a given player if this player is guaranteed a win by following the strategy. Using this standard terminology from game theory, we say that a classical formula is valid iff player “∃” has a winning strategy. We can think of the player “∃” as “proponent” and the player “∀” as “opponent.”

For stochastic formulas, we associate a probability prob-stoc(ϕ) with each formula ϕ. One way of explaining this probability is using a variant of the classical formula game described above, this time between players called “¶” (opponent) and “∃” (proponent). The game is played in essentially the same way as the classical game, except for the way that player “¶”chooses the values of variables. Specifically, the play follows the quantifier order from left to right, with each player selecting a truth value for each variable with the appropriate quantifier. The value of a formula is computed by associating a specific strategy with each player. The simpler of the two is player “¶”, who chooses truth values at random. That is, the player “¶” assigns independently to each variable 1 or 0, each with probability 1/2. Player “∃” chooses truth values so as to maximize the probability that the formula is satisfied. In other words

prob-stoc(ϕ) =^{def} Probability that ϕ is satisfied if “∃” plays optimally.

This informal description may be made more precise by defining prob-stoc(ϕ) by recursion on the length of the quantifier sequence. Specifically, suppose Q_{i+1}x_{i+1} … Q_{n}x_{n}M is a formula with ¶ and ∃ quantifiers, and free boolean variables x_{0}, …, x_{i}. The value V(b_{0}, …, b_{i} | Q_{i+1}x_{i+1} … Q_{n}x_{n}M) of formula Q_{i+1}x_{i+1} … Q_{n}x_{n}M given truth values b_{0}, …, b_{i} is defined inductively as follows:

V(b_{0}, …, b_{n} | M)  = \{ \begin{matrix}1 & if M is satisfied by b_{0}, …, b_{n} \\ 0 & if M is not satisfied by b_{0}, …, b_{n} \end{matrix}
V(b_{0}, …, b_{i} | ¶x_{i+1} … Q_{n}x_{n}M) = 1/2(V(b_{0}, …, b_{i}, 0 | Q_{i+2}x_{i+2} … Q_{n}x_{n}M)
+V(b_{0}, …, b_{i}, 1 | Q_{i+2}x_{i+2} … Q_{n}x_{n}M))
V(b_{0}, …, b_{i} | ∃x_{i+1} … Q_{n}x_{n}M) = max{V(b_{0}, …, b_{i}, 0 | Q_{i+2}x_{i+2} … Q_{n}x_{n}M),
V(b_{0}, …, b_{i}, 1 | Q_{i+2}x_{i+2} … Q_{n}x_{n}M)}

Another view of the value of a stochastic formula game is that this is the probability that player “∃” will win a game played on the classical formula obtained by replacing each ¶ by ∀, when ∀ follows a random strategy and ∃ plays optimally.

3 Recognition and optimization problems

There are three important recognition problems associated with the classical, existential and stochastic boolean formulas defined above. In this extended abstract we mention only the latter case. This is given by the “language”

stoc =^{def} { ϕ | ϕ is a stochastic boolean formula with prob-stoc(ϕ) > 1/2 }.

The language stoc is often called ssat in the literature. (Both acronyms are meant to abbreviate “stochastic satisfiability.”) A standard result of “exact-solution” complexity theory [27] establishes that stoc is polynomial-space (pspace) complete.

This language-recognition problem has an associated number function that one may attempt to approximate. The main idea is to generalize the interpretation of a boolean matrix so that one counts the number of satisfied clauses and then ask for the maximum possible count. More specifically, if one interprets a matrix as a function from {0, 1}^{n} to N, the set of natural numbers, by counting the number of satisfied clauses, then one can see that some vectors in {0, 1}^{n} come closer to satisfy the full matrix than others.

A useful intuition is to think of a matrix M = C_{1} ∧ … ∧ C_{j} with j clauses as stating a multiset of j conditions to be satisfied simultaneously. While it would be best to satisfy all conditions, this may not be possible. In this case, one would like to know how close one can come to this goal. In the associated game for stochastic formulas, player “∃” (i.e., proponent) tries to satisfy as many clauses as possible, but this time against an opponent that plays randomly. The number function max-stoc gives the expected number of clauses that “∃” will be able to satisfy (when playing optimally), i.e.,

max-stoc(ϕ) =^{def} ∑_{k} k Prob(exactly k clauses of M are satisfied, when “∃” plays optimally).

This has a precise recursive definition as above, except that the base case is replaced by:

V(b_{0}, …, b_{n} | M) = the number of clauses of M satisfied by b_{0}, …, b_{n}.

Intuitively, max-stoc is the expected score for “∃” when “∃” plays optimally against a random adversary. Note that this use of boolean formulas does not respect logical equivalence: It is easy to find logically equivalent purely existential formulas ϕ and ϕ′ with max-stoc(ϕ) ≠ max-stoc(ϕ′).

The games just described and their associated optimal score functions readily extend to a more general setting where the conditions to be satisfied simultaneously are boolean matrices rather than disjunctive clauses. That is, one counts the number of simultaneously satisfiable boolean matrices from a given multiset {M_{1}, …, M_{j}}. The game is played on generalized prenex formulas Qx_{0}Qx_{1} … Qx_{n}{M_{1}, …, M_{j}}. The terminology regarding formulas is also used for generalized formulas. Also, for instance, the base case of the two previous recursive definitions is replaced by

V(b_{0}, …, b_{n} | {M_{1}, …, M_{j}}) = the number of matrices in {M_{1}, …, M_{j}} satisfied by b_{0}, …, b_{n}.

The game played on formulas is a special case when the boolean matrices M_{1}, …, M_{j} are disjunctive clauses.

4 Approximate solutions to optimization problems

Intuitively, we approximate a function f by computing a function in some “neighborhood” of f. Let D ⊆ {0, 1}^{∗}, and let R be the set of real numbers. For a function f: D → R, the neighborhood of f consists of all functions g: D → R such that, for every string x ∈ D, the difference between f(x) and g(x) is relatively small. One measure of error that appears in the literature [12, 6, 5] is

Definition 4.1 Let D ⊆ {0, 1}^{∗}, and let f be a real-valued function on D. Let 0 < ϵ < 1, where ϵ may depend on |x|, the length of a string x ∈ D. The ϵ-neighborhood of f is the set

ϵ-nbhd(f) = \{g: D → R | ∀x ∈ D, ϵ(|x|) ≤ \frac{g(x)}{f(x)} ≤ \frac{1}{ϵ(|x|)}\}

Intuitively, this is approximation up to factor 1/ϵ. Also this is basically approximation with relative error at most 1 − ϵ.

5 Lower bounds for approximation problems

The approximation problems for prob-stoc and max-stoc are hard, in the technical sense that computing a close approximation would also solve every known recognition problem in an established complexity class, in this case pspace. However, the precise form of lower bound that can be proved using current techniques differs from one problem to the next. Let us give a short intuitive explanation of one approach.

Standard complexity classes are formulated using languages, or recognition problems. Therefore, one natural and appealing form of lower bound for approximation is to show that if one can compute a function efficiently in an ϵ-neighborhood of f, then one can efficiently decide any language in np, for example. Since there is a substantial body of literature classifying problems in np (such as [13]), and historical attempts to develop efficient algorithms for the np-complete problems have not been successful, this would give strong evidence that no polynomial-time algorithm exists for computing a function within an ϵ-neighborhood of f. A similar argument for pspace would suggest that no such approximation could be computed in less than polynomial space. Little was known about such lower bounds for approximations until recently. However, recently there has been substantial progress in this area. We refer the reader to the monographs [31, 3] and to the survey paper [4] for np lower bounds.

In general, a reduction from a language recognition problem to an approximation must translate a yes/no question about a language to a yes/no question about functions.

Definition 5.1 Let D ⊆ {0, 1}^{∗}, and let g be a rational-valued function on D. The function g is pspace-hard if, for any language L ∈ pspace and its associated characteristic function χ_{L}, there exist polynomial-time computable functions h_{1}, h_{2} such that χ_{L} = h_{2} ∘ g ∘ h_{1} .

Definition 5.2 Let D ⊆ {0, 1}^{∗}, and let f be a real-valued function on D. Let ϵ be a real-valued function on the natural numbers such that ϵ(n) < 1, for all n. The function f is pspace-hard to approximate within multiplicative ratio ϵ if every rational-valued function g ∈ ϵ-nbhd(f) is pspace-hard.

One way to establish the required reductions^{1} for language L and function f is to translate any string x to a function argument s(x) such that

x ∈ L implies f(s(x)) ≥ d_{2}(x),
x ∉ L implies f(s(x)) ≤ d_{1}(x),

where d_{1}(x) < d_{2}(x) are sufficiently far apart so that, for any g ∈ ϵ-nbhd(f), one can decide membership in L by computing g(s(x)).

The following theorem is proved in [9].

Theorem 5.3 ([9]) There exists a positive real constant ϵ < 1 such that the function max-stoc on 3-CNF stochastic formulas is pspace-hard to approximate within multiplicative ratio ϵ.

1 pspace-hardness of approximation was defined in [9] and [10] in terms of Turing-reducibility, but their results as well as ours satisfy the more restrictive definition of many-one reducibility used here. It is possible that some approximation problems exist that are pspace-hard with respect to Turing reductions, but not many-one reducibility.

For such problems our definition would be too restrictive, but for all the problems we have studied our definition is more convenient.

That is, computing any function h in the ϵ-neighborhood of max-stoc would allow us to decide membership in any language L in pspace, using time and space at most a polynomial greater than the time and space needed to compute h. A similar theorem regarding the clause-counting game on classical formulas is obtained in [10]. In [9] it is also observed that

Theorem 5.4 ([9]) There exists a positive constant c such that prob-stoc on stochastic formulas is pspace-hard to approximate within multiplicative ratio 2^{−n^{c}}, where n is the length of a stochastic formula.

Using the latter theorem and the techniques of [18], it can be shown that

Theorem 5.5 There exists a positive real number c such that the function max-stoc on generalized stochastic formulas is pspace-hard to approximate within multiplicative ratio n^{−c}, where n is the length of the generalized stochastic formula.

6 Linear logic proof games

Linear logic, introduced in [14], is a refinement of classical logic. While the central notions of truth (emphasized in classical logic) and proof construction (emphasized in intuitionistic logic) remain important in linear logic, it might be said that the emphasis in linear logic is on state. Linear logic is sometimes described as being resource sensitive because it provides an intrinsic and natural accounting of process states, events, and resources [15, 28, 29].

A connection between linear logic and randomized interaction was investigated in [22], which introduced a game semantics of a fragment of linear logic by means of probabilistic games. Other notions of game semantics for linear logic were considered in [8, 1, 2, 17, 20, 19, 11]. Another direction is emphasized here: linear logic proof game simulations of probabilistic games from complexity theory. Such simulations are then used to show that certain problems in linear logic that are known to be hard to decide are also hard to approximate.

We shall consider so-called multiplicative-additive fragment of propositional linear logic, mall. Its proof rules are presented below. This fragment is pspace-complete [21]. Although this fragment does not contain linear logic modalities (or: exponentials), some of the other aspects of linear logic may be seen already in mall. For instance, two standard “structural” rules contraction and weakening are removed, which produces a linear system in which each assumption must be used exactly once in a proof. In this system, formulas indicate finite resources that cannot necessarily be discarded or duplicated without effort. Another feature of linear logic is the distinction between two natural forms of conjunction and disjunction, one form called “multiplicative,” and the other “additive.” For instance, considering the hypotheses as resources, a proof of a multiplicative conjunction ⊗ as a conclusion must partition the resources used to establish each conjunct, whereas the additive conjunction & requires the sharing of all of the resources. The distinction between the multiplicative and the additive connectives is reflected in the mall inference rules, given below.

Let p, q be propositional atoms, let A, B be mall formulas, let Γ, Δ, Θ, Ξ be finite multisets of mall formulas, and let Σ be a finite multiset of literals or constants 1, 0. We write Δ ⊎ Θ for the (disjoint) multiset union of Δ and Θ. As usual, we write Γ, A for the multiset obtained by adding an instance of A to Γ. An expression of the form ⊢ Γ is called a sequent. An expression of the form ⊢ Σ is called a primitive sequent.

The English names for mall inference rules are: identity, cut, par, tensor, bottom, one, plus, with, and top. ⊗ and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} are multiplicative connectives; 1 and ⊥ are multiplicative propositional constants. ⊕ and & are additive connectives; 0 and ⊤ are additive propositional constants. There is no rule for 0. Linear negation ^{⊥}, mentioned in the identity and cut rules, is defined by recursion on the structure of formulas: (p^{⊥})^{⊥} is p, (A ⊗ B)^{⊥} is A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥}, (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} is A^{⊥} ⊗ B^{⊥}, 1^{⊥} is ⊥, ⊥^{⊥} is 1, (A & B)^{⊥} is A^{⊥} ⊕ B^{⊥}, (A ⊕ B)^{⊥} is A^{⊥} & B^{⊥}, ⊤^{⊥} is 0, and 0^{⊥} is ⊤.

mall proof rules are

I  \overline{⊢ p, p^{⊥}}  \frac{⊢ A, Γ  ⊢ A^{⊥}, Δ}{⊢ Γ, Δ} Cut

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  \frac{⊢ A, B, Γ}{⊢ (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B), Γ}  \frac{⊢ A, Γ  ⊢ B, Δ}{⊢ (A ⊗ B), Γ, Δ}  ⊗

⊥  \frac{⊢ Γ}{⊢ ⊥, Γ}  \overline{⊢ 1}  1

⊕1  \frac{⊢ A, Γ}{⊢ (A ⊕ B), Γ}  \frac{⊢ A, Γ  ⊢ B, Γ}{⊢ (A & B), Γ}  &

⊕2  \frac{⊢ B, Γ}{⊢ (A ⊕ B), Γ}  \overline{⊢ ⊤, Γ}  ⊤

mall enjoys the cut-elimination property and the subformula property [14, 21]. In particular, if a mall formula is provable, then it is provable without the use of the cut rule, and the required proof rules involve only subformulas of the given formula.

Let us describe several variations of the proof game discussed in [22], all involving the same moves. There are two players, called proponent and opponent, and a separate verifier. Proponent’s goal is to play a number of moves demonstrating or giving evidence for a sequent. In order to do this, proponent plays proof rule instances. Opponent tries to force the direction of proponent’s evidence in a way that makes it impossible for proponent to win. Opponent plays special markers that may block one side of proponent’s & moves. If proponent plays a ⊗ move, then opponent does not block either of the premises.

Verifier scores completed plays of the game. Various forms of the game differ in the way they are scored. The main objective of proponent is to never allow opponent to succeed. However, in some forms of the game proponent will be more ambitious, that is, in addition to the main requirement, proponent will try to achieve the best score possible.

Let us first consider a simple version of the game against a randomized opponent, which can be described as an avg/max game played on mall sequents. Proponent chooses the inference rule to be applied. In the case ⊗, proponent chooses a partition and requires both associated expressions to be evaluated. In the case ⊕, proponent chooses which of the two expressions will be evaluated. In the case &, opponent chooses by a fair coin toss which of the two expressions will be evaluated. In the case of a primitive sequent, verifier simply computes the value. Each sequent containing the constant ⊤, each identity axiom, and each primitive sequent containing only the constant 1 is scored 1 by verifier. All other primitive sequents are scored 0. Each completed play of the game is scored as the minimum of the scores of terminal sequents obtained in the play. Note that the number of moves is finite; indeed, it is polynomial in the size of a given mall sequent. Proponent wins when each encountered primitive sequent is an identity axiom or the constant 1.

Let us define the function μ, which represents the expected score when proponent plays optimally.

μ(Γ) = max{μ(Γ′; A) | Γ = Γ′, A},

μ(Γ; A ⊗ B) = max{min{μ(Δ, A), μ(Θ, B)} | Δ ⊎ Θ = Γ},
μ(Γ; A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) = μ(Γ, A, B),

μ(Γ; A ⊕ B) = max{μ(Γ, A), μ(Γ, B)},

μ(Γ; A&B) = \frac{1}{2}[μ(Γ, A) + μ(Γ, B)],

μ(Γ; ⊥) = μ(Γ),
μ(Γ; ⊤) = 1,

μ(Σ) = \{ \begin{matrix}1 & if Σ is 1 or an axiom, \\ 0 & otherwise. \end{matrix}

Let us emphasize that, for any mall sequent ⊢ Ξ, the value μ(Ξ) is the maximum possible value satisfying these recursive conditions. Specifically, if any encountered sequent contains composite formulas, then several clauses regarding μ(Γ; A) might be applicable.

It may be seen that a mall sequent ⊢ Ξ is provable iff μ(Ξ) = 1. Furthermore, if ⊢ Ξ is unprovable and does not contain & , then μ(Ξ) = 0. However, μ(Ξ) may be arbitrarily close to 1 if ⊢ Ξ is unprovable and contains & .

The more involved version of the linear logic proof game against a randomized opponent may also be presented as an avg/max game. The players’ moves and the winning condition are the same as in the simple game just described. However, in this version of the game, proponent also attempts to use as many certain preferred axioms as possible. Preferred axioms are, say, instances of a distinguished axiom ⊢ d, d^{⊥}, where the propositional atom d is fixed in advance. In this version, no points are awarded for a sequent containing the constant ⊤, but proponent gets one point for each instance of the distinguished axiom ⊢ d, d^{⊥} encountered in a play. No points are awarded if a primitive sequent ⊢ Σ is any other identity axiom ⊢ p, p^{⊥} or a single constant ⊢ 1. If Σ is any other multiset of literals or constants, that is, a possibly empty multiset of literals or constants 1, 0 other than an identity axiom or the single constant 1, then proponent receives a penalty of −2^{n} points, where n is length of the original sequent. Each completed play of the game is now scored as the sum of the scores of primitive sequents obtained at the end of the play. Note that proponent wins iff this sum is ≥ 0.

Let us define the function ρ, which represents the expected score for proponent when proponent plays optimally.

ρ(Γ) = ρ_{n}(Γ), where n = |Γ|,
ρ_{n}(Γ) = max{ρ_{n}(Γ′; A) | Γ = Γ′, A},
ρ_{n}(Γ; A ⊗ B) = max{ρ_{n}(Δ, A) + ρ_{n}(Θ, B) | Δ ⊎ Θ = Γ},
ρ_{n}(Γ; A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) = ρ_{n}(Γ, A, B),
ρ_{n}(Γ; A ⊕ B) = max{ρ_{n}(Γ, A), ρ_{n}(Γ, B)},

ρ_{n}(Γ; A&B) = \frac{1}{2}[ρ_{n}(Γ, A) + ρ_{n}(Γ, B)],

ρ_{n}(Γ; ⊥) = ρ_{n}(Γ),
ρ_{n}(Γ; ⊤) = 0,
ρ_{n}(Σ) = \{ \begin{matrix}1 & if Σ is the distinguished axiom d, d^{⊥}, \\ 0 & if Σ is another axiom or 1, \\ −2^{n} & otherwise. \end{matrix}

Observe again that, for any mall sequent ⊢ Ξ, the value ρ(Ξ) is the maximum possible value satisfying these recursive conditions, now with n fixed as the number of symbols in Ξ.

It may be seen that a mall sequent ⊢ Ξ is provable iff ρ(Ξ) ≥ 0. Furthermore, if ⊢ Ξ is unprovable and does not contain the distinguished propositional atom d, then ρ(Ξ) ≤ −1.

Game score functions considered here are intrinsic to the proof system mall. In particular, they are invariant with respect to certain permutability properties, important “structural” properties of mall. That is, our game score functions are invariant with respect to invertible inference rules of mall. The following theorem is proved by induction on the length of Γ.

Theorem 6.1 The following equalities hold, with n the length of the longest sequent in each equality:

• ρ_{n}(Γ, A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) = ρ_{n}(Γ, A, B),

• ρ_{n}(Γ, A&B) = \frac{1}{2}(ρ_{n}(Γ, A) + ρ_{n}(Γ, B)),

• If Γ does not contain &, then ρ_{n}(Γ, A ⊕ B) = max{ρ_{n}(Γ, A), ρ_{n}(Γ, B)},

and similarly for μ.

Let us also observe that many isomorphisms of linear logic are respected by the score functions we consider, e.g., A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C) ≅ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C, A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B&C) ≅ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)&(A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C), A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥ ≅ A, A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ≅ B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A, A ⊗ B ≅ B ⊗ A, A ⊗ 1 ≅ A, A ⊗ (B ⊗ C) ≅ (A ⊗ B) ⊗ C, etc. Notable exceptions are A&⊤ ≅ A and A&(B&C) ≅ (A&B)&C.

7 Representing games in the linear logic proof game

In this section, stochastic (generalized) formula games discussed in Section 2 will be represented by linear logic games introduced in Section 6. The simple game on formulas will be represented by the simple version of the linear logic proof game. The clause-counting games will be represented by means of the advanced version of the linear logic proof game. Of course, the representations themselves will be computable in polynomial time.

In the instances we consider, a natural way to define game representations is to emphasize optimal strategies, that is, optimal with respect to score, rather than winning strategies:

Definition 7.1 A game representation is an assignment that maps • inputs to inputs,

• proponent’s moves to sequences of proponent’s moves,

• opponent’s moves to sequences of moves containing exactly one opponent’s move,

• proponent’s strategies to proponent’s strategies, and

• proponent’s optimal strategies to proponent’s optimal strategies.

In the instances we consider, these conditions imply that the game score is preserved.

The reader will observe that the proof of the pspace-hardness of mall in [21] in fact establishes a polynomial-time representation of the simple evaluation game on classical formulas (discussed here at the beginning of Section 2) by means of the simple linear logic proof game with a universal opponent, who may make clever choices in blocking one of the premises of a & rule instance.

Let us summarize the main results.

Theorem 7.2 There exists a polynomial-time representation of the prob-stoc game by the simple linear logic proof game with the randomized opponent. In particular, the associated polynomial-time encoding [|·|] of stochastic formulas by mall sequents satisfies the condition prob-stoc(ϕ) = μ([|ϕ|]) for all closed ϕ.

Theorem 7.3 There exists a polynomial-time representation of the max-stoc game by the advanced linear logic proof game with the randomized opponent. In particular, the associated polynomialtime encoding [| · |] of generalized stochastic formulas by mall sequents satisfies the condition max-stoc(ϕ) = ρ([|ϕ|]) for all closed ϕ.

7.1 Lower bounds for linear logic proof game

The existence of the game representations just discussed implies that, for each version of the linear logic game defined in Section 6, approximating the optimal score within a certain multiplicative ratio is pspace-hard.

Regarding the simple linear logic game against a stochastic opponent, Theorem 7.2 and the result from [9] cited here as Theorem 5.4 yield the following lower bound.

Theorem 7.4 There exists a positive real number c such that the function μ is pspace-hard to approximate within the multiplicative ratio 2^{−n^{c}}, where n is the length of a sequent.

In other words, computing any function g that, for every mall formula F, satisfies

2^{−|F |^{c}} ≤ \frac{g(F)}{μ(F)} ≤ 2^{|F |^{c}}

would amount to the ability to recognize every pspace language. As an illustration of the meaning of the condition, note that even a very large constant g fails to satisfy the condition, since the values of μ can be very close to zero. On the other hand, the theorem implies that the function μ is pspace-hard to approximate up to any constant factor.

Note that the similar result in the case of the simple linear logic game against a universal opponent is a trivial consequence of the pspace-completeness of mall known from [21]. Indeed, the score v when proponent plays optimally is discrete (v(Ξ) = 1 if Ξ is provable, else v(Ξ) = 0), and thus approximating v within a multiplicative ratio amounts to computing v exactly.

Let us close by considering lower bounds for the advanced version of the linear logic game, in which proponent’s goal is to maximize the number of occurrences of the distinguished identity axiom in a cut-free mall proof.

Theorem 7.5 The function ρ is pspace-hard to approximate within any positive multiplicative ratio on provable mall sequents.

This theorem may be obtained directly from the pspace-completeness of mall known from [21]. However, the set of provable mall sequents on which the function ρ is pspace-hard to approximate may be further restricted in several ways by using Theorems 5.5 and 7.3, and the result from [9] cited here as Theorem 5.3. Let us say that a constraint is a mall formula of the form (A ⊗ z_{1})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (z_{1}^{⊥} ⊗ z_{2}) …^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (z_{n}^{⊥} ⊗ ⋆), where & does not occur in A, each z_{i} is a literal, and where ⋆ abbreviates the formula d^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d^{⊥} related to the distinguished axiom ⊢ d, d^{⊥}. Note that the size of a constraint includes the size of the formula A. Let us say that a sequent is constrained if the distinguished formula ⋆ occurs only in constraints. Note that provability of constraints is in np, in contrast with the general mall provability, which is pspace-complete.

Theorem 7.6 There exists a positive real number c such that the function ρ is pspace-hard to approximate within multiplicative ratio n^{−c} on provable constrained mall sequents, where n is the length of the sequent. Furthermore, there exists a positive real number ϵ < 1 such that the function ρ is pspace-hard to approximate within multiplicative ratio ϵ on provable constrained mall sequents where every constraint is of constant size.

On the other hand, proof-theoretic properties of linear logic allow us to restrict provable mall sequents to those that contain only formulas of depth at most 2.

Theorems 7.3, 7.5, and 7.6 have analogs in the case in which the game is played against a universal opponent, but that case must be omitted here. The reader is referred to [23]. Our results also have implications for proof search heuristics in linear logic. This is discussed in [24].

Acknowledgements: We would like to thank Madhu Sudan for directing us to [10, 9], and Sanjeev Arora and Joan Feigenbaum for their informative email correspondence and for their help with the literature. Scedrov would like to thank Stanford University and SRI International for hosting him during his visit in the spring of 1995. All the authors would like to thank the Isaac Newton Institute for Mathematical Sciences in Cambridge, England for hosting them at various times in the fall of 1995.

References

[1] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59:543–574, 1994.

[2] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF (Extended abstract). In Proc. TACS ’94, Springer LNCS Vol. 789, pages 1–15, 1994.

[3] S. Arora. Probabilistic checking of proofs and hardness of approximation problems. Technical Report CS-TR-476-94, Department of Computer Science, Princeton University, 1994. Revised version of a Ph.D. Dissertation, University of California, Berkeley, 1994.

[4] S. Arora and C. Lund. Hardness of approximations. In Approximation Algorithms for NP-hard Problems. PWS Publishing, 1996.

[5] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and hardness of approximation problems. In Proc. 33-rd Annual IEEE Symposium on Foundations of Computer Science, pages 14–23. IEEE Computer Society Press, Los Alamitos, California, 1992.

[6] S. Arora and S. Safra. Probabilistic checking of proofs; A new characterization of NP. In Proc. 33-rd Annual IEEE Symposium on Foundations of Computer Science, pages 2–13. IEEE Computer Society Press, Los Alamitos, California, 1992.

[7] L. Babai and S. Moran. Arthur-Merlin games: a randomized proof system, and a hierarchy of complexity classes. J. Computer System Sciences, 36:254–276, 1988.

[8] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183–220, 1992.

[9] A. Condon, J. Feigenbaum, C. Lund, and P. Shor. Random debaters and the hardness of approximating stochastic functions. In Proc. 9-th Annual IEEE Conference on Structure in Complexity Theory, pages 280–293. IEEE Computer Society Press, Los Alamitos, California, 1994. Full version to appear in SIAM Journal of Computing.

[10] A. Condon, J. Feigenbaum, C. Lund, and P. Shor. Probabilistically checkable debate systems and nonapproximability of PSPACE-hard functions. Chicago Journal of Theoretical Computer Science, page http://www.cs.chicago.edu/publications/cjtcs/articles/1995/4/contents.html, 1995, No. 4. Extended abstract in Proc. 25-th ACM Symposium on Theory of Computing, pages 305-314, ACM, New York, 1993.

[11] V. Danos, H. Herbelin, and L. Regnier. Game semantics and abstract machines. In Proc. 11-th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, July 1996.

[12] U. Feige, S. Goldwasser, L. Lovász, S. Safra, and M. Szegedy. Approximating clique is almost NP-complete. In Proc. 32-nd Annual IEEE Symposium on Foundations of Computer Science, pages 2–12. IEEE Computer Society Press, Los Alamitos, California, 1991.

[13] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., 1979.

[14] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[15] J.-Y. Girard. Linear logic: its syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in linear logic. London Mathematical Society Lecture Note Series, Volume 222, Cambridge University Press, 1995.

[16] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proof systems. SIAM J. Computing, 18:186–208, 1989.

[17] J. M. E. Hyland and C.-H. L. Ong. Pi-calculus, dialogue games and PCF. In Proceedings of the 7th acm Conference on Functional Programming Languages and Computer Architecture, pages 96–107. ACM Press, 1995.

[18] H.B. Hunt III, M.V. Marathe, and R.E. Stearns. Generalized CNF satisfiability problems and non-efficient approximability. In Proc. 9-th Annual IEEE Conference on Structure in Complexity Theory, pages 356–366. IEEE Computer Society Press, Los Alamitos, California, 1994.

[19] A. Joyal. Free lattices, communication, and money games. In: Proceedings of the 10-th International Congress of Logic, Methodology, and Philosophy of Science, Firenze, 1995.

[20] F. Lamarche. Games semantics for full propositional linear logic. In Proc. 10-th Annual IEEE Symposium on Logic in Computer Science, San Diego, pages 464–473, June 1995.

[21] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239–311, 1992. Extended abstract in Proc. 31-st Annual IEEE Symposium on Foundations of Computer Science, pages 662-671, 1990.

[22] P.D. Lincoln, J.C. Mitchell, and A. Scedrov. Stochastic interaction and linear logic. In J.-Y Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 147–166. London Mathematical Society Lecture Notes, Volume 222, Cambridge University Press, 1995.

[23] P.D. Lincoln, J.C. Mitchell, and A. Scedrov. Linear logic proof games and optimization. Preliminary report, January 1996. Available by anonymous ftp from ftp.cis.upenn.edu as pub/papers/scedrov/approx.[dvi,ps].Z. See pub/papers/TableOfContents.

[24] P.D. Lincoln, J.C. Mitchell, and A. Scedrov. The complexity of local proof search in linear logic. In Proceedings Linear Logic ’96, Tokyo Meeting, page http://www.elsevier.nl:80/mcs/tcs/pc/Menu.html. Electronic Notes in Theoretical Computer Science, 1996, to appear.

[25] C. Lund, L. Fortnow, H. Karloff, and N. Nisan. Algebraic methods for interactive proof systems. J. ACM, 39:859–868, 1992.

[26] R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, 1995.

[27] C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

[28] A. Scedrov. A brief guide to linear logic. In G. Rozenberg and A. Salomaa, editors, Current Trends in Theoretical Computer Science, pages 377–394. World Scientific Publishing Co., 1993.

[29] A. Scedrov. Linear Logic and Computation: A Survey. In H. Schwichtenberg, editor, Proof and Computation, Proceedings Marktoberdorf Summer School 1993, volume 139, pages 379– 395. NATO Advanced Science Institutes, Series F, Springer-Verlag, Berlin, 1995.

[30] A. Shamir. IP = PSPACE. J. ACM, 39:869–877, 1992.

[31] M. Sudan. Efficient checking of polynomials and proofs and the hardness of approximation problems. ACM Distinguished Dissertation Series, Springer-Verlag, 1996. Revised version of a Ph.D. Dissertation, University of California, Berkeley, 1993.