합류성

합류라는 이름은 두 수역이 만나는 것을 의미하는 지리에서 영감을 받았다. 컴퓨터 과학 및 수학에서 **합류성**(confluence)은 재작성 시스템의 속성으로, 이러한 시스템에서 어떤 항들이 둘 이상의 방식으로 재작성되어 동일한 결과를 낼 수 있는지를 설명한다. 이 문서는 추상 재작성 시스템의 가장 추상적인 설정에서 속성을 설명한다.
# 동기 부여 예시
right 초등 산술의 일반적인 규칙은 추상 재작성 시스템을 형성한다. 예를 들어, 식 (11 + 9) × (2 + 4)는 왼쪽 괄호에서 시작하거나 오른쪽 괄호에서 시작하여 평가할 수 있다. 그러나 두 경우 모두 결국 동일한 결과를 얻는다. 모든 산술 식이 축소 전략에 관계없이 동일한 결과로 평가된다면, 산술 재작성 시스템은 접지 합류적이라고 한다. 산술 재작성 시스템은 재작성 시스템의 세부 사항에 따라 합류적이거나 접지 합류적일 수 있다.date=Oct 1994 - 두 번째, 더 추상적인 예시는 각 군 원소가 그 역원의 역원과 같다는 다음 증명에서 얻는다.p=134: axiom and proposition names follow the original text {| |+ 군 공리 |- | **A1** || 1 ⋅ a || = a |- | **A2** || a−1 ⋅ a || = 1 |- | **A3** || (a ⋅ b) ⋅ c || = a ⋅ (b ⋅ c) |} {| |+ **R4** 증명: a−1⋅(a⋅b) = b |- | || a−1 ⋅ (a ⋅ b) || |- | = || (a−1 ⋅ a) ⋅ b || by A3(r) |- | = || 1 ⋅ b || by A2 |- | = || b || by A1 |} {| |+ **R6** 증명: (a−1)−1 ⋅ 1 = a |- | || (a−1)−1 ⋅ 1 || |- | = || (a−1)−1 ⋅ (a−1 ⋅ a) || by A2(r) |- | = || a || by R4 |} {| |+ **R10** 증명: (a−1)−1 ⋅ b = a ⋅ b |- | || (a−1)−1 ⋅ b || |- | = || (a−1)−1 ⋅ (a−1 ⋅ (a ⋅ b)) || by R4(r) |- | = || a ⋅ b || by R4 |} {| |+ **R11** 증명: a ⋅ 1 = a |- | || a ⋅ 1 || |- | = || (a−1)−1 ⋅ 1 || by R10(r) |- | = || a || by R6 |} {| |+ **R12** 증명: (a−1)−1 = a |- | || (a−1)−1 || |- | = || (a−1)−1 ⋅ 1 || by R11(r) |- | = || a || by R6 |} - 이 증명은 주어진 군 공리 A1–A3에서 시작하여 R4, R6, R10, R11, R12의 다섯 가지 명제를 확립하며, 각 명제는 이전 명제를 사용하고 R12는 주 정리이다. 일부 증명은 R6의 증명 첫 단계에서 "1"을 "a−1 ⋅ a"로 재작성하기 위해 공리 A2를 역으로 적용하는 것과 같이 명확하지 않거나 심지어 창의적인 단계를 필요로 한다. 항 재작성 이론을 개발한 역사적 동기 중 하나는 경험이 없는 사람, 심지어 컴퓨터 프로그램이 찾기 어려운 이러한 단계의 필요성을 피하기 위함이었다. 항 재작성 시스템이 합류적이고 종료적이라면, 두 표현식(항) s와 t 사이의 등식을 증명하는 간단한 방법이 존재한다. s에서 시작하여 가능한 한 왼쪽에서 오른쪽으로 등식그때는 왼쪽에서 오른쪽 방향을 강조하기 위해 재작성 규칙이라고 불렀다.을 적용하여 결국 항 s′를 얻는다. 유사한 방식으로 t에서 항 t′를 얻는다. 두 항 s′와 t′가 문자 그대로 일치한다면, s와 t는 같다고 증명된다. 더 중요한 것은, 일치하지 않는다면 s와 t는 같을 수 없다는 것이다. 즉, 같다고 증명될 수 있는 모든 두 항 s와 t는 그 방법으로 증명될 수 있다. 이 방법의 성공은 재작성 규칙을 적용하는 특정 정교한 순서에 의존하지 않는다. 합류성은 규칙 적용의 어떤 순서도 결국 동일한 결과로 이어진다는 것을 보장하기 때문이다(종료성은 어떤 순서도 결국 끝에 도달한다는 것을 보장합니다). 따라서 어떤 등식론에 대해 합류적이고 종료적인 항 재작성 시스템이 제공될 수 있다면,크누스-벤딕스 완비화 알고리즘은 주어진 등식 집합으로부터 그러한 시스템을 계산하는 데 사용될 수 있다. 예를 들어 군에 대한 그러한 시스템은 여기에 일관성 있게 번호가 매겨진 명제와 함께 표시된다. 이를 사용하여 R6의 증명은 항 (a−1)−1⋅1에 R11과 R12를 어떤 순서로든 적용하여 항 a를 얻는 것으로 구성된다. 다른 규칙은 적용할 수 없다. 항 등식을 증명하는 데 창의성이 전혀 필요하지 않는다. 따라서 이 작업은 컴퓨터 프로그램에 적합해진다. 현대적인 접근 방식은 항 재작성 시스템보다 더 일반적인 추상 재작성 시스템을 다룬다. 후자는 전자의 특수한 경우이다.
# 일반적인 경우와 이론
d로 축소되어야 한다. 재작성 시스템은 노드가 표현식을 나타내고 모서리가 재작성을 나타내는 유향 그래프로 표현될 수 있다. 예를 들어, 표현식 a가 b로 재작성될 수 있다면, 우리는 b를 a의 축소항(또는 a가 b로 축소되거나 a가 b의 확장)이라고 말한다. 이는 화살표 표기법으로 표현된다. a → b는 a가 b로 축소됨을 나타낸다. 직관적으로, 이는 해당 그래프에 a에서 b로 향하는 유향 모서리가 있음을 의미한다. 두 그래프 노드 c와 d 사이에 경로가 있다면, 그것은 축소 시퀀스를 형성한다. 예를 들어, c → c′ → c′′ → ... → d′ → d라면, 우리는 c → d라고 쓸 수 있으며, 이는 c에서 d로의 축소 시퀀스의 존재를 나타낸다. 형식적으로, →는 →의 반사-전이 폐포이다. 이전 단락의 예를 사용하면, (11+9)×(2+4) → 20×(2+4)이고 20×(2+4) → 20×6이므로, (11+9)×(2+4) → 20×6이다. 이를 바탕으로 합류성은 다음과 같이 정의될 수 있다. a ∈ S는 합류적이다. 이는 a → b와 a → c인 모든 b, c ∈ S 쌍에 대해 b → d와 c → d인 d ∈ S가 존재할 때이다(표기 b \mathbin\downarrow c). 모든 a ∈ S가 합류적이면, →는 합류적이라고 말한다. 이 속성은 오른쪽 다이어그램의 모양을 따서 다이아몬드 속성이라고도 불린다. 일부 저자는 다이아몬드 속성이라는 용어를 모든 곳에서 단일 축소를 가진 다이어그램의 변형에 사용한다. 즉, a → b와 a → c일 때마다 b → d와 c → d인 d가 존재해야 한다. 단일 축소 변형은 다중 축소 변형보다 엄격하게 강력한다.
## 접지 합류성
항 재작성 시스템은 모든 기저 항이 합류적일 때, 즉 변수가 없는 모든 항이 합류적일 때 **접지 합류적**이다.language=en
## 지역 합류성
pages=243-320 Here: p.268, Fig.2a+b. 그림 2: 무한 비순환적이며 지역적으로 합류적이지만 전역적으로 합류적이지 않은 재작성 시스템 원소 a ∈ S는 a → b와 a → c인 모든 b, c ∈ S에 대해 b → d와 c → d인 d ∈ S가 존재할 때 **지역적으로 합류적**이라고 한다(또는 약하게 합류적pp=10-11). 모든 a ∈ S가 지역적으로 합류적이면, →는 지역적으로 합류적이라고 불리거나 약한 처치-로서 속성을 가진다고 말한다. 이는 b와 c가 한 단계에서 a로부터 축소되어야 한다는 점에서 합류성과 다르다. 이에 비유하여 합류성은 때때로 전역 합류성이라고도 불린다. 축소 시퀀스에 대한 표기법으로 도입된 관계 →는 그 자체로 재작성 시스템으로 볼 수 있으며, 그 관계는 →의 반사-전이 폐포이다. 축소 시퀀스의 시퀀스 역시 축소 시퀀스이므로(또는 동등하게, 반사-전이 폐포를 형성하는 것이 멱등적이므로), → = →이다. 따라서 →는 →가 지역적으로 합류적일 때만 합류적이다. 재작성 시스템은 (전역적으로) 합류적이지 않고도 지역적으로 합류적일 수 있다. 예시는 그림 1과 2에 나와 있다. 그러나 뉴먼의 보조정리는 지역적으로 합류적인 재작성 시스템이 무한 축소 시퀀스를 가지지 않을 때 (이 경우 종료적 또는 강하게 정규화적이라고 합니다) 전역적으로 합류적이라고 명시한다.
## 처치-로서 속성
재작성 시스템은 모든 객체 x, y에 대해 x \stackrel{*}{\leftrightarrow} y가 x\mathbin\downarrow y를 함의할 때에만 **처치-로서 속성**을 가진다고 한다. 알론조 처치와 존 버클리 로서는 1936년에 람다 대수가 이 속성을 가진다고 증명했다.Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936 그래서 이 속성의 이름이 붙었다.p=9 (람다 대수가 이 속성을 가진다는 사실은 처치-로서 정리로도 알려져 있다.) 처치-로서 속성을 가진 재작성 시스템에서 단어 문제는 공통 후계자를 찾는 것으로 축소될 수 있다. 처치-로서 시스템에서 객체는 기껏해야 하나의 정규형을 가진다. 즉, 객체의 정규형은 존재한다면 유일하지만, 존재하지 않을 수도 있다. 예를 들어 람다 대수에서 표현식 (λx.xx)(λx.xx)는 무한한 베타 축소 시퀀스 (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...가 존재하기 때문에 정규형을 가지지 않는다.page=184 재작성 시스템은 합류적일 때 필요충분조건으로 처치-로서 속성을 가진다.p=11 이 동등성 때문에 문헌에서 정의의 상당한 변형이 발견된다. 예를 들어 "Terese"에서는 처치-로서 속성과 합류성이 동의어이며 여기에 제시된 합류성 정의와 동일하게 정의된다. 여기에서 정의된 처치-로서 속성은 이름이 붙지 않지만 동등한 속성으로 주어진다. 다른 텍스트와의 이러한 차이는 의도적이다.p=11
## 준합류성
지역 합류성의 정의는 전역 합류성의 정의와 달리 주어진 요소로부터 단일 재작성 단계에서 도달한 요소만을 고려한다. 단일 단계에서 도달한 한 요소와 임의의 시퀀스에 의해 도달한 다른 요소를 고려함으로써, 우리는 준합류성이라는 중간 개념에 도달한다. a ∈ S는 a → b와 a → c인 모든 b, c ∈ S에 대해 b → d와 c → d인 d ∈ S가 존재할 때 **준합류적**이라고 한다. 모든 a ∈ S가 준합류적이면, →는 준합류적이라고 말한다. 준합류적인 요소가 반드시 합류적일 필요는 없지만, 준합류적인 재작성 시스템은 반드시 합류적이며, 합류적인 시스템은 자명하게 준합류적이다.
## 강합류성
강합류성은 재작성 시스템이 전역적으로 합류적이라고 결론내릴 수 있게 해주는 지역 합류성의 또 다른 변형이다. 원소 a ∈ S는 a → b와 a → c인 모든 b, c ∈ S에 대해 b → d와 c → d 또는 c = d인 d ∈ S가 존재할 때 **강합류적**이라고 한다. 모든 a ∈ S가 강합류적이면, →는 강합류적이라고 말한다. 합류적인 요소가 반드시 강합류적일 필요는 없지만, 강합류적인 재작성 시스템은 반드시 합류적이다.
# 합류적인 시스템의 예시
* 그뢰브너 기저로 작업하는 경우, 아이디얼 계수 다항식의 축소는 합류적인 재작성 시스템이다. * 마츠모토의 정리는 땋기 관계의 합류성에서 따르다. * λ-항의 β-축소는 처치-로서 정리에 의해 합류적이다.
# 내용주
group=note