목차
도입
프로그래밍 언어의 의미를 어떻게 정의할 수 있을까?
대부분의 프로그래머들이 사용하는 프로그래밍 언어는 사람들이 쓰는 자연어를 통해 정의되어 있다.
"for
문은 이렇게 작동하고, for
를 써서 이렇게 생긴 프로그램을 작성할 수 있으며 이렇게 돌아간다."라고 설명하는 방식이다.
하지만 프로그래밍 언어가 작동 방식을 정의하기 위해서 자연어를 사용하는 것에는 한계가 있다. 어떤 프로그램이 가지는 성질을 명확히 보이기 위해서는, 그 프로그램을 작성하기 위해 사용한 언어의 의미를 엄밀하게 표현할 수 있어야 하기 때문이다. 사람들이 일상 속에서 사용하는 언어를 통해 프로그래밍 언어를 모호함 없이 정확히 설명하는데에는 한계가 있다.
자연의 법칙을 설명하기 위한 언어가 수학이 된 것도 이와 같은 맥락에 있다. 모호함 없이 규칙을 가장 잘 설명할 수 있는 언어가 수학이기 때문이다.
프로그래밍 언어의 의미를 엄밀하게 정의내리는 여러 방법 중, 프로그램 각각의 의미를 수학적으로 잘 정의된 의미공간의 대상에 직접 대응하는 방식을 "직접 의미구조(denotational semantics)"라고 부른다. 이는 각 프로그램을 실행해서 간접적으로 의미를 정의내리는, "실행 의미구조(operational semantics)"에 비해 직접적인 방식이다.
하지만 이를 집합 이론으로 표현하는 것은 불가능하다. 간단히 어떤 값들의 집합 과 값을 받아 값을 내놓는 함수들의 집합 을 생각해보자. 그리고 이런 함수도 마찬가지로 값 집합 에 들어있어야 한다고 하자. Python에서 함수를 값으로 쉽게 취급할 수 있는 것처럼 말이다:
그런데 는 칸토어(Cantor)의 대각선 논변에 따라 (집합 세상에서는) 원소가 하나 들어있는 집합을 제외하면 해가 존재하지 않는다. 프로그래밍 언어에서 표현할 수 있는 대상이 하나뿐이라면 당연히 쓸모가 없을 것이고, 실제로 우리가 프로그래밍 할 때는 풍부한 값들을 다루게 된다.
프로그래밍 언어가 다루는 값들의 공간을 엄밀하게 정의한 것은 다나 스콧(Dana Scott)과 크리스토퍼 스트래치(Christopher Strachey)의 의미공간 이론(domain theory)이다.
칸토어의 함정에 빠지지 않고 이 공간을 잘 정의할 수 있는 아이디어의 핵심은 바로 "정의된 정도"를 순서 관계로 보는 것이다.
본 글에서는 순서 관계가 정의된 집합들에 대해서 먼저 다루고, 다음 글에서는 이를 통해 프로그래밍 언어의 의미구조를 정의한다.
순서 집합들
Cpo(complete-partial order)라고 부르는 완비부분순서는 사람에 따라 아래에서 정의할 방향 완비부분순서 dcpo를 의미할 수도, 뾰족한 방향 완비부분순서 cppo를 의미할 수도 있다.
원순서(preordered set, proset)
집합 에서 정의된 이항 관계 가 반사적(reflexive)이고 전이적(transitive)이라면 원순서(preorder)라고 한다:
- 반사성: ,
- 전이성: .
그리고 이러한 집합 를 원순서 집합(preordered set, proset)이라고 부른다. ◻
부분순서(partially ordered set, poset)
Proset 에서 가 반대칭적(antisymmetric)이라면 부분순서라고 한다:
- 반대칭성: .
이러한 집합 를 부분순서 집합(poset)이라고 부른다. ◻
방향 완비부분순서(directed-complete partial order, dcpo)
Poset 의 모든 방향 부분집합(directed subset) 이 항상 최소 윗뚜껑(least upper bound) 를 가지면, 를 방향 완비부분순서(directed-complete partial order, dcpo)라고 한다.
방향 부분집합 은 비어있지 않으면서 모든 두 쌍의 원소들에 대해 항상 윗뚜껑(upper bound)이 포함된 부분집합이다:
- ,
- .
여기서 유의할 점은, 꼭 일 필요는 없다는 것이다. ◻
자체를 그냥 dcpo라고 흔히 부른다. 영어에서는 너무 길어져서 direct-complete partially ordered set라고는 거의 부르지 않는 것으로 보인다.
조건이 왜 필요할까? 해당 조건이 없어도 방향 부분집합의 두 번째 조건은 공허하게 성립(vacuously true)할텐데 말이다.
Poset은 바닥이 없어도 되기 때문에, 공집합에 대해서는 최소 윗뚜껑이 없을 수 있기 때문이다. 바닥이 갖춰지지 않은채 뚫려있으면 어떤 원소를 윗뚜껑이라고 가져와도 더 작은 값을 찾을 수 있으므로, 은 있을 수 없다.
뾰족한 방향 완비부분순서(pointed directed-complete partial order, pointed dcpo, cppo)
Dcpo 가 바닥(bottom) 을 가지면 뾰족한 방향 완비부분순서(pointed dcpo, cppo)라고 부른다. ◻
추가된 조건을 통해, 방향 부분집합뿐만이 아니라 공집합에 대해서도 항상 윗뚜껑이 포함된다는 것을 알 수 있다.
지금까지 다룬 dcpo(당연히 cppo 포함)는 방향 부분집합에 대해서만 최소 윗뚜껑을 찾았는데, 조금 더 강력하게 모든 부분집합에 대해서 최소 윗뚜껑이 있는 구조를 원할 때도 있다. 이러한 구조는 격자에서 찾아볼 수 있다.
만남/이음 반격자 (joint/meet-semilattice)
Poset 에서 모든 유한한 부분집합 에 대해 항상 최소 윗뚜껑 이 존재하면 만남 반격자(joint semilattice)라고 한다. 비슷하게 모든 유한한 부분집합 에 대해 항상 최대 밑뚜껑 이 존재하면 이음 반격자(meet semilattice)라고 한다. ◻
완비 격자 (complete lattice)
Poset 에서 모든 부분집합 에 대해 항상 최소 윗뚜껑 과 최대 밑뚜껑 이 존재하면 완비 격자(complete lattice)라고 한다. 즉, 완비 격자는 만남 반격자와 이음 반격자를 모두 만족하는 구조이다. ◻