프로그래밍의 도를 찾아서

도입

프로그래밍 언어의 의미를 어떻게 정의할 수 있을까?

대부분의 프로그래머들이 사용하는 프로그래밍 언어는 사람들이 쓰는 자연어를 통해 정의되어 있다. "for 문은 이렇게 작동하고, for를 써서 이렇게 생긴 프로그램을 작성할 수 있으며 이렇게 돌아간다."라고 설명하는 방식이다.

하지만 프로그래밍 언어가 작동 방식을 정의하기 위해서 자연어를 사용하는 것에는 한계가 있다. 어떤 프로그램이 가지는 성질을 명확히 보이기 위해서는, 그 프로그램을 작성하기 위해 사용한 언어의 의미를 엄밀하게 표현할 수 있어야 하기 때문이다. 사람들이 일상 속에서 사용하는 언어를 통해 프로그래밍 언어를 모호함 없이 정확히 설명하는데에는 한계가 있다.

자연의 법칙을 설명하기 위한 언어가 수학이 된 것도 이와 같은 맥락에 있다. 모호함 없이 규칙을 가장 잘 설명할 수 있는 언어가 수학이기 때문이다.

프로그래밍 언어의 의미를 엄밀하게 정의내리는 여러 방법 중, 프로그램 각각의 의미를 수학적으로 잘 정의된 의미공간의 대상에 직접 대응하는 방식을 "직접 의미구조(denotational semantics)"라고 부른다. 이는 각 프로그램을 실행해서 간접적으로 의미를 정의내리는, "실행 의미구조(operational semantics)"에 비해 직접적인 방식이다.

하지만 이를 집합 이론으로 표현하는 것은 불가능하다. 간단히 어떤 값들의 집합 $D$ 과 값을 받아 값을 내놓는 함수들의 집합 $D → D$ 을 생각해보자. 그리고 이런 함수도 마찬가지로 값 집합 $D$ 에 들어있어야 한다고 하자. Python에서 함수를 값으로 쉽게 취급할 수 있는 것처럼 말이다:

def f(x):
  return x
 
g = f(f)

그런데 $D = D → D$ 는 칸토어(Cantor)의 대각선 논변에 따라 (집합 세상에서는) 원소가 하나 들어있는 집합을 제외하면 해가 존재하지 않는다. 프로그래밍 언어에서 표현할 수 있는 대상이 하나뿐이라면 당연히 쓸모가 없을 것이고, 실제로 우리가 프로그래밍 할 때는 풍부한 값들을 다루게 된다.

프로그래밍 언어가 다루는 값들의 공간을 엄밀하게 정의한 것은 다나 스콧(Dana Scott)과 크리스토퍼 스트래치(Christopher Strachey)의 의미공간 이론(domain theory)이다.

칸토어의 함정에 빠지지 않고 이 공간을 잘 정의할 수 있는 아이디어의 핵심은 바로 "정의된 정도"를 순서 관계로 보는 것이다.

본 글에서는 순서 관계가 정의된 집합들에 대해서 먼저 다루고, 다음 글에서는 이를 통해 프로그래밍 언어의 의미구조를 정의한다.

순서 집합들

Cpo(complete-partial order)라고 부르는 완비부분순서는 사람에 따라 아래에서 정의할 방향 완비부분순서 dcpo를 의미할 수도, 뾰족한 방향 완비부분순서 cppo를 의미할 수도 있다.

원순서(preordered set, proset)

집합 $A$ 에서 정의된 이항 관계 $⊑$ 가 반사적(reflexive)이고 전이적(transitive)이라면 원순서(preorder)라고 한다:

반사성: $∀ a ∈ A.\ a ⊑ a$ ,
전이성: $∀ a, b, c ∈ A.\ (a ⊑ b) ∧ (b ⊑ c) ⇒ (a ⊑ c)$ .

