타르스키 고정점 정리

순서론에서 타르스키 고정점 정리() 또는 크나스터-타르스키 정리()는 완비 격자에서 자신으로 가는 단조함수의 고정점이 존재한다는 정리이다.

이는 이론 컴퓨터 과학의 형식 의미론 및 추상 해석 분야에서 중요한 정리이다.

 정의 
완비 격자 과 단조함수 가 주어졌다고 하자. 타르스키 고정점 정리에 따르면, 의 고정점의 집합

역시 완비 격자를 이룬다. (그러나, 가 의 부분 격자일 필요는 없다. 즉, 에서의 상한과 하한은 에서와 일치하지 않을 수 있다.) 특히, 의 최대 고정점과 최소 고정점이 존재하며, 특히 는 적어도 하나의 고정점을 갖는다. 또한, 의 최대·최소 고정점은 각각 다음과 같이 주어진다.

 증명 
타르스키를 따라, 다음 순서대로 증명한다.
 (가) 는 의 최대 고정점이다.
 (나) 는 의 최소 고정점이다.
 (다) 는 완비 격자이다.
명제 (가)의 증명. 라고 하자. 임의의 에 대하여, 이므로, 이다. 따라서 이다. 반대로, 이므로, 의 정의에 따라 이다. 따라서 이다. 따라서, 은 의 고정점이다. 모든 고정점은 에 속하므로, 은 의 최대 고정점이다.

명제 (나)의 증명. 의 반대 격자 를 생각하자. 역시 완비 격자를 이루며, 는 위에서도 단조함수이다. 따라서 에 대하여 명제 (가)가 성립한다. 이는 정확히 에 대한 명제 (나)와 일치한다.

명제 (다)의 증명. 가 의 임의의 부분 집합이라고 하자. 에서 의 상한이 존재함을 보이면 충분하다. 의 에서의 상한 를 생각하자. 그렇다면 구간 는 의 상계의 집합이며, 완비 격자를 이룬다 (이는 부분 격자이기도 하지만, 부분 완비 격자가 아닐 수 있다). 임의의 에 대하여 이므로, 이다. 에 대하여, 만약 라면, 이다. 따라서, 를 위의 함수 로 여길 수 있다. 명제 (나)에 따라, 의 최소 고정점이 존재한다. 이는 의 고정점이며, 의 상계가 되는 가장 작은 의 고정점이다. 다시 말해, 의 에서의 상한이다.

 고정점 집합이 부분 격자가 아닌 경우 
고정점 집합은 완비 격자이지만, 부분 격자가 아닐 수 있다. 예를 들어, 다음과 같은 부분 순서 집합을 생각하자.

그렇다면, 은 완비 격자를 이룬다. 이제 이며

라고 하자. 는 위의 단조함수이며, 와 은 의 고정점이지만, 는 의 고정점이 아니다. (와 의 에서의 상한은 가 아닌 이다.) 따라서, 는 의 부분 격자가 아니다.

 귀결 
완비 격자는 공집합일 수 없으므로, 이 정리는 상기한 에 적어도 한개의 고정점이 있음을, 나아가서 최소 고정점이 있음을 보장한다.

조건을 추가하여 임의의 부분 순서 집합에 대하여 유사한 결과를 증명할 수 있다. 이를 동역학계 이론에 적용하여 프랙탈의 일종인 반복함수계(iterated function system) 연구에 사용할 수 있다.

모든 증가수열 에 대해 이면, 의 최소 고정점은 이며, 이는 정리의 구성적 버전(Kleene fixed-point theorem)을 제공한다.

이론 컴퓨터 과학에서, 단조함수에 대한 최소 고정점 정리는 프로그램 의미론을 정의하는 데 사용된다. 이 경우 특히 격자 L을 특정 집합의 모든 부분집합들을 모은 것, 즉 멱집합 격자로 가정하는 특수한 케이스에 대하여 집중하는 것이 일반적이다. 그리고 나서 f의 고정점이 되기 위해 필요한 조건을 가지는 최소의 집합을 찾아낸다.

 역 
반대로, 모든 단조함수의 고정점이 존재하는 격자는 완비 격자이다. 즉, 타르스키 고정점 정리는 완비 격자의 정의로 삼을 수 있다. 그러나 모든 단조함수가 고정점이 존재하는 부분 순서 집합은 완비 격자일 필요가 없다.

 역의 증명 
격자 이 완비 격자 위에 항상 고정점이 없는 단조함수 를 구성하면 족하다. 두 부분 집합 에 대하여, 다음 조건들을 생각하자.
 (라) 는 정렬 전순서 집합이다.
 (마) 의 반대 순서 집합 는 정렬 전순서 집합이다.
 (바) 임의의 및 에 대하여, 
 (사) 동시에 의 상계이자 의 하계인 의 원소가 존재하지 않는다.
만약 와 가 위 조건들을 만족시킨다면, 함수

는 단조함수이며, 고정점이 존재하지 않는다. 따라서, 조건 (라)~(사)를 만족시키는 와 를 찾는 것으로 족하다. 모든 부분 집합의 상한이 존재하는 부분 순서 집합은 완비 격자이므로, 상한이 없는 의 부분 집합 가 존재한다. 편의상 그 크기 가 최소라고 하자. 이 격자이므로, 은 0이거나 무한 기수이다. 이제, 임의의 순서수 에 대하여, 의 크기는 미만이므로, 상한

