시퀀트 계산과 선형 논리에서의 Par(곱적 선택)과, 예외/continuation 관점에서의 고전 논리의 계산적 해석을 설명하는 글입니다.
URL: https://ryanbrewer.dev/posts/par
제목: Par 3부: Par, 계속
2025년 3월 8일
이 글은 논리에 대한 연재글의 세 번째이자 마지막 글이지만, 나중에 여기서 다룬 개념들로 다시 돌아올 가능성은 큽니다. 여기에서 소개하는 아이디어들은 프로그래밍 언어 이론, 특히 타입 이론과 람다 계산에 관한 중요한 논문들을 이해하는 데 매우 유용합니다. 첫 번째 글에서는 논리를 수행하는 하나의 체계로서 시퀀트와 시퀀트 계산(Sequent Calculus)을 설명했고, 이 글에서는 그 개념들이 이해되었다고 가정하겠습니다. 두 번째 글에서는 선형 논리를 다루었는데, 시퀀트 계산을 연구한 결과 중 가장 놀라운 성과이기 때문입니다. 이제 마침내 모든 것을 하나로 모아서, 수수께끼 같던 Par의 의미를 깊이 파고들고, 그 과정에서 고전 논리의 계산적 해석에 대해서도 더 알아보겠습니다.
우선, Par가 대체 뭔지부터 다시 상기해야 합니다. Par는 연산자의 이름이고, 실제 현상은 기술적으로는 곱적 선택(multiplicative disjunction)이라 부릅니다. 이 글에서는 가끔 곱적 선택이라고 부르겠지만, 대부분 사람들은 그냥 비공식적으로 par라고 합니다. par의 규칙은 대략 다음과 같습니다:
⅋-Intro는, 시퀀트의 오른쪽에 있는 명제들의 목록이 있을 때, 그 중 임의의 둘을 — 를 라고 부르자 — 골라서 " par "라고 읽는 새로운 명제를 만들 수 있다고 말한다.
사실 규칙은 더 없이 단순합니다. 그냥 쉼표 하나를 par로 바꾸었을 뿐입니다. 여기서 얻을 수 있는 핵심은, par가 시퀀트 계산에 대해 아주 근본적인 무언가를 표현한다는 점입니다. 시퀀트의 오른쪽에 있는 어떤 쉼표도 본질적으로는 par이고, 이 규칙을 이용해 둘 사이를 자유롭게 오갈 수 있습니다. 또는 이렇게 말할 수도 있습니다. 오른쪽에 있는 명제들의 모음 전체를 하나의 거대한 곱적 선택으로 볼 수 있습니다.
하지만 이렇게 말하면 질문을 뒤로 미룬 것에 불과합니다. 애초에 시퀀트의 오른쪽에 명제들의 모음이 있다는 게 무슨 뜻인지 설명해야 하기 때문입니다! 이건 사실 전혀 쉬운 질문이 아닙니다. 실제로 너무 이해가 안 돼서, 많은 연구자들이 아예 오른쪽에 명제를 하나 이상 둘 수 없는 대체 논리들을 사용함으로써 이 문제를 피하고 있습니다. 직관주의 선형 논리(Intuitionistic Linear Logic, ILL)는 바로 이 목적을 위해 설계되었습니다. 그런데 이건 좀 묘한 체계입니다. 이 맥락에서 선형 논리(고전 선형 논리 Classical Linear Logic, CLL라 부르겠습니다)는 이미 구성적(constructive)이기 때문에, 굳이 이를 다시 직관주의적으로 만들 필요는 별로 없기 때문입니다.
어쨌든, 이 글을 다 읽고 나면 곱적 선택이 직관적일 뿐 아니라 놀라울 정도로 아름답게 느껴지기를 바랍니다. 비록 매우 단순한 개념이지만, 이를 제대로 설명하기 위해 이 글에서는 여러 가지 개념들을 새로 소개할 것입니다. 조금 더 부드럽고 친절하게 만들기 위해서입니다.
Disjunctive syllogism은 논리학에서 아주 오래되고 단순한 개념인데, 이름만 괴상하게 어렵습니다. 그 내용은 이렇습니다. 내가 " 또는 "라는 선택 명제를 믿고 있고, 이어서 예를 들어 가 거짓이라는 것을 알게 되면, 논리적으로 는 참이라고 결론지을 수 있습니다. 자연 연역(Natural Deduction)의 표기법으로 쓰면 대략 다음과 같이 쓸 수 있습니다:
, 를 전제로 하고, 를 부정하면 를 얻는다.
직관주의 논리에서 ¬는 일반적으로 를 라고 정의합니다. 계산적으로 보면, 이것은 의 증명(값)이 있으면 그 증명과 이 함수를 결합해 의 증명을 만들 수 있고, 의 증명은 절대 존재할 수 없으므로, 그런 증명을 없앤다는 의미입니다. 따라서 disjunctive syllogism의 의미는 P -> Never 타입의 함수(여기서 Never는 아무 값도 가지지 않는 타입이라고 합시다)를, 태그된 합 타입(tagged union type) P | Q의 값과 결합하여 다음과 같은 의사코드로 표현할 수 있다는 것입니다:
f: P -> Never
d: P | Q
let proof: Q =
case d {
Left p ->
// Never는 값이 없으므로, 이 경우 분기는 비어 있다
case f(p) {} // 이건 아무거나(당연히 Q도 포함해서) 증명한다
Right q -> q
}
오늘날 널리 쓰이는 많은 증명 보조기(proof assistant)들이 이 해석을 사용합니다. 지난 글에서 선형 논리에 대한 병렬성(parallelism) 해석을 이야기했을 때, 부정을 "값을 만들어내는 대신 소비하는 것"으로 이해할 수 있다고 했는데, 여기서도 그 아이디어가 그대로 반영됩니다. 왜냐하면 이 함수는 증명을 만들어내는 대신, 의 증명을 소비하는 함수이기 때문입니다. 이것은 계속 등장할 테마이고, 전반적으로 부정을 이해하는 데 매우 유용한 철학처럼 보입니다.
중요한 여담 하나: 이 분야를 공부하면서 제 이해를 크게 방해했던 것 중 하나는, 위에서 f(p) 같은 값이 등장할 때였습니다. 이 표현은 타입이 Never입니다! 정의상 그런 값은 존재할 수 없다는 걸 알고 있죠! 그런데 실제 프로그램에서 어떤 명제(예: p)의 증명과, 그 명제의 부정(예: f)에 대한 증명을 동시에 갖는 것이 꽤 흔합니다. 이게 아주 헷갈렸습니다. 제가 개인적으로 필요했던 "유레카" 모먼트는, 우리가 인간으로서 어떤 것을 불가능하다고 판단할 때, 보통 서로 모순되는 두 생각을 함께 두고 그것을 통해 판단한다는 점을 깨닫는 것이었습니다. 즉, 서로 모순되는 두 증거를 동시에 갖는 것은 굉장히 흔한 일인데, 그것들이 "정신적 영역" 안에만 있는 한 괜찮습니다. 우리는 "실제 세계(ground truth)"가 둘 중 하나만 지지한다는 것을 알지만, 실제 세계가 무엇을 지지하는지 알아내기 위해서는 우리 내부의 추론에서 둘 다 _고려_해야 합니다. 증명을 작성하는 것은 실제 세계에 대해 결론을 내리기 위한 추론 과정이며, 그렇기 때문에 때로는 모순되는 증거를 함께 다루고, 모순을 적극적으로 활용해야 합니다. 그리고 물론, 이 맥락에서 제가 프로그램에 대해 말할 때, 그 프로그램들은 곧 증명입니다 :)
이 모든 것이 par와는 어떻게 연결될까요? 아직은 충분히 근본적인 수준에 닿지 않았습니다. 조금 더 깊이 파고들어야 합니다. 다음 퍼즐 조각은 "continuation"이라는 개념입니다.
당신이 하나의 프로그램(혹은 증명)이라고 상상해 봅시다. 열심히 돌아가며 일을 하고 있습니다. 한 걸음씩 나아가며 무언가를 변형시키고, 최종 목표를 향해 조금씩 다가갑니다. 이제 그 중간의 어떤 한 단계를 택해 초점을 맞춰 봅시다. 항상, 그 시점 이후의 나머지 프로그램 전체를, 현재 상태를 인수로 받아서 실행해 주는 do_the_rest(...) 같은 함수(혹은 보조 증명)가 존재한다고 상상할 수 있습니다. 이런 종류의 함수를 적절하게 "continuation"이라고 부릅니다. 물론 모든 단계에는 이론상 해당하는 continuation이 있습니다. 그리고 각 단계에서, 그 단계의 계산을 수행한 다음 그에 해당하는 continuation을 호출하고, 이것을 끝까지 반복한다고 상상할 수 있습니다. 다음은 이를 보여 주는 간단한 의사코드입니다:
rustfn main() { foo(1) } fn foo(x) { bar(x + 1) } fn bar(x) { print(x) exit }
이 코드는 1 + 1을 계산하지만, 매번 한 단계씩만 수행하고, 그 즉시 그 시점 이후의 "나머지 프로그램"을 대표하는 함수를 호출합니다. 즉, continuation을 호출하는 방식입니다. 이 형태로 어떠한 프로그램도 작성할 수 있고, 다만 상당히 번거롭기는 합니다. 우리가 하는 일은 단지 프로그램의 연산 순서를 (엄청나게) 명시적으로 드러내는 것뿐입니다.
여기서 continuation이 흥미로운 이유는, 이 함수들이 결코 반환하지 않는다는 점입니다. 마지막 continuation은 프로그램을 종료할 뿐입니다. (정의상 "마지막 continuation"이므로) 더 이상 해야 할 일이 없기 때문입니다. 위의 세 함수 중 어느 것도 값을 반환하지 않습니다. main은 foo를 호출하고, foo는 bar를 호출하며, bar는 프로그램을 끝내기 때문에 foo나 main으로 다시 돌아갈 수 없습니다. 따라서 continuation에 어울리는 타입은 어떤 타입 P에 대해 P -> Never입니다. 우리는 방금 이 타입을 본 적이 있습니다. continuation은 곧 부정(negation)입니다!
(참고: 여기서 exit는 그 전에 무언가 마지막 단계를 가져야 합니다. 증명/프로그램의 마지막 단계라고 생각하세요. 그러니까 exit: Never라기보다는 exit: P -> Never로 생각할 수 있습니다. "증명" let p: P = exit는 물론 받아들여지지 않을 것입니다. 제가 exit를 값 밑에 쓰고 함수 호출처럼 안 쓰는 건 단지 문법 선택의 문제입니다. 사실, 우리가 어떤 명제 P의 증명이라고 부르는 것들은, 진짜로는 (P -> Never) -> Never의 증명입니다. 왜냐하면 이 새로운 exit 인자를 받고 마지막에 그것을 호출하기 때문입니다. 논리적으로 이것은 P의 이중 부정(double negation)이고, 고전 논리에서는 여전히 동치입니다! 이것이 바로 continuation passing style, CPS에 대한 논리적 관점입니다. 익숙하신 분도 있을 겁니다.)
이제 방금 살펴본 disjunctive syllogism에 이 아이디어를 적용해 봅시다. 우리가 " 또는 "라는 선택 명제와 하나의 continuation 을 가지고 있다면, 이를 이용해 의 증명을 만들 수 있어야 합니다. 여기서 중요한 점은, 우리가 지금까지 써 왔던 일반적인 태그드 유니언 타입으로서의 선택(이제부터는 "가법 선택 additive disjunction"이라 부르겠습니다)으로는 이게 전혀 작동하지 않는다는 것입니다. 이전에 봤던 증명을 다시 떠올려 봅시다:
rustf: P -> Never d: P | Q let proof: Q = case d { Left p -> // Never는 값이 없으므로, 이 경우 분기는 비어 있다 case f(p) {} // 이건 아무거나(당연히 Q도 포함해서) 증명한다 Right q -> q }
여기서, 이전과 달리 f는 continuation입니다. 따라서 f(p)가 불가능한 값(결국 f는 아무것도 반환하기 전에 프로그램을 종료해 버리기 때문)이긴 하지만, 이 증명의 _행동_은 "Q를 증명하거나, 혹은 의 증명을 가진 채 어떤 프로그램을 실행하고 나서 종료해 버리는 것"입니다. 이것은 우리가 기대하는 "Q의 증명"과는 분명히 다릅니다.
그렇다면 이 새로운 continuation 세계에서 우리가 기대하는 행동은 무엇일까요? 즉, 의 증명을 사용하는 프로그램인 continuation 이 어떻게 실제로 의 반박(refutation)처럼 느껴지는 걸까요? 핵심은 앞에서 이야기한 Never 타입입니다. 즉, 의 증명을 이용해 그 프로그램을 실행하면, 다시는 되돌아올 수 없다는 사실입니다.
조금 전의 그 중요한 여담을 떠올려 봅시다. 모순을 찾아서, 서로 모순되는 여러 증거를 다루는 것이, 진실한 결론에 도달하기 위해 중요한 과정이라고 했습니다. 이런 식으로 뭔가를 반증(refute)할 때, 우리는 그 모순된 세계에서 빠져나와, 더 이상 모순된 두 생각을 동시에 믿지 않는 상태로 나옵니다. 하지만 그 과정에서 무언가를 배웁니다. 그 세계로는 다시 돌아가지 않습니다. 왜냐하면 그 세계의 핵심 가설 중 하나를 완전히 부정했기 때문입니다.
우리의 continuation 해석에서는, 의 증명과 를 증명하는 continuation, 이 둘을 함께 가지면, 우리는 의 증명과 함께하는 어떤 세계로 들어가서 다시는 돌아오지 않을 수 있습니다. 그렇게 해서 를 반증하는 것입니다. 우리가 의 증명을 만들지 않는 한, 우리는 여전히 우리의 continuation을 들고 다닙니다. 그동안은 전체 명제 에 대한 온전한 증명으로 동작합니다. 어쩌면 이는 탁월한 반증이라기보단, 언젠가 그것을 무효화할(즉, 의 증명) 무언가를 찾으면, 우리가 가진 세계( 의 증명을 가진 세계)에서, 의 증명을 가진 세계로 갈아탈 수 있다는 정도일 뿐입니다. 그럼에도 이것은 "무언가를 알아가는 과정"에 대한 멋진 철학적 관점입니다.
그렇다면 이것이 disjunctive syllogism에 대해 무엇을 의미할까요? disjunctive syllogism이 어떻게 작동하는지 다시 떠올려봅시다. 우리는 어떤 선택 명제 를 가지고 있고, continuation 를 가지고 있습니다. 물론, 여기서 우리가 기대하는 것은 이를 통해 를 이끌어내는 것입니다. 그리고 또, 의 증명이 있다면, 우리의 선택 명제를 이용해 를 증명하기를 바라게 되겠지요.
이제, 전통적인 태그드 유니언 방식의 선택(가법 선택)을 쓰는 대신, 이 disjunctive syllogism만을 수행하는 새로운 선택 개념(par!)을 도입할 수 있습니다. 이 방식은, 어떤 par , 에 대해, par가 일단 왼쪽인 가 참이라고 즉시 가정하는 식으로 동작합니다. 그러다가 반증(즉, )이 등장하면, 다시 돌아가서 "아, 잠깐만요, 사실은 오른쪽()이 참이었습니다!"라고 말하는 겁니다. 이 동작을 강조하기 위해, 이제는 case 대신 try/catch를 문법으로 사용하겠습니다:
rustf: P -> Never let proof: P = try { // P를 증명하거나, 아니면 `throw` 호출 } catch (q: Q) { // Q를 증명했다! exit } // 여기까지 왔다는 건 P를 증명했다는 뜻! f(proof)
대략 try 블록은 Q continuation(catch 블록)을 인수로 받아 P를 돌려주는 함수라고 볼 수 있습니다. 즉, 타입은 (Q -> Never) -> P쯤 됩니다. 이 함수의 매개변수 이름은 throw라고 합시다. 좀 더 명확히 하기 위해 간단한 예제 프로그램 몇 개를 보겠습니다.
rustf : P -> Never proof_of_q : Q // 이 프로그램은 즉시 throw한다 let proof : P = try { throw(proof_of_q) } catch (q: Q) { // Q를 증명했다! exit } // 여기까지 왔다는 건 P를 증명했다는 뜻! f(proof)
try 블록을 "를 증명하는 함수"로 상상해 보면, 대략 fn(throw: Q -> Never) { throw(proof_of_q) } 처럼 생겼을 겁니다. 이제 다른 예제를 보겠습니다.
rustf: P -> Never proof_of_p: P let proof: P = try { proof_of_p } catch (q: Q) { // Q를 증명했다! exit } // 여기까지 왔다는 건 P를 증명했다는 뜻! f(proof)
이 프로그램은 흥미롭습니다. 왜냐하면 여기서는 실제로 Q를 전혀 증명하지 않기 때문입니다. 그럼에도 불구하고 우리는 의 부정, 즉 이 try/catch 전체의 continuation(여기서는 f)에 대한 증명을 제공했습니다! 이 부정은 proof_of_p로 바로 호출되어 즉시 반박되고, try/catch 이후의, 가 참인 세계로 넘어가게 됩니다.
이제 P를 R -> S (논리 기호로는 )라고 해 봅시다. 이제 (R -> S) | Q에 대한 조금 더 교묘한 예제를 보겠습니다.
rustf: (R -> S) -> Never proof_of_q: Q let proof: R -> S = try { fn(s: R): S { throw(proof_of_q) // hehehe } } catch (q: Q) { // Q를 증명했다! exit } // 여기까지 왔다는 건 R이면 S라는 걸 증명했다는 뜻! f(proof)
여기서는 R -> S 타입의 함수를 만들어 내서, 그걸로 "증명"을 구성했습니다. 하지만 나중에, 얼마나 나중인지는 신도 모를 때, 이 함수를 실제로 사용하려고 하면, 엄청 멀리 과거로 순간이동해서 proof_of_q를 들고 catch 블록으로 돌아가게 됩니다.
지금까지는 논리적 해석을 중심으로 코드 조각들을 설명했지만, 프로그래밍에 익숙한 분이라면 이 코드들의 의미는 이미 꽤 직관적으로 느껴지실 겁니다.
여기서 기억해 둘 점은, par는 오직 try 블록에만 타입을 부여한다는 것입니다. catch 블록은 즉시 오른쪽의 부정(continuation)에 대한 증명을 사용해 par 타입을 제거(eliminate)하여 왼쪽에 대한 증명을 추출합니다. 그래서 par는 자바의 throwing 키워드와 굉장히 비슷하게 생각할 수 있습니다. T throwing E는, E 타입의 예외를 처리하기 위해 try/catch로 감싸고 나면 결국 T 타입의 값인 것과 같다는 식입니다. 물론, 자바 코드에서는 throw가 어디서나 등장할 수 있으므로, 자바에서 try는 사실상 구성(introduction)이 아니라 추출(elimination)에 더 가깝습니다. 내가 사용하는 문법에서 논리적으로 try 블록은 par 타입을 구성하는 도입 형식(introduction form)으로, throw 키워드를 도입하고, catch 블록은 내부 값을 꺼내는 제거 형식(elimination form)으로 볼 수 있습니다.
try와 catch는 제가 par 타입을 위해 선택한 문법일 뿐입니다. 일부 문헌에서는 제거 형식에 handle이라는 키워드를 쓰기도 합니다. 개인적으로는 이런 문법에 너무 집중할 필요는 없다고 생각합니다. 이쪽 시스템들의 스코프 규칙에 관한 논문이 정말 압도적으로 많아서, 정작 핵심 아이디어를 가려버리는 경우가 많기 때문입니다.
(이 이야기들이 "알제브라적 효과 시스템(algebraic effect system)"을 아시는 분들께는 크게 와닿을 수 있습니다. 이것은 try/catch를 일반화하는 개념입니다. 그런 직관을 갖고 계시다면 아주 좋습니다. 다만, 효과 시스템을 모르더라도 이 글을 이해하는 데에는 전혀 문제가 없습니다.)
정리하자면, par는 try 블록에 타입을 부여함으로써 예외와 예외 처리(exception handling)를 표현합니다. 이것이 지난 글에서 언급했던 여러 해석과는 다른, 선형 논리의 "continuation" 의미론입니다. 그리고 이 해석이 흥미로운 이유는, 이것이 실제로 고전 논리에 대한 의미론이기 때문입니다. (모든 선형 논리의 증명은 자동으로 고전 논리의 증명이기도 하다는 점을 떠올려 보세요.) 이 생각을 염두에 두고, 이제 한 발짝 물러서서, 고전 논리에 대한 구성적 해석을 바라보겠습니다.
일부 증명 이론가들은, "무언가를 믿고 있다가, 반증이 나타나면 되돌아가는" 이 행위가 고전 논리의 핵심, 즉 배중률(law of excluded middle, LEM) 의 정수(essence)라고 믿습니다. 다르게 말하면, 배중률은 분리 삼단논법(disjunctive syllogism)에 대해서만 타당하다는 것입니다. Philip Wadler는 LEM의 계산적 내용(computational content)을 설명하는 유명한 이야기 하나를 들려줍니다. 이 이야기는 이 논문의 4절에 나오는데, 대략 이런 식입니다.
어느 날, 악마가 한 남자 앞에 나타나 이상한 제안을 했다. "내가 이상한 제안을 하나 하겠소." 악마가 말했다. "내가 두 가지 중 하나를 하겠소. 첫째, 자네의 어떤 소원이든 하나 들어주겠소. 대신 그 _값_으로 10억 달러를 내야 하오. 둘째, 내가 자네에게 10억 달러를 주겠소."
남자는 잠시 생각했다. "함정이 뭐죠? 당신이 첫 번째를 선택하고, 제가 10억 달러를 못 준다면 어떻게 됩니까?"
"아무 일도 없소." 악마가 말했다. "당연히 자네의 소원을 들어줄 수 없겠지. 그뿐이오."
"다른 비용은 전혀 없나요?" 남자는 의심스러웠다. 어느 쪽도 나쁘지 않고, 한쪽은 심지어 굉장했다. 도무지 단점을 찾을 수가 없었다.
"없소." 악마가 재차 확인했다. "자네가 해야 할 일은 그저 이 제안을 받아들이는 것뿐이오."
"좋습니다. 받아들이죠. 그럼, 어떤 선택을 하셨습니까?"
"나는 첫 번째 선택을 고르겠소. 자네가 10억 달러를 준다면, 어떤 소원이든 들어주겠소."
남자는 실망했다. 하지만 이게 가장 합리적인 예상이기도 했다. 더 나쁜 쪽이었으니까. 그는 당연히 10억 달러가 없었고, 그냥 그 일을 잊고 삶을 이어갔다.
하지만 세월이 흐르면서, 그 교환은 마음 한 구석에서 떠나질 않았다. 어떤 소원이든? 만약 돈으로 행복을 살 수 있는 때가 있다면, 아마 지금일 것이다. 남자는 논리학을 공부하기 시작했고, 자연스럽게 돈도 모이기 시작했다.
어느 날, 남자는 마침내 10억 달러 현금을 손에 쥐게 되었다. (멋진 프로그래밍 언어를 만들어서였다고 하자.) 어쨌든, 10억 달러를 손에 쥐고(물리학은 따지지 말자), 남자는 악마를 다시 찾아가기로 했다. 악마를 찾아낸 그는 이렇게 선언했다. "여기 10억 달러요! 이제 제 어떤 소원이든 들어줄 건가요?"
악마는 돈을 받아 들었다. "고맙소! 참 친절하군. 하지만 나는 자네가 두 가지 중 하나를 받게 해 주겠다고만 약속했지, 어떤 걸 줄지 미리 정직하게 말하겠다고 약속한 적은 없소! 자네가 실제로 받게 되는 건 두 번째 선택이오." 악마는 10억 달러를 다시 돌려주었다. "여기 10억 달러요!"
Wadler의 버전에서는, 악마가 이런 짓을 하는 이유가, 10억 달러를 벌 만큼 되려면 꽤 끔찍한 사람이어야 하기 때문이라고 합니다. Wadler는 분명, 윤리적인 방식으로 억만장자가 되는 유일한 길이 있다는 걸 모르는 것 같습니다(제 꿈의 프로그래밍 언어를 만드는 것 말이죠).
농담은 여기까지 하고, Wadler의 이야기는 LEM의 계산적 행동이, 우리가 실제로 LEM을 사용할 때 머릿속에 떠올리는 것과는 꽤 다르다는 점을 설득력 있게 보여 줍니다. 누군가는 이렇게 말할 수도 있습니다. "명제 수준에서는 LEM과 같을지 몰라도, 우리가 LEM이라고 말할 때 진짜 의미하는 것과는 다르다." 이런 논점은 직관주의 논리 쪽에 유리한 주장으로 받아들여집니다. 고전 논리의 구성적 변형들(예: 고전 선형 논리)에 맞서는 주장인 셈입니다.
이 현상이 나타난 이유는, 구성적 고전 논리가 초기 함수형 언어들의 call/cc ("call with current continuation") 연산자에서 발견되었기 때문입니다. call/cc는 말 그대로 현재 continuation을 인자로 함수에 넘겨 호출하는 연산입니다. 그래서 다음과 같은 코드를 쓸 수 있습니다:
rust// 7 또는 4를 출력한다 print(2 + callcc( fn(k: int -> Never): Never { // k는 continuation이다. // 즉, `print(2 + _); exit` if (random_number > 0.5) { print(7) exit } else { k(2) // 4를 출력한다 } } ))
보통 call/cc는 동적 타입 언어에서 사용되지만, 이를 정적 타입으로 본다면 타입은 ((T -> Never) -> Never) -> T 정도가 됩니다. 논리적으로 이것은 바로 이중 부정 제거(double negation elimination)입니다! 그리고 우리는 이것이 고전 논리에서만 타당하고, 심지어 이를 사용해 LEM을 증명할 수 있다는 것을 알고 있습니다:
rust// call/cc로 구현한 Wadler의 악마 // B는 10억 달러 let excluded_middle<B>: (B -> Never) | B = callcc(fn(k: ((B -> Never) | B) -> Never) { k(Left(fn(b): Never { k(Right(b)) })) })
여기서 우리가 먼저 Left로 진행하며, B -> Never에 대한 "증명"을 제공한다는 점을 볼 수 있을 겁니다. 하지만 이 증명이 실제로 10억 달러를 받는 순간, 우리는 같은 예전 continuation k로 돌아가서, 이번에는 방금 받은 10억 달러를 이용해 Right 쪽을 증명하게 됩니다.
이러한 LEM 표현은 확실히 낯설고 직관적이지 않게 보입니다. 한동안 이것이 구성적 고전 논리를 설명하는 가장 좋은 방식이었습니다. 사실 고전 논리에 대해 어떠한 구성적 해석이 존재한다는 것 자체가 모두에게 놀라운 일이었습니다! 귀여운 우연처럼 보이지만, 어딘가 가짜 같기도 했습니다. 왜 우리는 굳이 (틀릴 수도 있는) 왼쪽을 먼저 가정해야만 할까요? 이렇게 Wadler의 비유가 쏟아내는 비판은 이해할 만합니다. 게다가, 이건 여전히 가법 선택(additive disjunction)밖에 알려지지 않았던 시절의 이야기라, Left와 Right 생성자를 쓰고 있습니다. 이 모든 이야기에 대해 훌륭한 자료를 찾고 싶다면 Vikraman Choudhury의 이 논문을 강력히 추천합니다.
하지만 이 글을 여기까지 따라온 지금 시점에서, 우리는 실제로 무슨 일이 일어나고 있는지 알고 있습니다:
rust// par를 사용한 Wadler의 악마 // B: 10억 달러 let excluded_middle<B>: (B -> Never) par B = try { fn(b: B): Never { throw(b) } }
여기서는 우리가 par를 도입하기만 하고 제거하지는 않으므로, catch 블록이 없습니다. 그건 excluded_middle의 사용자들이 제공해야 합니다.
이제 보시다시피, Wadler의 악마는 단지 를 특수화한 것에 불과합니다. LEM은 가법 선택이 아니라 곱적 선택입니다. 여기서 벌어지는 "이동"은 더 이상 그다지 신비롭거나 부자연스럽게 느껴지지 않습니다! par는 자바의 throwing 키워드와 비슷하다는 점을 떠올려 보세요. 구성적 고전 논리는 try/catch 예외 처리가 확장된, 아주 평범한 직관주의 논리일 뿐입니다! (기술적으로는 간단한 효과 시스템이기는 하지만, 이 글처럼 직관 위주의 설명에서는 이 정도만 알아두면 충분합니다.)
이 모든 이야기는 LEM의 계산적 버전을 훨씬 더 직관적이고 친근하게 만든다고 생각합니다. 우리가 말하고자 하는 바는, LEM이 구성적으로 유효한 것은 오직 분리 삼단논법(par, 곱적 선택)에 대해서뿐이며, 그 증명은 대부분의 프로그래머들이 잘 알고 있는 try/catch 문을 사용한다는 것입니다. 선형 논리의 언어로 말하면, LEM은 가법 선택이 아니라 곱적 선택입니다.
앞에서 보았듯이, call/cc를 사용하면 가법 LEM도 증명할 수 있습니다. 하지만 그렇게 하려면 continuation을 두 번 언급해야 합니다! 따라서 구성적 고전 논리에서는 이론상 가법과 곱적 두 종류의 배중률을 모두 가질 수 있지만, 고전 선형 논리에는 오직 곱적 LEM만 존재하고, 그래서 전반적으로 더 정직하고 철학적으로도 더 일관된 느낌을 줍니다. 태그드 유니언은 언제든 다른 곳으로 점프할 수 있다는 인상을 주지 않지만, throwing 키워드는 분명 그런 인상을 줍니다! 그래서 저는 Wadler의 악마를, 구성적 고전 논리가 꽤 혼란스러울 수 있다는 합리적인 주장으로 보지만, 고전 선형 논리는 이를 매우 우아하게 처리한다고 봅니다.
그렇다 해도, 예외 처리 직관이 선형 논리에서는 조금 어긋나는 지점이 하나 있습니다. 바로, 증명에서 매개변수는 정확히 한 번만 사용되어야 하기 때문에, try 블록은 반드시 throw해야 한다는 점입니다. throw도 이론상 매개변수이기 때문입니다! 그렇다면 어차피 항상 throw할 게 보장된 try/catch가 무슨 의미가 있을까요? 실제로, 선형 논리에서 프로그래밍을 할 때 par가 가장 자주 등장하는 방식은, 선형 함의가 로 정의된다는 점입니다. 다시 말해, 함수 타입이 par 타입을 부여받습니다! 이것을 이해하는 데에도 예외 처리 직관이 여전히 도움이 됩니다.
(not A) par B 타입의 값을 가지고 있다고 해 봅시다. 이 값은 우리가 not B, 즉 B continuation, 프로그램/증명을 끝내기 위해 B 타입의 값을 사용하는 continuation을 제공하기 전에는 아무것도 할 수 없습니다. 우리가 이 continuation을 제공하면, 우리는 A continuation(타입 not A)에 접근할 수 있게 됩니다. 선형 논리에서, 우리는 이것이 반드시 A 타입의 값을 소비하여 B 타입의 값을 계산한 후, 우리가 제공한 B continuation으로 throw한다는 것을 알고 있습니다. 즉, 우리가 ("호출자"로서) (not A) par B 타입의 값을 받고, 여기에 A 타입 값과 B continuation을 제공하면, 이 값은 A 타입 값을 사용해 B 타입 값을 계산하고, 그것을 우리의 B continuation에 넘겨주게 됩니다. 이것이 반드시 일어난다는 것이 보장됩니다. 선형 논리는 이렇게 함수의 입력(not A)과 출력(B)을 깔끔하게 분리합니다.
이 모든 것의 재미있는 부산물은, LEM이 사실상 항등 함수(identity function)에 불과하다는 점입니다! 우리가 조금 전 LEM을 증명했던 코드를 다시 보면 알 수 있습니다:
rust// par로 구현한 Wadler의 악마 // B: 10억 달러 let excluded_middle<B>: (B -> Never) par B = try { fn(b: B): Never { throw(b) } }
우리가 여기에 B continuation(catch 블록)과 B 타입 값을 제공하면, 이 코드는 그 값을 그 즉시 B continuation으로 건네 줍니다. 어떤 의미에서, LEM이 고전 선형 논리 안에서 구성적으로 증명 가능한 이유는, 그것이 사실 그냥 과 동치이기 때문입니다. 그리고 이런 항등 함수는 어떤 구성적 논리(심지어 직관주의 논리)에서도 너무나 자명하게 참입니다.
이렇게 해서 시퀀트 계산, 선형 논리, 그리고 par에 관한 연재를 마무리합니다. 그 과정에서 고전 논리를 구성적으로 다루는 방법도 함께 배웠습니다! 이 글이 par에 대해 보다 분명한 이해를 남겼기를 바랍니다. 그렇지 않더라도, 언제든 이런 주제로 이야기 나누는 걸 좋아하니 부담 없이 연락 주세요 :)
Mastodon에 올렸던 제짧은 글(tout) 하나가, 이 글의 핵심 아이디어를 아주 간결하게 요약했다는 평을 의외로 많이 받아서, 빠른 참고용으로 여기에 링크를 남겨 둡니다: https://mathstodon.xyz/@ryanbrewer/113997740674738592.
© 2025 Ryan Brewer.