경로 순서 지정(용어 다시 쓰기)

Path ordering (term rewriting)
"사전 경로 순서 지정"은 여기로 리디렉션됩니다.사전 순서는 사전 정렬을 참조하십시오.

이론 컴퓨터 과학에서, 특히 용어 재작성에서 경로 순서는 다음과 같은 모든 용어의 집합에 대한 근거가 있는 엄격한 총 순서(>)입니다.

f(...) > g(s,...,s) i=1,...,n일 경우 f > g, f(...) > s,

여기서 (>).는 모든 함수 기호 집합에 대한 사용자 지정 총 우선 순위입니다.

직관적으로, f(...) 항은 f(...)보다 작은 항들로부터i 만들어진 어떤 항 g(...)보다 더 큰 우선순위가 낮은 근기호 g를 사용합니다.특히 구조적 귀납법에 의해 f(...)보다 작은 기호만 포함하는 항보다 f(...)가 더 큽니다.

경로 순서는 용어 재작성에서 축소 순서로 사용되는 경우가 많으며, 특히 Knuth-Bendix 완료 알고리즘에서 그러합니다.예를 들어, 수학적 표현식을 "배포"하기 위한 용어 다시 쓰기 시스템은 x*(y+z) → (x*y) + (x*z) 규칙을 포함할 수 있습니다.종료를 증명하려면 x*(y+z) 항이 (x*y)+(x*z) 항보다 큰 항에 대해 축소 순서(>)를 찾아야 합니다.전자 항은 후자보다 함수 기호와 변수가 모두 적기 때문에 이는 사소한 것이 아닙니다.그러나, 우선순위를 설정하면 x*(y+z) > x*y와 x*(y+z) > x*z 모두 달성하기 쉽기 때문에 경로 순서를 사용할 수 있습니다.

특정 일반 재귀 함수에 대한 시스템도 있을 수 있는데, 예를 들어 아커만 함수에 대한 시스템은 규칙 A(a, b) → A(a, A(a, b))를 포함할 수 있습니다. 여기서 b는 b의 계승자를 나타냅니다.

두 개의 항과 t가 주어지면, 각각 근기호 f와 g를 사용하여 그들의 관계를 결정하기 위해 그들의 근기호들을 먼저 비교합니다.

  • 만약 .< g>이면 s의 밑문 중 하나가 t를 지배할 수 있습니다.
  • 만약 f > g이면, s가 t의 각 밑면을 지배합니다.
  • f = g이면 s와 s의 바로 밑부분을 재귀적으로 비교해야 합니다.특정 방법에 따라 경로 순서의 다양한 변화가 있습니다.[2][3]

후자의 변형은 다음과 같습니다.

  • 다중 집합 경로 순서 지정(mpo), 원래 재귀적 경로 순서 지정(rpo)[4]이라고 함
  • 사전 기록 경로 순서 지정(lpo)[5]
  • Dershowitz, Jouannaud (1990)[6][7][8]에 의해 재귀적 경로 순서라고 불리는 mpo와 lpo의 조합.

Dershowitz, Okada (1988)는 더 많은 변종들을 나열하고, 그것들을 Ackermann의 순서 표기 체계와 연관시킵니다.특히, n개의 함수 기호를 갖는 재귀적 경로 순서의 순서 유형에 부여된 상한은 큰 수열 [7]서수에 대한 베블렌 함수를 사용하여 π(n,0)입니다.

형식적 정의

다중 집합 경로 순서 지정(>)은 [9]다음과 같이 정의할 수 있습니다.

s = f(s,...,s) > t = g(t,...,t) 한다면
f .> g 그리고. s > tj 일별로 j◦{1,...,n}, 아니면
si ≥ t 어느 정도는 i∈{1,...,m}, 아니면
f = g 그리고. {s1,...,sm } >> {t1,...,tn }

어디에

  • (≥)는 mpo(>)의 반사적 폐쇄를 나타냅니다.
  • {s,...,sm }은 s의 밑면의 다중집합을 의미하며, 비슷한 요새를 나타냅니다1.
  • (>)는 {s1,...,s}에서 {t1,...,tn}을(를) 가져올 수 있는 경우 {s1,...,smm}> {t1,...,tn}로 정의된 (>)의 다중 집합 확장을 나타냅니다.
    • 적어도 하나의 요소를 삭제함으로써, 또는
    • 요소를 완전히 더 작은(w.r.t.mpo)[10] 요소의 다중 집합으로 대체함으로써.

일반적으로 주문 함수는 주문을 다른 주문에 매핑하고 다음 [11]속성을 만족시키는 함수 O입니다.

  • (>)가 추이적이면 O(>)도 추이적입니다.
  • (>)가 무굴절이면 O(>)도 마찬가지입니다.
  • s > t인 경우 f(...,s,...) O(>) f(...,t,...)입니다.
  • O는 관계에서 연속적입니다. 즉, R, R, R, R, ...이 관계의 무한 순서라면, O(∪ R) = ∪ O(R)입니다.

다중 집합 확장, 위의 매핑(>)을 위의 (>)에 매핑하는 것은 주문 기능의 한 예입니다: (>)=O(>).또 다른 순서 함수는 사전 기록 경로 순서로 이어지는 사전 기록 확장입니다.

참고문헌

  1. ^ N. Dershowitz, "종료"(1995) 페이지 207
  2. ^ Nachum Dershowitz, Jean-Pierre Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. 여기: 섹션 5.3, 페이지 275
  3. ^ Gerard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Archived from the original on 2014-07-14. 여기: Chapter 4, p.55-64
  4. ^ 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.
  5. ^ S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL.
  6. ^ 카민, 레비 (1980)
  7. ^ a b N. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science (PDF). pp. 104–111.
  8. ^ Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing.
  9. ^ Huet (1986), 섹션 4.3, def.1, p.57
  10. ^ Huet (1986), 섹션 4.1.3, 페이지 56
  11. ^ Huet (1986), 섹션 4.3, 페이지 58