ルート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.

収録刊行物

• 情報処理学会研究報告. PRO, [プログラミング]

  情報処理学会研究報告. PRO, [プログラミング] 97 (9), 109-116, 1997-01-23

  一般社団法人情報処理学会

キーワード

• 項書き換えシステム
• チャーチ・ロッサ性
• 非線形
• 深さ保存
• 重み保存
• E重なり

詳細情報

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