1: %\documentclass[10pt,twocolumn]{article}
2: \documentclass[10pt]{article}
3:
4: \input{environment}
5:
6:
7: \renewcommand{\topfraction}{1}
8: \renewcommand{\bottomfraction}{1}
9: \renewcommand{\textfraction}{.10}
10: \renewcommand{\floatpagefraction}{.70}
11: \renewcommand{\dbltopfraction}{.95}
12: \renewcommand{\dblfloatpagefraction}{.95}
13: \setcounter{topnumber}{9}
14: \setcounter{bottomnumber}{9}
15: \setcounter{totalnumber}{20}
16: \setcounter{dbltopnumber}{9}
17:
18: \raggedbottom
19: \setlength{\parindent}{0cm}
20: \begin{document}
21: \title{Context Semantics, Linear Logic and Computational Complexity\thanks{The
22: author is partially supported by PRIN project
23: FOLLIA (2004) and ANR project NOCOST (2005).}}
24: \author{Ugo Dal Lago\\
25: {\it Laboratoire d'Informatique de Paris-Nord}\\
26: {\it Universit\'e Paris 13, France}\\
27: \texttt{dallago@lipn.univ-paris13.fr}}
28: \maketitle
29: \begin{abstract}
30: We show that context semantics can be fruitfully applied
31: to the quantitative analysis of proof normalization
32: in linear logic. In particular, context semantics lets us
33: define the \emph{weight} of a proof-net as a measure of
34: its inherent complexity: it is both an upper bound
35: to normalization time (modulo a polynomial overhead,
36: independently on the reduction strategy) and a lower
37: bound to the number of steps to
38: normal form (for certain reduction strategies). Weights are
39: then exploited in proving strong soundness theorems
40: for various subsystems of linear logic, namely elementary
41: linear logic, soft linear logic and light linear logic.
42: \end{abstract}
43: \input{introduction}
44: \input{syntax}
45: \input{soundness}
46: \input{subsystems}
47: \input{conclusions}
48:
49: \bibliographystyle{latex8}
50:
51: \begin{thebibliography}{10}\setlength{\itemsep}{-1ex}\small
52:
53: \bibitem{Asperti98book}
54: A.~Asperti and S.~Guerrini.
55: \newblock {\em The optimal implementation of functional programming languages}.
56: \newblock Cambridge University Press, 1998.
57:
58: \bibitem{Asperti02tocl}
59: A.~Asperti and L.~Roversi.
60: \newblock Intuitionistic light affine logic.
61: \newblock {\em ACM Transactions on Computational Logic}, 3(1):137--175, 2002.
62:
63: \bibitem{baillot01fi}
64: P.~Baillot and M.~Pedicini.
65: \newblock Elementary complexity and geometry of interaction.
66: \newblock {\em Fundamenta Informaticae}, 45(1-2):1--31, 2001.
67:
68: \bibitem{dallago05lics}
69: U.~Dal~Lago.
70: \newblock The geometry of linear higher-order recursion.
71: \newblock In {\em Proc. 20th Annual Symposium on Logic in Computer Science},
72: pages 366--375. IEEE Computer Society, 2005.
73:
74: \bibitem{Dallago06lics}
75: U.~Dal~Lago.
76: \newblock Context semantics, linear logic and computational complexity.
77: \newblock In {\em Proc. 21st Annual Symposium on Logic in Computer Science},
78: pages 169--178. IEEE Computer Society, 2006.
79:
80: \bibitem{Danos03ic}
81: V.~Danos and J.-B. Joinet.
82: \newblock Linear logic and elementary time.
83: \newblock {\em Information and Computation}, 183(1):123--137, 2003.
84:
85: \bibitem{danos95advances}
86: V.~Danos and L.~Regnier.
87: \newblock Proof-nets and {H}ilbert space.
88: \newblock In J.-Y. Girard, Y.~Lafont, and L.~Regnier, editors, {\em Advances in
89: Linear Logic}, pages 307--328. Cambridge University Press, 1995.
90:
91: \bibitem{Danos99tcs}
92: V.~Danos and L.~Regnier.
93: \newblock Reversible, irreversible and optimal lambda-machines.
94: \newblock {\em Theoretical Computer Science}, 227(1-2):79--97, 1999.
95:
96: \bibitem{Girard88cl}
97: J.-Y. Girard.
98: \newblock Geometry of interaction 2: deadlock-free algorithms.
99: \newblock In {\em Proc. Conference on Computer Logic}, volume 417 of {\em
100: LNCS}, pages 76--93, 1988.
101:
102: \bibitem{Girard89lc}
103: J.-Y. Girard.
104: \newblock Geometry of interaction 1: interpretation of system {F}.
105: \newblock In {\em Proc. Logic Colloquium '88}, pages 221--260, 1989.
106:
107: \bibitem{Girard95pn}
108: J.-Y. Girard.
109: \newblock Proof-nets: the parallel syntax for proof-theory.
110: \newblock In A.~Ursini and P.~Agliano, editors, {\em Logic and Algebra}, volume
111: 180 of {\em Lecture Notes in Pure and Applied Mathematics}, pages 97--124.
112: Marcel Dekker, New York, 1995.
113:
114: \bibitem{Girard98ic}
115: J.-Y. Girard.
116: \newblock Light linear logic.
117: \newblock {\em Information and Computation}, 143(2):175--204, 1998.
118:
119: \bibitem{Girard92tcs}
120: J.-Y. Girard, A.~Scedrov, and P.~J. Scott.
121: \newblock Bounded linear logic: A modular approach to polynomial-time
122: computability.
123: \newblock {\em Theoretical Computer Science}, 97(1):1--66, 1992.
124:
125: \bibitem{Gonthier92popl}
126: G.~Gonthier, M.~Abadi, and J.-J. L\'evy.
127: \newblock The geometry of optimal lambda reduction.
128: \newblock In {\em Proc. 12th ACM Symposium on Principles of Programming
129: Languages}, pages 15--26, 1992.
130:
131: \bibitem{Gonthier92lics}
132: G.~Gonthier, M.~Abadi, and J.-J. L\'evy.
133: \newblock Linear logic without boxes.
134: \newblock In {\em Proc. 7th Annual Symposium on Logic in Computer Science},
135: pages 223--234, 1992.
136:
137: \bibitem{Lafont04tcs}
138: Y.~Lafont.
139: \newblock Soft linear logic and polynomial time.
140: \newblock {\em Theoretical Computer Science}, 318:163--180, 2004.
141:
142: \bibitem{Mackie95popl}
143: I.~Mackie.
144: \newblock The geometry of interaction machine.
145: \newblock In {\em Proc. 22nd ACM Symposium on Principles of Programming
146: Languages}, pages 198--208, 1995.
147:
148: \bibitem{Pinto01tlca}
149: J.~S. Pinto.
150: \newblock Parallel implementation models for the lambda-calculus using the
151: geometry of interaction.
152: \newblock In {\em Proc. 5th International Conference on Typed Lambda Calculi
153: and Applications}, pages 385--399, 2001.
154:
155: \bibitem{Terui01lics}
156: K.~Terui.
157: \newblock Light affine lambda calculus and polytime strong normalization.
158: \newblock In {\em Proc. of 16th Annual IEEE Symposium on Logic in Computer
159: Science}, pages 209--220, 2001.
160:
161: \bibitem{Terui04lics}
162: K.~Terui.
163: \newblock Proof nets and boolean circuits.
164: \newblock In {\em Proc. 7th Annual Symposium on Logic in Computer Science},
165: pages 182--191, 2004.
166:
167: \end{thebibliography}
168:
169: %\bibliography{csll}
170: %\input{appendix}
171: \end{document}
172: