최소 고정점
Least fixed point![]() |
순서론에서 수학의 한 분야, 부분 순서가 정해진 집합에서 그 자체로 함수의 최소 고정점(lfp 또는 LFP, 때로는 가장 작은 고정점)은 포셋의 순서에 따라 서로 고정점보다 적은 고정점이다.함수는 최소 고정점을 가질 필요는 없지만, 고정점을 가질 경우 최소 고정점은 고유하다.
예를 들어, 실제 숫자에 통상적인 순서가 있는 경우, 실제 함수 f(x) = x의2 최소 고정점은 x = 0(다른 고정점만 1과 0 < 1이기 때문에)이다.이와는 대조적으로 f(x) = x + 1은 고정점이 전혀 없으므로 최소점이 없고, f(x) = x는 고정점이 무한히 많지만 최소점이 없다.
예
=( , ) 을(를) 지시된 그래프로 하고 을(를) 꼭지점으로 한다.The set of vertices accessible from can be defined as the least fixed-point of the function , defined as 에서 동시에 액세스할 수 있는 정점 집합은 유사한 최소 고정점으로 정의된다. 의 강하게 연결된 구성 요소는 이 두 최소 고정점의 교차점이다 .
Let =( V, , , ) 는 문맥이 없는 문법이다 .The set of symbols which produces the empty string can be obtained as the least fixed-point of the function , defined as , where denotes the power set of .
적용들
많은 고정점 이론들은 최소 고정점을 찾기 위한 알고리즘을 산출한다.최소 고정점에는 임의 고정점에는 없는 바람직한 특성이 있는 경우가 많다.
변절 의미론
컴퓨터 과학에서, 변성 의미론 접근법은 주어진 프로그램 텍스트로부터 그것의 의미론이라고 불리는 상응하는 수학적 함수를 얻기 위해 최소한의 고정점을 사용한다.이를 위해 mathematical {\디스플레이 스타일 인 인공수학 물체가 도입돼 '정의되지 않음'이라는 예외적 가치를 나타낸다.프로그램 데이터 유형과 같이 지정됨int
, its mathematical counterpart is defined as it is made a partially ordered set by defining for each and letting any two different members 은 (는) 비교할 수 없는 w.r.t. {\ 그림을 참조하십시오.
프로그램 정의의 의미론int f(int n){...}
일부 수학 함수 : → Z f 프로그램 정의인 경우f
일부 입력에 대해 종료되지 않음n
, this can be expressed mathematically as The set of all mathematical functions is made partially ordered by defining if, for each the relation holds, that is, i( ) 이 () (). )과 덜 정의되었거나 같음 예: 표현식의 의미론x+x/x
의 정의보다 적다x+1
, 전자가 아니라 후자가 아닌 을 (를) , 에 매핑하면, 그들은 달리 동의한다.
일부 프로그램 텍스트 지정f
, 그것의 수학 상대는 함수에서 "수치"에 의해 얻을 수 있는 함수에 이르는 일부 매핑의 최소 고정 지점으로 얻는다.f
. 예를 들어, C 정의
인트로 사실의(인트로 n) { 만일 (n == 0) 그때 돌아오다 1; 다른 돌아오다 n * 사실의(n-1); }
매핑으로 변환됨
- defined as
매핑 은(는) 비반복적인 방식으로 정의되지만fact
재귀적으로 정의되었다.Under certain restrictions (see Kleene fixed-point theorem), which are met in the example, necessarily has a least fixed point, , that is for all [1] 는 것을 보여줄 수 있다.
의 더 큰 고정점은 예: 함수 {fact}}에 의해 정의된다.
그러나 이 함수는 의 n 예: 통화)에 대해 위의 프로그램 텍스트의 동작을 올바르게 반영하지 않는다.fact(-1)
돌아오기는커녕 아예 종지부를 찍지도 않을 것이다.0
. 가장 덜 고정된 점 {\{\ {만 수학 프로그램 의미로서 합리적으로 사용할 수 있다.
서술적 복잡성
임메르만과[2][3] 바디는[4] 독립적으로 선형 순서가 정해진 구조의 다항식 시간 계산 가능 특성이 FO(LFP)에서 정의 가능하다는 서술적 복잡성 결과를 보여주었다.그러나 FO(LFP)는 너무 약해서 주문되지 않은 구조물의 모든 다항식 시간 특성을 표현하지 못한다(예를 들어 구조물의 크기가 짝수인 경우).
최대 고정점
가장 큰 고정점 또한 결정될 수 있다.실수의 경우 정의는 최소 고정점과 대칭이지만 컴퓨터 공학에서는 최소 고정점보다 일반적으로 덜 사용된다.구체적으로는, 도메인 이론에서 발견되는 포지션은 대개 가장 큰 요소를 가지지 않기 때문에, 상호 비할 수 없는 복수의 최대 고정점이 있을 수 있으며, 가장 큰 고정점은 존재하지 않을 수도 있다.이 문제를 해결하기 위해 최적의 고정점은 다른 모든 고정점과 호환되는 가장 정의된 고정점으로 정의되었다.최적 고정점은 항상 존재하며, 가장 큰 고정점이 존재하는 경우 가장 큰 고정점이다.최적 고정점은 최소 고정점과 수렴하지 않는 재귀 및 코어커서 함수에 대한 공식적인 연구를 가능하게 한다.[5]불행히도 효과적인 재귀적 정의의 최적 고정점은 계산 불가능한 함수일[6] 수 있으므로 주로 이론적 관심사다.
참고 항목
메모들
- ^ C.A. Gunter; D.S. Scott (1990). "Semantic Domains". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 633–674. ISBN 0-444-88074-7. 여기: 페이지 636-638
- ^ N. Immerman, 다항 시간에서 계산할 수 있는 관계 쿼리, 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. pp. 147–152. doi:10.1145/800070.802187. 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. pp. 137–146. doi:10.1145/800070.802186.
- ^ Charguéraud, Arthur (2010). "The Optimal Fixed Point Combinator" (PDF). Interactive Theorem Proving. 6172: 195–210. doi:10.1007/978-3-642-14052-5_15. Retrieved 30 October 2021.
- ^ Shamir, Adi (October 1976). The fixedpoints of recursive definitions (Ph.D. thesis). Weizmann Institute of Science. OCLC 884951223. 여기: 예 12.1, 페이지 12.2-3