Cited By
View all- Seiller TPellissier LLéchine U(2024)Unifying lower bounds for algebraic machines, semanticallyInformation and Computation10.1016/j.ic.2024.105232301(105232)Online publication date: Dec-2024
Interaction Graphs: Non-Deterministic Automata
Article No.: 21, Pages 1 - 24
Abstract
This article exhibits a series of semantic characterisations of sublinear nondeterministic complexity classes. These results fall into the general domain of logic-based approaches to complexity theory and so-called implicit computational complexity (icc), i.e., descriptions of complexity classes without reference to specific machine models. In particular, it relates strongly to icc results based on linear logic, since the semantic framework considered stems from work on the latter. Moreover, the obtained characterisations are of a geometric nature: each class is characterised by a specific action of a group by measure-preserving maps.
References
[1]
Clément Aubert, Marc Bagnol, Paolo Pistone, and Thomas Seiller. 2014. Logic programming and logarithmic space. In Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS’14) (Lecture Notes in Computer Science), Jacques Garrigue (Ed.), Vol. 8858. Springer, 39--57.
[2]
Clément Aubert, Marc Bagnol, and Thomas Seiller. 2016. Unary resolution: Characterizing Ptime. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FOSSACS’16).
[3]
Clément Aubert and Thomas Seiller. 2016a. Characterizing co-NL by a group action. Math. Struct. Comput. Sci. 26, 4 (2016), 606--638.
[4]
Clément Aubert and Thomas Seiller. 2016b. Logarithmic space and permutations. Info. Comput. 248 (2016), 2--21.
[5]
Patrick Baillot. 2011. Elementary linear logic revisited for polynomial time and an exponential time hierarchy. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS’11) (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 7078. Springer, 337--352.
[6]
Theodore Baker, John Gill, and Robert Solovay. 1975. Relativizations of the question. SIAM J. Comput. 4, 4 (1975), 431--442.
[7]
Stephen Bellantoni and Stephen Cook. 1992. A new recursion-theoretic characterization of the polytime functions. Comput. Complex. 2 (1992). Retrieved from
[8]
Stephen A. Cook. 1971. Characterizations of pushdown machines in terms of time-bounded computers. J. ACM 18, 1 (Jan. 1971), 4--18.
[9]
Vincent Danos and Jean-Baptiste Joinet. 2003. Linear logic 8 elementary time. Info. Comput. 183, 1 (2003), 123--137.
[10]
Damien Gaboriau. 2000. Coût des relations d’équivalence et des groupes. Inventiones Mathematicae 139 (2000), 41--98.
[11]
Jean-Yves Girard. 1987. Linear logic. Theor. Comput. Sci. 50, 1 (1987), 1--101.
[12]
Jean-Yves Girard. 2011. Geometry of interaction : Logic in the hyperfinite factor.Theor. Comput. Sci. 412 (2011), 1860--1883.
[13]
Jean-Yves Girard. 2012. Normativity in logic. In Epistemology versus Ontology, Peter Dybjer, Sten Lindström, Erik Palmgren, and Göran Sundholm (Eds.). Logic, Epistemology, and the Unity of Science, Vol. 27. Springer, 243--263.
[14]
Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci. 97, 1 (April 1992), 1--66.
[15]
Martin Hyland and Andrea Schalk. 2003. Gluing and orthogonality for models of linear logic. Theor. Comput. Sci. 294 (2003).
[16]
D. Leivant and J.-Y. Marion. 1993. Lambda calculus characterizations of poly-time. Fundam. Info. 19 (1993).
[17]
Daniel Leivant and Jean-Yves Marion. 1994. Ramified recurrence and computational complexity II: Substitution and poly-space. Lecture Notes Comput. Sci. 933 (1994).
[18]
Buckhard Monien. 1976. Transformational methods and their application to complexity problems. Acta Informatica 6 (1976), 95--108.
[19]
Alberto Naibo, Mattia Petrolo, and Thomas Seiller. 2016. On the computational meaning of axioms. In Epistemology, Knowledge and the Impact of Interaction. Springer, 141--184.
[20]
A. A. Razborov and S. Rudich. 1997. Natural proofs. J. Comput. Syst. Sci. 55 (1997).
[21]
Thomas Seiller. 2012a. Interaction graphs: Multiplicatives. Ann. Pure Appl. Logic 163 (Dec. 2012), 1808--1837.
[22]
Thomas Seiller. 2012b. Logique Dans Le Facteur Hyperfini : Géometrie De L’interaction Et Complexité. Ph.D. Dissertation. Université Aix-Marseille. Retrieved from http://tel.archives-ouvertes.fr/tel-00768403/.
[23]
Thomas Seiller. 2015a. Measurable preorders and complexity. In Proceedings of the Topology, Algebra and Categories in Logic Conference.
[24]
Thomas Seiller. 2015b. Towards a Complexity-through-Realizability Theory. Retrieved from http://arxiv.org/pdf/1502.01257.
[25]
Thomas Seiller. 2016a. Interaction graphs: Additives. Ann. Pure Appl. Logic 167 (2016), 95--154.
[26]
Thomas Seiller. 2016b. Interaction graphs: Full linear logic. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’16). ACM, New York, NY, USA, 427--436.
[27]
Thomas Seiller. 2017a. Interaction graphs: Exponentials. Submitted. Retrieved from http://arxiv.org/pdf/1312.1094.
[28]
Thomas Seiller. 2017b. Interaction graphs: Graphings. Ann. Pure Appl. Logic 168, 2 (2017), 278--320.
[29]
Thomas Seiller. 2018. A correspondence between maximal Abelian sub-algebras and linear logic fragments. Math. Struct. Comput. Sci. 28, 1 (2018), 77--139.
Index Terms
- Interaction Graphs: Non-Deterministic Automata
Recommendations
Interaction Graphs: Full Linear Logic
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceInteraction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all Geometry of Interaction (GoI) constructions introduced so far. This series of work was inspired from Girard's hyperfinite GoI, and ...
Realizability models and implicit complexity
New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced ...
Light logics and optimal reduction: Completeness and complexity
Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2018
269 pages
Copyright © 2018 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 August 2018
Accepted: 01 May 2018
Revised: 01 October 2017
Received: 01 September 2016
Published in TOCL Volume 19, Issue 3
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed
Funding Sources
- European Commision's Marie Sklodowska-Curie Individual Fellowship (H2020-MSCA-IF-2014)
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 104Total Downloads
- Downloads (Last 12 months)7
- Downloads (Last 6 weeks)0
Reflects downloads up to 30 Nov 2024
Other Metrics
Citations
Cited By
View all- Seiller TPellissier LLéchine U(2024)Unifying lower bounds for algebraic machines, semanticallyInformation and Computation10.1016/j.ic.2024.105232301(105232)Online publication date: Dec-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in