Copyright (c) 2016-, All Rights Reserved by Kwanghoon Choi
(아래 내용을 자유롭게 이용하되 다른 웹 사이트 등을 통한 배포를 금합니다.)
인덕션을 사용한 증명은 꽤 익숙하지만, 코인덕션을 사용한 증명은 난해하다. 이 메모를 통해 인덕션과 코인덕션의 원리를 이해해보려 한다.
1. 인덕션과 코인덕션의 수학적 정의 (벤자민 피어스의 <타입과 프로그래밍언어> 책의 21.1절에서)
전체 집합(universal set) U를 가정하자.
[정의] 함수 F \in P(U) -> P(U)가 아래와 같은 성질을 만족하면 단조증가(monotone)한다고 정의한다.
- X \subseteq Y 이면 F(X) \subseteq F(Y)이다.
이후에 언급된 F는 P(U)에 대한 단조증가 함수라고 가정하자. F를 생성함수(generating function)라 부른다.
[정의] X는 U의 부분집합이라고 가정할 때,
- F(X) \subseteq X이면, X는 F에 관해 닫혀있는(F-closed)는 집합이라고 정의하고,
- X \subseteq F(X)이면, X는 F에 관해 일관성이 있는(F-consistent) 집합이라고 정의하며,
- F(X) = X이면, X는 F의 고정점(fixed point)라고 정의한다.
[정리] Knaster-Tarski (Tarski 1955)
- 모든 F 닫힘 집합들의 교집합은 F의 최소 고정점이고,
- 모든 F 일관성 집합들의 합집합은 F의 최대 고정점이다.
[정의] F의 최소 고정점을 \mu F, 최대 고정점을 \nu F라고 정의한다.
[따름 정리]
- 인덕션 원리(Principle of induction) : 만일 X가 F에 관해 닫혀 있다면 \mu F \subseteq X이다.
- 코인덕션 원리(Principle of coinduction) : 만일 X가 F에 관해 일관성이 있다면 X \subseteq \nu F이다.
2. 인덕션 원리의 일반적인 서술과 비교
우리가 아는 인덕션 원리는 보통 이렇게 서술한다. 어떤 술어 명제 P가 존재해서, P(0)가 참이고, 또한 P(i)가 참이면 P(i+1)이 참임을 보일 수 있다면 모든 자연수 i에 대해 P(i)는 참이다. 위의 따름 정리와 연관시켜 설명해본다.
전체 집합 U를 자연수의 집합인 예를 살펴보자. 어떤 명제 P (U의 부분 집합)가 있어서 P(0)이 참이고 P(i)가 참이면 P(i+1)이 참이라고 하자. 생성함수 F를 다음과 같이 정의한다.
- F(X) = { 0 } U { i+1 | i \in X }
F의 정의에 의해 F(P) \subseteq P이다. 왜냐하면,
- F(P)에 0이 포함되어 있는데, P(0)은 참이므로 0 \in P이다.
- 만일 P에 i가 포함되어 있다면 F(P)에 i+1이 포함된다. P(i)가 참이면 P(i+1)도 참이므로 i+1 \in P이다.
이 결과, P는 F에 관해 닫혀있(는 집합이)다. 따름 정리에 의하면
- \mu F \subseteq P
모든 자연수 (\mu F)가 P에 포함되어 있으므로, 인덕션에 의해 모든 자연수 n에 대해 항상 P가 성립함을 보였다.
인덕션 원리에서 주어진 명제가 F에 대해 닫혀있음을 보이는 과정이 우리가 일반적으로 인덕션 원리를 적용해서 증명하는 과정과 일치한다.
3. 코인덕션 원리를 적용한 간단한 증명 예
따름 정리의 코인덕션 원리를 사용하는 증명 방법은
- \nu F (코인덕티브 방식으로 정의한 집합, coinductively defined set)에 어떤 원소 x가 포함되는지를 보이기 위해서
- x를 포함하는 집합 X가 F에 관하여 일관성이 있음으로 보이면 된다.
간단한 오토마타 A = (q0, Q, F, R)을 가정하자. Q는 q0를 포함한 상태 집합, F는 Q의 부분집합으로 최종 상태, R은 Q x Q의 부분집합으로 전이 규칙을 전이한다.
주어진 오토마타가 무한한 전이를 반복할 수 있음을 증명하는 문제를 코인덕션 원리를 가지고 증명해보자. 오토마타의 전이는 다음의 문법으로 생성되는 상태 나열(state sequence)로 표현한다.
Trace ::= q0 | Trace . q
주어진 오토마타 A에 대해, 무한한 전이를 표현하는 생성함수 F를 다음과 같이 정의한다.
- F :: P(Trace) -> P(Trace)
- F(X) = { t . q | t \in X, ( laststate(t), q ) \in R, q \not\in F }
\nu F는 무한한 전이들의 모두 모아놓은 집합이다. (왜냐하면, F 일관성을 갖는 집합을 모두 합해 놓았기 때문이다.)
오토마타 A0 = ( q0, {q0}, {}, { (q0, q0) } )는 직관적으로 무한히 반복되는 전이를 갖고 있다. 이를 코인덕션 원리로 증명한다.
- X를 { q0 . q0 . .... }라고 하자. 즉 q0가 무한히 반복되는 원소를 하나 가지고 있는 집합이다.
- X \subseteq F(X)이다. X에 있는 무한 전이 끝에 q0를 붙여도 동일한 무한 전이가 되기 때문이다.
- 집합 X는 F에 관해 일관성이 있으므로, 코인덕션 원리에 의해 X \subseteq \nu F이다.
- \nu F는 A0의 모든 무한 전이를 포함하는 집합이므로 A0가 무한 전이를 포함하고 있음을 증명하였다.
코인덕션 원리로 표현하기 편리한 성질이 있다. 무한한 전이를 포함한다는 것은 이러한 성질의 한가지 사례이다. 인덕션 원리의 경우 X의 원소 수가 무한한 것은 허용하지만, 원소 자체가 무한한 성질을 가지고 있지 못한다. 따라서 이 오토마타 증명 예제의 경우 코인덕션 원리로 증명하는 것이 더 용이하다.
4. 인덕션 원리과 코인덕션 원리의 표현력의 관계
인덕션 원리로 증명할 수 없는 것을 코인덕션 원리로 증명하거나 혹은 반대의 경우가 된는 명제가 있을까? H교수에 의하면 코인덕션 원리로 증명할 수 있는 것은 인덕션 원리로 증명할 수 있다고 한다. 그러나 증명이 복잡해진다고 한다. 이를 간단하게 설명할 수 있을까? 무한히 반복되는 것을 함수로 인코딩해서 표현하는 기법을 응용해야할 수도 있겠다.
[ Help !!! ]