일반 양식(추상 재작성)

Normal form (abstract rewriting)

추상적 재작성에서,[1] 객체는 더 이상 다시 쓸 수 없는 경우, 즉 다시 고칠 수 없는 정상적인 형태다.재작성 시스템에 따라 개체는 몇 가지 정상적인 형태로 다시 쓰거나 아예 없는 경우도 있다.재작성 시스템의 많은 특성은 정상적인 형태와 관련이 있다.

정의

공식적으로 (A,→)가 추상적 재작성 시스템인 경우, x→y, 즉 x는 불가해한 용어일 정도로 y existsA가 존재하지 않는 경우 x normalA는 정상적인 형식이다.

물체 a는 최종적으로 정상적인 형태를 산출하는 a에서 시작하는 적어도 하나의 특정한 재쓰기 순서가 존재하는 경우 약하게 정규화된다.재작성 체계는 표준화 특성이 약하거나 모든 물체가 약하게 정상화되는 경우 (약하게) 정상화(WN)된다.객체 a는 어떤 것에서 시작하는 모든 재쓰기 순서가 결국 정상적인 형태로 종료되는 경우 강력하게 정규화된다.추상적 재작성 시스템은 각각의 개체가 강하게 정상화되고 있다면 강력하게 정상화, 종료, 노에테리아 또는 (강력한) 정상화 속성(SN)을 가지고 있다.[2]

모든 객체 a와 일반 형태 b에 대해 일련의 재작성으로 b에 도달할 수 있고 a가 b로 감소하는 경우에만 역작성할 수 있다면 재작성 시스템은 정상적인 형식 속성(NF)을 가지고 있다.모든 정상 형태 a, b ∈ S에 대해 a에서 일련의 다시 쓰기로 도달할 수 있고 a가 b와 동일한 경우에만 역방향으로 다시 쓸 수 있는 경우, 재작성 시스템은 고유한 정상 형태 속성(UN)을 가진다.재쓰기 시스템은 축소(UN→)와 관련하여, 모든 용어가 정상 형태 a와 b로 축소되는 경우, b와 같은 고유한 정상 형태 속성을 가진다.[3]

결과.

이 절에서는 잘 알려진 결과를 몇 가지 제시한다.첫째, SN은 WN을 암시한다.[4]

혼합물(약칭 CR)은 NF가 UN을→ 의미한다는 것을 의미한다.[3]역방향 함축은 일반적으로 유효하지 않다.{a→b→a→c→c→c→c→c→c→d→e}은(는) UN이지만→ b=e와 b는 정상적인 형태여서 UN이 아니다.{a→b→c→b→b}은(는) UN이지만 b=c로 NF는 아니고, c로 줄이지 않는다. {a→b→c→b→b→c}은(는) 정상 형태가 없기 때문에 NF로 줄이지 않지만 a로 줄인 CR은 b와 c로, b는 공통 환원되지 않는다.

WN과 UN은→ 결합을 암시한다.따라서 WN이 유지하면 CR, NF, UN, UN이→ 일치한다.[5]

예

예를 들어, 단일 규칙 g(x,y)→x를 갖는 재쓰기 시스템이라는 용어를 사용하여 g(g)(4,2),g(3,1)라는 용어를 다음과 같이 다시 쓸 수 있으며, g:의 가장 바깥쪽 발생에 규칙을 적용할 수 있다.

