$\mathtt{while} \; B \; C$의 표시적 의미론_{denotational semantics} 적 관계는 다음과 같았다:

$\llbracket \mathtt{while} \; B \; C \rrbracket (m) = \begin{cases} \llbracket \mathtt{while} \; B \; C \rrbracket (\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases}$

하지만, 이 관계를 통해 $\mathtt{while} \; B \; C$의 의미를 제대로 나타내지 못한다는 결론을 얻었다. 유한한 반복 안에 이 의미가 끝난다는 보장이 없기 때문이다.

여기서 $\llbracket \mathtt{while} \; B \; C \rrbracket$만 $X$로 바꿔서 적어보자.

$X(m) = \begin{cases} X(\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases}$

이 식을 모든 메모리 $m \in \mathbb{M}$에 대하여 만족하는 함수 X를 찾으면, 그게 $\llbracket \mathtt{while} \; B \; C \rrbracket$의 의미이다. 다시 적으면,

$X = \mathcal{F}_{B,C} (X) \quad \text{where} \; \mathcal{F}_{B,C} (X) = \lambda m. \begin{cases} X(\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases}$

의 해가 $\llbracket \mathtt{while} \; B \; C \rrbracket$이다.

그러면 이 $X = \mathcal{F}_{B,C} (X)$의 고정점을 찾는 문제에 대해 두 가지 의문이 생긴다.

1. 해가 존재하는가?
2. 여러 개의 해가 존재한다면, 어떤 해를 고를 것인가?

이 의문들만 해결된다면, 표시적 의미론에서 재귀 관계에 놓인 문법의 의미를 표현하는 문제가 풀린다. 해의 존재성은, ‘해가 존재한다’는 공간을 앞으로 정의할 것이고, 해의 선택은 최소 고정점least fixed point을 정의해서 선택할 것이다. 그러면 다음의 결과가 while의 의미이다.

$\llbracket \mathtt{while} \; B \; C \rrbracket = \textbf{lfp} \mathcal{F}_{B,C}$

이제 구체적으로 의문들을 어떻게 해결하는 지 알아볼 때이다.

의미론과 도메인 이론

우선 $X$가 속하는 의미_semantics 의 공간을 서술하는 이론을 알아야 하는데, 이를 도메인 이론_{domain theory} 라고 부른다. 이 이론은 완비 부분 순서complete partial order로부터 시작한다.

부분순서 집합

부분 순서partial order는 집합의 포함관계를 떠올리면 된다. 엄밀하게는 집합 $D$에서 정의된 부분순서 $\sqsubseteq$는 다음 성질을 만족하는 관계이다.

1. 반사성reflexivity: 모든 $a \in D$에 대해 $a \sqsubseteq a$이다.
2. 추이성transitivity: $a \sqsubseteq b$이고 $b \sqsubseteq c$이면 $a \sqsubseteq c$이다.
3. 비대칭성antisymmetry: $a \sqsubseteq b$이고 $b \sqsubseteq a$이면 $a = b$이다.

부분적인 순서라 불리는 이유는, 집합에서 임의의 두 원소를 골랐을 때 비교가 가능하다는 보장을 하지 않기 떄문이다. 부분순서이면서 일반적인 수의 대소 관계처럼 어떤 두 원소를 골라도 비교가 가능한 경우에는 전순서total order라고 부른다.

부분순서 집합의 완비성

부분 순서 집합의 완비성completeness은 해석학에서 실수의 완비성 공리에서 다루는 그것과 거의 동일하다. 실수의 완비성 공리는 상계upper bound가 있는 공집합이 아닌 부분집합은 언제나 상한least upper bound이 있다, 즉 실수가 충분히 빽빽하게 채워져 있다는 내용이다. 완비 부분 순서도 상계가 있는 부분집합이 언제나 상한을 가지는 관계를 의미한다. 엄밀하게는 다음과 같다:

부분 순서 집합 $(D, \sqsubseteq)$에서, 일부 $X \subseteq D$를 가져왔을 때 $d \in D$가 $X$의 상계라는 것은 다음을 의미한다.

$\forall x \in X, \; x \sqsubseteq d$

이런 상계 $d$는 여러 개 있을 수 있다. 만약 $d$가 모든 다른 $X$의 상계보다 작다면, 이를 상한 또는 최소상계라고 부르고, $\bigsqcup X$로 표기한다.

부분순서 집합에서 부분집합을 취했을 때 전순서이면 이를 체인이라고 부른다. 부분순서집합 $(D, \sqsubseteq)$이 완비하다complete는 것은, 모든 체인 $X \subset D$의 상한이 집합 $D$에 속함을 의미한다.

$\bigsqcup X \in D$

흥미롭게도, 아무것도 없는 빈 집합도 체인이기 때문에, 이의 상한 $\bot = \bigsqcup \emptyset$이라는, 최소원소가 $D$에 존재한다.

연속성

두 부분순서 집합 $D_1, D_2$에 대해, 함수 $f: D_1 \to D_2$가 연속이라는 것은, 체인의 상한이 함수에 의해 보존될 때를 의미한다:

$\forall \text{chain} \; X \subseteq D_1, \; \bigsqcup f(X) = f (\bigsqcup X)$

의미론과 도메인

프로그래밍 언어에서 메모리의 집합 $\mathbb{M}$은 변수를 값으로 대응시키는 함수들의 집합 $\mathbb{X} \to \mathbb{V}$로 볼 수 있고, 코드의 의미는 이전 글에서 다루었듯, $\mathbb{M} \to \mathbb{M}$에 속한다. 부울 값을 반환하는 식의 의미는 $\mathbb{M} \to \mathbb{B}$가 될 것이다.

• 값은 부울과 정수 집합으로 이루어져 있다. $\mathbb{V} = \mathbb{Z} + \mathbb{B}$
• 메모리 도메인 $\mathbb{M} = \mathbb{X} \to \mathbb{V}$
• 코드 의미 도메인 $\llbracket C \rrbracket \in \mathbb{M} \to \mathbb{M}$
• 부울 식의 의미 도메인 $\\llbracket B \rrbracket \in \mathbb{M} \to \mathbb{B}$

우리가 풀고자 하는 $\mathcal{F}_{B,C}: \mathbb{M} \to \mathbb{M}$의 고정점을 찾기 위해서, 이 대상 도메인들이 어떤 좋은 성질을 만족했으면 좋겠고, 그것이 바로 완비부분순서 관계의 존재와 함수의 연속성이다. 완비부분순서를 주기 위해서 몇 가지 테크닉이 필요하다:

들어올려진 집합

어떤 집합 $S$에 대해, 새로운 원소 $\bot$을 추가한 집합 $S_{\bot} = S + \\{\bot \\}$을 고려하자. 여기에 순서를

$d \sqsubseteq d' \iff (d = d') \lor (d = \bot)$

로 주면, $(S_{\bot}, \sqsubseteq)$는 완비부분순서집합이고, $S$의 들어올려진 집합lifted set이라 불린다.

곱집합

두 완전부분순서 집합 $(D_1, \sqsubseteq_1)$, $(D_2, \sqsubseteq_2)$에 대해, 이들의 곱집합Cartesian product $D_1 \times D_2$에서 관계를

$(d_1, d_2) \sqsubseteq(d_1 ^\prime, d_2 ^\prime) \iff (d_1 \sqsubseteq_1 d_1^\prime ) \wedge (d_2 \sqsubseteq_2 d_2 ^\prime)$

으로 자연스럽게 주었을 때, $(D_1 \times D_2, \sqsubseteq)$ 역시 완전부분순서 집합이다.

분리합

두 완전부분순서 집합 $(D_1, \sqsubseteq_1)$, $(D_2, \sqsubseteq_2)$에 대해,

$D_1 + D_2 = \left\{ (d_1, 1) \mid d_1 \in D_1 \right\} \cup \left\{ (d_2, 2) \mid d_2 \in D_2 \right\} \cup \left\{ \bot \right\}$

으로 $D_1$과 $D_2$의 분리합separated sum을 정의하고,

$(d_1, 1) \sqsubseteq (d_1 ^\prime, 1) \iff d_1 \sqsubseteq_1 d_1 ^\prime \\ (d_2, 2) \sqsubseteq (d_2 ^\prime, 2) \iff d_2 \sqsubseteq_2 d_2 ^\prime$

으로 관계를 주면 $(D_1 + D_2, \sqsubseteq)$는 완전부분순서 집합이다.

연속 함수

두 완전부분순서 집합 $(D_1, \sqsubseteq_1)$, $(D_2, \sqsubseteq_2)$에 대해, $D$를 $D_1$에서 $D_2$로 가는 연속함수들의 집합이라 했을 때,

$f \sqsubseteq f^\prime \iff \forall d_1 \in D_1,\; f(d_1) \sqsubseteq_2 f^{\prime}(d_1)$

이면 $(D, \sqsubseteq)$는 완전부분순서 집합이다. 편의상 이제부터 $D$를 연속이라는 개념을 내포하는 의미의 $D_1 \to D_2$로 표현하자.

또한, 이 공간에서 가장 작은 원소 $\bot$은,

$\forall d_1 \in D_1, \; f(d_1) = \bot_2$

어떤 원소든지 $D_2$의 가장 작은 원소인 $\bot_2$로 보내버리는 함수가 되는데, 그 이유는 어떤 $D_1 \to D_2$인 함수 $f$를 들고오더라도 $\bot \sqsubseteq f$이기 때문이다.

집합에 완비부분순서를 주기

위 기술들을 이용하면, 완비부분순서를 가지는 집합들을 정의할 수 있다.

• 변수 도메인 $\mathbb{X} _\bot$
• 정수 도메인 $\mathbb{Z} _\bot$
• 부울 도메인 $\mathbb{B} _\bot$
• 값 도메인 $\mathbb{V} = \mathbb{Z} _\bot + \mathbb{B}_\bot$
• 메모리 도메인 $\mathbb{M} = \mathbb{X}_\bot \to \mathbb{V}$
• 코드 의미 도메인 $\llbracket C \rrbracket \in \mathbb{M} \to \mathbb{M}$
• 부울 식 의미 도메인 $\llbracket B \rrbracket \in \mathbb{M} \to \mathbb{B}_\bot$

그리고 $\mathcal{F}_{B,C}$는 프로그램의 의미를 받아서 의미를 내놓는 함수이므로, $(\mathbb{M} \to \mathbb{M}) \to (\mathbb{M} \to \mathbb{M})$이다.

고정점으로 돌아와서

이제 $\mathcal{F}_{B,C}$가 연속이고, 코드의 의미를 완비부분순서가 있는 공간에 속한 원소로 생각할 수 있게 되었다.

최소 고정점

$(D, \sqsubseteq)$가 부분순서 집합일 때, 함수 $f: D \to D$의 최소 고정점 $\textbf{lfp} f$는 고정점 중 최소인 원소를 의미한다.

$f(\textbf{lfp} f) = \textbf{lfp} f \wedge \forall d \in D, \; f(d) = d \implies \textbf{lfp} f \sqsubseteq d$

아직은 고정점이 존재하는 지도 모르고, 모든 고정점이 한 고정점과 비교가 가능해서 그 고정점보다 큰 지도 알 수가 없다. 하지만 아주 쓸만한 정리가 있는데,

Kleene의 고정점 정리

$(D, \sqsubseteq)$가 부분순서 집합이고 $f: D \to D$가 연속함수일 때, $f$는 최소고정점이 존재하고, 그 값은

$\textbf{lfp}f = \bigsqcup _{i \ge 0 } f^i (\bot)$

이다.

최소 고정점과 재귀의 관계

$\mathcal{F} _{B,C}$도 $(\mathbb{M} \to \mathbb{M}) \to (\mathbb{M} \to \mathbb{M})$인 연속함수로 정의했으므로, Kleene의 고정점 정리에 의하면 최소고정점이

$\textbf{lfp} \mathcal{F}_{B,C} = \bigsqcup _{i \ge 0} \mathcal{F} _{B,C} ^i (\bot)$

가 된다. 그러면 우리가 통상적으로 아는 while의 의미를 이 최소고정점이라는 개념이 잘 설명하고 있을까?

값 도메인의 최소인 $\bot_\mathbb{V}$는 분리합 $\mathbb{B}_{\bot} + \mathbb{Z}_{\bot}$의 최소 원소이고,

