On the termination of Russel's description elimination algorithm (2009)
Grabmayer, Clemens, Leo, Joop, Oostrom, Vincent Van, Visser, Albert
In this paper we study the termination behaviour of Russell’s description elimination rewrite system. We discuss certain claims made by Saul Kripke in his paper.
Modularity of Confluence Constructed (2009)
Abstract. We present a novel proof of Toyama’s famous modularity of confluence result for term rewriting systems. Apart from being short and intuitive, the proof is modular itself in that it...
MODULARITY OF CONSTRUCTIVE CONFLUENCE (2009)
Abstract. We prove modularity of constructive confluence for term rewriting systems using a novel decomposition of terms into tall aliens and bases. The proof is modular itself in that it factors...
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...
Modularity of Confluence Constructed (2008)
Abstract. We present a novel proof of Toyama’s famous modularity of confluence result for term rewriting systems. Apart from being short and intuitive, the proof is modular itself in that it...
MODULARITY OF CONSTRUCTIVE CONFLUENCE (2008)
Abstract. We prove modularity of constructive confluence for term rewriting systems using a novel decomposition of terms into tall aliens and bases. The proof is modular itself in that it factors...
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...
Lambda Calculus with Patterns (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Abstract. In this paper we revisit the λ-calculus with patterns, originating from the practice of functional programming language design. We treat this feature in a framework ranging from pure...
Decreasing Diagrams Converted (2008)
Abstract. The decreasing diagrams technique is a complete method to reduce confluence of a rewrite relation to local confluence. Whereas previous presentations have focussed on the proof the...
Decomposition Orders another generalisation of the fundamental theorem of arithmetic (2008)
Bas Luttik, Vincent Van Oostrom
We discuss unique decomposition in partial commutative monoids. Inspired by a result from process theory, we propose the notion of decomposition order for partial commutative monoids, and prove that...
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...
Iterative Path Orders 1 Iterative Path Orders Extended abstract (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
In the first half of this paper we give an alternative version of the recursive path order (RPO) for first-order term rewriting, which is ‘iterative ’ rather than recursive. Hence the name...
Iterative Lexicographic Path Orders (2008)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Abstract. We relate Kamin and Lévy’s original presentation of lexicographic path orders (LPO), using an inductive definition, to a presentation, which we will refer to as iterative lexicographic...
V.: Confluence by decreasing diagrams, converted (2008)
Abstract. The decreasing diagrams technique is a complete method to reduce confluence of a rewrite relation to local confluence. Whereas previous presentations have focussed on the proof the...
Abstract. A fundamental result in rewriting is: E | = s ≈ t ⇐⇒1 E ⊢ s = t ⇐⇒2 s ↔ ∗ E t 1. is Birkhoff’s theorem expressing that semantic consequence (|=) coincides with syntactic...
Abstract. A fundamental result in rewriting is: E j = s t ()1 E ` s = t
Separability and Translatability of Sequential Term Rewrite Systems Into the Lambda Calculus (2007)
Sugwoo Byun Kyungsung, Sugwoo Byun, Richard Kennaway, Vincent Van Oostrom
this paper the question of which
Confluence by Developments and Development Closed Critical Pairs (2007)
In the absence of termination confluence of rewriting systems is often hard to establish. The class of orthogonal rewriting systems (rewriting systems where rules do not interfere with one another,...
Exercise 3.5.11.(vii) of [Bar84], displays two lambda terms (2007)
F12.67> (z is preserved by . 1. If ends in t, then since t contains only one , we must have that z j y and r j a((y:\Gamma\Gamma\Gamma, which cannot rewrite to s, 2. If ends in s, then since s...
A Geometric Proof of Confluence by Decreasing Diagrams (2007)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
Recently a new confluence criterion for confluence was found using decreasing diagrams, as a generalization of several wellknown confluence criteria in abstract rewriting such as the strong...
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems (2007)
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
We study perpetuality of reduction steps, as well as perpetuality of redexes, in orthogonal rewrite systems. A perpetual step is a reduction step which retains the possibility of infinite reductions....
Maarten Janssen, Paola Monachesi, Vincent Van Oostrom, Vincent Van Oostrom, Opleiding Cognitieve, Kunstmatige Intelligentie
1.1 Organisatie van het Vak............................. 1 1.2 Beoordeling van het Vak............................. 2 1.2.1 Opbouw naar de Presentatiedag.................... 2 1.3 Overzicht van de...
Maarten Janssen, Paola Monachesi, Vincent Van Oostrom, Vincent Van Oostrom, Opleiding Cognitieve, Kunstmatige Intelligentie, ...
1.1 Organisatie van het Vak............................. 1 1.2 Beoordeling van het Vak............................. 2 1.2.1 Opbouw naar de Presentatiedag.................... 2 1.3 Overzicht van de...
An Easy Expansion Exercise (2007)
Vincent Van Oostrom, Atsugi Japan
This is a collection of five short notes on-calculus:
. DRAFT Iterative path orders (2004)
Jan Willem Klop, Vincent Van Oostrom, Roel De Vrijer
In Dershowitz’s original presentation recursive path orders (RPO) are defined by means of recursion. In Bergstra and Klop’s presentation RPOs are operationally defined by means of a set of term...
Four Equivalent Equivalences of Reductions (2002)
Vincent Van Oostrom, Roel De Vrijer
Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a di#erent order. We present four characterisations of such a notion of...
Oostrom, Uniform normalisation beyond orthogonality (2001)
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
Abstract. A rewrite system is called uniformly normalising if all its steps are perpetual, i.e. are such that if s → t and s has an infinite reduction, then t has one too. For such systems...
Oostrom, Uniform normalisation beyond orthogonality (2001)
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
Abstract. A rewrite system is called uniformly normalising if all its steps are perpetual, i.e. are such that if s → t and s has an infinite reduction, then t has one too. For such systems...
Oostrom. Perpetuality and uniform normalization in orthogonal rewrite systems (2001)
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
We present two characterizations of perpetual redexes, which are redexes whose contractions retain the possibility of infinite reductions. These characterizations generalize and strengthen existing...
Maarten Janssen, Vincent Van Oostrom, Opleiding Cognitieve, Kunstmatige Intelligentie
1.1 Organisatie van het Vak............................. 1 1.2 Beoordeling van het Vak............................. 2 1.2.1 Opbouw naar de Presentatiedag.................... 2 1.3 Overzicht van de...
A geometric proof of confluence by decreasing diagrams (2000)
J. W. Klop, V. Van Oostrom, R. De Vrijer, Mathematisch Centrum (smc, The Dutch Foundation, Jan Willem Klop, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Vincent Van Oostrom, No (symmetry Rewrite
F11.95> to a pair of terms over ] X, with (x) = 0. The combination of a symbol with its arity is called a function symbol. The combination of a name with its rule is called an axiom. Subequational...
maps each # to a pair of terms over # # X, with #(x) = 0. The combination of a symbol with its arity is called a function symbol. The combination of a name with its rule is called an axiom....
Strong convergence of term rewriting using strong dependency pairs (Extended Abstract) (1999)
Jürgen Giesl, Vincent Van Oostrom
Introduction. Let R be a finite term rewrite system over a finite signature [4]. Recall the theorem of Arts and Giesl [1] that R is terminating if and only if R satisfies the dependency pair...
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems (1999)
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
this paper is to study sufficient conditions for uniform normalization. Here a term t is uniformly normalizing, UN for short, if either it does not have any normal form (t is not weakly normalizing),...
Normalisation in Weakly Orthogonal Rewriting (1999)
. A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. Outermost-fair rewriting is known to be (head-)normalising for almost orthogonal...
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Femke van Raamsdonk Roel de Vrijer (Eds.)
Vincent Oostrom, Richard Kennaway, Richard Kennaway, Vincent Van Oostrom
We present an axiomatic approach to the concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively...
Finite Family Developments (1997)
Consider Adam and Eve. Count generations starting from them. Supposing that there will always be people, then it's true that for any generation X, eventually there will be people belonging to...
Logical Description of Context-Free Graph Languages (1996)
Joost Engelfriet, Vincent Van Oostrom
. A graph language L is in the class C-edNCE of context-free edNCE graph languages if and only if L = f(T ) where f is a function on graphs that can be defined in monadic second-order logic and T is...
A redex family is a set of redexes which are `created in the same way'. Families specify which redexes should be shared in any so-called optimal implementation of a rewriting system. We...
Meaningless Terms in Rewriting (1996)
Richard Kennaway, Vincent Van Oostrom
We present an axiomatic approach to the concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively...
Development Closed Critical Pairs (1996)
. The class of orthogonal rewriting systems (rewriting systems where rewrite steps cannot depend on one another) is the main class of not-necessarily-terminating rewriting systems for which...
Meaningless Terms in Rewriting (1996)
Richard Kennaway, Vincent Van Oostrom
We present an axiomatic approach to the concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively...
Abc-Active Terms in Transfinite Lambda Calculus (1996)
Richard Kennaway, Vincent Van Oostrom
. This document contains proofs of some claims made in our paper "Meaningless terms in rewriting" [KvOdV96]. It depends on a knowledge of that paper. Theorem 1. In transfinite lambda...
Meaningless Terms in Rewriting (1996)
Richard Kennaway, Vincent Van Oostrom
. We present an axiomatic approach to meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in two ways. First, they are shown to imply important...
Diagram Techniques for Confluence (1996)
Marc Bezem, Jan Willem Klop, Vincent Van Oostrom
We develop diagram techniques for proving confluence in abstract reductions systems. The underlying theory gives a systematic and uniform framework in which a number of known results, widely...
Regular Description of Context-Free Graph Languages (1996)
Joost Engelfriet, Vincent Van Oostrom
. A set of (labeled) graphs can be defined by a regular tree language and one regular string language for each possible edge label, as follows. For each tree t from the regular tree language the...
Meaningless Terms in Rewriting (1996)
Richard Kennaway, Vincent Van Oostrom
We present an axiomatic approach to concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively justified...
Context-sensitive Conditional Expression Reduction Systems (1995)
Zurab Khasidashvili, Vincent Van Oostrom
We introduce Context-sensitive Conditional Expression Reduction Systems (CERS) by extending and generalizing the notion of conditional TRS to the higher order case. We justify our framework in two...
Context-sensitive Conditional Expression Reduction Systems (1995)
Zurab Khasidashvili, Vincent Van Oostrom
We introduce Context-sensitive Conditional Expression Reduction Systems (CERS) by extending and generalizing the notion of conditional TRS to the higher order case. We justify our framework in two...
Developing Developments (1994)
Confluence of orthogonal rewriting systems can be proved using the Finite Developments Theorem. We present, in a general setting, several adaptations of this proof method for obtaining confluence of...
Weak Orthogonality Implies Confluence: the Higher-Order Case (1994)
O Ntt, Vincent Van Oostrom, Vincent Van Oostrom, Femke Van Raamsdonk, Femke Van Raamsdonk
In this paper we prove confluence for weakly orthogonal Higher-Order Rewriting Systems. This generalises all the known `confluence by orthogonality' results. AMS Subject Classification (1991):...
Confluence by Decreasing Diagrams (1994)
We present a confluence criterion, local decreasingness, for abstract reduction systems. This criterion is shown to be a considerable generalisation of several well-known confluence criteria. 1...
Confluence by Decreasing Diagrams (1994)
We present a confluence criterion, local decreasingness, for abstract reduction systems. This criterion is shown to be a considerable generalisation of several well-known confluence criteria. 1...
Confluence by Decreasing Diagrams (1994)
We present a confluence criterion, local decreasingness, for abstract reduction systems. This criterion is shown to be a considerable generalisation of several well-known confluence criteria. 1...
Combinatory reduction systems: Introduction and survey (1993)
Jan Willem Klop, Vincent Van Oostrom, Femke Van Raamsdonk
Combinatory Reduction Systems, or CRSs for short, were designed to combine the usual first-order format of term rewriting with the presence of bound variables as in pure-calculus and various...
Comparing Combinatory Reduction Systems and Higher-Order Rewrite Systems (1993)
Vincent Van Oostrom, Femke Van Raamsdonk
In this paper two formats of higher-order rewriting are compared: Combinatory Reduction Systems introduced by Klop [Klo80] and Higher-order Rewrite Systems defined by Nipkow [Nipa]. Although it...
Comparing Combinatory Reduction Systems and Higher-Order Rewrite Systems (1993)
Vincent Van Oostrom, Femke Van Raamsdonk
In this paper two formats of higher-order rewriting are compared: Combinatory Reduction Systems introduced by Klop and Higher-order Rewrite Systems defined by Nipkow. Although it always has been...
Comparing Combinatory Reduction Systems and Higher-Order Rewrite Systems (1993)
Vincent Van Oostrom, Femke Van Raamsdonk
In this paper two formats of higher-order rewriting are compared: Combinatory Reduction Systems introduced by Klop [Klo80] and Higher-order Rewrite Systems defined by Nipkow [Nipa]. Although it...
Lambda calculus with patterns (1990)
The-calculus is an extension of the-calculus with a pattern matching facility. The form of the argument of a function can be speci ed and hence-calculus is more convenient than ordinary-calculus. We...
Lambda Calculus with Patterns (1990)
The OE-calculus is an extension of the -calculus with a pattern matching facility. The form of the argument of a function can be specified and hence OE-calculus is more convenient than ordinary...
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
We study perpetuality of reduction steps, as well as perpetuality of redexes, in orthogonal rewrite systems. A perpetual step is a reduction step which retains the possibility of infinite reductions....
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
We study perpetuality of reduction steps, as well as perpetuality of redexes, in orthogonal rewrite systems. A perpetual step is a reduction step which retains the possibility of infinite reductions....
Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems
Zurab Khasidashvili, Mizuhito Ogawa, Vincent Van Oostrom
We present two characterizations of perpetual redexes, which are redexes whose contractions retain the possibility of infinite reductions. These characterizations generalize and strengthen existing...