재작성 문서 원본 보기

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

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

== 간단한 예제 ==
[[논리학]]에선, [[CNF]]를 결정하는 절차를 재작성을 통해 표현할 수 있다.

:<math>\neg\neg A \to A</math>
:<math>\neg(A \land B) \to \neg A \lor \neg B</math> ([[드 모르간의 법칙]])
:<math>\neg(A \lor B)  \to \neg A \land\neg B</math>
:<math> (A \land B) \lor C \to (A \lor C) \land (B \lor C)</math> ([[분배법칙]])
:<math> A \lor (B \land C) \to (A \lor B) \land (A \lor C)</math>,

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

== 추상 재작성 시스템 ==
{{본문|추상 재작성 시스템}}

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

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

=== 표준 형식, 연결 가능성, 재배치 문제 ===
{{빈 문단}}

=== 처치-로서 속성, 합류성 ===
{{본문|합류성}}
=== 종료성과 수렴성 ===
{{빈 문단}}

== 문자열 재작성 시스템 ==
{{빈 문단}}

== 항 재작성 시스템 ==
{{빈 문단}}

== 같이 보기 ==
* [[컴파일러]]
* [[L-system]]
* [[참조 투명성]]
== 참조 ==
<references/>

{{전거 통제}}

[[분류:재작성 시스템|*]]