다시쓰기 순서

Rewrite order
규칙 l::=r로 s를 t에 다시 쓰는 중.만약 l와 r이 다시 쓰기 관계에 의해 연관되어 있다면 s와 t도 마찬가지다.단순화 순서는 항상 l와 s, 그리고 유사하게 r과 t와 관련이 있다.

이론 컴퓨터 과학에서, 특히 공식 방정식에 대한 자동화된 추론에서, 감소 순서는 끝없는 루프를 막기 위해 사용된다.순서를 다시 쓰는 것, 그리고 다시 관계를 다시 쓰는 것은 이론적 조사에 유용한 것으로 밝혀진 이 개념의 일반화다.

동기

직관적으로, 감소 순서 R은 t가 어떤 의미에서 s보다 적절하게 "시뮬러"인 경우 두 가지 공식 표현식 s와 t를 연관시킨다.

예를 들어 용어의 단순화는 컴퓨터 대수 프로그램의 일부일 수 있으며, 규칙 집합 {x+0 → x , 0+x → x*0 → 0, 0*x → 0, x*1 → x, 1*x → x }을 사용하고 있을 수 있다.용어를 단순화할 때 끝없는 루프가 불가능함을 증명하기 위해 "표현 t가 표현 s보다 적절하게 짧을 경우 sRt"로 정의한 축소 순서를 사용할 수 있다. 집합에서 규칙을 적용하면 항을 항상 적절하게 단축할 수 있다.

반대로, 규칙 x**(y+z) → x*y+x*z를 이용한 "분산"의 종료를 확립하기 위해서는, 이 규칙이 x의 중복으로 인해 용어 크기를 날려버릴 수도 있기 때문에, 보다 정교한 축소 순서가 필요할 것이다.다시 쓰기 명령의 이론은 그러한 경우에 적절한 질서를 제공하는 것을 돕는 것을 목적으로 한다.

형식 정의

만약 그것이 컨텍스틌던 1가지 이슈 때문이었습니다 그리고 예시화 아래에 따라서 닫힌다면(→)또한과 전이 반사하지 않는은 형식적으로, 용어의 텔레비전은 이항 관계(→), 공식적으로:pu의 경우 l→r 모든 조건을 u[lσ]p→u[rσ]p를 암시하 l, r, u, 각 경로 및 각 대체 σ. 그 때에서 rewriteordering,[1]나 개정이라고 불리는에서 rewrite관계라고 불린다. preorder. 후자(→)가 더구나 근거가 있는 경우에는 감량주문,[2] 즉 감량예약주문이라고 한다.2진수 관계 R을 감안할 때, 그것의 재작성 마감은 R을 포함하는 가장 작은 재작성 관계다.[3]하위어 순서를 포함하는 전이적이고 반사적인 재작성 관계를 단순화 순서라고 한다.[4]

재작성 관계 개요[주 1]
다시 쓰다
관계		 다시 쓰다
주문		 환원
주문		 단순화
주문
문맥상 폐쇄된.
x R y는 u[x]pRu[y]p를 의미한다. 		네 네 네 네
즉흥적으로 폐쇄된.
x R y는 xσRyσ을 의미한다.		 네 네 네 네
하위 관계 포함
ysubter of x는 x R y를 내포함 		네
반사적인
항상 x x x 		(아니오) (아니오) 네
불변의
never x r x 		네 네 (아니오)
타동성의
x R y 및 y R z는 x R z를 의미한다. 		네 네 네
근거가 있는
무한 체인 xRxRxR이123 없음...[note 2] 		네 (네)

특성.

  • 반대, 대칭적 폐쇄, 반사적 폐쇄, 그리고 다시 쓰기 관계의 전이적 폐쇄는 다시 쓰기 관계가 되는데, 이는 연합과 두 다시 쓰기 관계의 교차점이 그러하듯이 다시 쓰기 관계가 된다.[1]
  • 다시 쓰기 명령의 반전은 다시 다시 쓰기 명령이다.
  • 기초 용어 집합에 총체적인 재작성 순서가 존재하지만(단축에 대한 총계) 모든 용어 집합에 총체적인 재작성 순서는 있을 수 없다.[note 3][5]
  • 용어 재작성 시스템 {l1::=r1,...,ln::=rn, ...{}은(는) 규칙이 감소 순서의 하위 집합인 경우 종료하는 중임.[note 4][2]
  • 반대로, 모든 종료 용어 재작성 시스템에 대해 (:=)의 전이적 폐쇄는 감산 순서로서,[2] 그러나, 지상 총량까지 확장할 필요는 없다.예를 들어 기본 용어 재작성 시스템 {f(a)::=f(b), g(b)::=g(a) }이(가) 종료되지만 상수 a와 b가 비할 수 없는 경우에만 축소 순서를 사용하여 그렇게 표시할 수 있다.[note 5][6]
  • 기초 총액 및 근거가 충분한 재작성 순서는[note 6] 반드시 기초 조건의 적절한 하위 기간 관계를 포함한다.[note 7]
  • 반대로 함수 기호의 집합이 유한할 때 하위 용어 관계를[note 8] 포함하는 재작성 순서는 반드시 근거가 충분하다.[5][note 9]
  • 유한 용어 재작성 시스템 {l1::=r1,...,ln::=rn, ...}은(는) 규칙이 단순화 순서의 엄격한 부분 집합인 경우 종료하는 것이다.[4][8]

메모들

  1. ^ 괄호화된 항목은 정의의 일부가 아닌 유추된 속성을 나타낸다.예를 들어, (비어 있지 않은 도메인 집합에서) 회복 불가능한 관계는 반사적일 수 없다.
  2. ^ 모든 x가i 일부 n을 초과하는 모든 i에 대해 동일하다는 것을 제외하고, 반사적 관계에 대해서는
  3. ^ x는 y를 의미하므로, 후자는 전자의 인스턴스(instance)이므로 변수 x, y.
  4. ^ 예: 모든 i에 대해 li > r인i 경우, 여기서 (>)는 감소 순서일 경우, 시스템은 세부적으로 많은 규칙을 가질 필요가 없다.
  5. ^ 예: a>b가 g(a)>g(b)를 암시했기 때문에, 두 번째 재작성 규칙은 감소하지 않고 있었다.
  6. ^ 즉, 지상 총량 감축 주문
  7. ^ 또는 t > t 어떤 용어의 t > t 위치 p에 대해, 무한 내림차인 t > t[t]p > t[t]pp > ...[6][7]을 의미한다.
  8. ^ 즉, 단순화 주문
  9. ^ 이 성질의 증명은 히그만의 보조정리 즉, 보다 일반적으로 크러스칼의 트리 정리에 기초하고 있다.

참조

Nachum Dershowitz; Jean-Pierre Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. doi:10.1016/B978-0-444-88074-1.50011-1. ISBN 9780444880741.

  1. ^ a b Dershowitz, Jouannaud (1990), 제2장 1, 페이지 251
  2. ^ a b c Dershowitz, Jouannaud (1990), 제5.1장, 페이지.270
  3. ^ Dershowitz, Jouannaud (1990), 제2장 2.2절, 페이지 252
  4. ^ a b Dershowitz, Jouannaud (1990), 제5.2장, 페이지 274
  5. ^ a b Dershowitz, Jouannaud (1990), 제5.1장, 페이지 272
  6. ^ a b Dershowitz, Jouannaud (1990), 제5.1장, 페이지 271
  7. ^ David A. Plaisted (1978). A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems (Technical report). Univ. of Illinois, Dept. of Comp. Sc. p. 52. R-78-943.
  8. ^ N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. S2CID 6070052. 여기: p.287; 개념은 약간 다르게 명명되었다.