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

Bibliographic Information

Other Title
  • On the Church-Rosser Property of Root-E-overlapping and Depth-Preserving Term Rewriting Systems

Search this article

Description

項書き換えシステムが強深さ保存であるとは、すべての書き換え規則の両辺に現れる各変数において、その変数の左辺における出現位置の最小深さが右辺の最大深さ以上であるときである。本稿では強深さ保存項書き換えシステムのチャーチ・ロッサー性を保証する十分条件を与え、この条件の判定方法について述べる。各関数記号に対して正の整数(重みと呼ぶ)を割り当てることにより、強深さ保存の概念を強重み保存の概念に自然に拡張することができ、強重み保存項香き換えシステムのチャーチ・ロッサー性を保証する同様な十分条件を導くことができる。
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.

Journal

  • IPSJ SIG Notes

    IPSJ SIG Notes 97 (9), 109-116, 1997-01-23

    Information Processing Society of Japan (IPSJ)

Keywords

Details 詳細情報について

  • CRID
    1574231876937576704
  • NII Article ID
    110002929354
  • NII Book ID
    AN10485570
  • Text Lang
    en
  • Data Source
    • CiNii Articles

Report a problem

Back to top