그리고 이러한 집합 $A$ 를 원순서 집합(preordered set, proset)이라고 부른다. ◻

부분순서(partially ordered set, poset)

Proset $(A, ⊑)$ 에서 $⊑$ 가 반대칭적(antisymmetric)이라면 부분순서라고 한다:

반대칭성: $∀ a, b ∈ A.\ (a ⊑ b) ∧ (b ⊑ a) ⇒ a = b$ .

이러한 집합 $A$ 를 부분순서 집합(poset)이라고 부른다. ◻

방향 완비부분순서(directed-complete partial order, dcpo)

Poset $(A, ⊑)$ 의 모든 방향 부분집합(directed subset) $S$ 이 항상 최소 윗뚜껑(least upper bound) $⊔S$ 를 가지면, $⊑$ 를 방향 완비부분순서(directed-complete partial order, dcpo)라고 한다.

방향 부분집합 $S$ 은 비어있지 않으면서 모든 두 쌍의 원소들에 대해 항상 윗뚜껑(upper bound)이 포함된 부분집합이다:

$S ≠ \varnothing$ ,
$∀ a, b ∈ S.\ ∃ c ∈ S.\ (a ⊑ c) ∧ (b ⊑ c)$ .

여기서 유의할 점은, 꼭 $c = a ⊔ b$ 일 필요는 없다는 것이다. ◻

$(A, ⊑)$ 자체를 그냥 dcpo라고 흔히 부른다. 영어에서는 너무 길어져서 direct-complete partially ordered set라고는 거의 부르지 않는 것으로 보인다.

$S ≠ \varnothing$ 조건이 왜 필요할까? 해당 조건이 없어도 방향 부분집합의 두 번째 조건은 공허하게 성립(vacuously true)할텐데 말이다.

Poset은 바닥이 없어도 되기 때문에, 공집합에 대해서는 최소 윗뚜껑이 없을 수 있기 때문이다. 바닥이 갖춰지지 않은채 뚫려있으면 어떤 원소를 윗뚜껑이라고 가져와도 더 작은 값을 찾을 수 있으므로, $⊔ \varnothing$ 은 있을 수 없다.

뾰족한 방향 완비부분순서(pointed directed-complete partial order, pointed dcpo, cppo)

Dcpo $(A, ⊑)$ 가 바닥(bottom) $⊥$ 을 가지면 뾰족한 방향 완비부분순서(pointed dcpo, cppo)라고 부른다. ◻

추가된 조건을 통해, 방향 부분집합뿐만이 아니라 공집합에 대해서도 항상 윗뚜껑이 포함된다는 것을 알 수 있다.

지금까지 다룬 dcpo(당연히 cppo 포함)는 방향 부분집합에 대해서만 최소 윗뚜껑을 찾았는데, 조금 더 강력하게 모든 부분집합에 대해서 최소 윗뚜껑이 있는 구조를 원할 때도 있다. 이러한 구조는 격자에서 찾아볼 수 있다.

만남/이음 반격자 (joint/meet-semilattice)

Poset $(A, ⊑)$ 에서 모든 유한한 부분집합 $S$ 에 대해 항상 최소 윗뚜껑 $⊔S$ 이 존재하면 만남 반격자(joint semilattice)라고 한다. 비슷하게 모든 유한한 부분집합 $S$ 에 대해 항상 최대 밑뚜껑 $⊓S$ 이 존재하면 이음 반격자(meet semilattice)라고 한다. ◻

완비 격자 (complete lattice)

Poset $(A, ⊑)$ 에서 모든 부분집합 $S$ 에 대해 항상 최소 윗뚜껑 $⊔S$ 과 최대 밑뚜껑 $⊓S$ 이 존재하면 완비 격자(complete lattice)라고 한다. 즉, 완비 격자는 만남 반격자와 이음 반격자를 모두 만족하는 구조이다. ◻

의미공간 이론: 몇 가지 순서 구조들

목차