8 Search Results for "Simonsen, Jakob Grue"


Document
The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting

Authors: Jakob Grue Simonsen

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)


Abstract
We study the implicit computational complexity of constructor term rewriting systems where every function and constructor symbol is unary or nullary. Surprisingly, adding simple and natural constraints to rule formation yields classes of systems that accept exactly the four classes of languages in the Chomsky hierarchy.

Cite as

Jakob Grue Simonsen. The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{simonsen:LIPIcs.FSCD.2021.5,
  author =	{Simonsen, Jakob Grue},
  title =	{{The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.5},
  URN =		{urn:nbn:de:0030-drops-142439},
  doi =		{10.4230/LIPIcs.FSCD.2021.5},
  annote =	{Keywords: Constructor term rewriting, Chomsky Hierarchy, Implicit Complexity}
}
Document
Near Optimal Adjacency Labeling Schemes for Power-Law Graphs

Authors: Casper Petersen, Noy Rotbart, Jakob Grue Simonsen, and Christian Wulff-Nilsen

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
An adjacency labeling scheme labels the n nodes of a graph with bit strings in a way that allows, given the labels of two nodes, to determine adjacency based only on those bit strings. Though many graph families have been meticulously studied for this problem, a non-trivial labeling scheme for the important family of power-law graphs has yet to be obtained. This family is particularly useful for social and web networks as their underlying graphs are typically modelled as power-law graphs. Using simple strategies and a careful selection of a parameter, we show upper bounds for such labeling schemes of ~O(sqrt^{alpha}(n)) for power law graphs with coefficient alpha;, as well as nearly matching lower bounds. We also show two relaxations that allow for a label of logarithmic size, and extend the upper-bound technique to produce an improved distance labeling scheme for power-law graphs.

Cite as

Casper Petersen, Noy Rotbart, Jakob Grue Simonsen, and Christian Wulff-Nilsen. Near Optimal Adjacency Labeling Schemes for Power-Law Graphs. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 133:1-133:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{petersen_et_al:LIPIcs.ICALP.2016.133,
  author =	{Petersen, Casper and Rotbart, Noy and Simonsen, Jakob Grue and Wulff-Nilsen, Christian},
  title =	{{Near Optimal Adjacency Labeling Schemes for Power-Law Graphs}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{133:1--133:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.133},
  URN =		{urn:nbn:de:0030-drops-62684},
  doi =		{10.4230/LIPIcs.ICALP.2016.133},
  annote =	{Keywords: Labeling schemes, Power-law graphs}
}
Document
Complexity Hierarchies and Higher-Order Cons-Free Rewriting

Authors: Cynthia Kop and Jakob Grue Simonsen

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


Abstract
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes such as admitting product types or non-left-linear rules.

Cite as

Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2016.23,
  author =	{Kop, Cynthia and Grue Simonsen, Jakob},
  title =	{{Complexity Hierarchies and Higher-Order Cons-Free Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23},
  URN =		{urn:nbn:de:0030-drops-59972},
  doi =		{10.4230/LIPIcs.FSCD.2016.23},
  annote =	{Keywords: higher-order term rewriting, implicit complexity, cons-freeness, ETIME hierarchy}
}
Document
Term Rewriting Systems as Topological Dynamical Systems

Authors: Soren Bjerg Andersen and Jakob Grue Simonsen

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)


Abstract
Topological dynamics is, roughly, the study of phenomena related to iterations of continuous maps from a metric space to itself. We show how the rewrite relation in term rewriting gives rise to dynamical systems in two distinct, natural ways: (A) One in which any deterministic rewriting strategy induces a dynamical system on the set of finite and infinite terms endowed with the usual metric, and (B) one in which the unconstrained rewriting relation induces a dynamical system on sets of sets of terms, specifically the set of compact subsets of the set of finite and infinite terms endowed with the Hausdorff metric. For both approaches, we give sufficient criteria for the induced systems to be well-defined dynamical systems and for (A) we demonstrate how the classic topological invariant called topological entropy turns out to be much less useful in the setting of term rewriting systems than in symbolic dynamics.

Cite as

Soren Bjerg Andersen and Jakob Grue Simonsen. Term Rewriting Systems as Topological Dynamical Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 53-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{andersen_et_al:LIPIcs.RTA.2012.53,
  author =	{Andersen, Soren Bjerg and Simonsen, Jakob Grue},
  title =	{{Term Rewriting Systems as Topological Dynamical Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{53--68},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.53},
  URN =		{urn:nbn:de:0030-drops-34841},
  doi =		{10.4230/LIPIcs.RTA.2012.53},
  annote =	{Keywords: Term rewriting, dynamical systems, topology, symbolic dynamics}
}
Document
The Exact Hardness of Deciding Derivational and Runtime Complexity

Authors: Andreas Schnabl and Jakob Grue Simonsen

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)


Abstract
For any class C of computable total functions satisfying some mild conditions, we prove that the following decision problems are complete for the existential part of the second level of the arithmetical hierarchy: (A) Deciding whether a term rewriting system (TRS for short) has runtime complexity bounded by a function in C. (B) Deciding whether a TRS has derivational complexity bounded by a function in C. In particular, the problems of deciding whether a TRS has polynomially (exponentially) bounded runtime complexity (respectively derivational complexity) are complete for this level of the arithmetical ierarchy. This places deciding polynomial derivational or runtime complexity of TRSs at the same level as deciding nontermination or nonconfluence of TRSs. We proceed to show that the related problem of deciding for a single computable function f whether a TRS has runtime complexity bounded from above by f is complete for the universal part of the first level of the arithmetical hierarchy. We further prove that analysing the implicit complexity of TRSs is even more difficult: The problem of deciding whether a TRS accepts a language of terms accepted by some TRS with runtime complexity bounded by a function in C is complete for the existential part of the third level of the arithmetical hierarchy. All of our results are easily extended to the notion of minimal complexity (where the length of shortest reductions to normal form is considered) and remain valid under any computable reduction strategy. Finally, all results hold both for unrestricted TRSs and for the class of orthogonal TRSs.

Cite as

Andreas Schnabl and Jakob Grue Simonsen. The Exact Hardness of Deciding Derivational and Runtime Complexity. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 481-495, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{schnabl_et_al:LIPIcs.CSL.2011.481,
  author =	{Schnabl, Andreas and Simonsen, Jakob Grue},
  title =	{{The Exact Hardness of Deciding Derivational and Runtime Complexity}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{481--495},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.481},
  URN =		{urn:nbn:de:0030-drops-32516},
  doi =		{10.4230/LIPIcs.CSL.2011.481},
  annote =	{Keywords: term rewriting, derivational complexity, arithmetical hierarchy}
}
Document
Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus

Authors: Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)


