논리적인 말?

언제 어떤 문장이 "논리적이다"고 할 수 있을까? 일상적으로는 우리는 이를 남용해 의미가 있어 보이는 것을 "논리적이다"라고 수식하고는 한다. 그러나 필자는 이 남용이 "논리적"이라는 표현을 너무 가볍게 보고 있는 것이라 말하겠다. 어떤 것이 진정 논리적이기 위해서는 의미가 있는 것은 물론이거니와 최소한 다음의 두 조건을 더 만족해야한다.

1. 몇몇 가정으로부터 그것을 증명해야 한다.
2. 증명에 쓰인 체계가 모순을 보일 수 없어야 한다.

이 글에서는 이 중 1 번을 중점으로 설명하여 "좋은 가정 아래" 어떤 것이 논리적임을 증명하는 두 방법에 대해 다루어 볼 것이다. 두 방법 중 하나는 함수형 언어로 쓰인 프로그램과 유사한 구조를 가지며 나머지 하나는 일반적인 함수형 언어와는 상이한 구조를 가진다. 이 중 두번째 방법에 대해서는 (약간의 부정행위를 하면…\ldots) 2 번을 간단하게 보일 수 있기 때문에 이 또한 다룰 것이다.

논리적 증명의 대상

어떻게 어떤 것이 논리적이라는 걸 증명할 수 있는 지에 설명하기에 앞서 짚고 넘어가야 할 매우 중요한 요소가 하나 있다. 바로

는 것이다. 이 글에서는 철학적인 복잡도를 덜기 위해 이 대상을 다음과 같이 단순히 설명할 것이다.

논리적일 수 있는 대상은 명제(proposition)에 대한 판단(judgment)이다.

여기서 명제는 다음과 같이 정의되는 대상이다.

1. 단위 명제(Atomic Proposition) AA는 명제이다.
2. 참 명제(True Proposition) ⊤\top은 명제이다.
3. 거짓 명제(False Proposition) ⊥\bot은 명제이다.
4. 명제 PP와 QQ가 있을 때, P∧QP \land Q(PP 그리고 QQ)는 명제이다.
5. 명제 PP와 QQ가 있을 때, P∨QP \lor Q(PP 또는 QQ)는 명제이다.
6. 명제 PP와 QQ가 있을 때, P→QP \to Q(PP라면 QQ)는 명제이다.

여기서 단위 명제란 우리가 선택한, 더이상 세밀하게 분석하지 않을 논리적인 최소 단위이다. 예를 들어 1+1=21 + 1 = 2와 0+2=30 + 2 = 3을 단위 명제로 두었을 때^[1] 다음과 같은 것들이 명제이다.

• ⊤\top
• 1+1=21 + 1 = 2
• (1+1=2)∧(0+2=3)(1 + 1 = 2) \land (0 + 2 = 3)
• (0+2=3)→⊥(0 + 2 = 3) \to \bot
• ⊤→⊥\top \to \bot

그렇다면 판단이란 무엇인가? 우리가 명제에 가지는 논리적 태도이다. 이 글에서는 다음과 같은 판단만을 이야기 할 것이다.

P trueP\ \texttt{true}, 즉 명제 PP가 참이다.

이를 "진리 판단"("truth judgment")이라고 한다. 좀 더 엄밀히는 다음과 같이 가정을 포함한 판단에 대해 다룰 것이다.

• Γ⊢P true\Gamma \vdash P\ \texttt{true}

이 판단은 어떤 진리 판단의 나열 Γ\Gamma을 가정했을 때 명제 PP가 참이라고 말하는 판단이다. 이를 "가정적 판단"("hypothetical judgement")이라고 한다. 또한 여기서 Γ\Gamma를 "가정"("hypothesis") 혹은 "전건"("前件", "antecedent")이라고 하고, P trueP\ \texttt{true}를 "귀결("consequent") 혹은 "후건"("後件", "succedent")이라고 한다. 요약하자면 이 절의 핵심 질문

에 대한 답은 다음과 같다.

진짜 논리적이 되는 방법 1 - 자연 연역(Natural Deduction)

이제 어떤 가정적 판단이 논리적인지 증명하는 한 방법에 대해서 알아보자. 우선 PP가 참이라는 판단이 가정 중 하나라면 당연히 그 가정 아래에서는 PP가 참이라고 판단할 수 있을 것이다. 이를 간략하게 표현한 규칙(rule)이

이다. 이 규칙 표현은 줄 위의 것들을 전제(premise)로 줄 밑의 결론(conclusion)을 추론(infer)해 낼 수 있음을 말한다. 전제에 쓰여있는 P true∈ΓP\ \texttt{true} \in \Gamma는 P trueP\ \texttt{true}가 가정의 나열 Γ\Gamma에 포함되어 있음을 말한다. 또한 줄 옆에 써져있는 "hyp"는 이 추론 규칙(inference rule)의 이름으로서 가정(hypothesis)을 사용한다는 것을 나타낸다.

