Modular Church-Rosser Modulo: The Full Picture (2009)
Jean-pierre Jouannaud, Yoshihito Toyama
Abstract. In [17], Toyama proved that the union of two confluent term-rewriting systems that share absolutely no function symbols or constants is likewise confluent, a property called modularity. The...
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
Program transformation by templates (Huet and Lang, 1978) is a technique to improve the efficiency of programs. In this technique, programs are transformed according to a given program transformation...
Persistency of Con uence 1 (2008)
Takahito Aoto, Yoshihito Toyama
Abstract: A property P of term rewriting systems (TRSs, for short) is said to be persistent if for any many-sorted TRS R, R has the property P if and only if its underlying unsorted TRS (R) has the...
Tree lifting orderings for termination (2007)
Takahito Aoto, Yoshihito Toyama
transformations of term rewriting systems
RAPT: A program transformation system based on term rewriting (2006)
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
Abstract. Chiba et al. (2005) proposed a framework of program transformation by template and automated verification of its correctness based on term rewriting. This paper describes a design and...
Contents of Survey (1983) (2005)
Yoshihito Toyama, Kokich Futatsugi, Yoshihito Toyama
2. What is term rewriting system 3. Theory of term rewriting systems confluence, termination, Knuth-Bendix completion,
Argument filtering transformation (1999)
Keiichirou Kusakari, Masaki Nakamura, Yoshihito Toyama
Abstract. To simplify the task of proving termination of term rewriting systems, several elimination methods, such as the dummy elimination, the distribution elimination, the general dummy...
The Hierarchy of Dependency Pairs (1999)
Keiichirou Kusakari, Keiichirou Kusakari, Yoshihito Toyama, Yoshihito Toyama
this paper, we study the relation for the termination property between a term rewriting system, the set of its dependency pairs and the union of them. 1 Introduction
Argument Filtering Transformation (1999)
Keiichirou Kusakari, Keiichirou Kusakari, Masaki Nakamura, Masaki Nakamura, Yoshihito Toyama, Yoshihito Toyama
this paper, we show that the argument filtering method combining with the dependency pair technique is essential in all the above elimination methods. We present remarkable simple proofs for the...
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems (1998)
IWAMI, Munehiro, SAKAI, Masahiko, TOYAMA, Yoshihito
Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The...
Termination Transformation by Tree Lifting Ordering (1998)
Takahito Aoto, Yoshihito Toyama
. An extension of a modular termination result for term rewriting systems (TRSs, for short) by A. Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination...
Persistency of confluence (1997)
Takahito Aoto, Yoshihito Toyama
A property P of TRSs is said to be persistent if for any manysorted TRS hF; Ri, hF; Ri has the property P iff its underlying unsorted TRS h\Theta(F); \Theta(R)i has the property P. Here \Theta...
On Composable Properties of Term Rewriting Systems (1997)
Takahito Aoto, Yoshihito Toyama
. A property of term rewriting system (TRS, for short) is said to be composable if it is preserved under unions. We present composable properties of TRSs on the base of modularity results for direct...
Extending persistency of confluence with ordered sorts (1996)
Takahito Aoto, Yoshihito Toyama
A property P of TRSs is said to be persistent if for any TRS hF; Ri and any sort attachment consistent with R, hF
Semantics and Strong Sequentiality of Priority Term Rewriting Systems (1996)
Masahiko Sakai And, Masahiko Sakai, Yoshihito Toyama
. This paper gives an operational semantics of priority term rewriting systems (PRS) by using conditional systems, whose reduction is decidable and stable under substitution. We also define the class...
Modularity of confluence: A simplified proof (1994)
Jan Willem Klop, Aart Middeldorp, Yoshihito Toyama, Roel De Vrijer
In this note we present a simple proof of a result of Toyama which states that the disjoint union of confluent term rewriting systems is confluent.
The Functional Strategy and Transitive Term Rewriting Systems (1993)
Yoshihito Toyama, Sjaak Smetsers, Marko Van Eekelen, Rinus Plasmeijer
The functional strategy has been widely used implicitly (Haskell, Miranda, Lazy ML) and explicitly (Clean) as an efficient, intuitively easy to understand reduction strategy for term (or graph)...
Completeness of combinations of constructor systems (1991)
Aart Middeldorp, Yoshihito Toyama
A term rewriting system is called complete if it is both confluent and strongly normalising. Barendregt and Klop showed that the disjoint union of complete term rewriting systems does not need to be...