재작성

위키백과, 우리 모두의 백과사전.
이동: 둘러보기, 검색

수학, 컴퓨터 과학 및 논리학에서 재작성은 다양한 부분을 다루고 있다. (특별히 비결정적인 부분에서 중요하다) 이는 부분식을 다른 항으로 교체하여 이루어진다. 재작성 시스템에서 다루는 것은 물체들의 집합과 그들 간의 관계 및 변환이다.

재작성은 비결정적일 수 있다. 한 구문(term)을 작성하는 하나의 규칙은 여러 가지 방법으로 해당 구문에 적용될 수 있다. 또한 복수의 규칙이 적용될 수도 있다. 재작성 시스템은 하나의 구문을 다른 구문으로 수정하는 알고리즘을 제공하는 것이 아니라 여러 규칙을 묶어 제공한다. 적절한 알고리즘을 구성하는 규칙들의 집합은 컴퓨터 프로그램 그 자체 혹은 몇몇 재작성(term-rewriting) 기반 선언 프로그래밍 언어로 간주되기도 한다.

간단한 예제[편집]

논리학에선, CNF를 결정하는 절차를 재작성을 통해 표현할 수 있다.

\neg\neg A \to A
\neg(A \land B) \to \neg A \lor \neg B (드 모르간의 법칙)
\neg(A \lor B)  \to \neg A \land\neg B
 (A \land B) \lor C \to (A \lor C) \land (B \lor C) (분배법칙)
 A \lor (B \land C) \to (A \lor B) \land (A \lor C),

여기서 (\to) 기호는 좌측 규칙이 우측 규칙으로 재작성 가능함을 나타낸다. 이러한 시스템에서, 재작성은 좌측의 규칙을 우측의 규칙으로 해석하는 논리의 작동이다.

추상 재작성 시스템[편집]

이상의 예제를 볼 때, 재작성 시스템은 추상적인 표현을 통해 이해할 수 있다. 추상적인 표현을 구체화하기 위해서는 이들 객체(object) 및 규칙(rule)들의 집합을 구체화하는 것이 필요하다. 일반적으로, 대부분 이러한 개념의 일차원적인 환경은 추상 소거 시스템(abstract reduction system, ARS)이라 한다. 최근 관련 서적의 저자들은 추상 재작성 시스템[1]이라고도 한다.

다음 예제를 통해 이해해보자. T = {a, b, c} 인 객체 T가 존재하고, ab, ba, ac, bc 와 같은 이진 관계를 정의하는 규칙들이 존재한다고 하자. (규칙들을 보면 ab가 모두 c와 관계가 있다는 것이 중요한 특징이다.) 또한, c는 위 시스템에서 가장 단순한 형태의 구문(term)이라 할 수 있다. 왜냐하면 이상의 어떠한 구문들도 c로는 재작성될 수 있지만, c는 어떠한 형태로도 재작성될 수 없기 때문이다. 이를 통해 가장 기초적인 개념을 이해할 수 있다.[2]

표준 형식, 연결 가능성, 재배치 문제[편집]

처치-로서 속성, 합류성[편집]

종료성과 수렴성[편집]

문자열 재작성 시스템[편집]

항 재작성 시스템[편집]

참조[편집]

  1. Bezem et al, p. 7,
  2. Baader and Nipkow, pp. 8-9