이런 추론 규칙을 명제를 만드는 각각의 방법에 대해 정의할 수 있다. 참 명제 ⊤\top에 대해서는

라는 규칙을 줄 수 있다. 이 규칙 I⊤\text{I}\top은 어떤 Γ\Gamma를 가정하든 참 명제는 참이라고 판단할 수 있다는 규칙이다. 여기서 이름의 I\text{I}는 참 명제를 결론에 소개(Introduce)하는 규칙이라는 뜻이다. 대칭적으로 거짓 명제에 대해서는

라는 규칙을 줄 수 있다. 이 규칙 E⊥\text{E}\bot은 어떤 가정들 Γ\Gamma로 부터 거짓 명제가 참이라고 판단했다면 그 가정들 아래에서는 아무 명제나 참이라고 판단할 수 있다는 규칙이다^[2]. 여기서 이름의 E\text{E}는 우리가 거짓 명제가 참임을 결론으로 가지는 전제에 도달했을 때 그 결론을 제거(Eliminate)하여 다른 결론에 도달할 수 있도록 하는 규칙이라는 뜻이다.

⊤\top과 ⊥\bot을 제외한 명제를 만드는 방법들은 이 두 종류의 규칙(I\text{I} 규칙과 E\text{E} 규칙)을 모두 가진다. P∧QP \land Q의 경우는 다음과 같다.

I∧\text{I}\land는 Γ\Gamma를 가정하여 PP와 QQ 각각이 참이라 판단했다면 같은 가정에서 P∧QP \land Q도 참이라고 판단할 수 있다는 규칙이다. 반대로 E∧\text{E}\land는 Γ\Gamma를 가정하여 P∧QP \land Q이 참이라 판단했고 Γ\Gamma에 더해 P trueP\ \text{true}와 Q trueQ\ \text{true}를 가정했을 때 RR이라는 명제가 참이라고 판단할 수 있다면 Γ\Gamma만 가정하고도 RR이 참이라고 판단할 수 있다는 뜻이다. P∨QP \lor Q와 P→QP \to Q를 위한 규칙도 나열하면 다음과 같다.

여기서 I∨1\text{I}\lor_1과 I∨2\text{I}\lor_2는 PP나 QQ 중 하나가 참이라고 판단했다면 P∨QP \lor Q가 참이라고 판단할 수 있다는 규칙이며 E∨\text{E}\lor는 P∨QP \lor Q가 참이라고 판단할 수 있고 PP가 참이라고 가정하든 QQ가 참이라고 가정하든 RR이 참이라고 판단할 수 있다면 그 가정 없이 RR이 참이라고 판단할 수 있다는 규칙이다. I→\text{I}\to는 PP가 참임을 가정해서 QQ가 참이라고 판단할 수 있다면 P→QP \to Q 또한 참이라고 판단할 수 있다는 규칙이며 E→\text{E}\to는 P→QP \to Q가 참이라고 판단할 수 있고 PP가 참이라고 판단할 수 있다면 QQ가 참이라고 판단할 수 있다는 규칙이다. 이렇게 소개 규칙과 제거 규칙의 쌍으로 논리적 증명을 하는 방식을 "자연 연역"("Natural Deduction")이라고 한다.

자연 연역으로 단순한 논리적 증명을 하는 방법의 예시를 들어보겠다. 어떤 단위 명제 AA, BB, CC에 대해서 A→BA \to B와 B→CB \to C가 참이라고 판단했다면 A→CA \to C 또한 참이라 판단할 수 있다. 이 증명은 다음과 같다. 우선 A→BA \to B 그리고 B→CB \to C와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.

이를 써서 다음과 같이 증명을 끝낼 수 있다.

따라서 논리적으로 A→BA \to B 그리고 B→CB \to C가 참임을 가정했을 때 A→CA \to C가 참이라고 판단할 수 있다.

자연 연역과 함수형 언어

혹자는 위 규칙들에서 미묘한 친숙함을 발견했을지도 모른다. 이를 좀 더 구체적으로 살펴보기 위해 →\to의 규칙들을 다시 살펴보자.

여기에 약간의 조작을 가해보자. 우선 Γ\Gamma를 단순한 판단의 나열로 취급하는 대신 이름 붙은 판단들로 취급하자. 예를 들어 위의 P trueP\ \texttt{true} 라는 판단에 xx라는 이름을 붙이면 다음과 같은 규칙을 얻는다.

더욱이 각각의 규칙들에 지금까지의 증명을 나타내는 항들을 더해보도록 하겠다. 예를 들어 I→\text{I}\to 규칙에서 Γ,x:P true⊢Q true\Gamma, x {:} P\ \texttt{true} \vdash Q\ \texttt{true}가 어떤 항 MM으로 나타내지는 증명이라면 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}의 증명은 fun (x:P)⇒M\mathtt{fun}\ (x \mathbin{:} P) \Rightarrow M이라는 항으로 나타내도록 하자. 마찬가지로 E→\text{E}\to 규칙에서 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}가 MM, Γ⊢P true\Gamma \vdash P\ \texttt{true}가 NN이라는 항으로 나타내진다면 Γ⊢Q true\Gamma \vdash Q\ \texttt{true}의 증명은 M NM\ N으로 나타내도록 하자. 이 항들을 판단에 끼워넣으면 다음과 같이 규칙을 바꿔 쓸 수 있다.

이는 (단순한) 함수형 언어의 형 검사 규칙과 동일하다! 함수 fun (x : P) => M이 형 P -> Q를 가지는지 검사하고 싶을 때는 x : P를 가정한 뒤 M이 형 Q를 가지는지 검사하면 된다. 또한 함수 M을 인자 N에 적용하는 것이 형 Q를 가지는지 알고 싶다면 함수 M이 형 P -> Q를 가질 때 인자 N이 형 P를 가지는지 검사하면 된다. 마찬가지 변화를 다음과 같이 모든 추론 규칙들에 적용할 수 있다.

⊤\top은 단위(unit) 자료형에 대응되며 ⊥\bot은 빈 자료형에 대응되고 P∧QP \land Q는 P 형과 Q 형의 쌍(pair) 자료형에 대응된다. 같은 방식으로 P∨QP \lor Q는 P 형과 Q 형의 합(sum) 자료형^[3]에 대응된다. 항에서부터 각각의 추론 규칙이 (I\texttt{I} 규칙의 경우) 각 자료형의 생성자(constructor)나 (E\texttt{E} 규칙의 경우) 패턴 맞추기(pattern matching)의 형 검사 규칙에 대응된다는 것을 볼 수 있을 것이다. 이를 처음 구체화시킨 두 사람의 이름을 따 이 대응을 "커리-하워드 대응"("Curry-Howard correspondence")이라고 부른다. 이 대응이 발견됨으로써 논리적인 사고와 프로그래밍 언어의 이해 간에 중요한 연결고리가 생겼고 이는 현재에도 프로그래밍 언어의 발전과 논리학의 발전 양측에 모두 지대한 영향을 끼치고 있다.

이 대응을 따랐을 때 어떤 판단을 증명한다는 것은 그 판단의 형을 가지는 프로그램(program)을 짜는 것과 동일하다. 이를 보다 구체적으로 이해하기 위해 앞서의 예시 증명을 다시 반복해보자. 증명의 너비를 줄이기 위해 Γ\Gamma를 x:A→B true,y:B→C true,z:A truex{:}A \to B\ \texttt{true},\allowbreak y{:}B \to C\ \texttt{true}\allowbreak, z{:}A\ \texttt{true} 대신 사용하겠다.

즉 함수 x : A -> B와 인자 z : A가 있을 때 함수 적용 x z이 B trueB\ \texttt{true}의 증명이다. 이어서,

따라서 fun (z : A) => y (x z)가 x : A -> B와 y : B -> C가 주어졌을 때 A→C trueA \to C\ \texttt{true}의 증명이다.

지금까지 자연 연역에 대해서 알아보았다. 자연 연역은 함수형 언어를 쓰는 사람들에게는 어찌보면 매우 친숙할 수 있는 증명 방식이다. 그러나 자연 연역을 사용했을 때 거짓을 증명할 수 없다는 것을 보이는 것은 쉽지 않다. 자연 연역을 처음 도입한 게르하르트 겐첸(Gerhard Gentzen)은 같은 논문에서 거짓을 증명할 수 없다는 것을 보다 쉽게 보일 수 있는 다른 방식 또한 소개하였는데, 그것이 바로 논건 대수(論件 代數, Sequent Calculus)^[4]이다.

진짜 논리적이 되는 방법 2 - 논건 대수(論件 代數, Sequent Calculus)

논건 대수 또한 명제의 진리에 대한 가정적 판단을 추론 규칙을 통해 이끌어낸다는 점은 자연 연역과 동일하다. 자연 연역과 논건 대수의 가장 큰 차이점은 명제를 만드는 각 방법에게 어떤 식으로 추론 규칙을 부여하는지에 있다. 자연 연역에서는 소개 규칙(I\text{I} 규칙)과 제거 규칙(E\text{E} 규칙)이라는 분류를 통해 ∧\land, ∨\lor, …\ldots에 추론 규칙을 부여했다. 논건 대수의 접근법은 이와는 살짝 다르다. 예를 들어 논건 대수에서의 P∧QP \land Q의 규칙에 대해 살펴보자.

차이점을 눈치챘는가? 크게 두 차이점이 있다.

1. 규칙의 이름이 다르다. 😅
2. E∧\text{E}\land을 대체하는 L∧\text{L}\land의 꼴이 다르다.

먼저 이름의 차이를 설명하고 넘어가자. 자연 연역의 경우 I∧\text{I}\land 규칙은 ∧\land를 소개(introduce)하는 규칙, E∧\text{E}\land 규칙은 ∧\land를 제거(eliminate)하는 규칙이었다. 반면에 논건 대수의 R∧\text{R}\land 규칙은 ∧\land를 오른쪽(Right side)에 소개하는 규칙이고 L∧\text{L}\land 규칙은 ∧\land를 왼쪽(Left side)에 소개하는 규칙이다. E∧\text{E}\land와 L∧\text{L}\land의 꼴의 차이는 이 접근법의 차이에서부터 자연스럽게 따라나온 것이다.

명제를 만드는 다른 방법들에 있어서도 논건 대수의 방식을 따라서 추론 규칙을 마련해 줄 수 있다.

그리고 논건 대수가 자연 연역과 동등함을 (비교적) 쉽게 보이기 위해서는 명제를 만드는 각 방식의 R\text{R}과 L\text{L} 규칙에 더해 다음의 두 규칙을 추가해야한다.

여기서 init\text{init} 규칙은 자연 연역에서의 hyp\text{hyp} 규칙과 같은 꼴이다. 반면에 cut\text{cut} 규칙은 직접적으로 비교할만한 자연 연역에서의 규칙이 존재하지 않는데, 이는 논건 대수가 자연 연역과 전혀 다른 방식으로 증명을 전개하기 때문이다. 자연 연역에서는 예를 들어 I∧\text{I}\land 규칙으로 만들어진 P∧QP \land Q가 참이라는 판단을 바로 E∧\text{E}\land에 사용할 수 있었다. 함수형 언어로 말하자면

case (M, N) of
  (x, y) => L

같은 꼴의 사용이 가능했다. 그러나 논건 대수에서는 R∧\text{R}\land 규칙은 가정적 판단의 (오른쪽) 후건에, L∧\text{L}\land 규칙은 가정적 판단의 (왼쪽) 전건에 ∧\land를 새로 만들어낼 뿐이고 두 규칙이 상호작용할 수 있는 방법이 없다. 이 공백을 해결해주는 규칙, 즉 자연 연역의 I\texttt{I}/E\texttt{E} 규칙 쌍의 상호작용에 의한 증명을 논건 대수에서도 표현할 수 있게 해주는 규칙이 바로 cut\text{cut} 규칙이다.

그런데 이 상호작용은 과연 필요한 것인가? 위의 함수형 언어를 통한 예시에서 보다 분명히 볼 수 있는 것은 예시의 I∧\text{I}\land와 E∧\text{E}\land 규칙의 연달은 사용이 사실은 불필요하다는 점이다. 이는 자연 연역에서는 저런 식의 증명 대신 L에서 x가 등장하는 자리에 M을 치환해넣고, y가 등장하는 자리에 N을 치환해넣은 증명 또한 가능하기 때문이다. 이런 상호작용의 불필요성에 대한 대한 자연 연역에서의 직관을 이에 대응되는 논건 대수의 cut\text{cut} 규칙에 대해서 구체화한 것이 바로 다음의 cut\text{cut} 제거 정리이다.

cut\text{cut} 제거 정리의 의의는 단순히 필요없는 규칙을 제거하는 정도에 멈추지 않는다. cut\text{cut}을 제거하고 나면 논건 대수에서 가정 없이는 거짓을 증명하지 못한다는 것이 자명해지기 때문이다.

증명은 다음의 네 문장이면 충분하다.

1. 귀결이 ⊥ true\bot\ \texttt{true}인 R\text{R} 규칙이 존재하지 않기 때문에 어떤 R\text{R} 규칙도 쓸 수 없다.
2. 가정이 없기 때문에 어떤 L\text{L} 규칙도 쓸 수 없다.
3. 마찬가지로 가정이 없기 때문에 init\text{init} 규칙을 쓸 수 없다.
4. 따라서 어떤 규칙도 판단 ⊢⊥ true\vdash \bot\ \texttt{true}을 결론으로 주지 않는다.

앞서 이 글의 서두에서 논건 대수의 일관성을 보이기 위해 "약간의 부정행위"를 저지를 것이라고 말했다. 오해가 없도록 명시하자면 위의 증명은 cut\text{cut}을 제거한 논건 대수에 있어서는 문제가 없다. 부정행위라고 부를 만한 부분은 바로 cut\text{cut} 제거 정리의 증명이 더 어렵다는 점이다. 이 증명은 단순화하기 쉽지 않기 때문에 글에서 직접적으로 다루지는 않을 것이고, 이것이 바로 서두에서 언급한 "부정행위"이다. 다만 이 어려운 증명도 수학적 귀납법(Induction) 이상의 지식은 필요로 하지 않기 때문에, 시도해보고자 하는 독자가 있다면 직접 시도해 볼 수 있을 것이다^[5].

논건 대수의 소개를 앞서의 예시 증명을 논건 대수에서 반복하는 것으로 마치도록 하자. 우선 A→BA \to B와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.

이를 써서 다음과 같이 증명을 끝낼 수 있다.

앞서의 자연 연역 증명의 구조가 크게 다름에 주의해서 논건 대수 증명의 구조를 이해해보도록 하자. 앞서의 자연 연역 증명은

의 구조를 가지고 있다. 즉 결론에 I\texttt{I} 규칙을 적용하고 어떤 가정에 E\texttt{E} 규칙을 적용해서 이 둘이 만나는 지점을 찾는 것이 증명의 구조이다. 이와는 다르게 논건 대수의 증명은

와 같이 (여러 개의) init\texttt{init} 규칙에서 시작해서 L\texttt{L} 규칙으로 가정, R\texttt{R} 규칙으로 귀결을 변경해 결론에 도달할 때까지 차례로 내려오는 구조를 가진다. 이런 구조의 차이가 바로 (자연 연역의) hyp\texttt{hyp} 규칙과 (논건 대수의) init\texttt{init} 규칙이 (같은 꼴임에도 불구하고) 다른 이름을 가지게 된 이유이자 논건 대수의 init\texttt{init} 규칙이 시작점(initial point)에 해당하는 이름을 가지게 된 이유이다.

논건 대수의 항

논건 대수를 좀 더 컴퓨터 공학적으로 이해할 수 있을까? 이를 위해 자연 연역의 경우와 마찬가지로 논건 대수에도 증명에 커리-하워드 대응을 통해 항을 주려고 시도할 수 있다. 그러나 앞서 언급한 것처럼 논건 대수 증명은 자연 연역의 증명, 그러니까 함수형 언어와 구조가 크게 다르다. 따라서 원본 그대로의 논건 대수에 주는 항은 상대적으로 복잡하고 다양한 개념들(생산자, 소비자, 소비자를 생산자로 바꾸기, 생산자와 소비자가 거래하게 하기, …\ldots)을 요구하고, 결과적으로 이는 컴퓨터 공학적인 직관성이 떨어지는 복잡한 항을 만들어 내게 된다. 이어질 2 편에서는 논건 대수에 약간의 변형을 가하면 직관적이고 쉽게 이해가 가능한 항을 줄 수 있으며, 항이 뜻하는 바가 저수준(low-level) 자료 표현(data representation)과 자연스럽게 연결될 수 있음을 설명할 것이다.

마치며

2 편의 "논리와 저수준 자료표현" 연작 중 1 편인 이 글에서는 논리적 증명을 하는 두 방법과 커리-하워드 대응에 대해서 설명했다. 1 편의 내용은 말하자면 2 편의 바탕 및 서두 역할을 하고 있다. 이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며 이만 마치도록 하겠다.

---

1. 이 중 두번째 단위 명제는 일반적인 자연수 체계에서 거짓이나, 명제의 정의 자체는 명제가 참인지 거짓인지에 대해 논하지 않는다는 것을 강조하기 위해 단위 명제에 포함하였다. ↩︎

2. 거짓도 참이라면 대체 무엇이 참이 아니겠는가? ↩︎

3. 이는 Rust나 OCaml의 Result 형 혹은 Haskell의 Either형과 같은 형이다. ↩︎

4. 전건(前件, antecedent)과 후건(後件, succedent)을 개별적으로 다룰 수 있다는 의미에서 "Sequent Calculus"를 논건 대수(論件 代數)라고 번역하였다. 보다 일반적으로 "시퀀트 대수"라는 표현이 쓰이나, 이는 "시퀀트"가 의미하는 바가 "논리에서 다루는 물건/사건/…\ldots"이라는 표현보다 직관성이 떨어진다고 보아 재번역을 하였다. ↩︎

5. 증명에 대한 구체적인 질문이 있다면 답글을 남겨주기를 바란다. ↩︎

마지못해 패키지를 만들어야 할 것 같은 사람을 위한 설명입니다. 제대로된 패키지를 만들고 싶은 경우에는 부족한 점이 많습니다.

대부분의 경우에는 프로그램을 직접 소스에서 빌드하는 일도 적고, 그걸 시스템 전역에 설치하는 일도 흔치는 않을 것입니다. 좋은 패키지매니저와 관리가 잘되는 패키지 저장소들을 두고 아주 가끔은 직접 빌드를 할 일이 생기고, 흔치 않게 시스템 전역에 설치할 일이 생길 수 있습니다. 어지간한 프로그램들은 요즈음의 장비에서는 별 불만 없이 빌드 할 만한 시간이 소요되나, 컴파일러처럼 한번 빌드했으면 다시는 하고 싶지 않은 프로그램을 다시 설치해야하는 경우도 있을 수 있습니다. 하필 이런 프로그램들은 결과물도 덩치가 매우 큽니다. 이럴 때는 최대한 간단하고 필요한 항목만 패키지에 넣어서 만들어두고 다시 활용하면 좋을 것이기에 이런 경우를 위한 rpmbuild에 대한 나름 최소한의 사용 방법을 정리해봅니다.

