ルートE重なりな深さ保存項書き換えシステムのチャーチ・ロッサー性について

書誌事項

タイトル別名
  • On the Church-Rosser Property of Root-E-overlapping and Depth-Preserving Term Rewriting Systems

この論文をさがす

説明

項書き換えシステムが強深さ保存であるとは、すべての書き換え規則の両辺に現れる各変数において、その変数の左辺における出現位置の最小深さが右辺の最大深さ以上であるときである。本稿では強深さ保存項書き換えシステムのチャーチ・ロッサー性を保証する十分条件を与え、この条件の判定方法について述べる。各関数記号に対して正の整数(重みと呼ぶ)を割り当てることにより、強深さ保存の概念を強重み保存の概念に自然に拡張することができ、強重み保存項香き換えシステムのチャーチ・ロッサー性を保証する同様な十分条件を導くことができる。
A term rewriting system (TRS) is said to be strongly depth-preserving if for any rewrite rule and any variable appearing in the both sides, the minimal depth of the variable occurrences in the left-hand-side is greater than or equal to the maximal depth of the variable occurrences in the right-hand-side. This paper gives a sufficient condition for Church-Rosser of strongly depth-preserving TRS's and describes how to check this condition. By assigning a positive integer (called weight) to each function symbol, the notion of strongly depth-preserving is naturally extended to that of strongly weight-preserving and a similar sufficient condition for church-Rosser of strongly weigh-preserving TRS's is obtained.

収録刊行物

キーワード

詳細情報 詳細情報について

  • CRID
    1574231876937576704
  • NII論文ID
    110002929354
  • NII書誌ID
    AN10485570
  • 本文言語コード
    en
  • データソース種別
    • CiNii Articles

問題の指摘

ページトップへ