Abstract
We present Anagopos, an open source tool for visualizing reduction graphs of terms in lambda calculus and term rewriting. Anagopos allows step-by-step generation of reduction graphs under six different graph drawing algorithms. We provide ample examples of graphs drawn with the tool.

Cite as

Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen. Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 61-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{grathwohl_et_al:LIPIcs.RTA.2011.61,
  author =	{Grathwohl, Niels Bj{\o}rn Bugge and Ketema, Jeroen and Pallesen, Jens Duelund and Simonsen, Jakob Grue},
  title =	{{Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{61--70},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.61},
  URN =		{urn:nbn:de:0030-drops-31286},
  doi =		{10.4230/LIPIcs.RTA.2011.61},
  annote =	{Keywords: term rewriting, lambda calculus, reduction graphs, visualization}
}
Document
Higher-Order (Non-)Modularity

Authors: Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)


Abstract
We show that, contrary to the situation in first-order term rewriting, almost none of the usual properties of rewriting are modular for higher-order rewriting, irrespective of the higher-order rewriting format. We show that for the particular format of simply typed applicative term rewriting systems modularity of confluence, normalization, and termination can be recovered by imposing suitable linearity constraints.

Cite as

Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen. Higher-Order (Non-)Modularity. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 17-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{appel_et_al:LIPIcs.RTA.2010.17,
  author =	{Appel, Claus and van Oostrom, Vincent and Simonsen, Jakob Grue},
  title =	{{Higher-Order (Non-)Modularity}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{17--32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.17},
  URN =		{urn:nbn:de:0030-drops-26427},
  doi =		{10.4230/LIPIcs.RTA.2010.17},
  annote =	{Keywords: Higher-order rewriting, modularity, termination, normalization}
}
Document
Weak Convergence and Uniform Normalization in Infinitary Rewriting

Authors: Jakob Grue Simonsen

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)


Abstract
We study infinitary term rewriting systems containing finitely many rules. For these, we show that if a weakly convergent reduction is not strongly convergent, it contains a term that reduces to itself in one step (but the step itself need not be part of the reduction). Using this result, we prove the starkly surprising result that for any orthogonal system with finitely many rules, the system is weakly normalizing under weak convergence if{f} it is strongly normalizing under weak convergence if{f} it is weakly normalizing under strong convergence if{f} it is strongly normalizing under strong convergence. As further corollaries, we derive a number of new results for weakly convergent rewriting: Systems with finitely many rules enjoy unique normal forms, and acyclic orthogonal systems are confluent. Our results suggest that it may be possible to recover some of the positive results for strongly convergent rewriting in the setting of weak convergence, if systems with finitely many rules are considered. Finally, we give a number of counterexamples showing failure of most of the results when infinite sets of rules are allowed.

Cite as

Jakob Grue Simonsen. Weak Convergence and Uniform Normalization in Infinitary Rewriting. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 311-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{simonsen:LIPIcs.RTA.2010.311,
  author =	{Simonsen, Jakob Grue},
  title =	{{Weak Convergence and Uniform Normalization in Infinitary Rewriting}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{311--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.311},
  URN =		{urn:nbn:de:0030-drops-26609},
  doi =		{10.4230/LIPIcs.RTA.2010.311},
  annote =	{Keywords: Infinitary rewriting, weak convergence, uniform normalization}
}
  • Refine by Author
  • 7 Simonsen, Jakob Grue
  • 1 Andersen, Soren Bjerg
  • 1 Appel, Claus
  • 1 Grathwohl, Niels Bjørn Bugge
  • 1 Grue Simonsen, Jakob
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Computability
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Grammars and context-free languages

  • Refine by Keyword
  • 2 term rewriting
  • 1 Chomsky Hierarchy
  • 1 Constructor term rewriting
  • 1 ETIME hierarchy
  • 1 Higher-order rewriting
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 2 2010
  • 2 2011
  • 2 2016
  • 1 2012
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail