의미론과 재귀 (1)
프로그래밍 언어는 문법syntax과 의미론semantics의 결합으로 볼 수 있다. 어떤 가상의 기계가 있다고 가정하고 실행하는 과정을 한 단계씩 나아가는 과정을 설명하는 의미론을 실행적operational 의미론 이라고 하고, 프로그램을 어떤 함수로 간주해서 그 함수가 수학적으로 무엇인지를 묘사하는 방법을 표시적denotational 의미론이라고 한다. 즉, 표시적 의미론에서 프로그램 $P$의 의미를 메모리를 받아서 메모리를 내놓는 형태의 함수로 생각한다.
\[\llbracket P \rrbracket : \mathbb{M} \to \mathbb{M}\]재귀
의미론이 가장 접근하기 까다로운 상황이 있는데, 바로 재귀이다. B가 조건, C가 while문 내부의 코드라고 했을 때 ${\tt while} \; B \; C$의 의미를 살펴보자. $\mathbb{M}$을 메모리의 집합, 그리고 $\mathbb{B}$를 부울값의 집합, 즉 {true, false}로 놓자. 이 때 B는 메모리를 받아서 부울 값을 반환하는 함수, C는 메모리를 받아서 메모리를 반환하는 함수이다.
\[\llbracket B \rrbracket : \mathbb{M} \to \mathbb{B} \quad \llbracket C \rrbracket : \mathbb{M} \to \mathbb{M}\]예를 들어,
x = 1;
while (5 >= x + 2) {
x += 1;
}
에서 B는 5 >= x + 2, C는 x+=1에 해당한다. B는 현재의 메모리에서 x의 값을 기반으로 부울 값을 반환하고, C는 x의 값을 불러와 1을 더한 값으로 덮어씌우는, 메모리를 받아 메모리를 반환하는 함수이다.
재귀 - 실행적 의미론
실행적 의미론에서 while을 정의할 때는 직접 반복을 실행하는 방식으로 나타낸다. B의 의미가 false라면 실행을 하지 않은 채로 바로 현재 메모리 m을 반환할 것이다. 상태를 실행해야 할 남은 명령 C와 메모리 m의 쌍 $\langle C, m \rangle$으로 둘 때, 큰 스텝big-step 의미는 다음과 같다.
\[\cfrac {\llbracket B \rrbracket(m) = \mathtt{false}} {\langle \mathtt{while} \; B \; C , \; m \rangle \rightarrow \langle \mathtt{skip} , m \rangle}\]skip은 ‘더 이상 실행할 명령이 없다’는 뜻으로, 실행이 정상적으로 종료됨을 의미한다. B가 true인 경우에는 C를 한 번 실행해보고 while을 다시 돌려볼 것이다.
\[\cfrac {\llbracket B \rrbracket(m) = \mathtt{true}} {\langle \mathtt{while} \; B \; C , \; m \rangle \rightarrow \langle C ; \; \mathtt{while} \; B \; C, m \rangle}\]이렇게 이 두 식을 통해 실행적 의미론에서 while의 의미를 나타낼 수 있다.
재귀 - 표시적 의미론
표시적 의미론에서는 실행적 의미론에서 쓰던 ‘마저 실행해야 할 코드’ $C$ 따위는 쓸 수가 없다. 기계가 절차적으로 코드를 실행하는 스펙을 묘사하고 싶은게 아니라, 수학적으로 ${\tt while} \; B \; C$가 메모리를 어떻게 바꾸는 함수인지를 앎이 목적이기 때문이다!
여기서 분명히 해야 할 것은, 절차적으로 코드를 실행하는게 아니라고 해서 언어를 귀납적으로 접근하지 않는다는 것은 아니다. 예를 들면 코드 $C_0$를 실행하고 $C_1$을 실행하는 문법 $C_0 ; C_1$의 의미를 표시적 의미론에서는 이렇게 적는다.
\[\llbracket C_0 ; C_1 \rrbracket (m) = \llbracket C_1 \rrbracket \circ \llbracket C_0 \rrbracket (m)\]다르게는 $\llbracket C_1 \rrbracket ( \llbracket C_2 \rrbracket (m))$으로 적기도 한다. 즉, $\llbracket C_0 \rrbracket$와 $\llbracket C_1 \rrbracket$ 모두 메모리를 바꾸는 함수 $\mathbb{M} \to \mathbb{M}$이고, 이를 순차적으로 실행한다는 것은 이 두 함수에 대한 합성 $\circ$으로 표현할 수 있는 것이다.
이제 while의 의미를 써내려가보자. B의 의미가 true이면.. C를 실행 후 while을 실행하고, false이면.. m을 반환하고.
\[\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}\]하지만, $\llbracket \mathtt{while} \; B \; C \rrbracket$를 정의하려고 식을 썼더니, 그 안에도 같은 게 들어있다. 이걸 while의 수학적인 정의라고 부를 수 있을까?
혹자는 재귀적인 관계로 피보나치 수열이 정의되니까, 괜찮지 않을까 생각할 수도 있다.
\[f_n = \begin{cases} 0 & \text{if } n = 0 \\ 1 & \text{if } n = 1 \\ f_{n-1} + f_{n-2} &\text{if } n \ge 2 \end{cases}\]이 관계를 정의로도 볼 수 있는 이유는 임의의 자연수 $n$에 대해, $f_n$의 값이 존재한다는 것을 귀납적으로 쉽게 알 수 있기 때문이다. 하지만 ${\tt while} \; B \; C$의 경우에는, B가 $\mathtt{true}$인 경우만 봐도 위의 관계를 돌려보면 루프에 빠져버리기 때문에 의미가 정의되지 않는다. 억지로 정의로 만들려고 한다면 관계 뒤에다가 “단, 루프에 빠지지 않고 언젠가 false인 경우로 종료될 때”라고 조건을 붙여놔도 되겠지만, ‘프로그램이 종료될 때’의 정의는 또한 결국에는 의미론이 해결해야 할 문제이다. 다음 글에서는 표시적 의미론에서 어떻게 while을 정의하는 지에 대해 더 자세히 알아볼 예정이다.
Leave a comment