표시적 의미론

언어에는 문법syntax과 의미semantics가 있다. 예를 들어, 한국어에서는 목적어가 동사 앞에 나온다. 일반적인 상황에서는, ‘나는 좋아한다 사과를’이라고 말하면 문법에 맞지 않는다. 문법에는 맞지만 말이 안 되는 상황이 있다. 일반적인 상황에서는, ‘사과는 나를 좋아한다’라는 표현을 정상적이라고 보기 어렵다.​¶¶​

1950년대에 고급 프로그래밍 언어를 만들기 위한 시도가 이어지면서 프로그래밍 언어의 문법과 의미에 대한 고민이 함께 시작되었다. 문법은 비교적 빨리 해결되었다. 때마침 촘스키와 같은 젊은 언어학자들이 언어의 구조에 대한 새로운 접근 방법을 제시했고, 이를 적극적으로 받아들여 BNF가 등장했다.​11​ BNF는 프로그래밍 언어의 문법을 일련의 규칙들로 정의하는 방법이다. 따라서 누군가 작성한 소프트웨어 프로그램에 문법적 오류가 없는지는, 프로그램을 구성하고 있는 각 문장이 BNF 규칙에 어긋나지 않는지 따져보면 되었고, 이 과정은 알고리듬을 통해 자동화할 수 있었다.

그런데 프로그래밍 언어의 의미를 자동으로 검증하기란 쉽지 않았다. 예를 들어 C언어로 작성한 아래와 같은 코드가 있다고 하자. 문법적으로는 완벽한 코드이다.

int x;
x= 2 ^ 3;

우리는 이 코드가 수행되었을 때 x에 어떤 값이 들어가야 할지를 이미 예상하고 있다.​##​ 통상적으로 ^는 제곱power of을 의미하는 경우가 많다. 그런 상식에 기반하여 x에 8이 들어갈 것이라고 해석한다면 문제가 발생한다. 왜냐하면 C언어에서는 ^가 비트끼리 XOR하는 연산자이기 때문이다. 따라서 위의 코드가 C언어로 작성된 것이라면 x에는 1의 값이 들어간다.

자 이렇듯 우리가 소프트웨어 프로그램을 작성할 때는 코드가 의도에 맞게 수행되어 의도한 결과를 만들어내길 기대한다. 그렇다면 프로그램이 수행되기 전에 그냥 코드만 보고도 어떤 결과가 나올지 자동으로 알아낼 방법은 없을까? 이렇게 자동으로 알아낸 결과가 원래 의도한 바와 다르다면 그 프로그램은 잘못 작성한 셈이 된다.

이를 시도했던 초기의 연구자 중 한 명이 스트레이치였다.​***​ 그는 프로그램 코드를 수학적으로 모델링한 후에, 이 수학적 모델링을 이리저리 전개해서 프로그램의 결과물이 원래 원했던 의도와 부합하는지를 검증하고 싶어 했다. 이런 시도에 순수 수학자였던 스콧이 관심을 가졌고 논리학을 접목했다.

스콧은 수학자였으므로 수학적 사고에서 출발했다.

숫자numeral는 어떤 특정한 언어를 사용한 ‘표현’인 반면에 수number는 이 표현이 의도하는 수학적 ‘객체'(추상적 객체)이다. 우리는 수에 관한 이론 결과를 소통하기 위해 이런 표현을 쓸 수밖에 없다. 하지만 이런 기호들이 그 개념 자체와 혼동되어서는 안 될 것이다.​12​

예를 들어, 우리는 ‘하나’라는 개념을 표현하기 위해 숫자 1을 쓰기도 하고 한글로 ‘하나’, 영어로 ‘one’ 등의 기호를 사용하기도 한다. 또한, 2 + 2, 4, 1 + (1 + (1 + 1))) 등은 모두 같은 수를 나타내는 서로 다른 표현들이다. 이런 관점을 컴퓨터 프로그램에 적용할 수 있다. ‘숫자를 내림차순으로 정렬하는 일’을 하는 프로그램은 사용하는 언어에 따라 다를 수 있고, 같은 언어를 사용하더라도 어떤 알고리듬을 사용하느냐에 따라 다른 형태의 코드로 나타날 수 있다. 하지만 그 프로그램이 ‘의도’하는 것은 하나이다. 프로그램 코드에서 이 ‘의도’를 자동으로 찾아내려는 것이 ‘의미론’의 목표이다.