rpmbuild

rpmbuild는 rpm-build 패키지로 설치가 가능하며, 나름 단순하게 rpm으로 패키징을 할 수 있는 유틸리티입니다. spec파일에 패키지 정보, 빌드 명령, 설치 명령, 패키지가 포함해야 할 파일 목록을 작성해서 rpmbuild에 입력으로 넣어주면 빌드부터 시작해서 rpm패키지를 만들어줍니다. native 프로그램의 경우 디버그 심볼을 알아서 분리해서 별도의 패키지로 만들어주고, 필요한 의존성도 추정해서 명시해줍니다. 또한, 필요한 경우 하나의 spec 명세로 연관된 서브 패키지도(ex. 실행파일 패키지인 curl과 라이브러리 패키지 libcurl, 라이브러리를 사용하기 위한 개발 패키지 libcurl-devel) 같이 만들 수 있습니다.

작업 환경

rpmbuild는 기본으로 ~/rpmbuild/{BUILD,RPMS,SOURCES,SPECS,SRPMS,BUILDROOT}의 경로에서 동작하며 각 경로의 용도는 다음과 같습니다.

• SOURCES에는 압축된 소스코드가 위치합니다.
• SPECS에는 패키지 정의인 spec파일을 둡니다.
• BUILD밑에서 빌드 작업이 진행됩니다.
• RPMS에 바이너리 rpm결과물이 생성됩니다.
• SRPMS에는 소스 rpm결과물이 생성됩니다.
• BUILDROOT는 패키징 하기 위해 빌드 결과물을 모으는 경로입니다.

spec파일

spec파일은 패키지를 어떻게 빌드하고 어떤 항목들이 패키지에 포함될지, 패키지의 이름, 설명 및 의존성 등의 메타데이터, 패키지 설치, 삭제시의 스크립트를 정의할 수 있습니다. 보통 시작 부분에는 메타데이터 정의로 시작하며, 다음과 같은 기본적인 형태를 취합니다. 나름 단순하게 만든 python을 위한 spec을 예시로 들어보겠습니다.

Summary: Python %{version}
Name: python-alternative
Version: %{version}
Release: 1%{?dist}
Obsoletes: %{name} <= %{version}
Provides: %{name} = %{version}
URL: https://www.python.org
Requires: libffi openssl
AutoReq: no
License: PSFL

Source: https://www.python.org/ftp/python/%{version}/Python-%{version}.tgz

BuildRequires: libffi-devel openssl-devel
BuiltRoot: %{_tmppath}/%{name}-%{version}-%{release}-root

%define major_version %(echo "%{version}" | sed -E 's/^([0-9]+)\\..+/\1/' | tr -d)
%define minor_version %(echo "%{version}" | sed -E 's/^[0-9]+\\.([0-9]+)\\..+/\1/' | tr -d)

%description
Python

%package devel
Summary: python development files
Requires: %{name} = %{version}-%{release}

%description devel
Python development package

%prep
%setup -q -n Python-%{version}

%build
./configure --prefix=%{_prefix}

%install
%{__make} altinstall DESTDIR=%{buildroot}
%{__ln_s} -f %{_bindir}/python%{major_version}.%{minor_version} %{buildroot}/%{_bindir}/python%{major_version}

%clean
%{__rm} -rf %{buildroot}

%files
%{_bindir}/python*
%exclude %{_bindir}/idle*
%{_bindir}/pip*
%{_bindir}/pydoc*
%exclude %{_bindir}/2to3*
%{_libdir}/libpython*
%{_prefix}/lib/libpython*
%{_prefix}/lib/python*
%{_mandir}/man1/python*

%files devel
%{_includedir}/python*
%{_prefix}/lib/pkgconfig/python*

%로 매크로를 사용할 수 있으며, %package, %description, %files 같은 매크로는 인자를 주어서 서브 패키지를 정의하는데도 쓸 수 있습니다. 앞선 예제처럼 devel 이라고작성하면 메인 패키지이름 뒤에 붙여서 python-alternative-devel가 되며, curl - libcurl과 같은 경우에는 메인의 이름은 curl이고, 딸린 패키지를 정의할 때는 %package -n libcurl과 같이 -n옵션을 추가해서 지정할 수 있습니다. 몇몇 매크로는 단계를 정의하는 것과 같은 동작을 하며 다음과 같습니다.

%package

