합류성

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

합류성은 추상 재작성 시스템의 중요한 속성으로, 동일한 시작점에서 서로 다른 재작성 규칙을 적용했을 때, 최종적으로 동일한 결과에 도달할 수 있는지를 나타낸다. 산술 규칙이나 군론의 증명 과정과 같은 예시를 통해 설명되며, 국소 합류성, 준합류성, 강합류성과 같은 관련 성질이 존재한다. 합류성은 처치-로서 속성과 밀접한 관련이 있으며, 람다 계산법과 같은 시스템의 정규형을 결정하는 데 중요한 역할을 한다. 또한, 그뢰브너 기저나 마쓰모토 정리 등 다양한 분야에 응용된다.

합류성

📚 더 읽어볼만한 페이지

재작성 시스템 - 항 (논리학)
항(논리학)은 변수, 상수, 함수 기호로 재귀적으로 정의되는 구문 요소로서, 담론 영역에서 수학적 객체를 나타내며 트리 구조, 구조적 동일성, 기저항, 선형항 등의 속성을 가지고, 항 연산을 통해 부분항 대체, 깊이 측정, 패턴 매칭 등이 가능하다.
재작성 시스템 - 처치-로서 정리
처치-로서 정리는 람다 대수와 재작성 시스템에서 중요한 정리로, β-축약, η-축약 등 다양한 축약 규칙에 적용되어 특정 조건 하에서 항의 정규형이 유일함을 보장하며, 람다 계산법의 여러 변형에도 적용되어 함수형 프로그래밍의 평가와 관련된 중요한 의미를 가진다.

1. 개요
2. 동기 부여 예시
- 2.1. 산술식
- 2.2. 군론
3. 정의
4. 관련 성질

2. 동기 부여 예시

합류성의 개념을 이해하기 위해, 산술식과 군론의 예를 살펴볼 수 있다.

* 산술식: 일반적인 초등 산술 규칙은 추상적인 재작성 시스템을 형성한다. 예를 들어, (11 + 9) × (2 + 4)와 같은 표현식은 왼쪽 또는 오른쪽 괄호에서 시작하여 평가할 수 있지만, 어느 쪽을 먼저 계산하더라도 결국 동일한 결과를 얻는다. 이처럼 모든 산술 표현식이 계산 순서에 관계없이 동일한 결과로 평가되는 경우, 산술 재작성 시스템은 합류성을 가진다고 한다.

* 군론: 군론에서 각 군의 원소가 자신의 역원과 같다는 명제를 증명하는 과정은 항 재작성 시스템의 합류성을 보여주는 또 다른 예시이다. 이 증명은 주어진 군의 공리(A1, A2, A3)로부터 시작하여, 일련의 재작성 규칙(R4, R6, R10, R11, R12)을 통해 최종적으로 (a⁻¹)⁻¹ = a라는 결론을 도출한다. 각 단계는 이전 단계의 결과를 바탕으로 새로운 결과를 유도하며, 최종 결과는 재작성 순서에 관계없이 동일하다.

👆

좌우로 밀어서 보기

군 공리
A1	1 ⋅ a	= a
A2	a⁻¹ ⋅ a	= 1
A3	(a ⋅ b) ⋅ c	= a ⋅ (b ⋅ c)

2.1. 산술식

일반적인 초등 산술 규칙은 추상적인 재작성 시스템을 형성한다. 예를 들어, `(11 + 9) × (2 + 4)`라는 식은 왼쪽 또는 오른쪽 괄호에서 시작하여 평가할 수 있는데, 어느 쪽을 먼저 계산하더라도 결국 동일한 결과를 얻는다. 모든 산술 표현식이 계산 순서에 관계없이 동일한 결과로 평가되는 경우, 산술 재작성 시스템은 합류성을 가진다고 한다. 산술 재작성 시스템은 재작성 시스템의 세부 사항에 따라 합류성을 가질 수도, 가지지 않을 수도 있다.

일반적인 산술 규칙은 항 재작성 시스템으로 간주할 수 있다. 예를 들어 다음과 같은 식이 있다고 가정해 보자.

`(11 + 9) × (2 + 4)`

이 식을 계산하는 방법에는 두 가지가 있다. 왼쪽 괄호 안을 먼저 계산하거나, 오른쪽 괄호 안을 먼저 계산하는 것이다. 왼쪽 괄호 안을 먼저 계산하면 다음과 같다.