메모리 도메인의 최소인 $\bot_{\mathbb{M}} : \mathbb{X}_\bot \to \mathbb{V}$은 어떤 변수를 들고오더라도 $\bot_{\mathbb{V}}$를 반환하는 함수이고,

$\bot \in \mathbb{M} \to \mathbb{M}$은, 어떤 메모리를 들고오더라도 $\bot_{\mathbb{M}}$을 반환하는 함수이다.

$\mathcal{F}_{B,C} (X) = \lambda m. \begin{cases} X(\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases}$

였으니,

$\begin{aligned} \mathcal{F}_{B,C} (\bot) &= \lambda m. \begin{cases} \bot(\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases} \\ & = \lambda m. \begin{cases} \bot_{\mathbb{M}} & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases} \end{aligned}$

로 적어볼 수 있고,

$\begin{aligned} \mathcal{F}_{B,C} ^2 (\bot) &= \lambda m. \begin{cases} \mathcal{F}_{B,C} (\bot) (\llbracket C \rrbracket (m)) & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases} \\ &= \lambda m. \begin{cases} { \begin{cases} \bot_\mathbb{M} & \text{if } \llbracket B \rrbracket (\llbracket C \rrbracket (m)) = \texttt{true}\\ \llbracket C \rrbracket (m) & \text{if } \llbracket B \rrbracket (\llbracket C \rrbracket (m)) = \texttt{false} \end{cases} } & \text{if} \; \llbracket B \rrbracket (m) = \texttt{true} \\ m & \text{if} \; \llbracket B \rrbracket (m) = \texttt{false} \end{cases} \end{aligned}$

이다. 비슷하게,

$\mathcal{F} _{B,C} ^3 (\bot) = \lambda m. \begin{cases} m & \text{if } \llbracket B \rrbracket (m) = \texttt{false} \\ \llbracket C \rrbracket (m) & \text{if } \llbracket B \rrbracket(m) = \texttt{true} \wedge \llbracket B \rrbracket \circ \llbracket C \rrbracket (m) = \texttt{false} \\ \llbracket C \rrbracket \circ \llbracket C \rrbracket (m) & \text{if } \llbracket B \rrbracket (m) = \texttt{true} \wedge \llbracket B \rrbracket \circ \llbracket C \rrbracket (m) = \texttt{true} \wedge \\ & \quad \llbracket B \rrbracket \circ \llbracket C \rrbracket \circ \llbracket C \rrbracket (m) = \texttt{false} \\ \bot_{\mathbb{M}} & \text{if } \llbracket B \rrbracket (m) = \texttt{true} \wedge \llbracket B \rrbracket \circ \llbracket C \rrbracket (m) = \texttt{true} \wedge \\ & \quad \llbracket B \rrbracket \circ \llbracket C \rrbracket \circ \llbracket C \rrbracket (m) = \texttt{true} \end{cases}$

이다. 반복적으로 이를 하면서 결국에는 조건 $B$의 결과가 참이 될 때까지 돌리는 while문에 가까워진다는 점이 놀랍게도 관찰된다. 이들의 상한

$\textbf{lfp} \mathcal{F}_{B,C} = \bigsqcup _{i \ge 0} \mathcal{F} _{B,C} ^i (\bot)$

은, 각 메모리 $m \in \mathbb{M}$에 대하여 $\textbf{lfp} \mathcal{F}_{B,C} (m)$이 모든 $i$에 대해 $\mathcal{F} _{B,C} ^i (\bot)(m)$보다 메모리의 대소관계 $\sqsubseteq_{\mathbb{M}}$에서 크거나 같아야 한다는 의미인데,

$\forall i \ge 0. \quad \forall m \in \mathbb{M}. \quad \mathcal{F} _{B,C} ^i (\bot)(m) \sqsubseteq _\mathbb{M} \textbf{lfp} \mathcal{F}_{B,C} (m)$

충분히 많은 수의 반복을 했을 때 가지는 메모리라도 최소고정점의 결과에 포함된다. 즉, 실행적 의미론operational semantics이 풀어내는 while에 등장하는 재귀적인 관계를 표시적 의미론도 최소고정점을 통해 내포하고 있는 것이다.

참고자료

• KAIST CS524 Program Analysis - denotational semantics