g(g(4,2), g(3,1) → g(4,2) → 4.

마지막 용어인 4에는 규칙이 적용되지 않기 때문에 더 이상 다시 쓸 수 없으며, 따라서 이 용어 재쓰기 제도와 관련하여 g(4,2),g(3,1)라는 용어의 정상적인 형태다.규칙 시스템은 각 규칙 적용이 적절하게 기간 크기를 감소시키고, 따라서 어떤 용어로부터도 무한히 다시 쓰기 순서가 있을 수 없기 때문에 강력하게 정상화되고 있다.이와는 대조적으로, 2-규칙 체계 {g(x,y) → x, g(x,x) → g(3,x)}은 약하지만[note 2], g(3,x)를 포함하지 않는 각 용어는 강하게 정상화하고[note 3] 있지는 않다.[note 4] g(4,4)라는 용어는 이 시스템에서 두 가지 정상적인 형태인 viz. g(4,4)→4(,4)→g(4,4)→g(3,4)→3()를 가지므로 이 시스템은 합치되지 않는다.

다른 예:단일 규칙 시스템 {r(x,y) → r(y,x) }에는 (약하거나 강하게) 정상화하는 특성이 없으며, 예를 들어 r(4,2)에서 단일 재작성 시퀀스인 viz. r(4,2) → r(4,2) → r(2,4) → r(2,4) → r(2,4) → ...이 무한히 길기 때문이다.

미유형 람다 미적분

순수한 비형식 람다 미적분은 강한 정상화 속성도 충족시키지 못하고, 약한 정상화 속성도 충족시키지 못한다. . \ \이라는 용어를 고려하십시오(응용프로그램은 왼쪽 연관).그것은 다음과 같은 재작성 규칙을 가지고 있다. 용어에 대해

그러나 . x 을(를) 그 자체에 적용하면 어떻게 되는지 생각해 보십시오.

따라서 용어 ( x xx ) ( x ) (\ x.xxx은 강하게 정상화되지 않고 있다.그리고 이것이 유일한 감소 순서가므로 약하게 정상화하는 것도 아니다.

입력된 람다 미적분

단순 타이핑된 람다 미적분, 장 이브 지라드의 시스템 F, 티에리 코콴드의 시공 미적분 등 다양한 형태의 람다 미적분 시스템이 강력하게 정상화되고 있다.

정규화 속성이 있는 람다 미적분 시스템은 모든 프로그램이 종료되는 속성을 가진 프로그래밍 언어로 볼 수 있다.이것은 매우 유용한 속성이지만, 단점이 있다: 정규화 속성이 있는 프로그래밍 언어는 튜링 완성이 될 수 없다. 그렇지 않으면 프로그램 유형 확인을 통해 중단 문제를 해결할 수 있다.즉, 단순하게 입력된 람다 미적분(그리고 유사하게 시공 또는 시스템 F의 미적분에서 계산할 수 없는 계산 가능한 함수가 있다는 것을 의미한다) 예를 들어 자가 상호작용을 한다.[6]

참고 항목

메모들

  1. ^ 규칙이 적용되는 g의 각 발생은 굵은 글씨로 강조 표시된다.
  2. ^ g를 포함하는 모든 용어는 g가 없는 용어에 첫 번째 규칙의 한정된 개수의 적용에 의해 다시 쓰일 수 있기 때문에, 이것은 정상적인 형태다.
  3. ^ g(3,3)라는 용어 때문에, 두 번째 규칙은 어떤 정상적인 형태에도 도달하지 않고 계속해서 적용될 수 있다.
  4. ^ 주어진 용어의 경우, m과 n은 각각 동일한 인수에 적용된 g와 g의 총 수를 나타낸다.어떤 규칙이라도 적절히 적용하면 m + n의 값이 감소하는데, 이것은 오직 여러 번 미세하게만 가능하다.

참조

  1. ^ Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.
  2. ^ Ohlebusch, Enno (1998). "Church-Rosser theorems for abstract reduction modulo an equivalence relation". Rewriting Techniques and Applications. Lecture Notes in Computer Science. 1379: 18. doi:10.1007/BFb0052358. ISBN 978-3-540-64301-2.
  3. ^ a b Klop, J.W.; de Vrijer, R.C. (February 1989). "Unique normal forms for lambda calculus with surjective pairing". Information and Computation. 80 (2): 97–113. doi:10.1016/0890-5401(89)90014-X.
  4. ^ "logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?". Computer Science Stack Exchange. Retrieved 12 September 2021.
  5. ^ Ohlebusch, Enno (17 April 2013). Advanced Topics in Term Rewriting. Springer Science & Business Media. pp. 13–14. ISBN 978-1-4757-3661-8.
  6. ^ Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 June 2015). Genetic Programming Theory and Practice XII. Springer. p. 59. ISBN 978-3-319-16030-6. Retrieved 8 September 2021.