`20 × (2 + 4) = 20 × 6 = 120`

오른쪽 괄호 안을 먼저 계산하면 다음과 같다.

`(11 + 9) × 6 = 20 × 6 = 120`

이처럼 산술식은 여러 가지 방법으로 계산(재작성)할 수 있으며, 어떤 방법을 사용하든 최종 결과, 즉 정규형은 동일하다. 즉, 산술 규칙으로 구성된 항 재작성 시스템은 합류성을 가진다.

이를 항 재작성의 흐름으로 표현하면 다음과 같다.

👆

좌우로 밀어서 보기

왼쪽 계산		(11+9)×(2+4)		오른쪽 계산
	↙		↘
20×(2+4)				(11+9)× 6
	↘		↙
오른쪽 계산		20 × 6		왼쪽 계산
		↓
		120

2.2. 군론

군론에서 각 군의 원소가 자신의 역원과 같다는 명제를 증명하는 과정은 항 재작성 시스템의 합류성을 보여주는 예시이다.

👆

좌우로 밀어서 보기

군 공리
A1	1 ⋅ a	= a
A2	a⁻¹ ⋅ a	= 1
A3	(a ⋅ b) ⋅ c	= a ⋅ (b ⋅ c)

👆

좌우로 밀어서 보기

R4의 증명: a⁻¹⋅(a⋅b) = b
a⁻¹ ⋅ (a ⋅ b)
= (a⁻¹ ⋅ a) ⋅ b	A3(r)
= 1 ⋅ b	A2
= b	A1

👆

좌우로 밀어서 보기

R6의 증명: (a⁻¹)⁻¹ ⋅ 1 = a
(a⁻¹)⁻¹ ⋅ 1
= (a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ a)	A2(r)
= a	R4

👆

좌우로 밀어서 보기

**R10**의 증명: (a⁻¹)⁻¹ ⋅ b = a ⋅ b
(a⁻¹)⁻¹ ⋅ b
= (a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ (a ⋅ b))	R4(r)
= a ⋅ b	R4

👆

좌우로 밀어서 보기

**R11**의 증명: a ⋅ 1 = a
a ⋅ 1
= (a⁻¹)⁻¹ ⋅ 1	R10(r)
= a	R6

👆

좌우로 밀어서 보기

**R12**의 증명: (a⁻¹)⁻¹ = a
(a⁻¹)⁻¹
= (a⁻¹)⁻¹ ⋅ 1	R11(r)
= a	R6

주어진 군의 공리(A1, A2, A3)로부터 시작하여, 일련의 재작성 규칙(R4, R6, R10, R11, R12)을 통해 최종적으로 `(a⁻¹)⁻¹ = a`라는 결론을 도출한다. 이 과정에서 각 단계는 이전 단계의 결과를 바탕으로 새로운 결과를 도출하며, 최종 결과는 재작성 순서에 관계없이 동일하다.

3. 정의

추상 재작성 시스템 ``에서, `a`에서 `b`로의 축약(reduction)을 `a → b`, 축약의 유한 단계를 `a *→ b`로 표현한다. 합류성(Confluence)은 모든 `a, b, c ∈ A`에 대해, `a *→ b`이고 `a *→ c`이면, `b *→ d`이고 `c *→ d`인 `d ∈ A`가 존재한다는 성질이다. 즉, 어떤 항 `a`를 간략화하여 항 `b`와 `c`를 얻었다면, 반드시 `b`와 `c`로부터 공통된 항 `d`로 도달할 수 있어야 한다.

일반적인 항 쓰기 시스템에서는 특정 항을 다시 쓸 수 있는 규칙이나 다시 쓸 수 있는 부분이 여러 개 있으므로 다시 쓰기의 흐름은 한 가지가 아니다. 합류성이란, 같은 항에서 시작하는 서로 다른 쓰기 흐름에서 두 개의 항을 꺼냈을 때 항상 두 항을 같은 형태로 다시 쓸 수 있다는 것이다. 즉 임의의 항 `a`를 간략화하여 항 `b`, `c`를 얻었다면 반드시 `b`, `c`에서 합류할 수 있는 항 `d`가 존재한다는 것이다.

더 형식적으로, 추상 쓰기 계

\left\langle A, \to \right\rangle

에 대해, `a`에서 `b`로의 간략화 reduction^영어를 `a → b`, 간략화의 유한 단계를

a \overset{*} b