이 존재한다. 는 단조 초한 점렬이지만, 순단조가 아닐 수 있다. 중복된 항을 제거하여 순단조 초한 점렬 로 만들자 (길이가 인 것은 의 최소성을 사용하여 보일 수 있다). 이 경우, 는 정렬 전순서 집합이다. 만약 의 상한이 존재한다면, 이는 의 상한이 되어 모순이 일어난다. 따라서 의 상한이 존재하지 않는다. 의 상계들로 구성된 순감소 초한 점렬들의 집합 위에 다음과 같은 부분 순서를 주자.

즉, 끝에 항을 추가하면 더 큰 초한 점렬을 얻는다. 초른 보조정리에 따라, 이 부분 순서에 따른 극대 원소 가 존재한다 (가 기수일 필요는 없다). 의 반대 순서 집합 은 정렬 전순서 집합이다. 만약 가 존재한다면, 역시 의 상계이다. 의 상한이 존재하지 않으므로, 인 의 상계 가 존재한다. 이 경우, 는 의 상계이며, 이다. 이는 의 극대성과 모순이다. 따라서, 의 하한 역시 존재하지 않는다. 이제, 와 에 대하여 조건 (사)를 증명하는 일만 남았다. 귀류법을 사용하여, 이 의 상계이자 의 하계라고 하자. 그렇다면, 의 극대성에 따라 이다. 따라서 는 의 하한이며, 이는 모순이다.

 일반화 
격자 의, 공집합이 아닌 두 부분 격자 , 에 대하여, 다음과 같은 이항 관계를 정의하자.

특히, 만약 이라면, 임의의 에 대하여, 인 이 존재하며, 마찬가지로 임의의 에 대하여, 인 이 존재한다. 즉, 이며 이다. 이 이항 관계는 공집합이 아닌 부분 격자의 집합 위의 부분 순서를 이룬다. 의 원소는 자연스럽게 의 부분 격자로 여길 수 있다. 이 경우, 부분 격자의 순서는 원소의 순서를 확장한다. 따라서, 아래의 정리는 타르스키 고정점 정리를 일반화한다.

다음이 주어졌다고 하자.
 완비 격자 
 단조함수 . 여기서 은 의 부분 완비 격자의, 위에서 정의한 순서에 따른 부분 순서 집합이다. (부분 완비 격자는 완비 격자인 부분 격자보다 더 강한 개념이다. 전자는 모든 상한과 하한이 원래 격자와 일치하지만, 후자는 모든 유한 집합의 상한·하한의 일치만을 요구한다.)
그렇다면, 의 고정점 집합

은 완비 격자를 이룬다. 또한, 의 최대·최소 고정점은 다음과 같다.

 일반화의 증명 
타르스키 고정점 정리의 증명과 유사하게, 다음 네 명제를 보인다. 이들 가운데 명제 (아)와 (자), 명제 (차)와 (카)는 서로 쌍대이므로 하나씩만 증명하여도 좋다.
 (아) 에 대하여, 은 의 최대 고정점이다.
 (자) 에 대하여, 은 의 최소 고정점이다.
 (차) 모든 의 에서의 상한이 존재한다.
 (카) 모든 의 에서의 하한이 존재한다.
명제 (아)의 증명. 이므로, 이면 충분하다. 임의의 가 주어졌다고 하자. 의 정의에 따라, 이며 라고 하자. 이며 가 단조함수이므로, 이며 라고 하자. 이 부분 완비 격자이므로, 이다. 임의의 에 대하여 이므로, 이다. 의 단조성에 따라, 인 가 존재한다. 즉, 이며, 따라서 이다. 따라서, 은 의 고정점이 맞다.

명제 (차)의 증명. 가 의 에서의 상한이라고 하자. 그렇다면, 은 완비 격자를 이룬다. 임의의 에 대하여, 이며 이므로, 인 가 존재한다. 이 경우, 이며 이다. 따라서, 의 단조성에 의하여, 만약 라면, 은 공집합이 아니다. 또한, 는 의 부분 완비 격자이다. 따라서, 는 의 부분 완비 격자를 이룬다. 즉, 는 단조함수 를 정의한다. 명제 (자)에 따라, 의 최소 고정점이 존재하며, 이는 의 에서의 상한이다.

 역사 
섬네일|브로니스와프 크나스터 (1893~1980)
섬네일|알프레트 타르스키 (1901~1983)
1927년 브로니스와프 크나스터()와 알프레트 타르스키가 멱집합 격자 위 단조함수의 고정점의 존재를 증명하였다. 타르스키 고정점 정리의 오늘날 형태는 1939년 타르스키가 도입하였으며, 1939년~1942년 동안 타르스키의 몇몇 공개 강의에서 소개되었다. 타르스키 고정점 정리의 역은 앤 모렐()이 증명하였다. 타르스키 고정점 정리의 다중 값 일반화는 저우린()이 초모듈러 게임()의 내시 균형의 존재를 보이기 위하여 증명 및 사용하였다.

 같이 보기 
 고정점 정리
 완비 격자

 참고 문헌 

 외부 링크 
 

분류:격자 이론
분류:고정점 정리