Infinitary Combinatory Reduction Systems: Confluence (2009)
Ketema, Jeroen, Simonsen, Jakob Grue
We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fully-extended, orthogonal iCRSs are...
Abstract Vicious Circles in Rewriting Systems (2009)
Jeroen Ketema, Jan Willem Klop, Vincent Van Oostrom, Van Oostrom
We continue our study of the difference between Weak Normalisation (WN) and Strong Normalisation (SN). We extend our earlier result that orthogonal TRSs with the property WN do not admit cyclic...
Rewriting Transfinite Terms (2009)
Ketema, Jeroen, Blom, Stefan, Aoto, Takahito, Simonsen, Jakob Grue
We define rewriting over terms with positions of transfinite length.
Abstract Vicious Circles in Rewriting Systems (2008)
Jeroen Ketema, Jan Willem Klop, Vincent Van Oostrom, Van Oostrom
We continue our study of the difference between Weak Normalisation (WN) and Strong Normalisation (SN). We extend our earlier result that orthogonal TRSs with the property WN do not admit cyclic...
WRS 2004 Preliminary Version Some Undecidable Approximations of TRSs Abstract (2008)
In this paper we study the decidability of reachability, normalisation, and neededness in n-shallow and n-growing TRSs. In an n-growing TRS, a variable that occurs both on the left- and right-hand...
AFM5 Collected Scientific Publications: 2006 – 2007 References (2008)
Jeroen Ketema, Jakob Grue, Simonsen Infinitary Technical
[2] C. Kupke and Y. Venema. Coalgebraic fixed point logics have the finite model property. In
Abstract WRS 2004 Preliminary Version Vicious Circles in Orthogonal Term Rewriting Systems (2008)
Jeroen Ketema, Jan Willem Klop, Vincent Van Oostrom, Van Oostrom
In this paper we first study the difference between Weak Normalization (WN) and Strong Normalization (SN), in the framework of first order orthogonal rewriting systems. With the help of the Erasure...
Root Stabilisation Using Dependency Pairs (2008)
A dependency pair problem [1] is elegantly formulated as a relative termination problem [2]: For a TRS R = (Σ, R), does → DP(R) terminate relative to →R when the steps from → DP(R) occur as...
On Confluence of Infinitary Combinatory Reduction Systems (2008)
Jeroen Ketema, Jakob Grue Simonsen
Abstract. We prove that fully-extended, orthogonal infinitary combinatory reduction systems with finite right-hand sides are confluent modulo identification of hypercollapsing subterms. This provides...
Erasure and Termination in Higher-Order Rewriting (2008)
Jeroen Ketema, Femke Van Raamsdonk
Abstract. Two applications of the Erasure Lemma for first-order orthogonal term rewriting systems are: weak innermost termination implies termination, and weak normalization implies strong...
On Confluence of Infinitary Combinatory Reduction Systems (2008)
Jeroen Ketema, Jakob Grue Simonsen
Abstract. We prove that fully-extended, orthogonal infinitary combinatory reduction systems with finite right-hand sides are confluent modulo identification of hypercollapsing subterms. This provides...
Software ENgineering Vicious circles in rewriting systems (2004)
J. Ketema, J. W. Klop, V. Van Oostrom, Jeroen Ketema
CWI is the National Research Institute for Mathematics and Computer Science. It is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a founding member of ERCIM, the...
J. Ketema, J. W. Klop, V. Van Oostrom, Jeroen Ketema
Netherlands Organization for Scientific Research (NWO). CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented...