Stochastic Interaction and Linear Logic

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

Abstract

We present stochastic interactive semantics for propositional linear logic without modalities. The framework is based on interactive protocols considered in computational complexity theory, in which a prover (expert) with unlimited power interacts with a verifier or skeptic (bean counter) who can only toss fair coins or perform simple tasks when presented with the given formula or with subsequent messages from the prover. The additive conjunction & is described as random choice, which reflects the intuitive idea that the verifier can perform only “random spot checks”. This stochastic interactive semantic framework is shown to be sound and complete. Furthermore, the prover’s winning strategies correspond to proofs of the given formula. In this framework, the multiplicative and additive connectives of linear logic are described by means of probabilistic operators, giving a new basis for intuitive reasoning about linear logic and a potential new tool in automated deduction. We also investigate an arithmetic form of this semantic framework, in which a formula may be associated with a polynomiallike expression over a finite field of limited size so that the formula is provable iff the expression is nonzero.

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

†jcm@cs.stanford.edu WWW: http://theory.stanford.edu/people/jcm/home.html Department of Computer Science, Stanford University, Stanford, CA 94305. Supported in part by an NSF PYI Award, matching funds from Digital Equipment Corporation, the Powell Foundation, and Xerox Corporation; and the Wallace F. and Lucille M.

Davis Faculty Scholarship.

‡andre@cis.upenn.edu WWW: http://www.cis.upenn.edu/~andre Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395. Partially supported by NSF Grant CCR-91-02753 and by ONR Grant N00014-92-J-1916. Scedrov is an American Mathematical Society Centennial Research Fellow.

1 Introduction

Linear logic arose from the semantic study of the structure of proofs in intuitionistic logic. Girard presented the coherence space and phase space semantics of linear logic in his original work on linear logic [Gir87]. While these models provide mathematical tools for the study of several aspects of linear logic, they do not offer a simple intuitive way of reasoning about linear logic. More recently, Blass [Bla92], Abramsky and Jagadeesan [AJ94], Lamarche, and Hyland and Ong have developed semantics of linear logic by means of games and interaction. These new approaches have already proven fruitful in providing an evocative semantic paradigm for linear logic and have found a striking application to programming language theory in the work of Abramsky, Jagadeesan, and Malacaria [AJM93] and in the work of Hyland and Ong [HO93].

The game-theoretic notions used so far draw mainly on set theory and on proof theory. They do not yet fully explain linear logic formulas involving both multiplicative and additive connectives, i.e., the formulas of the multiplicative-additive fragment of linear logic, mall [Gir87, LMSS92, Sce93]. In contrast, the direct, structural relationship between the natural fragments of linear logic and the standard computational complexity classes that has emerged from [LMSS92, LS94a, LS94b] makes it possible to draw on game-theoretic notions stemming from computational complexity theory. Here we are particularly interested in the game-theoretic notions involving stochastic interaction. This setting, described in Papadimitriou [Pap94], involves interactive protocols in which a prover (expert) with unlimited power interacts with a verifier (score keeper) who can only toss coins or perform simple (say, polynomial time) tasks when presented with the input or with the prover’s messages.

A relevant setting was introduced in Papadimitriou [Pap85], described as “games against Nature” or “stochastic alternating polynomial time machines” (saptime) and shown to characterize polynomial space (pspace). More precisely, a set of finite strings L belongs to saptime if some verifier V can be convinced by some prover P to accept any x ∈ L with probability > 1/2, while P or any other prover can convince the verifier V to accept any x ∉ L only with probability < 1/2. In addition, if the probabilities are required to be bounded away from 1/2, one obtains “Arthur-Merlin games” proposed by Babai and Moran [BM88] or similar “interactive proof systems” proposed by Goldwasser, Micali, and Rackoff [GMR89]. Shamir [Sha92] and Shen [She92] have shown that all these formulations describe exactly pspace. Since mall is pspace-complete [LMSS92], there is a complexity-theoretic basis for finding a direct, structural relationship between the expert/user interactions just described and mall that goes beyond an immediate Turing reduction.

In Section 2 we give an intuitive overview of the game semantics approach. We describe a simplified ’linear game boy’ where a human player plays a game essentially trying to convince a little electronic machine (which has very limited computing power) that a given mall sequent is provable. Even if the human plays optimally, the human cannot convince the machine of the provability of an unprovable sequent very often. More specifically, the game can be played to win more than half the time if and only if the starting sequent is provable.

In Section 4 we present a formal semantics for mall based on games against Nature and prove it sound and complete for provability in mall. When the game-theoretic or the complexity-theoretic aspects are disregarded, the semantic notions involved may be distilled to a rather simple semantic characterization of mall provability akin to the ordinary truth tables, but involving probabilistic truth values. On the other hand, the prover’s winning strategies are for all practical purposes proofs of the given formula. In this framework the multiplicative and additive connectives of linear logic are described by means of probabilistic operators. A central feature is the description of the additive conjunction, &, as random choice. This approach offers a new basis for intuitive reasoning about linear logic and a potential new tool in automated deduction, and suggests a connection between linear logic and probabilistic logic such as sometimes used in artificial intelligence.

In Section 5 we present an arithmetic characterization of mall provability, in which a formula may be associated with a polynomial-like expression over a finite field of limited size so that the formula is provable iff the expression is nonzero. This characterization is obtained by combining certain aspects of the standard proof of Cook’s theorem on np-completeness of boolean satisfiability with the “arithmetization” of quantified boolean formulas discussed in, e.g., Shamir [Sha92]. Section 5 represents work in progress toward a complete semantics of mall based on interactive proof systems mentioned above. This extended abstract concludes with suggestions for further research.

We would like to thank Jean-Yves Girard, Andreas Blass, Yuri Gurevich, Bill Rounds, and Larry Moss for interesting and inspiring discussions.

2 Game Semantics

The general idea of game semantics may be illustrated using classical quantified propositional logic. This game will have two players, called for-all and there-exists, each smart enough to evaluate a quantifier-free proposition, given an assignment of truth values (true or false) to the propositional variables. The play begins with a quantified formula such as

∃P ∀Q ∃R [(P ∧ Q ∧ ¬R) ∨ (P ∧ ¬Q ∧ R)]

in prenex form that starts with an existential quantifier and alternates between ∀ and ∃. (Any formula can be put in this form or, alternatively, we can extend the game to more general syntactic forms.) The goal of there-exists, who moves first, is to choose values for the existentially-quantified variables that will make the matrix true. The goal for for-all is to choose values for the universallyquantified variables that will make the formula false. It is easy to see that if the players alternate, each choosing a truth value for the variables they are given until the quantifier prefix is exhausted, there-exists can win if the formula is valid and for-all is able to win otherwise. For example, on the valid formula above, there-exists may begin by letting P be true. Whatever value for-all chooses for Q, there-exists may win by letting R be the negation of Q. When there-exists has a way of winning, regardless of how for-all plays, we say there-exists has a winning strategy, and similarly for for-all. More formally, we can define a winning strategy for there-exists as a function that chooses moves in such a way that there-exists is guaranteed to win. A strategy is generally a function of the formula and the moves made by both players (up until the point where a next move is required).

An issue we are particularly concerned with is the length of the game and the amount of “thought” (or, more technically, computational resource) that is required to play the game optimally. In the game for quantified propositional logic, for example, if there-exists is going to compute a winning strategy as a function of the formula and moves of the other player, this may be done by a Turing machine whose space requirement is bounded by a polynomial in the length of the formula. (This is easily argued using formulas of the form ∃P [(P ∧ ϕ) ∨ (¬P ∧ ¬ϕ)], where there-exists must set P to the truth value of ϕ.) Similarly, if for-all is going to win when a formula is not valid, then polynomial space is also required. Therefore, we can say that in this game, both players require polynomial space. This seems reasonable, since deciding whether a classical quantified propositional formula is valid is a pspace-complete problem.

A recent trend in complexity theory, motivated by the study of cryptography and randomness, is the use of asymmetric “games” to characterize various computational problems. Returning to classical quantified propositional formulas, there exist asymmetric games in which one player may use unbounded resources, but the other only requires polynomial time (which is less than polynomial space), and the weaker player is allowed to play randomly by “flipping coins.” We will use this form of game for mall.

2.1 Game Board

We will give several forms of proof games, all using the same board and tiles. The difference between the games is that the first versions, given primarily to illustrate the main ideas that appear in the later versions, use simple rules that require complicated strategies for both players. In the later games, we change the rules so that one player may play effectively using only randomness and very simple (polynomial-time) computation. In all but the first cases, we will keep the games “short,” meaning that the length of each game (measured as the number of rounds of play) is bounded by the length of linear logic sequent that appears on the first tile played.

All games are played on a rectangular grid which looks like an uncolored checkerboard that extends infinitely up and to the right. A “home version” of this board designed for one-evening games in front of the fire can be bounded to some fixed size. In the “game boy” version we discuss below, the board is considered unbounded, with only a portion of the board displayed on the small lcd screen at any time.

There are two players, called the prover and the skeptic. The goal of the prover is to play a sequence of tiles demonstrating or giving evidence for a sequent. To do this, the prover plays tiles that contain one sequent in the lower left, and one or two shorter sequents in the top and right quadrants. The skeptic tries to force the direction of the provers evidence in a way that makes it impossible for the prover to win. The skeptic plays simple black (or cross-hatched) tiles that may block one side of one of the provers tiles. The skeptic also scores the game by blocking win or lose on a terminal prover tile, leaving the correct score exposed.