스콧은 프로그램의 상태에 주목했다. 여기서 말하는 ‘상태’는 프로그램의 수행 과정에서 사용되는 변수라고 보면 좋을 듯싶다. 따라서 상태는 어떤 단일한 값이 아니라 많은 값들의 집합이다. 그리고 프로그램에서 어떤 코드가 수행될 때마다 상태에 변화가 생기게 된다. 모든 코드 수행에 대해서 상태의 변화를 추적할 수만 있다면 우리는 프로그램이 종료했을 때의 상태 값을 통해서 이 프로그램이 우리의 의도대로 동작했는지를 알 수 있다.

프로그래밍 언어에서 흔히 수식expression이라고 부르는 것을 생각해보자. 프로그래밍 언어에서 수식이란 어떤 값을 만들어내는 계산이다. 스콧은 아래와 같이 정의했다.​12​

    \[ \varepsilon :: = (\varepsilon)\: | \: \pi \: |\: true\: |\: false\: |\: \varepsilon_0 \rightarrow \varepsilon_1,\: \varepsilon_2 \]

\varepsilon은 수식을 의미하고, \pi는 최소 수식atomic expression, 즉 더 이상 파고들 수 없는 수식을 의미한다. 위의 정의를 해석해보면, 수식이라 함은,

  • 어떤 수식에 괄호를 씌운 것이거나,
  • 최소 수식이거나,
  • 참true 혹은 거짓false이라는 값이거나,
  • 조건 수식conditional expression이다.

위의 정의에서 마지막에 있는 \varepsilon_0 \rightarrow \varepsilon_1,\: \varepsilon_2는 조건 수식을 표현하는 방법임에 유의하자. 이것의 의미는 \varepsilon_0이 참일 경우 \varepsilon_1이고 그렇지 않은 경우에는 \varepsilon_2임을 의미한다.

이제 앞에서 언급한 프로그램의 상태 변화를 생각해보자. 수식이 수행되면 우리는 어떤 값을 얻게 되는데, 동시에 그 수식이 수행되면서 프로그램 내부의 상태가 변화할 수 있다. 이것을 수학적으로 표현하면

    \[S \rightarrow [ T \times S ] \]

가 된다. S는 프로그램의 상태 집합을 의미하고 T는 수식이 표현하는 값의 집합이다. 이를 해석하자면, 프로그램의 어떤 상태에서 수식이 수행되면 어떤 값과 새로운 상태가 결정된다는 것이다.​†††​

이렇듯 우리가 프로그램 코드를 구성하는 모든 수식에 대해서 이와 같이 상태 전이를 정의할 수 있다면 이 수식들로 구성되는 프로그램이 수행되었을 때 초기 상태로부터 마지막 상태를 계산할 수 있게 될 것이다. 그렇게 되면 프로그램을 실제로 컴파일해서 컴퓨터에서 수행하지 않고도 이 프로그램이 의도한 결과를 만들어낼지를 알 수 있게 된다.

이렇게 상태 전이라는 방법을 사용해서 소프트웨어 프로그램을 수학적으로 모델링한 후 그 모델을 사용해서 프로그램의 의미semantics를 검증하는 방법을 표시적 의미론Denotational semantics이라고 부른다.

스콧은 단순한 수식뿐만 아니라 함수 호출, 재귀적 호출 등도 수학적으로 모델링했다. 스콧의 방법이 현대 프로그래밍 언어의 모든 요소를 다 모델링하지는 못했지만 의미semantics를 수학적으로 모델링하여 검증할 방법을 제시했다는 점에서 큰 의미가 있다.

표시적 의미론 외에도 공리적 의미론axiomatic semantics 등이 있다. 공리적 의미론은 프로그램 코드의 각 명령어command를 하나의 수식으로 모델링 한 후에 수학적 추론을 적용하여 결과를 수식으로 도출하는 방식이다.

1 2 3 4 5