8 Search Results for "Waldmann, Johannes"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.42
Degrees of Second and Higher-Order Polynomials

Authors: Donghyun Lim and Martin Ziegler

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

Abstract
Second-order polynomials generalize classical (=first-order) ones in allowing for additional variables that range over functions rather than values. We are motivated by their applications in higher-order computational complexity theory, extending for instance discrete classes (like P/FP or PSPACE/FPSPACE) to operators in Analysis [http://doi.org/10.1137/S0097539794263452], [http://doi.org/10.1145/2189778.2189780]. The degree subclassifies ordinary polynomial growth into linear, quadratic, cubic, etc. To similarly classify second-order polynomials, we (well-)define their degree by structural induction as an "arctic" first-order polynomial: a term/expression over integer variable D and operations + and ⋅ and binary max(). This generalized degree turns out to transform nicely under (now two kinds of) polynomial composition. As examples, we collect and determine the degrees of previous and new asymptotic analyses of algorithms and operators receiving function/oracle arguments. Then we motivate and introduce third-order polynomials and their degrees as arctic second-order polynomials, along with their transformations under three kinds of composition. Proceeding to fourth order and beyond yields a hierarchy, with characterization in Simply Typed Lambda Calculus.
Cite as

Donghyun Lim and Martin Ziegler. Degrees of Second and Higher-Order Polynomials. 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. 42:1-42:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lim_et_al:LIPIcs.FSTTCS.2025.42,
  author =	{Lim, Donghyun and Ziegler, Martin},
  title =	{{Degrees of Second and Higher-Order Polynomials}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{42:1--42:20},
  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.42},
  URN =		{urn:nbn:de:0030-drops-251225},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.42},
  annote =	{Keywords: Logic in Computer Science, Higher Order Program Analysis, Asymptotic Type Theory}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.76
Deciding Termination of Simple Randomized Loops

Authors: Éléanore Meyer and Jürgen Giesl

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program’s variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.
Cite as

Éléanore Meyer and Jürgen Giesl. Deciding Termination of Simple Randomized Loops. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 76:1-76:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.MFCS.2025.76,
  author =	{Meyer, \'{E}l\'{e}anore and Giesl, J\"{u}rgen},
  title =	{{Deciding Termination of Simple Randomized Loops}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{76:1--76:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.76},
  URN =		{urn:nbn:de:0030-drops-241833},
  doi =		{10.4230/LIPIcs.MFCS.2025.76},
  annote =	{Keywords: decision procedures, randomized programs, linear loops, positive almost sure termination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.6
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Authors: Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen

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

Abstract
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.
Cite as

Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2025.6,
  author =	{Ahrens, Emma and Kassing, Jan-Christoph and Giesl, J\"{u}rgen and Katoen, Joost-Pieter},
  title =	{{Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{6:1--6:21},
  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.6},
  URN =		{urn:nbn:de:0030-drops-236215},
  doi =		{10.4230/LIPIcs.FSCD.2025.6},
  annote =	{Keywords: Rewriting, Semirings, Semantics, Termination, Verification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.21
Sparse Tiling Through Overlap Closures for Termination of String Rewriting

Authors: Alfons Geser, Dieter Hofbauer, and Johannes Waldmann

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.
Cite as

Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Sparse Tiling Through Overlap Closures for Termination of String Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{geser_et_al:LIPIcs.FSCD.2019.21,
  author =	{Geser, Alfons and Hofbauer, Dieter and Waldmann, Johannes},
  title =	{{Sparse Tiling Through Overlap Closures for Termination of String Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.21},
  URN =		{urn:nbn:de:0030-drops-105282},
  doi =		{10.4230/LIPIcs.FSCD.2019.21},
  annote =	{Keywords: relative termination, semantic labeling, locally testable language, overlap closure}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.318
Matrix Interpretations on Polyhedral Domains

Authors: Johannes Waldmann

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds, and we discuss its relation with the usable rules criterion. We present an implementation and experiments.
Cite as

Johannes Waldmann. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 318-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{waldmann:LIPIcs.RTA.2015.318,
  author =	{Waldmann, Johannes},
  title =	{{Matrix Interpretations on Polyhedral Domains}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{318--333},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  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.RTA.2015.318},
  URN =		{urn:nbn:de:0030-drops-52059},
  doi =		{10.4230/LIPIcs.RTA.2015.318},
  annote =	{Keywords: termination of term rewriting, matrix interpretations, constraint programming, linear inequalities}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.97
Compression of Rewriting Systems for Termination Analysis

Authors: Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We adapt the TreeRePair tree compression algorithm and use it as an intermediate step in proving termination of term rewriting systems. We introduce a cost function that approximates the size of constraint systems that specify compatibility of matrix interpretations. We show how to integrate the compression algorithm with the Dependency Pairs transformation. Experiments show that compression reduces running times of constraint solvers, and thus improves the power of automated termination provers.
Cite as

Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann. Compression of Rewriting Systems for Termination Analysis. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 97-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bau_et_al:LIPIcs.RTA.2013.97,
  author =	{Bau, Alexander and Lohrey, Markus and N\"{o}th, Eric and Waldmann, Johannes},
  title =	{{Compression of Rewriting Systems for Termination Analysis}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{97--112},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.97},
  URN =		{urn:nbn:de:0030-drops-40561},
  doi =		{10.4230/LIPIcs.RTA.2013.97},
  annote =	{Keywords: termination of rewriting, matrix interpretations, constraint solving, tree compression}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.357
Polynomially Bounded Matrix Interpretations

Authors: Johannes Waldmann

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

Abstract
Matrix interpretations can be used to bound the derivational complexity of rewrite systems. We present a criterion that completely characterizes matrix interpretations that are polynomially bounded. It includes the method of upper triangular interpretations as a special case, and we prove that the inclusion is strict. The criterion can be expressed as a finite domain constraint system. It translates to a Boolean constraint system with a size that is polynomial in the dimension of the interpretation. We report on performance of an implementation.
Cite as

Johannes Waldmann. Polynomially Bounded Matrix Interpretations. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 357-372, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{waldmann:LIPIcs.RTA.2010.357,
  author =	{Waldmann, Johannes},
  title =	{{Polynomially Bounded Matrix Interpretations}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{357--372},
  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.357},
  URN =		{urn:nbn:de:0030-drops-26637},
  doi =		{10.4230/LIPIcs.RTA.2010.357},
  annote =	{Keywords: Derivational complexity of rewriting, matrix interpretation, weighted automata, ambiguity of automata, finite domain constraints}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1762
Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations

Authors: Georg Moser, Andreas Schnabl, and Johannes Waldmann

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
For a given (terminating) term rewriting system one can often estimate its \emph{derivational complexity} indirectly by looking at the proof method that established termination. In this spirit we investigate two instances of the interpretation method: \emph{matrix interpretations} and \emph{context dependent interpretations}. We introduce a subclass of matrix interpretations, denoted as \emph{triangular matrix interpretations}, which induce polynomial derivational complexity and establish tight correspondence results between a subclass of context dependent interpretations and restricted triangular matrix interpretations. The thus obtained new results are easy to implement and considerably extend the analytic power of existing results. We provide ample numerical data for assessing the viability of the method.
Cite as

Georg Moser, Andreas Schnabl, and Johannes Waldmann. Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 304-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{moser_et_al:LIPIcs.FSTTCS.2008.1762,
  author =	{Moser, Georg and Schnabl, Andreas and Waldmann, Johannes},
  title =	{{Complexity Analysis of Term Rewriting Based on  Matrix and Context Dependent Interpretations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{304--315},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1762},
  URN =		{urn:nbn:de:0030-drops-17626},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1762},
  annote =	{Keywords: Term Rewriting, Derivational Complexity, Termination, Automation}
}
  • Refine by Type
  • 8 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2019
  • 1 2015
  • 1 2013
  • 1 2010
  • Show More...

  • Refine by Author
  • 5 Waldmann, Johannes
  • 2 Giesl, Jürgen
  • 1 Ahrens, Emma
  • 1 Bau, Alexander
  • 1 Geser, Alfons
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Rewrite systems
  • 1 Mathematics of computing
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Termination
  • 2 matrix interpretations
  • 1 Asymptotic Type Theory
  • 1 Automation
  • 1 Derivational Complexity
  • 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