최소 고정점

수학의 한 분야인 순서론에서 부분 순서 집합("포셋"으로 줄여서)에서 자기 자신으로 가는 함수의 최소 고정점(least fixed point, lfp 또는 LFP, 때로는 가장 작은 고정점)은 포셋의 순서에 따라 다른 모든 고정점보다 작은 고정점이다. 함수는 최소 고정점을 가질 필요는 없지만, 만약 가진다면 그 최소 고정점은 유일하다.
예시
[편집]실수에 대한 일반적인 순서에서, 실수 함수 f(x) = x2의 최소 고정점은 x = 0이다 (다른 유일한 고정점은 1이고 0 < 1이기 때문이다). 대조적으로, f(x) = x + 1은 고정점이 전혀 없으므로 최소 고정점이 없으며, f(x) = x는 무한히 많은 고정점을 가지지만 최소 고정점은 없다.
가 유향 그래프이고 가 정점이라고 하자. 에서 접근 가능한 정점의 집합은 함수에 대한 최소 고정점으로 정의할 수 있으며, 이 함수는 로 정의된다. 에서 공동 접근 가능한 정점의 집합은 유사한 최소 고정점으로 정의된다. 의 강한 연결 요소는 이 두 최소 고정점의 교집합이다.
가 문맥 자유 문법이라고 하자. 빈 문자열 을 생성하는 기호의 집합 는 함수 의 최소 고정점으로 얻을 수 있으며, 이 함수는 로 정의되며, 여기서 는 의 멱집합을 나타낸다.
응용
[편집]많은 고정점 정리는 최소 고정점을 찾는 알고리즘을 제공한다. 최소 고정점은 종종 임의의 고정점이 갖지 않는 바람직한 특성을 갖는다.
표시적 의미론
[편집]
컴퓨터 과학에서 표시적 의미론 접근 방식은 주어진 프로그램 텍스트에서 그 의미론이라고 불리는 해당 수학적 함수를 얻기 위해 최소 고정점을 사용한다. 이를 위해 예외적인 값 "정의되지 않음"을 나타내는 인공적인 수학적 객체 가 도입된다.
예를 들어, 프로그램 데이터 형식 int
가 주어지면, 그 수학적 대응물은 으로 정의되며, 그림과 같이 각 에 대해 을 정의하고, 두 개의 서로 다른 멤버 는 에 대해 비교할 수 없도록 정의함으로써 부분 순서 집합이 된다.
프로그램 정의 int f(int n){...}
의 의미론은 어떤 수학적 함수 이다. 프로그램 정의 f
가 특정 입력 n
에 대해 종료되지 않는다면, 이는 수학적으로 으로 표현될 수 있다. 모든 수학적 함수의 집합은 각 에 대해 관계가 성립할 때, 즉 이 보다 덜 정의되거나 같을 때 를 정의함으로써 부분 순서가 된다. 예를 들어, 식 x+x/x
의 의미론은 x+1
의 의미론보다 덜 정의되는데, 전자는 후자와 달리 을 으로 매핑하고, 그 외에는 일치하기 때문이다.
어떤 프로그램 텍스트 f
가 주어지면, 그 수학적 대응물은 f
를 "번역"하여 얻을 수 있는 함수에서 함수로의 어떤 매핑의 최소 고정점으로 얻어진다.
예를 들어, C 정의
int fact(int n) { if (n == 0) return 1; else return n * fact(n-1); }
는 다음과 같은 매핑으로 번역된다
- 로 정의된다.
매핑 는 fact
가 재귀적으로 정의되었음에도 불구하고 비재귀적으로 정의된다.
예제에서 충족되는 특정 제약 조건(클레이니 고정점 정리 참조) 하에서, 는 반드시 최소 고정점 를 가지며, 이는 모든 에 대해 이다.[1]
다음과 같이 나타낼 수 있다.
의 더 큰 고정점은 예를 들어 함수이며, 다음과 같이 정의된다.
그러나 이 함수는 음수 에 대한 위 프로그램 텍스트의 동작을 정확하게 반영하지 않는다. 예를 들어, fact(-1)
호출은 전혀 종료되지 않으며, 0
을 반환하지도 않는다.
오직 최소 고정점인 만이 수학적 프로그램 의미론으로 합리적으로 사용될 수 있다.
서술 복잡도
[편집]이머만[2][3] 과 바르디[4] 는 독립적으로 서술 복잡도 결과를 보여주었는데, 선형으로 순서화된 구조의 다항 시간 계산 가능한 속성은 FO(LFP), 즉 최소 고정점 연산자가 있는 1차 논리로 정의 가능하다는 것이다. 그러나 FO(LFP)는 비순서 구조의 모든 다항 시간 속성(예를 들어 구조가 짝수 크기를 갖는다는 것)을 표현하기에는 너무 약하다.
최대 고정점
[편집]함수의 최대 고정점은 최소 고정점과 유사하게, 포셋의 순서에 따라 다른 모든 고정점보다 큰 고정점으로 정의할 수 있다. 컴퓨터 과학에서 최대 고정점은 최소 고정점보다 훨씬 덜 일반적으로 사용된다. 특히, 도메인 이론에서 발견되는 포셋은 보통 최대 원소를 갖지 않으므로, 주어진 함수에 대해 여러 개의 서로 비교 불가능한 극대 고정점이 있을 수 있으며, 해당 함수의 최대 고정점은 존재하지 않을 수도 있다. 이 문제를 해결하기 위해, 최적 고정점은 다른 모든 고정점과 호환되는 가장 잘 정의된 고정점으로 정의되었다. 최적 고정점은 항상 존재하며, 최대 고정점이 존재한다면 그것이 최대 고정점이다. 최적 고정점은 최소 고정점으로는 수렴하지 않는 재귀 및 공동재귀 함수의 형식적 연구를 가능하게 한다.[5] 불행히도, 클레이니 재귀 정리가 최소 고정점이 효과적으로 계산 가능함을 보여주는 반면, 계산 가능 함수의 최적 고정점은 비계산 함수일 수 있다.[6]
같이 보기
[편집]각주
[편집]- ↑ C.A. Gunter; D.S. Scott (1990). 〈Semantic Domains〉. Jan van Leeuwen. 《Formal Models and Semantics》. Handbook of Theoretical Computer Science B. Elsevier. 633–674쪽. ISBN 0-444-88074-7. Here: pp. 636–638
- ↑ N. Immerman, Relational queries computable in polynomial time, Information and Control 68 (1–3) (1986) 86–104.
- ↑ Immerman, Neil (1982). 〈Relational Queries Computable in Polynomial Time〉. 《STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing》. 147–152쪽. doi:10.1145/800070.802187. Revised version in Information and Control, 68 (1986), 86–104.
- ↑ Vardi, Moshe Y. (1982). 〈The Complexity of Relational Query Languages〉. 《STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing》. 137–146쪽. doi:10.1145/800070.802186.
- ↑ Charguéraud, Arthur (2010). 〈The Optimal Fixed Point Combinator〉 (PDF). 《Interactive Theorem Proving》. Lecture Notes in Computer Science 6172. 195–210쪽. doi:10.1007/978-3-642-14052-5_15. ISBN 978-3-642-14051-8. 2021년 10월 30일에 확인함.
- ↑ Shamir, Adi (October 1976). 《The fixedpoints of recursive definitions》 (Ph.D. thesis) (영어). Weizmann Institute of Science. OCLC 884951223. Here: Example 12.1, pp. 12.2–3
참고 자료
[편집]- Immerman, Neil. Descriptive Complexity, 1999, Springer-Verlag.
- Libkin, Leonid. Elements of Finite Model Theory, 2004, Springer.