Abstract
The relationship between Boolean proof nets of multiplicative linear logic ( APN ) and Boolean circuits has been studied [Ter04] in a non-uniform setting. We refine this results by taking care of uniformity: the relationship can be expressed in term of the (Turing) polynomial hierarchy. We give a proofs-as-programs correspondence between proof nets and deterministic as well as non-deterministic Boolean circuits with a uniform depth-preserving simulation of each other. The Boolean proof nets class m &BN (poly ) is built on multiplicative and additive linear logic with a polynomial amount of additive connectives as the non-deterministic circuit class NNC (poly) is with non-deterministic variables. We obtain uniform-APN = NC and m & BN (poly ) = NNC (poly)= NP.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allender, E.W.: P-uniform circuit complexity. Journal of the Association for Computing Machinery 36(4), 912–928 (1989)
Barrington, D.A.M., Immerman, N., Straubing, H.: On uniformity within NC1. J. of Comput. and System Science 41(3), 274–306 (1990)
Boppana, R.B., Sipser, M.: The complexity of finite functions. MIT Press, Cambridge (1990)
Cook, S., Krajicek, J.: Consequences of the provability of NP⊆P/poly (2006)
Danos, V.: La logique linéaire appliquée à l’étude de divers processus de normalisation (et principalement du λ-calcul). PhD thesis, Univ. Paris VII (1990)
Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28(3), 181–203 (1989)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–102 (1987)
Hughes, D.J.D., van Glabbeek, R.J.: Proof nets for unit-free multiplicative-additive linear logic. In: Proc. IEEE Logic in Comput. Sci. (2003)
Hughes, D.J.D., van Glabbeek, R.J.: Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. on Comput. Logic (2005)
Karp, R., Lipton, R.: Some connections between nonuniform and uniform complexity classes. In: Proc. 12th ACM Symp. on Theory of Computing, pp. 302–309 (1980)
Laurent, O., Tortora de Falco, L.: Slicing polarized additive normalization. In: Linear Logic in Computer Science (2004)
Mairson, H., Terui, K.: On the computational complexity of cut-elimination in linear logic. Theoretical Computer Science 2841, 23–36 (2003)
Ruzzo, W.: On uniform circuit complexity. J. of Computer and System Science 21, 365–383 (1981)
Terui, K.: Proof nets and boolean circuits. In: Proc. IEEE Logic in Comput. Sci., pp. 182–191 (2004)
Tortora De Falco, L.: Additives of linear logic and normalization - part i: a (restricted) church-rosser property. T.C.S. 294(3), 489–524 (2003)
Venkateswaran, H.: Circuit definitions of nondeterministic complexity classes. Siam J. Comput. 21(4), 655–670 (1992)
Vollmer, H.: Introduction to Circuit Complexity – A Uniform Approach. Texts in Theoretical Computer Science. Springer, Heidelberg (1999)
Wolf, M.J.: Nondeterministic circuits, space complexity and quasigroups. Theoretical Computer Science 125(2), 295–313 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Mogbil, V., Rahli, V. (2007). Uniform Circuits, & Boolean Proof Nets. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-72734-7_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72732-3
Online ISBN: 978-3-540-72734-7
eBook Packages: Computer ScienceComputer Science (R0)