Hostname: page-component-7b7567c8c-mnklg Total loading time: 0 Render date: 2026-11-12T09:38:16.274Z Has data issue: false hasContentIssue false
  • English
  • Français

Linear Logic Proof Games and Optimization

Published online by Cambridge University Press:  15 January 2014

Patrick D. Lincoln,
John C. Mitchell and
Andre Scedrov
Patrick D. Lincoln
Affiliation:
Sri International Computer Science Laboratory, Menlo Park CA 94025, USA. E-mail: lincoln@csl.sri.com
John C. Mitchell
Affiliation:
Department of Computer Science, Stanford University, Stanford, CA 94305-9045, USA. E-mail: mitchell@cs.stanford.edu, http://theory.stanford.edu/people/jcm/home.html
Andre Scedrov
Affiliation:
Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395, USA. E-mail: scedrov@cis.upenn.edu, http://www.cis.upenn.edu/~scedrov
Get accessRights & Permissions [Opens in a new window]

Extract

§ 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 polynomial-time 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 canalsobeextended to PSPACE [10, 9], using a game that alternates between two players instead of a proof presented by a “single player.”

Information

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 2 , Issue 3 , September 1996, pp. 322 - 338
Copyright
Copyright © Association for Symbolic Logic 1996

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

REFERENCES

[1] Abramsky, S. and Jagadeesan, R., Games andfull completeness for multiplicative linear logic, this JOURNAL, vol. 59 (1994), pp. 543–574.Google Scholar
[2] Abramsky, S., Jagadeesan, R., and Malacarla, P., Full abstraction for PCF (extended abstract), Proceedings of the TACS '94, Springer LNCS, vol. 789, 1994, pp. 1–15.Google Scholar
[3] Arora, S., 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.Google Scholar
[4] Arora, S. and Lund, C., Hardness of approximations, Approximation algorithms for NP-hardproblems, PWS Publishing, 1996.Google Scholar
[5] Arora, S., Lund, C., Motwani, R., Sudan, M., and Szegedy, M., Proof verification and hardness of approximation problems, Proceedings of the 33-rd Annual IEEE Symposium on Foundations ofComputer Science, IEEE Computer Society Press, Los Alamitos, California, 1992, pp. 14–23.CrossRefGoogle Scholar
[6] Arora, S. and Safra, S., Probabilistic checking ofproofs; a new characterization of NP, Proceedings of the 33-rd Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press, Los Alamitos, California, 1992, pp. 2–13.CrossRefGoogle Scholar
[7] Babai, L. and Moran, S., Arthur-Merlin games: a randomized proof system, and a hierarchy of complexity classes, Journal of Computer and System Sciences, vol. 36 (1988), pp. 254–276.CrossRefGoogle Scholar
[8] Blass, A., A game semantics for linear logic, Annals of Pure and Applied Logic, vol. 56 (1992), pp. 183–220.CrossRefGoogle Scholar
[9] Condon, A., Feigenbaum, J., Lund, C., and Shor, P., Random debaters and the hardness ofapproximating stochastic functions, Proceedings of the 9-th Annual IEEE Conference on Structure in Complexity Theory, IEEE Computer Society Press, Los Alamitos, California, 1994, pp. 280–293, full version to appear in SIAM Journal on Computing .CrossRefGoogle Scholar
[10] Condon, A., Feigenbaum, J., Lund, C., and Shor, P., Probabilistically checkable debate systems and nonapproximability of PSPACE-hard functions, Chicago Journal of Theoretical Computer Science (1995), no. 4, http://www.cs.chicago.edu/publications/cjtcs/articles/1995/4/contents.html, extended abstract in Proceedings of the 25-th ACM Symposium on Theory of Computing, ACM , New York, 1993, pp. 305–314.CrossRefGoogle Scholar
[11] Danos, V., Herbelin, H., and Regnier, L., Game semantics and abstract machines, Proceedings of the 11-th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, 07 1996.Google Scholar
[12] Feige, U., Goldwasser, S., Lovasz, L., Safra, S., and Szegedy, M., Approximating clique is almost NP-complete, Proceedings of the 32-nd Annual IEEE Symposium on Foundations of Computer Science (Los Alamitos, California), IEEE Computer Society Press, 1991, pp. 2–12.Google Scholar
[13] Garey, M. R. and Johnson, D. S., Computers and intractability: A guide to the theory of NP-completeness, W. H. Freeman and Co., 1979.Google Scholar
[14] Girard, J. Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[15] Girard, J. Y., Linear logic: its syntax and semantics, Advances in linear logic (Girard, J. Y., Lafont, Y., and Regnier, L., editors), London Mathematical Society Lecture Note Series, vol. 222, 1995.CrossRefGoogle Scholar
[16] Goldwasser, S., Micali, S., and Rackoff, C., The knowledge complexity of interactive proof systems, SIAM Journal on Computing, vol. 18 (1989), pp. 186–208.CrossRefGoogle Scholar
[17] Hyland, J. M. E. and Ong, C. H. L., Pi-calculus, dialogue games and PCF, Proceedings of the 7th ACM Conference on Functional Programming Languages and Computer Architecture, ACM Press, 1995, pp. 96–107.Google Scholar
[18] Hunt, H. B. III, Marathe, M. V., and Stearns, R. E., Generalized CNF satisfiability problems and non-efficient approximability, Proceedings of the 9-th Annual IEEE Conference on Structure in Complexity Theory, IEEE Computer Society Press, Los Alamitos, California, 1994, pp. 356–366.CrossRefGoogle Scholar
[19] Joyal, A., Free lattices, communication, andmoney games, to appear in Proceedings of the 10-th international congress of logic, methodology, and philosophy of science, Firenze.Google Scholar
[20] Lamarche, F., Games semantics for full propositional linear logic, Proceedings of the 10-th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, 06 1995, pp. 464–473.Google Scholar
[21] Lincoln, P. D., Mitchell, J., Scedrov, A., and Shankar, N., Decision problems for propositional linear logic, Annals of Pure and Applied Logic, vol. 56 (1992), pp. 239–311, extended abstract in Proceedings of the 31-st Annual IEEE Symposium on Foundations of Computer Science , 1990, pp. 662–671.CrossRefGoogle Scholar
[22] Lincoln, P. D., Mitchell, J. C., and Scedrov, A., Stochastic interaction and linear logic, Advances in linear logic (Girard, J. Y, Lafont, Y., and Regnier, L., editors), London Mathematical Society Lecture Notes, vol. 222, Cambridge University Press, 1995, pp. 147–166.CrossRefGoogle Scholar
[23] Lincoln, P. D., Linear logic proof games and optimization, Preliminary report, 01 1996, available by anonymous ftp from ftp.cis.upenn.edu as pub/papers/scedrov/approx.[dvi,ps].Z.Google Scholar
[24] Lincoln, P. D., The complexity of local proof search in linear logic, extended abstract, Proceedings linear logic '96, Tokyo meeting, Electronic Notes in Theoretical Computer Science, 1996, to appear, p. http://www.elsevier.nl:80/mcs/tcs/pc/Menu.html.Google Scholar
[25] Lund, C., Fortnow, L., Karloff, H., and Nisan, N., Algebraic methods for interactive proof systems, Journal of the ACM, vol. 39 (1992), pp. 859–868.CrossRefGoogle Scholar
[26] Motwani, R. and Raghavan, P., Randomized algorithms, Cambridge University Press, 1995.CrossRefGoogle Scholar
[27] Papadimitriou, C., Computational complexity, Addison-Wesley, 1994.Google Scholar
[28] Scedrov, A., A brief guide to linear logic, Current trends in theoretical computer science (Rozenberg, G. and Salomaa, A., editors), World Scientific Publishing Co., 1993, pp. 377–394.CrossRefGoogle Scholar
[29] Scedrov, A., Linear logic and computation: A survey, Proof and computation, proceedings Marktoberdorf summer school 1993 (Schwichtenberg, H., editor), vol. 139, NATO Advanced Science Institutes, Series F, Springer-Verlag, Berlin, 1995, pp. 379–395.Google Scholar
[30] Shamir, A., IP = PSPACE, Journal of the ACM, vol. 39 (1992), pp. 869–877.CrossRefGoogle Scholar
[31] Sudan, M., 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.CrossRefGoogle Scholar