The tiles of the game are drawn in Figure 1. The main idea is that each prover tile contains an instance of a mall proof rule, tilted to the side to fit on a rectangular grid. The prover uses these to place a proof tree, or branch of a proof tree, on the board. When a proof rule has more than one hypothesis, the skeptic can block one, forcing the prover to try to complete the branch containing the other hypothesis. If the prover plays a tile with sequents Γ and Δ exposed to the top and right, then the skeptic may (or may not) block one of these edges. In either case, the only legal adjacent play for the prover is to place another prover tile with sequent Γ or Δ to the left of its diagonal, Γ if this is above the previous tile and Δ if it is to the right. We consider two sequents the same, for the purposes of the game, if they are identical as multisets. In other words, the formulas may appear in any order, but the number of occurrences of each type of formula must match.

The reason for the special “literal” tiles, with pseudo-hypotheses win and lose, is to allow the game to be “scored” by the skeptic. If the prover plays until there are no connectives remaining in the sequent, the only remaining play is a matching tile with literals. At this point, the prover either wins or loses, depending (in the simple form of the game) on whether the multiset of literals is an axiom or not. Although this is not important, we establish the convention that when the prover plays a literal tile, and the skeptic plays a solid tile in an adjacent square, this tile is considered winning if skeptic plays adjacent to lose, and losing if the skeptic plays adjacent to win. This is just to give some specific, visual representation of each play of the game.

Tiles for prover

Γ, Δ, A ⊗ B Γ, A Δ, B  ^{Γ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B Γ, A, B}  ^{Γ, A & B Γ, A Γ, B}
Γ, A ⊕ B Γ, A  ^{Γ, A ⊕ B Γ, B}  ^{L_{1}, …, L_{k} WIN LOSE}

Tile for skeptic

A, B arbitrary formulas, Γ an arbitrary multiset of formulas, and L_{1}, …, L_{k} literals. Figure 1: Tiles for prover and skeptic.

A, A^{⊥} WIN LOSE

A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥} A, A^{⊥}

(A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥}) ⊕ B A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥}
Figure 2: A winning play for (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥}) ⊕ B.

2.2 Elementary deterministic form

An elementary form of “game” using this board and set of tiles is just to let the prover play, from any initial tile in the lower left corner of the board. The skeptic checks to ensure that all tiles are legally played (that the multisets of formulas along all adjoining edges match). The skeptic also checks that all exposed edge tiles are literal tiles, and that they all can be scored as a win. In this form of game, the prover exhibits a proof tree and the skeptic evaluates each leaf, allowing the prover to win if each leaf of the tree is an axiom. An example play of this game is illustrated in Figure 2. Note that in some cases the prover will be required to make use of connector tiles (the last two prover tiles showing in Figure 1) that do not change the sequent along that branch of the proof. Rather, these tiles just extend the sequent out along a branch to reach a part of the board where there may be more room. It is the provers responsibility to plan the layout the proof so that all tiles are placed legally.

From a common-sense point of view, this is not much of a “game,” amounting more to a game of solitaire than a two-person game. More technically, a play of this game may involve more prover tiles than the number of connectives in the sequent on the lower left of the lower-left tile. The reason is that the tile (proof rule) for & has more symbols to the right of the diagonal (in the hypotheses) than the on the left (in the conclusion), duplicating all of the context of the & -formula. The next version of the game, which is close to the simple game described earlier for classical quantified propositional logic, we will have interaction between players and a linear bound on the number of prover (and hence skeptic) tiles used in any play of the game.

A, B, A^{⊥} ⊗ B^{⊥} A, A^{⊥} B, B^{⊥}  ^{B, B^{⊥} WIN LOSE}

\begin{matrix}A, B, \\ (A^{⊥} ⊗ B^{⊥}) \\ & C \end{matrix} A, B, A^{⊥} ⊗ B^{⊥} A, B, C
Figure 3: A winning play for A, B, (A^{⊥} ⊗ B^{⊥}) & C

2.3 Revised deterministic form

The next version of the game is similar in spirit to the simple game described for classical quantified propositional logic. The prover tries to show that a sequent is provable, and the skeptic tries to make this demonstration as difficult as possible. The prover is able to win if the sequent is provable, and the skeptic is able to keep the prover from winning if the sequent is not provable. However, in order to play effectively, both players must be able to understand provability for mall formulas.

In this game, the two players, prover and skeptic, alternate. The prover begins by placing a tile in the lower left corner of the board. The prover is not allowed to play connector tiles in this version of the game. If a tile has two sequents to the right of the diagonal, then the skeptic blocks one of them and the prover must continue by placing a tile with matching sequent against the remaining, unblocked side or the tile. If there is only one sequent to the right of the diagonal, the skeptic does not play and the prover may take another turn. When a literal tile is played, the skeptic plays a final tile, indicating that the prover has won or lost. An example play, in which prover wins on an unprovable sequent, as the result of a legal but suboptimal play by the skeptic, is shown in Figure 3.

Essentially, this game amounts to the construction of one branch of a proof tree, with the skeptic allowed to select a branch for the sequent chosen by the prover. If the prover begins by playing a provable sequent (and a correct proof rule), then the prover can win, since all branches can be completed. If the prover plays an unprovable sequent, then the skeptic can force the prover into a position where the branch of the proof tree exhibited on the game board cannot be completed. The length of any play is bounded by the number of connectives in the initial sequent, since each prover play reduces this number by one, and skeptic keeps all sequents but one blocked.

The shortcoming of this game is that in order to play optimally, each player must have pspace computing power. Since the prover has to construct a proof, the prover must begin with a provable sequent and choose the correct rule at each play. If the prover tries to play an unprovable sequent, then the skeptic must select the branch that cannot be completed. For example, if the prover begins with A & B, where A and B are complicated formulas with one provable and the other not, then the skeptic can win only by determining which is provable. As a real game, this is not very satisfying, since when both players have pspace computing power, both can determine from the very first tile whether they have a winning strategy or not. Therefore, if this game were actually played between two capable players, it is likely that one would concede immediately after the first play, realizing that the other player had a winning strategy. This would be a bit like two adults playing tic-tac-toe.

2.4 Probabilistic form

The probabilistic game may be played by a knowledgeable prover against a limited, probabilistic opponent. A rough analogy exists with small hand-held electronic games such as Game Boy. This may help establish some intuition for the game. In our probabilistic game, the skeptic has a fixed, simple strategy that is effective in a probabilistic sense. This strategy could be implemented with a minimal amount of circuitry (or simple program) in a Linear Game Boy that flips coins to decide some of its moves. This electronic game would have the properties that a knowledgeable prover could win most of the time by beginning with a provable sequent, and occasionally win with an unprovable sequent. At least in the daze of a transcontinental flight, such a game could keep a capable player occupied for several hours, winning sometimes and losing others.

Before giving the probabilistic analysis, we outline the skeptic’s randomized strategy in Figure 4. A change from the previous game is that in one case, the skeptic need not block one of the sequents on a binary prover tile. This forces the prover to complete more than one branch of the proof tree.

A technical detail related to our physical presentation of this logical game is that a proof with many branches may not fit on the rectangular game board without inserting additional “connector tiles.” Specifically, a full binary tree must have 2^{n} nodes within a distance n of the root, whereas a rectangular grid only has O(n^{2}) squares. Therefore, we allow the prover to use connector tiles that serve no purpose other than to bring the play of the game out from a congested area of the board to some region with enough unused squares to continue play. One may consider that at each play of any prover tile, connector tiles of arbitrary length and shape are automatically attached as needed. Since the connector tiles do not effect the logic of the game, and are not needed in any of the examples we show, we will generally ignore them in the rest of this paper.

An initially counter-intuitive aspect of this strategy is the skeptic’s play when the prover places a literal tile. However, this is absolutely critical to the success of the probabilistic strategy. An intuitive explanation is that if the prover begins with an unprovable sequent, then there is some branch of the proof tree of this sequent that does not lead to an axiom. However, if there are many & ’s in the sequent, the proof tree will have many branches, and the skeptic will choose among them randomly. Therefore, the prover has a very good chance of winning, since the skeptic will have only a very small probability of luckily guessing the branch that cannot be completed. A short example illustrating this phenomenon is given in Figure ??. The prover begins with the sequent A, A^{⊥} & B, allowing the skeptic to choose between A, A^{⊥} and A, B. If the skeptic chooses randomly, then the prover has a 50% chance of getting A, A^{⊥}, which is an axiom if A is a literal, and A, B, which is not. Therefore, if the skeptic were simply to mark win or lose deterministically, according to whether a sequence of literals is an axiom, the prover would have an equal chance of winning or

Play by prover  Response by skeptic
Γ, Δ, A ⊗ B Γ, A Δ, B  No play. The prover must continue both directions.
Γ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B Γ, A, B  Block blank side.
Γ, A & B Γ, A Γ, B  Flip a coin and block one exposed sequent.
Γ, A ⊕ B Γ, A  Block blank side.
Γ, A ⊕ B Γ, B  Block blank side.
L_{1}, …, L_{k} WIN LOSE  Allow win with probability (1 + ϵ)/2 if axioms, ϵ if not.

Figure 4: Probabilistic strategy for skeptic. losing from an unprovable sequent. Since the goal is to give the prover a good (over 50%) chance of winning only for provable sequents, some randomization is necessary on sequences of literals. With the strategy listed above, the prover has probability (1 + 3ϵ)/4 of winning, which will be less than 1/2 as long as ϵ is less than 1/3.

An analogous scenario that may make this strategy seem more intuitive involves a class of n students who are rewarded if they vote the correct answer to a true/false question. This might be a historical question, say, where there is a clear correct answer and students can be expected to know whether they know the answer. If even one student knows the correct answer, and the rest do not, the class can still vote the right answer with probability greater than one-half using randomness. Specifically, the student who knows the correct answer must vote correctly and the rest should flip coins and vote randomly. The connection between this classroom scenario and the proof game is that when a proof branch ends in an axiom, the skeptic really has very little knowledge about whether the initial sequent is really provable. In this case, a randomized response gives the best expected result. On the other hand, when the proof branch ends unsuccessfully, it is clear that the prover has failed and the skeptic can either reject the proof deterministically or (since the result is easier to analyze) allow success only with very low probability.

3 Preliminary Formalism

We now formalize the intuitive ’Game-Boy Semantics’ presented in the previous section, eventually making use of Papadimitrou’s games against nature. We begin with a simple form of the tile-based game, described as a min/max game semantics for mall. This min/max game is played by two equally powerful players, the “prover” P and the “verifier” V. They are attempting to find whether the value of a given mall sequent is 1 or 0, where the value v is the maximum possible satisfying the conditions given below. Let A, B be mall formulas, let Γ, Δ, Θ be mall sequents, i.e., finite multisets of mall formulas, and let Ξ be a finite multiset of literals. We write Δ ⊎ Θ for the (disjoint) multiset union of Δ and Θ.

The value of a sequent is defined as follows:

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

v(Γ, A ⊕ B) = max{v(Γ, A), v(Γ, B)},

v(Γ, A&B) = min{v(Γ, A), v(Γ, B)},

v(Ξ) = 1 if Ξ is an axiom, else 0 .

Let us emphasize that the value of a sequent is the maximum possible satisfying these conditions. Specifically, if a sequent contains composite formulas, then several clauses might be applicable.

Player P chooses the case to be applied. In the case ⊗, P chooses a partition of Γ and requires both associated expresions to be evaluated. In the case ⊕, P chooses which of the two expressions will be evaluated. In the case &, V chooses which of the two expressions will be evaluated. In the last case, V simply computes the value. Player V wins if one of the atomic sequents Ξ reached is not an axiom, else player P wins. Note that the number of moves is finite, indeed, it is polynomial in the size of a given mall sequent. A similar game is described in Section 6 of [Bla92].

It is readily seen that:

Proposition 3.1 The following are equivalent for any mall sequent Γ :

(1) Player P (prover) has a winning strategy,

(2) v(Γ) = 1,

(3) the sequent Γ is provable in mall.

One drawback of this setting is that it a priori requires the verifier to have just as much insight as the prover, namely, both need to have pspace capability [LMSS92]. (When A&B is unprovable, the verifier must be able to choose an unprovable conjunct.) In other words, this setting is not truly interactive because both the prover and the verifier can figure out in advance who can win the game.

4 A stochastic semantics

The next step in our analysis is to relate the probabilistic board-game strategy to “games against Nature” or “stochastic alternating polynomial time machines” (saptime) in the style of [Pap85]. A game against Nature may be formalized as consisting of a polynomial time Turing machine (the verifier, V) and an omnipotent prover, P. V may toss fair coins (i.e., consult a random oracle). V and P may exchange messages in polynomial time. A set of finite strings L belongs to the class saptime if P can convince V to accept any x ∈ L with probability > 1/2, while P or any other prover can convince V to accept any x ∉ L only with probability < 1/2. Note that np is a degenerate case of a protocol in which there are no coin tosses and the probabilities are 1 and 0, respectively. It is known that saptime = pspace [Pap85].

On the other hand, since mall is pspace-complete [LMSS92] it is natural to ask whether there exists a direct, structural relationship between mall and saptime that goes beyond an immediate Turing reduction.

We seek a semantics of mall based on randomization and interaction just described. This semantics should be compositional, sound and complete (in the sense of model theory), but it should also be efficient (in the sense of complexity theory), and it should imply that mall is in saptime.

In order to achieve this, we modify the game protocol described in Section 3 so that P can convince V to accept any provable mall sequent Γ with probability greater than 1/2, while P or any other prover can convince V to accept any unprovable mall sequent Γ with probability less than 1/2. The reader should keep in mind that in this setting the verifier has practically no insight: the verifier is simply a polynomial time Turing machine that can toss fair coins. More specifically, the verifier does not have the computational ability to figure out in advance who can win the game.

Let us observe that the simple two-valued semantic framework for mall given in Section 3 does not suffice if V chooses conjuncts in the case & only at random. Indeed, if a given sequent is unprovable, a dishonest prover may concentrate all false information only on one branch of the entire game, while all other branches correctly end up with an axiom. This actually happens if the input is a single formula of the form B_{1}& … &B_{k}, where the association is to the right, B_{k} is unprovable, but B_{i} is provable for each i < k. Thus a more subtle semantics is needed.

Instead of two values 0 and 1, let us consider yield functions, linear real functions on the closed unit interval [0, 1]. We continue the notation from Section 3. For each 0 ≤ ϵ ≤ 1 and a mall sequent Γ the yield y(ϵ, Γ) is the maximum possible subject to the following conditions:

y(ϵ, Γ, A ⊗ B) = max{min{y(ϵ, Δ, A), y(ϵ, Θ, B)} | Δ ⊎ Θ = Γ},

y(ϵ, Γ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) = y(ϵ, Γ, A, B),

y(ϵ, Γ, A ⊕ B) = max{y(ϵ, Γ, A), y(ϵ, Γ, B)},

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

y(ϵ, Ξ) = \frac{1}{2}(1 + ϵ) if Ξ is an axiom, else ϵ .

For any sequent Γ let σ(Γ) = y(0, Γ). It can be seen that 0 ≤ σ(Γ) ≤ 1/2 and that the yield of a sequent Γ is a line segment between the points (0, σ(Γ)) and (1, 1).

This time P is attempting to maximize the yield for a given mall sequent. P ’s moves are the same as before. V, however, now chooses by a fair coin toss which of the two expressions in the & case will be evaluated. In the atomic case, with probability ϵ V accepts without looking at an atomic sequent Ξ, with probability (1 − ϵ)/2 she rejects without looking at Ξ, and with probability (1 − ϵ)/2 she first checks whether Ξ is an axiom and then accepts iff Ξ is an axiom.

Theorem 4.1 For any sequent Γ, y(ϵ, Γ) = σ(Γ) + (1 − σ(Γ))ϵ. Furthermore:

(1) If a sequent Γ is provable in mall, then σ(Γ) = 1/2. Thus for any 0 < ϵ ≤ 1 it is the case that y(ϵ, Γ) > 1/2 and for any such ϵ the prover can convince the verifier to accept with probability > 1/2.

(2) If Γ is not provable in mall, then 0 ≤ σ(Γ) < 1/2. In this case there exists 0 < δ < 1 such that for any 0 ≤ ϵ ≤ δ, it is the case that y(ϵ, Γ) < 1/2. For such ϵ any prover can convince the verifier to accept only with probability < 1/2. It suffices to let δ = 2^{−k−1}, where k is the number of occurrences of the connective & in the sequent Γ.

Note that V has to be able to carry out only fair coin tosses and polynomial time tasks, because the two cases can be distinguished at ϵ = 2^{−k−1}, where k is the number of occurrences of the connective & in the given sequent. For the same reason, the number of moves is polynomial in the length of the given sequent.

The protocol just described can be reformulated in such a way that the yield of a given sequent turns out to be a single real number between 0 and 1. Namely, the yield will be the probability that the verifier accepts, which will depend only on the given sequent.

Let f(0) = f(1) = 1/2. For k > 1 let

f(k) = \frac{1}{2} + \frac{1}{2^{2k}} .

In the reformulated protocol V begins by tossing a fair coin. If heads, then she tosses an unfair coin with distribution f(k): 1 − f(k), where k is the sum of the nesting & depths in the formulas in the given sequent, and she rejects or accepts based solely on the unfair coin toss. That is, if the first (fair) coin toss is heads, V rejects with probability f(k) and accepts with probability 1 − f(k). If the first (fair) coin toss is tails, then P and V follow the simple protocol given in Section 3, except that in the case A&B, V first computes the nesting & depths of both A and B. Say A is &-deeper than B by m. V tosses a fair coin to decide which conjunct will be kept. If the choice is B, then V replaces B by B^{+} = (⊤& … (⊤&(⊤&B)) …), where there are m new &’s above B. The game now continues with a new round. The reader should observe that the unfair coin tosses may be replaced by independent subgames that involve only fair coin tosses.

It is not difficult to see that given a sequent Γ for which the sum of the nesting & depths of formulas in Γ is k, the overall probability of rejection due to the unfair coin tosses is

\frac{1}{2} − \frac{1}{2^{2k}} < ∑_{n=0}^{k} \frac{f(n)}{2^{1+k−n}} < \frac{1}{2}.

If the sequent Γ is provable, then the total probability of rejection is < 1/2 by the second inequality above, because P has a strategy in which the only rejections come from V ’s unfair coin tosses. Thus the probability of acceptance is > 1/2.

If Γ is not provable, then there is at least a 2^{−2k} probability that V actually discovers an atomic sequent Ξ that is not an axiom. By the first inequality above, the total probability of rejection is therefore > 1/2. Thus:

Theorem 4.2 In the reformulated protocol:

(1) If a sequent Γ is provable in mall, then the prover can convince the verifier to accept Γ with probability > 1/2.

(2) If Γ is not provable in mall, then any prover can convince the verifier to accept Γ only with probability < 1/2.

5 An arithmetic semantics

mall sequents of length n may also be seen as elements of a finite field Z/pZ, where p is a prime logarithmic in n, so that the sequent is provable iff the associated element is ≠ 0. In order to present the correspondence, let us first consider an assignment that to any mall sequent Γ and any integer i associates a polynomial expression ∥Γ∥_{i} with integer coefficients. It will be the case that polynomial expression ∥Γ∥_{i} always evaluates to an integer ≥ 0. Furthermore, it will be the case that the sequent Γ is provable iff ∥Γ∥_{i} > 0 for some integer i.

Although this arithmetic interpretation of mall sequents is defined below in only one step, let us mention that the interpretation could also be presented in the following two parts. The first part uses certain aspects of the standard proof of Cook’s theorem on np-completeness of boolean satisfiability to express mall sequents as quantified boolean formulas so that a mall sequent is provable iff the associated quantified boolean formula is valid. The second part is the “arithmetization” of quantified boolean formulas discussed in, e.g., Shamir [Sha92].

Let

f(x_{1}, …, x_{n}) = ∑_{k=1}^{n}(x_{k} · ∏_{j≠k}(1 − x_{k} + 1 − x_{j})).

It is straightforward to check that

Proposition 5.1 Let x_{k} = 0, 1, 1 ≤ k ≤ n. Then f(x_{1}, …, x_{n}) ≥ 0. Furthermore, f(x_{1}, …, x_{n}) > 0 iff there exists j, 1 ≤ j ≤ n, such that x_{j} = 1 and x_{k} = 0 for k ≠ j.

The assignment of polynomial expressions is defined as follows. For a sequent Ξ that consists entirely of literals, let

∥Ξ∥_{i} = 1 if Ξ is an axiom, else 0 .

Otherwise, if a multiset Γ = {A_{1}, …, A_{n}} contains some composite formulas, we let

∥A_{1}, …, A_{n}∥_{i} = ∑_{z_{i1}=0,1} … ∑_{z_{in}=0,1} f(z_{i1}, …, z_{in}) · (∑_{k=1}^{n} z_{ik} · ∥Γ \ A_{k}; A_{k}∥_{i+1}) ,

where ∥Γ \ A_{k}; A_{k}∥_{i}) is defined by cases according to the principal connective of A_{k}.

If A is a (positive or negative) literal we let

∥Γ; A∥_{i} = 0 .

In the case ⊗, for each 1 ≤ j < n and b_{m} = 0, 1 , m < j, we first define

∥C_{1}^{b_{1}}, …, C_{j−1}^{b_{j−1}}, C_{j}, C_{j+1} …, C_{n}; A ⊗ B∥_{i}

as

∑_{x_{ij0}=0,1} ∑_{x_{ij1}=0,1} f(x_{ij0}, x_{ij1}) · (∑_{b=0}^{1} x_{ijb} · ∥C_{1}^{b_{1}}, …, C_{j−1}^{b_{j−1}}, C_{j}^{b}, C_{j+1} …, C_{n}; A ⊗ B∥_{i+1})

and then for any choice b_{j_{1}} = … = b_{j_{l}} = 0 and b_{k_{1}} = … = b_{k_{r}} = 1 let

∥C_{1}^{b_{1}}, …, C_{n}^{b_{n}}; A ⊗ B∥_{i} = ∥C_{j_{1}}, …, C_{j_{l}}, A∥_{i+1} · ∥C_{k_{1}}, …, C_{k_{r}}, B∥_{i+1} .

We also let

∥Γ; A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B∥_{i} = ∥Γ, A, B∥_{i+1} ,

∥Γ; A_{1} ⊕ A_{2}∥_{i} = ∑_{t_{i1}=0,1} ∑_{t_{i2}=0,1} f(t_{i1}, t_{i2}) · (∑_{k=1}^{2} t_{ik} · ∥Γ, A_{k}∥_{i+1}) ,

∥Γ; A&B∥_{i} = ∏_{y_{i}=0,1}(1 − y_{i} + ∥Γ, A∥_{i+1})(y_{i} + ∥Γ, B∥_{i+1}) .

Proposition 5.2 ∥Γ∥_{i} ≥ 0 for any integer i and mall sequent Γ.

Lemma 5.3 For any integer i:

1. ∥A_{1}, A_{2}, …, A_{n}∥_{i} > 0 iff there exists j, 1 ≤ j ≤ n such that ∥A_{1}, …, A_{j−1}, A_{j+1}, …, A_{n}; A_{j}∥_{i+1} > 0.

2. ∥Γ; A ⊗ B∥_{i} > 0 iff there exists Δ, Θ such that Δ ⊎ Θ = Γ, ∥Δ, A∥_{i+n} > 0 and ∥Θ, B∥_{i+n} > 0, where n is the number of formulas in Γ.

3. ∥Γ; A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B∥_{i} > 0 iff ∥Γ, A, B∥_{i+1} > 0.

4. ∥Γ; A ⊕ B∥_{i} > 0 iff ∥Γ, A∥_{i+1} > 0 or ∥Γ, B∥_{i+1} > 0.

5. ∥Γ; A&B∥_{i} > 0 iff ∥Γ, A∥_{i+1} > 0 and ∥Γ, B∥_{i+1} > 0.

6. If a sequent Ξ consists entirely of literals, then ∥Ξ∥_{i} > 0 iff Ξ is an axiom.

Lemma 5.4 ⊢ Γ is provable in mall iff there exists an integer i such that ∥Γ∥_{i} > 0.

Proposition 5.5 ∥Γ∥_{i} > 0 implies that for all integers m, ∥Γ∥_{i+m} > 0.

Note that

Proposition 5.6 For any mall sequent Γ, the length of the expression ∥Γ∥_{0} (i.e., the number of symbols in the expression ∥Γ∥_{0}) is polynomial in the length of the sequent Γ.

For any (potentially open) subexpression Φ of ∥Γ∥_{0} let ν(Φ) be the maximal value of Φ under all possible 0, 1 substitutions. Because

ν( ∑_{x_{i}=0,1} Φ) ≤ 2ν(Φ)

and

ν( ∏_{x_{i}=0,1} Φ) ≤ ν(Φ)^{2},

one obtains as in [Sha92] (Theorem 3) that

Lemma 5.7 Let Γ be a mall sequent and let n be the length of the associated expression ∥Γ∥_{0}. Then the value of ∥Γ∥_{0} cannot exceed O(2^{2^{n}}).

As in [Sha92] (Theorem 4), such large bounds can be reduced modulo some smaller prime p. Indeed, let k be the length of a mall sequent Γ, let n be the length of the associated expression ∥Γ∥_{0} , and let the integer value of ∥Γ∥_{0} be ≠ 0. If this value is zero modulo all polynomial size primes, then by the Chinese remainder theorem it is zero modulo their product as well. But this product is much too big in comparison with the bound O(2^{2^{n}}) just given in Lemma 5.7 : Chebyshev function ϑ(x) = ln ∏_{p≤x} p is asymptotic to x by the prime number theorem and thus it suffices to consider x = 2^{n^{d}} for any constant d. Therefore the value of ∥Γ∥_{0} must be ≠ 0 modulo some prime p of length polynomial in n and hence in k by Proposition 5.6. Thus

Theorem 5.8 (Arithmetization) There exist a polynomial P such that for any mall sequent Γ of length k, ⊢ Γ is provable in mall iff ∥Γ∥_{0} ≠ 0 mod p for some prime p of length at most P(k).

6 Further research

Arithmetic semantics presented in Section 5 represents work in progress toward a complete semantics of mall based on “interactive proof systems” (ip) [BM88, GMR89]. In particular, we hope to relate mall to random evaluation protocols for polynomial expressions [Sha92, She92].

The semantic framework for mall discussed in this extended abstract might be just one instance of a broader relationship between linear logic and interactive protocols based on randomization. Indeed, interactive proof systems with two independent provers (mip) are known to be nexptimecomplete [BFL91]. On the other hand, the first order analog of mall, the multiplicative-additive fragment of first order linear logic mall1 is also nexptime-complete [LS94a, LS94b], thus the possibility of a direct relationship between mall1 and mip. The most satisfactory perspective would offer a single semantic framework for linear logic based on randomized interaction, which would have as instances the characterizations mll = np [Kan92, LW92], mall = ip ( =pspace), mall1 = mip ( =nexptime), and the undecidability of full linear logic [LMSS92].

References

[AJ94] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Accepted for publication in Journal of Symbolic Logic, 1994.

[AJM93] S. Abramsky, R. Jagadeesan, and P. Malacaria. Games and full abstraction for PCF. Manuscript, July 1993.

[BFL91] L. Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational Complexity, 1:3–40, 1991.

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

[BM88] 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.

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

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

[HO93] J.M.E. Hyland and L. Ong. Dialogue games and innocent strategies: an approach to intensional full abstraction for PCF. Manuscript, July 1993.

[Kan92] M. Kanovich. Horn programming in linear logic is NP-complete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 200– 210. IEEE Computer Society Press, Los Alamitos, California, June 1992. Full paper to appear in Annals of Pure and Applied Logic.

[LMSS92] 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.

[LS94a] P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIMEhard. Accepted for publication in Theoretical Computer Science, 1994. Available by anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/mall1.dvi.Z.

[LS94b] P. Lincoln and N. Shankar. Proof search in first order linear logic and other cut free sequent calculi. In Proc. 9-th Annual IEEE Symposium on Logic in Computer Science, Paris, July 1994.

[LW92] P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Manuscript, September 1992. Available using anonymous ftp from host ftp.csl.sri.com and the file pub/lincoln/comult-npc.dvi.

[Pap85] C. Papadimitriou. Games against Nature. J. Computer System Sciences, 31:288–301, 1985.

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

[Sce93] 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.

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

[She92] A. Shen. IP = PSPACE: Simplified Proof. J. ACM, 39:878–880, 1992.