11 Search Results for "Simonsen, Jakob Grue"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.16
The Agafonov and Schnorr-Stimm Theorems for Probabilistic Automata

Authors: Laurent Bienvenu, Hugo Gimbert, and Subin Pulari

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
For a fixed alphabet A, an infinite sequence X is said to be normal if every word w over A appears in X with the same frequency as any other word of the same length. A classical result of Agafonov (1966) relates normality to finite automata as follows: a sequence X is normal if and only if any subsequence of X selected by a finite automaton is itself normal. Another theorem of Schnorr and Stimm (1972) gives an alternative characterization: a sequence X is normal if and only if no gambler can win large amounts of money by betting on the sequence X using a strategy that can be described by a finite automaton. Both of these theorems are established in the setting of deterministic finite automata. This raises the question as to whether they can be extended to the setting of probabilistic finite automata. In the case of the Agafonov theorem, a partial positive answer was given by Léchine et al. (MFCS 2024) in a restricted case of probabilistic automata with rational transition probabilities. In this paper, we settle the full conjecture by proving that both the Agafonov and the Schnorr-Stimm theorems hold true for arbitrary probabilistic automata. Specifically, we show that a sequence X is normal if and only if any probabilistic automaton selects a normal subsequence of X with probability 1 and also show that a sequence X is normal if and only if any probabilistic finite-state gambler fails to win on X with probability 1.
Cite as

Laurent Bienvenu, Hugo Gimbert, and Subin Pulari. The Agafonov and Schnorr-Stimm Theorems for Probabilistic Automata. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bienvenu_et_al:LIPIcs.FSTTCS.2025.16,
  author =	{Bienvenu, Laurent and Gimbert, Hugo and Pulari, Subin},
  title =	{{The Agafonov and Schnorr-Stimm Theorems for Probabilistic Automata}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{16:1--16:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.16},
  URN =		{urn:nbn:de:0030-drops-250978},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.16},
  annote =	{Keywords: Normality, Agafonov theorem, probabilistic automata}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.67
Agafonov’s Theorem for Probabilistic Selectors

Authors: Ulysse Léchine, Thomas Seiller, and Jakob Grue Simonsen

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
A normal sequence over {0,1} is an infinite sequence for which every word of length k appears with frequency 2^{-k}. Agafonov’s eponymous theorem states that selection by a finite state selector preserves normality, i.e. if α is a normal sequence and A is a finite state selector, then the subsequence A(α) is either finite or a normal sequence. In this work, we address the following question: does this result hold when considering probabilistic selectors? We provide a partial positive answer, in the case where the probabilities involved are rational. More formally, we prove that given a normal sequence α and a rational probabilistic selector P, the selected subsequence P(α) will be a normal sequence with probability 1.
Cite as

Ulysse Léchine, Thomas Seiller, and Jakob Grue Simonsen. Agafonov’s Theorem for Probabilistic Selectors. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lechine_et_al:LIPIcs.MFCS.2024.67,
  author =	{L\'{e}chine, Ulysse and Seiller, Thomas and Simonsen, Jakob Grue},
  title =	{{Agafonov’s Theorem for Probabilistic Selectors}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{67:1--67:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.67},
  URN =		{urn:nbn:de:0030-drops-206238},
  doi =		{10.4230/LIPIcs.MFCS.2024.67},
  annote =	{Keywords: Normal sequences, probabilistic automata, Agafonov’s theorem}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.5
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
DOI: 10.4230/LIPIcs.ICALP.2016.133
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
DOI: 10.4230/LIPIcs.FSCD.2016.23
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
DOI: 10.4230/LIPIcs.RTA.2012.53
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
DOI: 10.4230/LIPIcs.CSL.2011.481
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
DOI: 10.4230/LIPIcs.RTA.2011.61
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
DOI: 10.4230/LIPIcs.RTA.2010.17
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
DOI: 10.4230/LIPIcs.RTA.2010.311
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 Type
  • 11 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2024
  • 1 2021
  • 2 2016
  • 1 2012
  • Show More...

  • Refine by Author
  • 8 Simonsen, Jakob Grue
  • 1 Andersen, Soren Bjerg
  • 1 Appel, Claus
  • 1 Bienvenu, Laurent
  • 1 Cerda, Rémy
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Computability
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Grammars and context-free languages
  • Show More...

  • Refine by Keyword
  • 2 probabilistic automata
  • 2 term rewriting
  • 1 Agafonov theorem
  • 1 Agafonov’s theorem
  • 1 Böhm trees
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact