The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract reduction systems. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps.
In this paper we investigate how the size of the label set influences the strength of the technique. Surprisingly, we find that two labels suffice for proving confluence of every confluent, countable system. In contrast, for proving commutation of rewrite relations, it turns out that the strength of the technique increases with more labels.
While decreasing diagrams is complete for proving confluence of countable systems, the technique is not complete for commutation. In our paper De Bruijn's Weak Diamond Property Revisited we give a counterexample to the completeness of decreasing diagrams for commutation.
} } @article{confluence:weak:diamond:2013, author = {J\"{o}rg Endrullis and Jan Willem Klop}, title = {{De Bruijn’s Weak Diamond Property Revisited}}, journal = {Indagationes Mathematicae}, volume = {24}, number = {4}, pages = {1050 -- 1072}, year = {2013}, note = {In memory of N.G. (Dick) de Bruijn (1918–2012)}, keywords = {rewriting, confluence}, type = {journal}, } @article{equal:mu:terms:2011, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Jan Willem Klop and Vincent van~Oostrom}, title = {{On Equal $\mu$-Terms}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3175--3202}, year = {2011}, doi = {10.1016/j.tcs.2011.04.011}, keywords = {rewriting}, type = {journal}, } @article{productivity:termination:2011, author = {J\"{o}rg Endrullis and Dimitri Hendriks}, title = {{Lazy Productivity via Termination}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3203--3225}, year = {2011}, doi = {10.1016/j.tcs.2011.03.024}, keywords = {rewriting, infinitary rewriting, productivity, termination}, type = {journal}, } @inproceedings{productivity:data:oblivious:2008, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks}, title = {{Data-Oblivious Stream Productivity}}, booktitle = {Proc.\ Conf.\ on Logic for Programming Artificial Intelligence and Reasoning (LPAR~2008)}, number = {5330}, pages = {79--96}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-540-89439-1\_6}, keywords = {rewriting, infinitary rewriting, productivity}, type = {conference}, } @article{productivity:streams:2010, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Ariya Isihara and Jan Willem Klop}, title = {{Productivity of Stream Definitions}}, journal = {Theoretical Computer Science}, volume = {411}, number = {4-5}, pages = {765--782}, year = {2010}, doi = {10.1016/j.tcs.2009.10.014}, keywords = {rewriting, infinitary rewriting, productivity}, type = {journal}, } @inproceedings{productivity:streams:2007, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Ariya Isihara and Jan Willem Klop}, title = {{Productivity of Stream Definitions}}, booktitle = {Proc.\ Symp.\ on Fundamentals of Computation Theory (FCT~2007)}, number = {4639}, pages = {274--287}, publisher = {Springer}, series = {LNCS}, year = {2007}, doi = {10.1007/978-3-540-74240-1\_24}, keywords = {rewriting, infinitary rewriting, productivity}, type = {conference}, } @inproceedings{bounded:expected:delay:2010, author = {Rena Bakhshi and J\"{o}rg Endrullis and Wan Fokkink and Jun Pang}, title = {{Brief Announcement: Asynchronous Bounded Expected Delay Networks}}, booktitle = {Proc.\ Symp.\ on Principles of Distributed Computing (PODC~2010)}, pages = {392--393}, publisher = {{ACM}}, year = {2010}, doi = {10.1145/1835698.1835787}, keywords = {protocols}, type = {conference}, } @article{bounded:expected:delay:2011, author = {Rena Bakhshi and J\"{o}rg Endrullis and Wan Fokkink and Jun Pang}, title = {{Fast Leader Election in Anonymous Rings with Bounded Expected Delay}}, journal = {Information Processing Letters}, volume = {111}, number = {17}, pages = {864--870}, year = {2011}, doi = {10.1016/j.ipl.2011.06.003}, keywords = {protocols}, type = {journal}, } @inproceedings{logic:most:2015, author = {J\"{o}rg Endrullis and Lawrence S. Moss}, title = {{Syllogistic Logic with "Most"}}, booktitle = {Proc.\ Int.\ Workshop on Logic, Language, Information, and Computation (WoLLIC~2015)}, volume = {9160}, pages = {124--139}, publisher = {Springer}, series = {LNCS}, year = {2015}, doi = {10.1007/978-3-662-47709-0\_10}, keywords = {logic}, type = {conference}, } @inproceedings{regularity:reflecting:2015, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks}, title = {{Regularity Preserving but Not Reflecting Encodings}}, booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2015)}, pages = {535--546}, publisher = {{IEEE} Computer Society}, year = {2015}, doi = {10.1109/LICS.2015.56}, keywords = {automata}, type = {conference}, } @inproceedings{automata:undecidability:2017, author = {J\"{o}rg Endrullis and Jeffrey Shallit and Tim Smith}, title = {{Undecidability and Finite Automata}}, booktitle = {Proc.\ Conf.\ Developments in Language Theory (DLT~2017)}, volume = {10396}, pages = {160--172}, publisher = {Springer}, series = {LNCS}, year = {2017}, doi = {10.1007/978-3-319-62809-7\_11}, keywords = {automata, undecidability}, type = {conference}, abstract = {Using a novel rewriting problem, we show that several natural decision problems about finite automata are undecidable. In contrast, we also prove three related problems are decidable.
We apply one result to prove the undecidability of a related problem about k-automatic sets of rational numbers.
} } @inproceedings{meanfield:2010, author = {Rena Bakhshi and J\"{o}rg Endrullis and Stefan Endrullis and Wan Fokkink and Boudewijn R. Haverkort}, title = {{Automating the Mean-Field Method for Large Dynamic Gossip Networks}}, booktitle = {Proc.\ Conf.\ on Quantitative Evaluation of Systems (QEST~2010)}, pages = {241--250}, publisher = {{{IEEE} Computer Society}}, year = {2010}, doi = {10.1109/QEST.2010.38}, keywords = {protocols}, type = {conference}, } @article{termination:local:2010, author = {J\"{o}rg Endrullis and Roel C. de~Vrijer and Johannes Waldmann}, title = {{Local Termination: Theory and Practice}}, journal = {Logical Methods in Computer Science}, volume = {6}, number = {3}, year = {2010}, keywords = {rewriting, termination, automata}, type = {journal}, } @inproceedings{termination:matrix:2006, author = {J\"{o}rg Endrullis and Johannes Waldmann and Hans Zantema}, title = {{Matrix Interpretations for Proving Termination of Term Rewriting}}, booktitle = {Proc.\ Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2006)}, volume = {4130}, pages = {574--588}, publisher = {Springer}, series = {LNCS}, year = {2006}, doi = {10.1007/11814771\_47}, keywords = {rewriting, termination}, type = {conference}, } @inproceedings{termination:automata:2015, author = {J\"{o}rg Endrullis and Hans Zantema}, title = {{Proving Non-termination by Finite Automata}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)}, volume = {36}, pages = {160--176}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2015}, doi = {10.4230/LIPIcs.RTA.2015.160}, keywords = {rewriting, termination, automata}, type = {conference}, } @article{termination:matrix:2008, author = {J\"{o}rg Endrullis and Johannes Waldmann and Hans Zantema}, title = {{Matrix Interpretations for Proving Termination of Term Rewriting}}, journal = {Journal of Automated Reasoning}, volume = {40}, number = {2-3}, pages = {195--220}, year = {2008}, doi = {10.1007/s10817-007-9087-9}, keywords = {rewriting, termination}, type = {journal}, } @inproceedings{termination:outermost:2009, author = {J\"{o}rg Endrullis and Dimitri Hendriks}, title = {{From Outermost to Context-Sensitive Rewriting}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)}, volume = {5595}, pages = {305--319}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-02348-4\_22}, keywords = {rewriting, termination}, type = {conference}, } @inproceedings{termination:matchbounds:2006, author = {J\"{o}rg Endrullis and Dieter Hofbauer and Johannes Waldmann}, title = {{Decomposing Terminating Rewrite Relations}}, booktitle = {Proc.\ Workshop on Termination (WST~2006)}, pages = {39--43}, year = {2006}, keywords = {rewriting, termination}, type = {workshop}, abstract = {In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:
One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm. Roughly speaking, the Böhm tree of a lambda term is its infinite normal form. If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible. But what if their Böhm trees coincide? For example, all fixed-point combinators have the same Böhm tree, namely \[ \lambda x. x(x(x(\ldots))) \]
We refine Böhm trees with a clock that records how many head reduction steps have been used to rewrite each subterm to head normal form. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.
We refer to Discriminating Lambda-Terms Using Clocked Boehm Trees (LMCS 2014) for an extended journal version of this paper. In the extended version we improve the precision of the clocks to atomic clocks and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
} } @inproceedings{lambda:reduction:under:substitution:2008, author = {J\"{o}rg Endrullis and Roel C. de~Vrijer}, title = {{Reduction under Substitution}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2008)}, volume = {5117}, pages = {425--440}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-540-70590-1\_29}, keywords = {rewriting, lambda calculus}, type = {conference}, } @inproceedings{lambda:clocks:functional:programs:2013, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop and Andrew Polonsky}, title = {{Clocks for Functional Programs}}, booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday}, pages = {97--126}, year = {2013}, doi = {10.1007/978-3-642-40355-2\_8}, series = {LNCS}, volume = {8106}, publisher = {Springer}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal}, abstract = {The contribution of this paper is twofold.
First, we derive a complete characterization of all simply-typed fixed-point combinator (fpc) generators using Barendregt's Inhabitation Machines. A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is. The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator. For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]
Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
} } @article{lambda:clocks:2014, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop and Andrew Polonsky}, title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2}, year = {2014}, doi = {10.2168/LMCS-10(2:4)2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal}, abstract = {As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.
Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.
To prove such beta-inconvertibilities, we refine the concept of Böhm trees: we introduce clocked Böhm trees's with annotations that convey information of the tempo in which the Böhm trees are produced. Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms. An analogous approach pertains to Levy-Longo trees and Berarducci trees.
We illustrate applicability of our refined Böhm trees at the following examples:
This paper is an extended version of Modular Construction of Fixed Point Combinators and Clocked Böhm Trees (LICS 2010).
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
} } @article{clocked:lambda:calculus:2017, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop and Andrew Polonsky}, title = {{Clocked Lambda Calculus}}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {5}, pages = {782--806}, year = {2017}, doi = {10.1017/S0960129515000389}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal}, abstract = {We introduce the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call clocked Böhm trees. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
} } @article{streams:forever:2013, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop}, title = {{Streams are Forever}}, journal = {Bulletin of the {EATCS}}, volume = {109}, pages = {70--106}, year = {2013}, keywords = {streams, degrees, automata}, type = {journal}, } @inproceedings{streams:degrees:polynomials:2016, author = {J\"{o}rg Endrullis and Juhani Karhum{\"{a}}ki and Jan Willem Klop and Aleksi Saarela}, title = {{Degrees of Infinite Words, Polynomials and Atoms}}, booktitle = {Proc.\ Conf.\ on Developments in Language Theory (DLT~2016)}, volume = {9840}, pages = {164--176}, publisher = {Springer}, series = {LNCS}, year = {2016}, doi = {10.1007/978-3-662-53132-7\_14}, keywords = {streams, degrees, automata}, type = {conference}, abstract = {A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.
While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.
In this paper we show that that techniques from continuous mathematics can be used to reason about finite state transducers. To be precise, we use the following methods from linear algebra and analysis:
The main result in this paper is the existance of an infinite number of atoms in the hierarchy of streams arising from finite state transduction.
See research for an introduction to finite state transducers, an overview of my research and many open questions.
} } @inproceedings{streams:degrees:transducibility:2015, author = {J\"{o}rg Endrullis and Jan Willem Klop and Aleksi Saarela and Markus A. Whiteland}, title = {{Degrees of Transducibility}}, booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)}, volume = {9304}, pages = {1--13}, publisher = {Springer}, series = {LNCS}, year = {2015}, doi = {10.1007/978-3-319-23660-5\_1}, keywords = {streams, degrees, automata}, type = {conference}, } @article{streams:degrees:2011, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop}, title = {{Degrees of Streams}}, journal = {Journal of Integers}, volume = {11B}, number = {A6}, pages = {1--40}, year = {2011}, note = {Proceedings of the Leiden Numeration Conference 2010}, keywords = {streams, degrees, automata}, type = {journal}, } @inproceedings{streams:eigenvalues:2014, author = {David Sprunger and William Tune and J\"{o}rg Endrullis and Lawrence S. Moss}, title = {{Eigenvalues and Transduction of Morphic Sequences}}, booktitle = {Proc.\ Conf.\ on Developments in Language Theory (DLT~2014)}, volume = {8633}, pages = {239--251}, publisher = {Springer}, series = {LNCS}, year = {2014}, doi = {10.1007/978-3-319-09698-8\_21}, keywords = {streams}, type = {conference}, } @inproceedings{streams:mix:automatic:2013, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks}, title = {{Mix-Automatic Sequences}}, booktitle = {Proc.\ Conf.\ on Language and Automata Theory and Applications (LATA~2013)}, volume = {7810}, pages = {262--274}, publisher = {Springer}, series = {LNCS}, year = {2013}, doi = {10.1007/978-3-642-37064-9\_24}, keywords = {streams, automata}, type = {conference}, } @inproceedings{streams:periodically:iterated:morphisms:2014, author = {J\"{o}rg Endrullis and Dimitri Hendriks}, title = {{On Periodically Iterated Morphisms}}, booktitle = {Joint Meeting and the Conference on Computer Science Logic (CSL) and the Symposium on Logic in Computer Science (LICS)}, pages = {39:1--39:10}, publisher = {{ACM}}, year = {2014}, doi = {10.1145/2603088.2603152}, keywords = {streams}, type = {conference}, } @inproceedings{streams:equality:2011, author = {Hans Zantema and J\"{o}rg Endrullis}, title = {{Proving Equality of Streams Automatically}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2011)}, volume = {10}, pages = {393--408}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.RTA.2011.393}, keywords = {rewriting, infinitary rewriting, streams}, type = {conference}, } @inproceedings{streams:degrees:squares:2015, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Hans Zantema}, title = {{The Degree of Squares is an Atom}}, booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)}, volume = {9304}, pages = {109--121}, publisher = {Springer}, series = {LNCS}, year = {2015}, doi = {10.1007/978-3-319-23660-5\_10}, keywords = {streams, degrees, automata}, type = {conference}, abstract = {A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.
While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.
In this paper we show that the degree of the stream \[ \prod_{i = 0}^\infty 1\, 0^{i^2} = 1 \, 0^0 \, 1 \, 0^1 \, 1 \, 0^4 \, 1 \, 0^9 \, 1 \, 0^{16} \, \cdots = 1101000010000000001 \cdots \] is an atom in the hierarchy of streams arising from finite state transduction.
In the paper Degrees of Infinite Words, Polynomials and Atoms we vastly generalise this result by showing that there is precisely one atom for each polynomial degree. See research for an introduction to finite state transducers, an overview of my research and many open questions.
} } @inproceedings{streams:zip:2012, author = {Clemens Grabmayer and J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop and Lawrence S. Moss}, title = {{Automatic Sequences and Zip-Specifications}}, booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2012)}, pages = {335--344}, publisher = {{IEEE} Computer Society}, year = {2012}, doi = {10.1109/LICS.2012.44}, keywords = {rewriting, streams}, type = {conference}, } @inproceedings{infinitary:normalization:2009, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Jan Willem Klop and Roel C. de~Vrijer}, title = {{Proving Infinitary Normalization}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2008)}, volume = {5497}, pages = {64--82}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-642-02444-3\_5}, keywords = {rewriting, infinitary rewriting}, type = {conference}, } @inproceedings{infinitary:weakly:orthogonal:unique:normal:forms:2010, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Jan Willem Klop and Vincent van~Oostrom}, title = {{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2010)}, volume = {6}, pages = {85--102}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2010}, doi = {10.4230/LIPIcs.RTA.2010.85}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {conference}, } @article{infinitary:weakly:orthogonal:2014, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Jan Willem Klop and Vincent van~Oostrom}, title = {{Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2:7}, pages = {1--33}, year = {2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal}, } @article{infinitary:highlights::2012, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Jan Willem Klop}, title = {{Highlights in Infinitary Rewriting and Lambda Calculus}}, journal = {Theoretical Computer Science}, volume = {464}, pages = {48--71}, year = {2012}, doi = {10.1016/j.tcs.2012.08.018}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal}, } @article{infintary:rewriting:coinductive:2018, author = {J\"{o}rg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva}, title = {{Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic}}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {1}, year = {2018}, doi = {10.23638/LMCS-14(1:3)2018}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {journal}, abstract = {We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.
The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework suitable for formalizations in theorem provers. To wit, we provide the first formalization of the compression lemma in Coq.
This paper is an extended version of A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (RTA 2015). We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).
} } @inproceedings{infintary:rewriting:coinductive:2015, author = {J\"{o}rg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva}, title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA 2015)}, volume = {36}, pages = {143--159}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2015}, doi = {10.4230/LIPIcs.RTA.2015.143}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference}, abstract = {We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.
The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework suitable for formalizations in theorem provers.
We refer to Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic (LMCS 2018) for an extended journal version of this paper.
We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).
} } @inproceedings{infintary:lambda:coinductive:2011, author = {J\"{o}rg Endrullis and Andrew Polonsky}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2012)}, volume = {19}, pages = {16--27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.TYPES.2011.16}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference}, abstract = {We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types.
The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.
The papers
extend the idea in this paper to reductions of length beyond omega.The extension to reduction lengths beyond omega requires mixing of induction and coinduction. Therefore the simpler setup presented in the current paper (Infinitary Rewriting Coinductively) is preferrable whenever there is no need for reductions longer than omega. This concerns for instance rewrite systems having the compression property, such as lambda calculus and left-linear term rewriting systems (with finite left-hand sides).
} } @inproceedings{circular:coinduction:2013, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Martin Bodin}, title = {{Circular Coinduction in Coq Using Bisimulation-Up-To Techniques}}, booktitle = {Proc.\ Conf.\ on Interactive Theorem Proving (ITP~2013)}, volume = {7998}, pages = {354--369}, publisher = {Springer}, series = {LNCS}, year = {2013}, doi = {10.1007/978-3-642-39634-2\_26}, keywords = {rewriting, coinduction, formal verification}, type = {conference}, } @article{rewriting:undecidability:levels:2011, author = {J\"{o}rg Endrullis and Herman Geuvers and Jakob Grue Simonsen and Hans Zantema}, title = {{Levels of Undecidability in Rewriting}}, journal = {Information and Computation}, volume = {209}, number = {2}, pages = {227--245}, year = {2011}, doi = {10.1016/j.ic.2010.09.003}, keywords = {rewriting, undecidability, termination, confluence}, type = {journal}, abstract = {Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.
In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.
Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.
This paper is an extended version of Degrees of Undecidability in Term Rewriting (CSL 2009).
} } @article{complexity:stream:equality:2014, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu}, title = {{On the Complexity of Stream Equality}}, journal = {Journal of Functional Programming}, volume = {24}, number = {2-3}, pages = {166--217}, year = {2014}, doi = {10.1017/S0956796813000324}, keywords = {rewriting, undecidability, streams}, type = {journal}, } @inproceedings{complexity:stream:equality:2012, author = {J\"{o}rg Endrullis and Dimitri Hendriks and Rena Bakhshi}, title = {{On the Complexity of Equivalence of Specifications of Infinite Objects}}, booktitle = {Proc.\ Int.\ Conf.\ on Functional Programming (ICFP~2012)}, pages = {153--164}, publisher = {{ACM}}, year = {2012}, doi = {10.1145/2364527.2364551}, keywords = {rewriting, undecidability, streams}, type = {conference}, } @inproceedings{complexity:productivity:2009, author = {J\"{o}rg Endrullis and Clemens Grabmayer and Dimitri Hendriks}, title = {{Complexity of Fractran and Productivity}}, booktitle = {Proc.\ Conf.\ on Automated Deduction (CADE~2009)}, volume = {5663}, pages = {371--387}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-02959-2\_28}, keywords = {rewriting, undecidability, productivity}, type = {conference}, } @inproceedings{rewriting:undecidability:degrees:2009, author = {J\"{o}rg Endrullis and Herman Geuvers and Hans Zantema}, title = {{Degrees of Undecidability in Term Rewriting}}, booktitle = {Proc.\ Conf.\ on Computer Science Logic (CSL~2009)}, volume = {5771}, pages = {255--270}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-04027-6\_20}, keywords = {rewriting, undecidability, termination, confluence}, type = {conference}, abstract = {Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.
In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.
Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.
We refer to Levels of Undecidability in Rewriting (Information and Computation 2011) for an extended journal version of this paper.
} }