개요
Widening은 fix point iterations에서 lattice가 infinite이거나, search space가 너무 크면 수렴에 무한히 (오랜)시간이 걸리는 문제를 해결하기 위해서, step을 한번에 크게 가져가는 것을 말한다.
widening operation은 [math]\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}[/math] 라는 기호로 표기한다.
여기서 다음 조건을 만족시키는 finite chain Y를 다음과 같이 정의 가능하다.
[math]\bigsqcup_{i \geq 0}F^i(\bot) \sqsubseteq Y_{lim}[/math]
여기서 Y는 [math]\bigtriangledown[/math]를 통해서 다음과 같이 정의된다.
[math]Y_0 = \bot[/math]
[math]Y_{i+1} = \begin{cases} Y_i & \mbox{if } F(Y_i) \sqsubseteq Y_i \\ Y_i \bigtriangledown F(Y_i) & \mbox{otherwise} \end{cases}[/math]
쉽게 설명 하자면, widening operator는 무조건 finite해야 하며 (당연히 유한 시간안에 operation을 끝내야 함으로), 또한 Y의 upper bound는 무조건 원래 수렴하는 step보다는 크다.
예시
x = 0;
while (*) {
x++;
}
[math]\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}[/math]
를 다음과 같이 정의하면
[math][a,b] \bigtriangledown \bot = [a,b][/math]
[math]\bot \bigtriangledown [c,d] = [c,d][/math]
[math] [a,b] \bigtriangledown [c,d] = [(c \lt a? - \infty : a), (b \lt d? + \infty : b)][/math]
처음 시작에서는 [0, 0]으로 range doamin이 시작하지만 다음 [0, 1]에서 widening되어서 [0, infty]로 widening된 결과를 가진다.