論文

査読有り
1996年12月

On the Church - Rosser Property of Non -E- overlapping and Strongly Depth - preserving Term Rewriting Systems

情報処理学会論文誌
  • Hiroshi Gomi
  • ,
  • Michio Oyamaguchi
  • ,
  • Yoshikatsu Ohta

37
12
開始ページ
2147
終了ページ
2160
記述言語
英語
掲載種別

A term rewriting system (TRS) is said to be depth-preserving if for any rewrite rule and any variable appearing in the both sides the maximal depth of the variable occurrences in the left-hand-side is greater than or equal to that of the variable occurrences in the right-hand-side and to be strongly depth-preserving if it is depth-preserving and for any rewrite rule and any variable appearing in the left-hand-side all the depths of the variable occurrences in the left-hand-side are the same. This paper shows that there exit non-E-overlapping and depth-preserving TRS's which are not Church-Rosser but all the non-E-overlapping and strongly depth-preserving TRS's are Church-Rosser.A term rewriting system (TRS) is said to be depth-preserving if for any rewrite rule and any variable appearing in the both sides, the maximal depth of the variable occurrences in the left-hand-side is greater than or equal to that of the variable occurrences in the right-hand-side, and to be strongly depth-preserving if it is depth-preserving and for any rewrite rule and any variable appearing in the left-hand-side, all the depths of the variable occurrences in the left-hand-side are the same. This paper shows that there exit non-E-overlapping and depth-preserving TRS's which are not Church-Rosser, but all the non-E-overlapping and strongly depth-preserving TRS's are Church-Rosser.

リンク情報
CiNii Articles
http://ci.nii.ac.jp/naid/170000125705
CiNii Resolver ID
http://ci.nii.ac.jp/nrid/9000346949742