로 표현했을 때, 합류성의 정의는 다음과 같다.
:

\forall a,b,c\in A,\,\exists d\in A,\,a\overset{*}b \quad\text{and}\quad a\overset{*}c

\implies b\overset{*}d \quad\text{and}\quad c\overset{*}d

이것을 그림으로 표현한 것이 그림 1이다. 실선은 전칭 기호, 점선은 존재 기호를 의미하며, *는 간략화의 유한 단계를 나타낸다.

쓰기 계가 합류성을 만족할 때, 다음이 성립한다.
* 항 `a`의 정규형은 많아야 1개만 존재한다.
* 등식

a = b

가 성립한다면, 적당한 항 `c`가 존재하여

a \overset{*} c

이고

b \overset{*} c

이다.

정규형이 많아야 한 개라는 점을 가리켜 "다시 쓰기 순서에 관계없이 결과가 유일하게 정해진다"라고 말하는 경우가 있지만, 애초에 정규형에 도달하는 것이 가능한지(즉, 해당 순서에서 다시 쓰기의 "결과"라고 할 수 있는 것이 존재하는지)는 다시 쓰기 순서에 따라 변동될 수 있으므로, 엄밀히 말하면 오해를 불러일으킬 수 있다. 항상 유일한 결과가 있다고 하기 위해서는 "결과"의 정의에 더하여 강 정규성 등의 성질이 추가로 필요하다.

4. 관련 성질

합류성과 관련된 성질로는 국소 합류성, 준 합류성, 강 합류성, 처치-로서 성질 등이 있다.

4.1. 처치-로서 성질 (Church-Rosser Property)

Church-Rosser property^영어이란, 추상 재작성 시스템 $\left\langle A, \to \right\rangle$ 의 임의의 $a,\,b \in\,A$ 에 대하여 $a \overset{*}{}\leftrightarrow{} b$ 라면 $a\,\overset{*}{}\to{}c \quad\text{and}\quad b\,\overset{*}{}\to{}c$ 가 되는 c가 존재하는 것이다. 여기서 $a \overset{*}{}\leftrightarrow{} b$ 는 a와 b 각각의 방향으로 유한 단계 내에 축약될 수 있음을 나타낸다.

처치-로서 성질은 합류성과 동치이다. 처치-로서 성질은 람다 계산에서의 베타 축약의 합류성을 나타내는 처치-로서 정리에 사용되었다.

4.2. 국소 합류성 (Local Confluence)

요소 a^영어 ∈ A^영어가 국소 합류성 (Local confluence^영어)을 가진다는 것은, $c\,\leftarrow\,a\,\rightarrow\,b$ 가 되는 임의의 b^영어, c^영어 ∈ A^영어에 대해 $c\,\overset{*}d\,\overset{*}b$ 가 되는 d가 존재한다는 것이다.

국소 합류성은 약 합류성 (Weak confluence^영어) 또는 약 처치-로서 성질 (Weak Church-Rosser property^영어)이라고도 불린다.

국소 합류성은 합류성보다 약한 성질이다. 모든 요소가 국소 합류성을 가질 경우에도, 재작성 규칙에 루프가 포함된 경우 등에는 시스템 전체의 합류성이 성립하지 않을 수 있다.

하지만, 시스템이 종결성과 국소 합류성을 모두 가질 경우, 시스템은 합류성을 가진다. (뉴먼 보조정리, Newman's lemma^영어)

4.3. 준합류성 (Semi-Confluence)

Semi-confluence^영어 요소 $a$ 가 준합류성을 가진다는 것은, $c\,\leftarrow\,a\,\overset{*}\rightarrow\,b$ 가 되는 임의의 $b, c$ 에 대해 $c\,\overset{*}d\,\overset{*}b$ 가 되는 $d$ 가 존재한다는 것이다.

모든 요소가 준합류성을 가진다면, 시스템은 합류성을 가진다.

4.4. 강합류성 (Strong Confluence)

요소 가 강합류성을 가진다는 것은, 가 되는 임의의 에 대해 가 되는 d가 존재한다는 것이다. 여기서 는 또는 중 하나가 성립함을 나타낸다.

모든 요소가 강합류성을 가지면, 시스템은 합류성을 가진다. 강합류성은 다음의 정리를 함께 사용할 수 있다.

추상 재작성 시스템 , 에서 이고 가 강합류성을 가지면, 는 합류성을 가진다.