최소 고정점

17/2이다. 수학의 한 분야인 순서론에서 부분 순서 집합("포셋"으로 줄여서)에서 자기 자신으로 가는 함수의 **최소 고정점**(least fixed point, **lfp** 또는 **LFP**, 때로는 **가장 작은 고정점**)은 포셋의 순서에 따라 다른 모든 고정점보다 작은 고정점이다. 함수는 최소 고정점을 가질 필요는 없지만, 만약 가진다면 그 최소 고정점은 유일하다.
# 예시
실수에 대한 일반적인 순서에서, 실수 함수 f(x) = x2의 최소 고정점은 x = 0이다 (다른 유일한 고정점은 1이고 0 < 1이기 때문이다). 대조적으로, f(x) = x + 1은 고정점이 전혀 없으므로 최소 고정점이 없으며, f(x) = x는 무한히 많은 고정점을 가지지만 최소 고정점은 없다. G = (V, A)가 유향 그래프이고 v가 정점이라고 하자. v에서 접근 가능한 정점의 집합은 f: \wp(V) \to \wp(V) 함수에 대한 최소 고정점으로 정의할 수 있으며, 이 함수는 f(X) = \\{ v \\} \cup \\{ x \in V: \text{ for some } w \in X \text{ there is an arc from } w \text{ to } x \\} 로 정의된다. v에서 공동 접근 가능한 정점의 집합은 유사한 최소 고정점으로 정의된다. v의 강한 연결 요소는 이 두 최소 고정점의 교집합이다. G = (V, \Sigma, R, S_0)가 문맥 자유 문법이라고 하자. 빈 문자열 \varepsilon을 생성하는 기호의 집합 E는 함수 f: \wp(V) \to \wp(V)의 최소 고정점으로 얻을 수 있으며, 이 함수는 f ( X ) = \\{ S \in V: \; S \in X \text{ or } (S \to \varepsilon) \in R \text{ or } (S \to S^1 \dots S^n) \in R \text{ and } S^i \in X \text{, for all } i \\}로 정의되며, 여기서 \wp(V)는 V의 멱집합을 나타낸다.
# 응용
많은 고정점 정리는 최소 고정점을 찾는 알고리즘을 제공한다. 최소 고정점은 종종 임의의 고정점이 갖지 않는 바람직한 특성을 갖는다.
## 표시적 의미론
표시적 의미론#재귀 프로그램의 의미 \mathbb{Z}_\bot의 부분 순서 컴퓨터 과학에서 표시적 의미론 접근 방식은 주어진 프로그램 텍스트에서 그 의미론이라고 불리는 해당 수학적 함수를 얻기 위해 최소 고정점을 사용한다. 이를 위해 예외적인 값 "정의되지 않음"을 나타내는 인공적인 수학적 객체 \bot가 도입된다. 예를 들어, 프로그램 데이터 형식 `int`가 주어지면, 그 수학적 대응물은 \mathbb{Z}_\bot = \mathbb{Z} \cup \\{ \bot \\} ;으로 정의되며, 그림과 같이 각 n \in \mathbb{Z}에 대해 \bot \sqsubset n을 정의하고, 두 개의 서로 다른 멤버 n,m \in \mathbb{Z}는 \sqsubset에 대해 비교할 수 없도록 정의함으로써 부분 순서 집합이 된다. 프로그램 정의 `int f(int n){...}`의 의미론은 어떤 수학적 함수 f: \mathbb{Z}_\bot \to \mathbb{Z}_\bot .이다. 프로그램 정의 `f`가 특정 입력 `n`에 대해 종료되지 않는다면, 이는 수학적으로 f(n) = \bot .으로 표현될 수 있다. 모든 수학적 함수의 집합은 각 n ,에 대해 f(n) \sqsubseteq g(n) 관계가 성립할 때, 즉 f(n)이 g(n)보다 덜 정의되거나 같을 때 f \sqsubseteq g를 정의함으로써 부분 순서가 된다. 예를 들어, 식 `x+x/x`의 의미론은 `x+1`의 의미론보다 덜 정의되는데, 전자는 후자와 달리 0을 \bot ,으로 매핑하고, 그 외에는 일치하기 때문이다. 어떤 프로그램 텍스트 `f`가 주어지면, 그 수학적 대응물은 `f`를 "번역"하여 얻을 수 있는 함수에서 함수로의 어떤 매핑의 최소 고정점으로 얻어진다. 예를 들어, C 정의 int fact(int n) { if (n == 0) return 1; else return n * fact(n-1); } 는 다음과 같은 매핑으로 번역된다 :F: (\mathbb{Z}_\bot \to \mathbb{Z}_\bot) \to (\mathbb{Z}_\bot \to \mathbb{Z}_\bot) , (F(f))(n) = \begin{cases} 1 & \text{if } n = 0, \\\ n \cdot f(n-1) & \text{if } n \neq \bot \text{ and } n \neq 0, \\\ \bot & \text{if } n = \bot. \\\ \end{cases}로 정의된다. 매핑 F는 `fact`가 재귀적으로 정의되었음에도 불구하고 비재귀적으로 정의된다. 예제에서 충족되는 특정 제약 조건(클레이니 고정점 정리 참조) 하에서, F는 반드시 최소 고정점 \operatorname{fact}를 가지며, 이는 모든 n \in \mathbb{Z}_\bot에 대해 (F(\operatorname{fact}))(n) = \operatorname{fact}(n)이다.year=1990 Here: pp. 636–638 다음과 같이 나타낼 수 있다. :\operatorname{fact}(n) = \begin{cases} n! & \text{if } n \geq 0, \\\ \bot & \text{if } n < 0 \text{ or } n = \bot. \end{cases} F의 더 큰 고정점은 예를 들어 \operatorname{fact}_0 , 함수이며, 다음과 같이 정의된다. :\operatorname{fact}_0(n) = \begin{cases} n! & \text{if } n \geq 0, \\\ 0 & \text{if } n < 0, \\\ \bot & \text{if } n = \bot, \end{cases} 그러나 이 함수는 음수 n ;에 대한 위 프로그램 텍스트의 동작을 정확하게 반영하지 않는다. 예를 들어, `fact(-1)` 호출은 전혀 종료되지 않으며, `0`을 반환하지도 않는다. 오직 최소 고정점인 \operatorname{fact} ,만이 수학적 프로그램 의미론으로 합리적으로 사용될 수 있다.
## 서술 복잡도
이머만N. Immerman, Relational queries computable in polynomial time, Information and Control 68 (1–3) (1986) 86–104.doi=10.1145/800070.802187 Revised version in Information and Control, 68 (1986), 86–104. 과 바르디doi=10.1145/800070.802186 는 독립적으로 서술 복잡도 결과를 보여주었는데, 선형으로 순서화된 구조의 다항 시간 계산 가능한 속성은 FO(LFP), 즉 최소 고정점 연산자가 있는 1차 논리로 정의 가능하다는 것이다. 그러나 FO(LFP)는 비순서 구조의 모든 다항 시간 속성(예를 들어 구조가 짝수 크기를 갖는다는 것)을 표현하기에는 너무 약하다.
# 최대 고정점
함수의 최대 고정점은 최소 고정점과 유사하게, 포셋의 순서에 따라 다른 모든 고정점보다 큰 고정점으로 정의할 수 있다. 컴퓨터 과학에서 최대 고정점은 최소 고정점보다 훨씬 덜 일반적으로 사용된다. 특히, 도메인 이론에서 발견되는 포셋은 보통 최대 원소를 갖지 않으므로, 주어진 함수에 대해 여러 개의 서로 비교 불가능한 극대 고정점이 있을 수 있으며, 해당 함수의 최대 고정점은 존재하지 않을 수도 있다. 이 문제를 해결하기 위해, 최적 고정점은 다른 모든 고정점과 호환되는 가장 잘 정의된 고정점으로 정의되었다. 최적 고정점은 항상 존재하며, 최대 고정점이 존재한다면 그것이 최대 고정점이다. 최적 고정점은 최소 고정점으로는 수렴하지 않는 재귀 및 공동재귀 함수의 형식적 연구를 가능하게 한다.access-date=30 October 2021 불행히도, 클레이니 재귀 정리가 최소 고정점이 효과적으로 계산 가능함을 보여주는 반면, 계산 가능 함수의 최적 고정점은 비계산 함수일 수 있다.language=en Here: Example 12.1, pp. 12.2–3
# 참고 자료
* Immerman, Neil. *Descriptive Complexity*, 1999, Springer-Verlag. * Libkin, Leonid. *Elements of Finite Model Theory*, 2004, Springer. 위키데이터 속성 추적 분류:순서론 분류:고정점