유사성을 보면 spec파일의 맨 첫부분은 메인 패키지의 %package에 해당하는 것이 아닌가 싶습니다. <Key>: <Value>의 형태로 메타정보를 작성합니다. 대부분은 Key를 보면 무슨 값인지 추측 할 만합니다. 나중에 설명할 %files에서 나열한 파일을 rpmbuild가 분석하여 자동으로 패키지가 필요로 하는 의존성을 추정해서 추가 해 줍니다. python 스크립트, perl 스크립트, native 실행파일 등을 분석해서 알아서 추가해주는 것 같은데, 경우에 따라서는 틀린 의존성을 추가해주기도 합니다. 이 때는 AutoReq: no를 설정하여 자동 의존성 추가를 막을 수 있습니다. 이 python-alternative 패키지는 /usr/local/bin/python%{version}을 설치하는데 아마도 같이 포함되는 python 스크립트에 의해서 /bin/python을 의존성으로 추정하여 요구합니다. 패키지 스스로가 제공하는 의존성은 미리 설치 되어있기를 요구하지 않게 동작하는 것 같으니 보통은 문제가 없습니다만, 이 경우에는 스스로 제공을 하지 않기 때문에 python을 설치하기 위해서 python이 필요한 경우가 발생하므로 AutoReq를 껐습니다.

%prep

준비단계로 소스코드의 압축을 해제하고 필요한경우 패치를 적용합니다. %setup 매크로를 이 안에서 보통 사용하며, %setup은 Source에 명시된 파일명의 압축 파일을 SOURCES 밑에서 찾아서 압축을 풉니다. 그리고 동일한 이름의 디렉토리로 이동을 합니다. 앞선 예제에서는 SOURCES/Python-%{version}.tgz의 압축을 풀고 Python-%{version}으로 이동을 합니다. 패치가 필요한 경우 보통 이 뒤에 패치를 적용하는 명령들을 추가 합니다.

%build

설정, 컴파일 등을 수행하는 단계입니다. 이곳에서 자주 하는 매크로로 %configure, %make_build 등이 있습니다. %configure는 configure를 prefix 및 기타 몇가지 일반적으로 쓰이는 옵션을 추가하여 실행해주며, %make_build는 make와 비슷하게 모든 타겟을 빌드 합니다. 예제에서는 둘다 안쓰고 있고, 심지어 실제 빌드는 안하는데 어쨌든 이후의 %install까지 지나고나서 빌드 결과물만 맞는 위치에 만들어지면 대충 패키지를 만드는데는 별 문제는 없는 것 같습니다.

%install

여기서 빌드 결과물을 설치하는 명령을 작성합니다. 일반적으로 %make_install을 사용하여 make install DESTDIR=%{buildroot}와 비슷한 명령을 수행하여 %{buildroot}밑에 빌드 결과물이 prefix를 유지하여 설치되게 합니다. 예제의 %{__ln_s} -f %{_bindir}/python%{major_version}.%{minor_version} %{buildroot}/%{_bindir}/python%{major_version}을 보면 추정 할 수 있듯이, 패키지에 포함시킬 파일들을 %{buildroot}밑에 생성을 하면 되며, 추가적인 심볼릭 링크는 패키지를 빌드하는 시점에는 존재하지 않지만, 패키지를 설치하게되면 존재하게 될 %{_bindir}/python%{major_version}.%{minor_version}를 향하는 것을 %{buildroot} 밑인 %{buildroot}/%{_bindir}/python%{major_version}에 만듭니다.

%files

패키지에 포함될 파일 목록을 작성합니다. glob 양식으로 파일 목록을 작성할 수 있습니다. %{buildroot} 밑에 생성 되었지만 어느 %files에도 포함되지 않은 파일이 있는 경우에는 빌드를 실패합니다. 그러므로 %exclude를 사용해서 명시적으로 제외해줘야 합니다.

기타 매크로

rpmbuild에서는 기본으로 다양한 매크로를 제공하고 있습니다. --define "_libdir %{_prefix}/lib64"와 같은 옵션을 실행시에 주어서 실행시점에 매크로를 덮어 쓸 수도 있고, 앞선 spec파일 내의 %define major_version 와 같이 다른 매크로와 셸 명령을 활용하여 매크로를 정의 할 수도 있습니다. 원하는 동작을 안하는 것 같은 경우에는 --show-rc옵션을 사용하여 매크로가 어떻게 정의되어있는지 확인해 볼 수 있습니다.

빌드

rpmbuild의 매뉴얼을 보면 자세하게 나와있지만 가장 단순하게는 rpmbuild -bb <specfile>로 바이너리 패키지를 빌드할 수 있습다. 이 때, 압축된 소스코드는 미리 SOURCES밑에 두어야 합니다.

private rpm package 배포

직접 비공개 패키지 저장소 프로그램을 실행하여 제공하는 방법도 있겠지만, 최대한 간단하게 할 수 있는 방법으로, rpm관련 패키지 설치 명령이 입력으로 http등의 URL도 받는 것을 활용하여 적당한 장비에서 http로 서빙을 해주면 됩니다.

웹 접근성의 중요성과 WAI-ARIA 표준을 바탕으로 한 의미론적인 UI를 설계한 사례를 블로그에 공개했습니다.

전문성 검증이 필요한 분야이다 보니, 퇴고 과정에 접근성 전문가 @resistan 님의 도움을 받았습니다.

