구조 유도

Structural induction

구조 귀납은 수학 논리(예: ł'정리의 증명), 컴퓨터 과학, 그래프 이론 및 기타 수학 분야에서 사용되는 증명 방법입니다.자연수에 대한 수학적 귀납의 일반화이며 임의의 노에테르 유도로 더욱 일반화 될 수 있다.구조 재귀는 일반적인 수학적 귀납에 대한 일반적인 재귀와 동일한 관계를 갖는 재귀 방법입니다.

구조 유도는 공식, 목록 또는 나무와 같은 어떤 종류의 재귀적으로 정의된 구조의 모든 x에 대해 어떤 명제 P(x)가 유지된다는 것을 증명하기 위해 사용된다.구조(수식의 경우 하위 형식, 리스트의 경우 하위 목록, 트리의 경우 하위 트리)에 충분한 근거가 있는 부분 순서가 정의됩니다.구조적 유도 증명은 제안이 모든 최소 구조에 대해 유지된다는 증거이며, 만약 그것이 특정 구조 S의 직접적인 하부 구조에 대해 유지된다면, 그것은 또한 S에 대해서도 유지되어야 한다. (공식적으로 말하면, 이것은 이 두 조건이 충분하다고 주장하는 잘 근거가 있는 유도의 공리의 전제를 만족시킨다.)제안서가 모든 x에 대해 유지되도록 하기 위해 필요합니다.

구조 재귀 함수는 동일한 아이디어를 사용하여 재귀 함수를 정의합니다. "기본 케이스"는 각 최소 구조와 재귀 규칙을 처리합니다.구조적 재귀는 대개 구조적 유도에 의해 정확함을 증명합니다. 특히 쉬운 경우, 유도 단계는 종종 생략됩니다.다음 예의 길이 및 ++ 함수는 구조적으로 재귀적입니다.

예를 들어 구조체가 목록인 경우 보통 부분 순서 "<"를 도입합니다. 순서에서는 목록 L이 목록 M의 끝일 때마다 L < M이 됩니다.이 순서에서는 빈 리스트[ ]가 일의의 최소 요소입니다.다음으로 어떤 제안 P(L)의 구조적 유도 증명은 두 부분으로 구성됩니다. 즉, P([])가 참이라는 증명과 P(L)가 어떤 리스트 L에 대해 참이고 L이 리스트 M의 꼬리일 경우 P(M)도 참이어야 합니다.

결국 함수 또는 구조가 어떻게 구성되어 있는지에 따라 둘 이상의 베이스 케이스 및/또는 둘 이상의 유도 케이스가 존재할 수 있습니다.그런 경우, 일부 제안서 P(l)의 구조적 유도 증명은 다음과 같이 구성된다.

  1. 각 베이스 케이스 BC에 대해 P(BC)가 참이라는 증거
  2. 어떤 인스턴스 I에 대해 P(I)가 참이고, 어떤 하나의 재귀 규칙을 한 번 적용함으로써 I로부터 M을 얻을 수 있다면 P(M)도 참이어야 한다는 증거입니다.

5대에 걸쳐 31명의 인물을 보여주는 고대 조상수

조상 트리는 일반적으로 알려진 데이터 구조이며, 알려진 한 개인의 부모, 조부모 등을 보여줍니다(예는 그림 참조).이는 재귀적으로 정의됩니다.

  • 가장 간단한 경우, 조상나무는 한 사람만을 보여준다(부모에 대해 아무것도 알려지지 않은 경우).
  • 또는, 조상 나무는 한 명의 사람과 가지에 의해 연결된 그들의 부모의 두 개의 조상 하위 트리를 보여준다(둘 중 하나가 알려진 경우, 둘 다라는 간단한 가정을 증명하기 위해 사용).

예를 들어, "g세대에 걸쳐 확장된 조상 나무는 최대g 2 - 1명의 사람을 나타낸다" 속성은 다음과 같이 구조적 유도에 의해 입증될 수 있다.

  • 가장 단순한 경우, 트리는 한 명의 사람, 즉 한 세대를 나타냅니다. 이러한 트리에 대한 속성은 1 ÷ 2 - 1이므로1 참입니다.
  • 대신, 이 나무는 한 사람과 그들의 부모님의 나무를 보여준다.후자 각각은 전체 나무의 하위 구조이기 때문에 입증할 특성을 충족한다고 가정할 수 있다(유도 가설).즉, p 2g 2 - 1과 q 2h 2 - 1을 가정할 수 있다. 여기g와 h는 각각 아버지와 어머니의 하위 트리가 확장되는 세대 수를 나타내며 p와 q는 이들이 나타내는 사람의 수를 나타낸다.
    • g h h의 경우, 전체 트리는 1 + h 세대에 걸쳐 확장되며 p + qg + 1 ( (2 - 1h) + 1 2hh 2 + 2 - 1 1 2 + 2 - 1 = 21+h - 1을 나타낸다. 즉, 전체 트리가 특성을 만족한다.
    • h g g의 경우 전체 트리가 1 + g 세대에 걸쳐 확장되며 유사한 추론에 의해 p + q + 1 21 + g 2 - 1 인물을 나타낸다. 즉, 이 경우에도 전체 트리가 특성을 만족한다.

따라서 구조유도에 의해 각 조상목은 그 특성을 만족시킨다.

또 다른 형식적인 예로서 다음 목록의 속성을 고려하십시오.

길이(L + + M) = 길이 L + 길이 M [EQ]

여기서 ++는 목록 연결 작업을 나타내고 L과 M은 목록입니다.

이를 증명하기 위해서는 길이와 연결 연산에 대한 정의가 필요합니다.(h:t)는 머리(첫 번째 요소)가 h이고 꼬리(남은 요소 목록)가 t인 목록을 나타내고 []는 빈 목록을 나타냅니다.길이 및 연결 연산의 정의는 다음과 같습니다.

길이 [] = 0 [LEN1] 길이 (h:t) = 1 + 길이 t [LEN2]
[ ] + + list = list [ APP 1 ] ( h : t ) + + list = h : ( t + + list ) [ APP 2 ]

우리의 제안 P(l)는 L이 L일모든 목록 M에 대해 EQ가 참이라는 것이다.모든 목록 l에 대해 P(l)가 참임을 보여주고 싶습니다.우리는 리스트에서 구조적 유도를 통해 이것을 증명할 것이다.

우선 P([])가 참임을 증명합니다.즉, L이 빈 리스트일 경우 EQ는 모든 리스트 M에 대해 참입니다.EQ를 고려합니다.

길이(L ++M) = 길이([] ++M) = 길이 M(APP1) = 0 + 길이 M = 길이 [] + 길이 M(LEN1) = 길이 L + 길이 M

그래서 정리의 이 부분은 증명되었다. 왼쪽과 오른쪽이 같기 때문에 L이 []일 EQ는 모든 M에 대해 참이다.

다음으로 비어 있지 않은 목록 I을 고려합니다.저는 비어있지 않기 때문에 헤드 아이템 x와 테일 리스트 xs가 있기 때문에 (x:xs)로 표현할 수 있습니다.유도 가설은 L이 xs일 M의 모든 값에 대해 EQ가 참이라는 것입니다.

길이(표준 + + M) = 길이 xs + 길이 M(표준)

이러한 경우, L = I = (x:dism)일 때 M의 모든 값에 대해서도 EQ가 참임을 보여주고 싶다.이전과 같이 진행됩니다.

길이 L + 길이 M = 길이 (x:420) + 길이 M = 1 + 길이 xs + 길이 M (LEN2 기준) = 1 + 길이 (가설 기준) = 길이 (x: (420 + M) = 길이 (x:420) + M (APP2 기준)= 길이(L ++ M)

따라서 구조적 유도로부터 모든 목록 L에 대해 P(L)가 참이라는 것을 알 수 있다.

순서부여

표준 수학 귀납이 정렬 원리와 같듯이 구조 귀납도 정렬 원리와 같습니다.특정 종류의 모든 구조 집합이 충분한 근거가 있는 부분 순서를 허용하는 경우, 비어 있지 않은 모든 부분 집합은 최소 요소를 가져야 합니다(이것은 "근거가 충분한" 정의입니다).이 맥락에서 이 보조법칙의 의의는 증명하고 싶은 정리에 반례가 있다면 최소한의 반례가 있어야 한다는 것을 추론할 수 있게 해준다는 것이다.만약 우리가 최소 반례의 존재를 더 작은 반례를 암시할 수 있다면, 우리는 모순을 가지고 있습니다. 그래서 반례의 집합은 비어 있어야 합니다.

이런 유형의 인수 예시로 모든 이진 트리 집합을 고려하십시오.전체 이진 트리의 잎 수가 내부 노드 수보다 1개 더 많다는 것을 보여 줍니다.예를 들어 반례가 있다고 가정하면 가능한 한 최소의 내부 노드 수를 가진 반례가 존재해야 합니다.이 반례 C에는 n개의 내부 노드와 l있으며, 여기 n + 1 µ l이 있습니다. 또한, C는 중요하지 않아야 합니다. 왜냐하면 사소한 트리는 n = 0l = 1이므로 반례가 아니기 때문입니다.따라서 C는 부모 노드가 내부 노드인 적어도1개의 리프를 가진다.트리에서 이 리프와 상위 노드를 삭제하여 리프 형제 노드를 상위 노드가 이전에 사용하던 위치로 승격합니다.이것은 n과 l을 모두 1로 줄여주므로 새 트리는 n + 1 µ l을 가지므로 더 작은 반례가 됩니다.그러나 가설에 따르면, C는 이미 가장 작은 반례 사례였다. 따라서, 처음부터 반례가 있었다는 가정은 틀렸을 것이다.여기서 'smaller'가 암시하는 부분순서는 S가 T보다 노드 수가 적을 마다 S < T라고 하는 순서입니다.

「 」를 참조해 주세요.

레퍼런스

  • Hopcroft, John E.; Rajeev Motwani; Jeffrey D. Ullman (2001). Introduction to Automata Theory, Languages, and Computation (2nd ed.). Reading Mass: Addison-Wesley. ISBN 978-0-201-44124-6.
  • YouTube의 "수학 논리 - 비디오 01.08 - 일반화 (구조적) 유도"

구조적 유도에 관한 초기 출판물은 다음과 같다.