Fixed point - 편집 역사

2023년 11월 8일 (수) 07:33에 Ahn9807님의 편집

2023-11-08T07:33:47Z

← 이전 판		2023년 11월 8일 (수) 07:33 판
12번째 줄:		12번째 줄:
	; Theoren: Kleene Fixed Point		; Theoren: Kleene Fixed Point
	<math>f: D \rightarrow D</math>가 [[Complete partial order]] D에 대해서 연속 함수일때 f는 least fixed point '''lfp'''를 가진다.		<math>f: D \rightarrow D</math>가 [[Complete partial order]] D에 대해서 연속 함수일때 f는 least fixed point '''lfp'''를 가진다.
	<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>		<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>

	위 수식이 의미하는 바는, [[수치 해석]]의 [[뉴턴법]]과 같은 점근을 통해서 해를 구하는 방식과 유사하다. 증명은 간단한데, f(x) = x이기 떄문에 f는 단조 증가 함수이다 (Monotonous increasing function).		위 수식이 의미하는 바는, [[수치 해석]]의 [[뉴턴법]]과 같은 점근을 통해서 해를 구하는 방식과 유사하다. 증명은 간단한데, f(x) = x이기 떄문에 f는 단조 증가 함수이다 (Monotonous increasing function).

2023년 11월 8일 (수) 07:33에 Ahn9807님의 편집

2023-11-08T07:33:33Z

← 이전 판		2023년 11월 8일 (수) 07:33 판
11번째 줄:		11번째 줄:

	; Theoren: Kleene Fixed Point		; Theoren: Kleene Fixed Point
	: <math>f: D \rightarrow D</math>가 [[Complete partial order]] D에 대해서 연속 함수일때 f는 least fixed point '''lfp'''를 가진다.		<math>f: D \rightarrow D</math>가 [[Complete partial order]] D에 대해서 연속 함수일때 f는 least fixed point '''lfp'''를 가진다.
	<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>		<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>

Ahn9807: 새 문서: 분류: Abstract interpretation == 개요 == Fixed point란 F(X) = X를 만족시키는 점들을 말한다. * x 는 만약 $f : A \rightarrow A, x \in A$ 을 만족시키면 fixed point이다. 이때 함수가 Monotonic function이고, Partial order이 정의되어 있다면, 항상 제일큰 fixed point와 가장 작은 fixed point가 존재할 것이다. * leat fixed point: Monotonic 그리고 partial order인 집합 A에서, 제일 작은 fixed point...

2023-11-08T07:32:01Z

새 문서: 분류: Abstract interpretation == 개요 == Fixed point란 F(X) = X를 만족시키는 점들을 말한다. * x 는 만약 <math>f : A \rightarrow A, x \in A </math>을 만족시키면 fixed point이다. 이때 함수가 Monotonic function이고, Partial order이 정의되어 있다면, 항상 제일큰 fixed point와 가장 작은 fixed point가 존재할 것이다. * leat fixed point: Monotonic 그리고 partial order인 집합 A에서, 제일 작은 fixed point...

새 문서

[[분류: Abstract interpretation]]

== 개요 ==
Fixed point란 F(X) = X를 만족시키는 점들을 말한다.

* x 는 만약 <math>f : A \rightarrow A, x \in A </math>을 만족시키면 fixed point이다.

이때 함수가 Monotonic function이고, [[Partial order]]이 정의되어 있다면, 항상 제일큰 fixed point와 가장 작은 fixed point가 존재할 것이다.

* leat fixed point: Monotonic 그리고 partial order인 집합 A에서, 제일 작은 fixed point

; Theoren: Kleene Fixed Point
: <math>f: D \rightarrow D</math>가 [[Complete partial order]] D에 대해서 연속 함수일때 f는 least fixed point '''lfp'''를 가진다.
<math>\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>

위 수식이 의미하는 바는, [[수치 해석]]의 [[뉴턴법]]과 같은 점근을 통해서 해를 구하는 방식과 유사하다. 증명은 간단한데, f(x) = x이기 떄문에 f는 단조 증가 함수이다 (Monotonous increasing function).
따라서 귀납법에 의하여,
:<math>\bot \sqsubseteq f(\bot) \sqsubseteq f(f(\bot)) \sqsubseteq \cdots \sqsubseteq f^n(\bot) \sqsubseteq \cdots</math>
가 성립하며, 최초에는 당연히 bottom보다 크거나 작기 때문에, 귀납법에 의해서 특정 fixed point의 값으로 수렴함을 알 수 있다.