같은 것과 같지 않은 것

국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.

• 국밥 두 그릇의 가격은 몇 원과 같은가?
• KTX의 속력은 몇 km/h와 같은가?
• 내일 기온은 몇 도와 같은가?

이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면

• x2+x+1=0x^2 + x + 1 = 0의 실수 해의 갯수는 0과 같다.
• 물 분자 내의 수소-산소 연결 사이의 각도는 104.5도와 같다.
• 합병 정렬의 시간 복잡도는 O(nlog⁡n)O(n\log{n})과 같다.

등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,

• x+4x + 4를 22로 나눈 나머지는 x+1x + 1을 22로 나눈 나머지와 같지 않다.
• 연결 리스트(Linked List)와 배열(Array)은 같지 않다.
• 함수 λ x→x\lambda\ x \to x와 정수 55는 같지 않다.

같은 것과 판정 문제(Decision Problem)

이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때

• 알고리즘이 참 값(True\mathtt{True})을 준다면 aa와 bb가 같고
• 알고리즘이 거짓 값(False\mathtt{False})을 준다면 aa와 bb가 같지 않은

알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.

이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.^[1]

그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.

1. 문법적 비교(Syntactic Comparison)
2. β\beta 동등성 (β\beta Equivalence)

1. 문법적 비교(Syntactic Comparison)

이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 JavaScript 프로그램은 문법적으로 같은 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x  =  5;
console.log( x );

공백문자의 사용에서 차이가 있으나, 그 외의 문법 요소는 모두 동일함에 유의하자. 반면 다음의 두 JavaScript 프로그램은 동일한 행동을 하지만 문법적으로는 다른 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x = 3 + 2;
console.log(x);

두 프로그램 모두 x에 5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.

문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는

3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로 3 + 2를 5로 바꾸잖아?

라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.

2. β\beta 동등성

바로 앞의 소절에서 단순 계산의 추가에 의해 같음이 같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 x를 c로 치환한 것을 같다고 취급해야한다. 예를 들어

let f = (x) => x + 3;

이 있다면, f(5)와 5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 a와 b를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.

더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.

let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;

g와 h는 같은 프로그램일까? 우리가 g와 h가 같은 프로그램이기를 원한다면 f(x)와 x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 g와 h의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 g와 h를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 x와 같이 값이 정해지지 않은 변수가 있을 때에도 f(x)을 호출하여 비교해야만 한다. 이는 우리가 단순히 모든 함수가 종료하는지 여부를 떠나서, 함수의 몸체에 등장하는 모든 부속 프로그램(Sub-program)이 종료하는지 아닌지를 따져야만 한다는 이야기이다.

이런 강한 제약조건으로 인해 β\beta 동등성을 통해서 프로그램 비교의 판정 문제를 해결 가능한 곳은 매우 제한적이지만, β\beta 동등성이 매우 유용한 한가지 경우가 있다. 바로 의존 형이론(Dependent Type Theory)의 형검사(Type Checking)이다.

의존 형이론과 형의 같음

의존 형이론은 형(Type)에 임의의 프로그램을 포함할 수 있도록 하는 형이론(Type Theory)의 한 종류이다. 예를 들어 명시적인 길이(n)를 포함한 벡터(Vector) 형을 Vector n Int과 같이 쓸 수 있다. 이 형은 n개의 Int값을 가진 벡터를 표현하는 형이다. 이제 append라는 두 벡터를 하나로 연결하는 함수를 만든다고 해보자. 대략 다음과 같은 형을 쓸 수 있을 것이다.

append : Vector n a -> Vector m a -> Vector (n + m) a

즉, append는 길이 n짜리 a 형의 벡터와 길이 m짜리 a 형의 벡터를 합쳐서 길이 n + m짜리 a 형의 벡터를 만드는 함수이다. 이 함수를 사용해서 길이 5의 벡터를 길이 2와 길이 3짜리 벡터 x, y로부터 만들고 싶다고 하자.

append x y : Vector (2 + 3) a

안타깝게도 우리는 길이 2 + 3짜리 벡터를 얻었지, 길이 5짜리 벡터를 얻진 못했다. 여기서 앞서의 질문이 다시 돌아온다.

아니, 2 + 3를 5로 계산하면 되잖아?"

그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) a과 Vector 5 a는 같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.

이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.

마치며

이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.

---

1. 두 함수가 같다라고 보는 방법에 따라 다르나, 두 함수가 항상 같은 값을 가진다면 같다고 하자. 이때 함수의 판정 문제는 정지 문제(Halting Problem)와 동일하다. 임의의 튜링 기계(Turing Machine) ff가 입력 nn을 받았을 때 종료하면 g(n)=1g(n) = 1, 아니면 g(n)=0g(n) = 0이라고 하면 이 함수 gg와 상수 함수 c(n)=1c(n) = 1가 같은 함수임을 보이는 것은 ff가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