Hostname: page-component-78c5997874-lj6df Total loading time: 0 Render date: 2024-11-20T00:34:42.524Z Has data issue: false hasContentIssue false
  • English
  • Français

GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION

Published online by Cambridge University Press:  19 June 2017

FEDERICO ASCHIERI
FEDERICO ASCHIERI*
Affiliation:
INSTITUT FÜR DISKRETE MATHEMATIK UND GEOMETRIE TECHNISCHE UNIVERSITÄT WIEN WIEDNER HAUPTSTRAßE 8-10/104, 1040 VIENNA, AUSTRIAE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

F.4.1Hyland–Ong Coquand game semanticsfirst-order logicboundsstrategy interactionscut-eliminationnormalization
Type
Articles
Information
The Journal of Symbolic Logic , Volume 82 , Issue 2 , June 2017 , pp. 672 - 708
Copyright
Copyright © The Association for Symbolic Logic 2017 

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.)

References

REFERENCES

Abramsky, S., Jagaadesan, R., and Malacaria, P., Full abstraction for PCF . Information and Computation, vol. 163 (2000), no. 2, pp. 409–470.CrossRefGoogle Scholar
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.Google Scholar
Aschieri, F., Constructive forcing, CPS translations and witness extraction in interactive realizability . Mathematical Structures in Computer Science, 2015. doi:10.1017/S0960129515000468.Google Scholar
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.CrossRefGoogle Scholar
Aschieri, F. and Berardi, S., Interactive learning-based realizability for Heyting arithmetic with EM1 . Logical Methods in Computer Science, vol. 6 (2010), no. 3.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Beckmann, A., Exact bounds for lengths of reductions in typed lambda-calculus , this Journal, vol. 66 (2001), no. 3, pp. 1277–1285.Google Scholar
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.CrossRefGoogle Scholar
Berardi, S. and de’Liguoro, U., Knowledge spaces and the completeness of learning strategies . Logical Methods in Computer Science, vol. 10 (2014), no. 1.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Clairambault, P., Bounding linear head reduction and visible interaction through skeletons . Logical Methods in Computer Science, vol. 11 (2015), no. 2.Google Scholar
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.Google Scholar
Coquand, T., A semantics of evidence for classical arithmetic , this Journal, vol. 60 (1995), no. 1, pp. 325–337.Google Scholar
Curien, P.-L. and Herbelin, H., The Duality of Computation , Proceedings of ICFP ’00, ACM, New York, 2000, pp. 233–243.Google Scholar
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.Google Scholar
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.Google Scholar
Gold, E. M., Language identification in the limit . Information and Control, vol. 10 (1967), no. 5, pp. 447–474.CrossRefGoogle Scholar
Heijltjes, W., Classical proof forestry . Annals of Pure and Applied Logic, vol. 161 (2010), no. 11, pp. 1346–1366.CrossRefGoogle Scholar
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é Paris 7, 1995.Google Scholar
Hetzl, S. and Weller, D., Expansion trees with cut, preprint, 2013, arXiv:1308.0429.Google Scholar
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.CrossRefGoogle Scholar
Jain, S. and Sharma, A., Mind change complexity of learning logic programs . Theoretical Computer Science, vol. 284 (2002), no. 1, pp. 143–160.CrossRefGoogle Scholar
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.Google Scholar
Kreisel, G., On weak completeness of intuitionistic predicate logic , this Journal, vol. 27 (1962), no. 2, pp. 139–158.Google Scholar
Miller, D., A compact representation of proofs. Studia Logica, vol. 46 (1987), no. 4, pp. 347–370.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Troesltra, A. and Schwichtenberg, H., Basic Proof Theory, Tracts in Theoretical Computer Science, vol. 43, Cambridge University Press, Cambridge, 2000.Google Scholar
Wadler, P., Propositions as types . Communications of the ACM, vol. 58 (2015), no. 12, pp. 75–84.CrossRefGoogle Scholar