×

zbMATH — the first resource for mathematics

Game semantics and the geometry of backtracking: a new complexity analysis of interaction. (English) Zbl 1401.03100
Author’s abstract: We present abstract complexity results about Coquand and Hyland-Ong game semantics, that will lead to new bounds on the length of first-order cut-elimination, normalization, interaction between expansion trees and any other dialogical process game semantics can model and apply to. In particular, we provide a novel method to bound the length of interactions between visible strategies and to measure precisely the tower of exponentials defining the worst-case complexity. Our study improves the old estimates on average by several exponentials.

MSC:
03F20 Complexity of proofs
03B70 Logic in computer science
03F05 Cut-elimination and normal-form theorems
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Abramsky, S., Jagaadesan, R., and Malacaria, P., Full abstraction for PCF. Information and Computation, vol. 163 (2000), no. 2, pp. 409-470. doi:10.1006/inco.2000.2930 · Zbl 1006.68028
[2] Abramsky, S. and Mccusker, G., Game semantics, Logic and Computation (Schwichtenberg, H. and Berger, U., editors), Proceedings of the 1997 Marktoberdorf Summer School, Springer-Verlag, Heidelberg, 1998.
[3] Aschieri, F., Constructive forcing, CPS translations and witness extraction in interactive realizability. Mathematical Structures in Computer Science, 2015. doi:10.1017/S0960129515000468. · Zbl 06781941
[4] Aschieri, F., Learning based realizability for HA + EM1 and 1-backtracking games: Soundness and completeness. Annals of Pure and Applied Logic, vol. 164 (2013), no. 6, pp. 591-671. doi:10.1016/j.apal.2012.05.002 · Zbl 1270.03117
[5] Aschieri, F. and Berardi, S., Interactive learning-based realizability for Heyting arithmetic with EM1. Logical Methods in Computer Science, vol. 6 (2010), no. 3. · Zbl 1201.03052
[6] Aschieri, F. and Zorzi, M., A “Game Semantical” Intuitionistic Realizability Validating Markov’s Principle, Proceedings of TYPES 2013, vol. 26, LIPIcs, 2014, pp. 24-44. · Zbl 1359.03044
[7] Aschieri, F. and Zorzi, M., On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand’s Theorem. Theoretical Computer Science, vol. 625 (2016), pp. 125-146. doi:10.1016/j.tcs.2016.02.028 · Zbl 1377.03050
[8] Beckmann, A., Exact bounds for lengths of reductions in typed lambda-calculus, this Journal, vol. 66 (2001), no. 3, pp. 1277-1285. · Zbl 1159.03305
[9] Berardi, S. and De’Liguoro, U., Toward the interpretation of non-constructive reasoning as non-monotonic learning. Information and Computation, vol. 207 (2009), no. 1, pp. 63-81. doi:10.1016/j.ic.2008.10.003 · Zbl 1169.68022
[10] Berardi, S. and De’Liguoro, U., Knowledge spaces and the completeness of learning strategies. Logical Methods in Computer Science, vol. 10 (2014), no. 1. · Zbl 1326.68167
[11] Berardi, S., Coquand, T., and Hayashi, S., Games with 1-backtracking. Annals of Pure and Applied Logic, vol. 161 (2010), no. 10, pp. 1256-1269. · Zbl 1241.03006
[12] Clairambault, P., Estimation of the Length of Interactions in Arena Game Semantics, Proceedings of FOSSACS 2011, vol. 6604, Lecture Notes in Computer Science, Springer, 2011. · Zbl 1326.68069
[13] Clairambault, P., Bounding linear head reduction and visible interaction through skeletons. Logical Methods in Computer Science, vol. 11 (2015), no. 2. · Zbl 1391.68018
[14] Coquand, T., A Semantics of Evidence for Classical Arithmetic (Huet, G. and Jones, C., editors), Proceedings of the Second Workshop on Logical Frameworks 1991, 1991, pp. 87-99.
[15] Coquand, T., A semantics of evidence for classical arithmetic, this Journal, vol. 60 (1995), no. 1, pp. 325-337. · Zbl 0829.03037
[16] Curien, P.-L. and Herbelin, H., The Duality of Computation, Proceedings of ICFP ’00, ACM, New York, 2000, pp. 233-243. · Zbl 1321.68146
[17] Danos, V., Regnier, L., and Herbelin, H., Game Semantics & Abstract Machines, Proceedings of LICS 1996, IEEE Computer Society Press, Los Alamitos, 1996, pp. 394-495.
[18] Felscher, W., Dialogues as a foundation for intuitionistic logic, Handbook of Philosophical Logic, vol. 3 (Gabbay, D. and Guenthner, F., editor), Kluwer, Dordrecht, 2002, pp. 341-372. · Zbl 0875.03019
[19] Gold, E. M., Language identification in the limit. Information and Control, vol. 10 (1967), no. 5, pp. 447-474. doi:10.1016/S0019-9958(67)91165-5 · Zbl 0259.68032
[20] Heijltjes, W., Classical proof forestry. Annals of Pure and Applied Logic, vol. 161 (2010), no. 11, pp. 1346-1366. doi:10.1016/j.apal.2010.04.006 · Zbl 1223.03039
[21] Herbelin, H., Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes, Ph.D. thesis, Université Paris7, 1995.
[22] Hetzl, S. and Weller, D., Expansion trees with cut, preprint, 2013, arXiv:1308.0429.
[23] Hyland, M. and Ong, L., On Full abstraction for PCF: I, II and III. Information and Computation, vol. 163 (2000), no. 2, pp. 285-408. doi:10.1006/inco.2000.2917 · Zbl 1006.68027
[24] Jain, S. and Sharma, A., Mind change complexity of learning logic programs. Theoretical Computer Science, vol. 284 (2002), no. 1, pp. 143-160. doi:10.1016/S0304-3975(01)00084-6 · Zbl 0997.68064
[25] Krivine, J.-L., Classical realizability, Interactive Models of Computation and Program Behavior, Panoramas et synthèses, Société Mathématique de France, Paris, 2009, pp. 197-229.
[26] Kreisel, G., On weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), no. 2, pp. 139-158. · Zbl 0117.01005
[27] Miller, D., A compact representation of proofs. Studia Logica, vol. 46 (1987), no. 4, pp. 347-370. · Zbl 0644.03033
[28] Oliva, P. and Powell, T., A game-theoretic computational interpretation of proofs in classical analysis, Gentzen’s Centenary: The Quest for Consistency (Kahle, R. and Rathjen, M., editors), Springer, Heidelberg, 2015, pp. 501-531. · Zbl 1378.03046
[29] Parigot, M., Lambda-my-calculus: An algorithmic interpretation of classical natural deduction, LPAR 1992, vol. 624, Lecture Notes in Computer Science, Springer, 1992, pp. 190-201. · Zbl 0925.03092
[30] Troesltra, A. and Schwichtenberg, H., Basic Proof Theory, Tracts in Theoretical Computer Science, vol. 43, Cambridge University Press, Cambridge, 2000. · Zbl 0957.03053
[31] Wadler, P., Propositions as types. Communications of the ACM, vol. 58 (2015), no. 12, pp. 75-84. doi:10.1145/2699407
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.