선형 논리와 선형 타입(Linear logic and linear types)

자판기에서 커피가 동전 두 개라고 합시다. '동전 두 개가 있으면 커피를 살 수 있다'와 '동전 두 개가 있다'에서 '커피가 있다'가 나옵니다. 보통의 논리로 적으면 $A,\; A \to B \vdash B$입니다. 그런데 보통의 논리에서는 같은 전제로 $B \land B$도, $B \land A$도 증명됩니다. 가정 A는 한 번 쓰고 나도 그대로 남아 있어서 몇 번이든 다시 쓸 수 있기 때문입니다. 참은 써도 닳지 않습니다. 동전은 닳습니다. 동전 두 개로 커피를 샀다면 동전은 없고, 커피를 두 잔 살 수도 없습니다. 1987년 프랑스 논리학자 장이브 지라르가 내놓은 선형 논리⁠(linear logic)⁠는 이 차이를 논리 안에 넣습니다. 가정은 자원이고, 증명은 모든 자원을 정확히 한 번씩 씁니다.

무엇을 고쳤는지는 정확히 말할 수 있습니다. 독일 논리학자 게르하르트 겐첸의 시퀀트 계산⁠(sequent calculus)⁠은 '가정 목록 Γ에서 C가 나온다'는 판단 $\Gamma \vdash C$를 규칙으로 쌓는 체계입니다. 여기에는 어떤 논리 연결사와도 상관없이 가정 목록만 다루는 구조 규칙이 셋 있습니다. 가정의 순서를 바꾸는 교환 규칙은 선형 논리도 그대로 둡니다. 문제는 나머지 둘입니다.

$$\dfrac{\Gamma \vdash C}{\Gamma,\, A \vdash C}\;\text{약화} \qquad\qquad \dfrac{\Gamma,\, A,\, A \vdash C}{\Gamma,\, A \vdash C}\;\text{축약}$$

약화는 쓰지 않는 가정을 더해도 된다는 규칙이고, 축약은 같은 가정 두 벌을 한 벌로 합쳐도, 곧 한 벌을 두 번 써도 된다는 규칙입니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 읽으면 약화는 받은 인자를 버리는 함수⁠(function)⁠ $\lambda x.\,\lambda y.\,x$를, 축약은 인자를 두 번 쓰는 함수 $\lambda x.\,(x, x)$를 허락합니다. 선형 논리는 이 두 규칙을 뺍니다. 그러면 λ로 묶인 변수⁠(bound variable)⁠가 몸통에 정확히 한 번 나오는 항만 남는데, 이것이 선형 람다 계산⁠(linear lambda calculus)⁠이고 그 타입이 선형 타입입니다. 함수 타입도 다른 기호로 적습니다. $A \multimap B$('롤리팝'이라고도 읽습니다)는 'A 하나를 소비해 B 하나를 만든다'입니다.

두 규칙을 빼면 '그리고'가 둘로 갈라집니다. 보통의 논리에서 $A \land B$를 증명하는 두 방법, 곧 같은 가정 Γ로 A와 B를 각각 증명하는 방법과 Γ를 둘로 나눠 한쪽으로 A, 다른 쪽으로 B를 증명하는 방법은 약화와 축약 덕분에 같은 힘을 가졌습니다. 이제는 다릅니다. 자판기 예로 네 연결사를 봅시다. 커피와 차는 동전 두 개, 사탕은 한 개입니다.

• A ⊗ B(텐서⁠, tensor⁠): A와 B를 둘 다, 한꺼번에 가집니다. 자원을 나눠서 한쪽으로 A를, 나머지로 B를 만듭니다. 커피 ⊗ 사탕에는 동전 2 + 1 = 3개가 듭니다.
• A & B(위드): 메뉴판입니다. 같은 자원으로 A도 만들 수 있고 B도 만들 수 있어서, 받는 쪽이 둘 중 하나를 고릅니다. 둘 다 받지는 못합니다. 커피 & 차에는 동전 2개면 됩니다.
• A ⊕ B(플러스): 둘 중 하나인데, 주는 쪽이 고릅니다. '오늘의 디저트'처럼, 받는 쪽은 둘 다에 대비해야 합니다. 커피 ⊕ 사탕을 내놓는 쪽은 동전이 1개면 사탕을, 2개면 커피를 고르면 됩니다.
• !A(오브 코스): A를 원하는 만큼(0번도 괜찮습니다) 꺼낼 수 있는 샘입니다. !가 붙은 가정에만 약화와 축약이 허락되어, 버려도 되고 복사해도 됩니다. 자판기 자체가 그렇습니다. 동전 두 개를 커피로 바꾸는 규칙은 한 번 쓰고 사라지지 않으니 $!(\text{동전} \otimes \text{동전} \multimap \text{커피})$로 적습니다.

동전 개로 목표 를 만들 수 있는지 세어 봅시다. 가정: .

세 가지를 확인할 수 있습니다. 첫째, 동전 3개로 커피만 원하면 증명되지 않습니다. 동전 하나가 남는데, 약화가 없으니 남은 자원을 버릴 수 없기 때문입니다. 버려도 된다고 말하려면 목표를 커피 ⊗ ⊤로 적어야 합니다. ⊤는 남는 것을 무엇이든 받아 주는 목표입니다. 둘째, 커피 & 차는 동전 2개로, 커피 ⊗ 커피는 4개로 증명되니 두 '그리고'는 정말 다릅니다. 셋째, 가정을 !동전으로 바꾸면 하나만 있어도 모든 목표가 증명됩니다. 둘째 줄의 '보통의 논리' 판정과 같아진 것입니다. 보통의 논리에서는 모든 가정에 !가 붙어 있는 셈이라 개수를 셀 수 없습니다. 지라르의 번역 $A \to B = {!A} \multimap B$가 이것을 정확히 말합니다. 직관주의 논리⁠(intuitionistic logic)⁠의 함수는 '인자를 몇 번이든 쓸 수 있는 선형 함수'입니다. 이 번역에 ∧를 &로, ∨를 ${!A} \oplus {!B}$로 옮기는 규칙을 더하면, 직관주의 논리에서 증명되는 식은 옮긴 뒤에도 선형 논리에서 증명되고, 증명되지 않는 식은 옮긴 뒤에도 증명되지 않습니다. 직관주의 논리가 선형 논리 안에 빠짐없이, 더하는 것 없이 들어가는 셈이고, 고전 논리도 비슷한 번역으로 들어갑니다. 선형 논리는 보통의 논리를 버리지 않습니다. 보통의 논리가 뭉뚱그리는 것을 더 잘게 나눌 뿐입니다.

지라르의 원래 선형 논리는 부정을 두 번 하면 제자리로 돌아오는 판(고전 선형 논리)입니다. 부정 $A^{\perp}$는 'A 하나를 소비할 의무'로 읽을 수 있어, 돈에 대한 빚과 닮았습니다. 고전 논리처럼 $A^{\perp\perp} = A$이고, 드모르간 법칙⁠(De Morgan's laws)⁠이 연결사의 짝을 바꿉니다.

$$(A \otimes B)^{\perp} = A^{\perp} \mathbin{\text{⅋}} B^{\perp}, \qquad (A \,\&\, B)^{\perp} = A^{\perp} \oplus B^{\perp}, \qquad (!A)^{\perp} = {?}A^{\perp}$$

?A('와이 낫')는 !의 거울상으로, 결론 쪽에서 A를 몇 번이든 내놓아도 되는 자리입니다. 넷째 이항 연결사 ⅋(파)는 이렇게 ⊗의 거울상으로 태어났고, 가장 낯섭니다. 가장 쓸모 있는 읽기는 $A \multimap B = A^{\perp} \mathbin{\text{⅋}} B$입니다. 'A를 받는 입구와 B를 내는 출구가 안에서 이어진 장치'라는 뜻입니다. ⊗로 묶인 두 부분은 서로 아무 끈으로도 이어지지 않은 독립⁠(independence)⁠된 두 덩어리이고, ⅋로 묶인 두 부분은 안에서 끈으로 이어질 수 있는 한 덩어리입니다.

이 끈 그림⁠(string diagram)⁠을 엄밀하게 만든 것이 지라르의 증명망입니다. 증명을 규칙의 나무 대신 공식들을 잇는 선의 그물로 그리면, 규칙을 적용한 순서만 다른 증명들이 같은 그림이 됩니다. 다만 선을 아무렇게나 이은 그물이 모두 증명은 아닙니다. 둘을 가르는 기준은 1989년 뱅상 다노스와 로랑 레니에가 찾았습니다. ⊗와 ⅋만 쓰고 단위 기호는 없는 조각에서, ⅋ 연결마다 두 선 가운데 하나를 지우는 모든 방법에 대해 남은 그래프가 순환이 없고 연결되어 있으면(곧 트리⁠(tree)⁠이면), 그리고 그때에만 그 그물은 어떤 시퀀트 증명을 그린 것입니다.

선형 람다 항에도 같은 끈 그림을 그릴 수 있습니다. 변수를 묶는 λ에서 끈이 나와 몸통의 사용처로 갑니다. 선형이려면 끈마다 끝이 정확히 하나여야 합니다. 항:

계산에서 선형성은 '이 값은 한 곳에만 있다'는 보장입니다. 러스트(2015년 1.0)의 변수는 값을 소유하고, 값을 다른 변수나 함수에 넘기면(이동) 원래 변수는 더 쓸 수 없습니다. 그래서 같은 메모리 블록을 두 곳에서 해제하는 오류가 (unsafe로 표시한 코드 밖에서는) 컴파일 단계에서 막힙니다. 정확히는 쓰지 않고 버리는 것(약화)은 허락하고 복사(축약)만 막으니, 선형이라기보다 아핀 타입에 가깝습니다. 복사해도 되는 정수⁠(integer)⁠ 같은 타입에는 Copy라는 표시를 달아 !처럼 다룹니다. 하스켈의 GHC 컴파일러⁠(compiler)⁠는 2021년 9.0판부터 인자를 정확히 한 번 쓰는 함수 타입 a %1 -> b를 확장 기능으로 제공합니다. 통신에서는 '정수를 보내고, 그다음 문자열을 받고, 끝낸다' 같은 규약을 타입으로 적는 세션 타입⁠(session types)⁠이 직관주의⁠(intuitionism)⁠ 선형 논리의 명제와 대응한다는 것이 알려져 있습니다(루이스 카이르스·프랭크 페닝, 2010). 채널의 한쪽 끝을 두 곳에서 쓰면 규약이 꼬이니, 끝을 정확히 한 번 쓰게 하는 선형성이 바로 필요한 성질입니다.

이름의 '선형'은 선형대수⁠(linear algebra)⁠와도 실제로 닿아 있습니다. 벡터 공간⁠(vector space)⁠의 텐서곱⁠(tensor product)⁠에서 $v \mapsto v \otimes v$는 선형변환⁠(linear transformation)⁠이 아닙니다. 2v를 넣으면 $(2v) \otimes (2v) = 4\,(v \otimes v)$가 나와 두 배가 아니라 네 배가 되기 때문입니다. 복사는 이차식입니다. 양자역학에서 닫힌 계의 상태 변화는 선형(유니터리)이므로, 아무 양자 상태나 받아 복사하는 장치는 있을 수 없습니다. 서로 직교⁠(orthogonality)⁠하는 몇 상태만 복사하는 장치는 만들 수 있지만, 그 장치에 두 상태를 겹친 상태를 넣으면 선형성 때문에 복사본이 아닌 다른 것이 나옵니다. 1982년 윌리엄 우터스·보이치에흐 주렉과, 따로 데니스 디크스가 증명한 복제 불가 정리입니다. 그래서 양자 프로그래밍 언어의 이론(예: 피터 셀린저와 브누아 발리롱의 양자 람다 계산⁠(lambda calculus)⁠, 2006)은 큐비트에 선형 타입⁠(linear type)⁠을 줍니다. 범주론⁠(category theory)⁠으로 말하면, 집합⁠(set)⁠과 함수의 범주⁠(category)⁠에는 모든 대상에 복사 $A \to A \times A$와 버리기 $A \to 1$가 자연스럽게 있어서 데카르트 닫힌 범주⁠(cartesian closed category)⁠가 직관주의 논리(∧와 →로 된 조각)의 모형이 됩니다. 반면 벡터 공간과 텐서곱처럼 이런 복사가 없는 대칭 모노이드⁠(monoid)⁠ 범주에 ⊸까지 갖춘 것(모노이드 닫힌 범주)이 선형 논리의 모형이 됩니다. 커링⁠(currying)⁠ $\mathrm{Hom}(A \otimes B,\, C) \cong \mathrm{Hom}(A,\, B \multimap C)$는 여전히 수반으로 성립하고, !는 모나드⁠(monad)⁠의 화살표를 뒤집은 쌍대 모나드(comonad)에 복사와 버리기 구조를 더한 것으로 해석됩니다.

자원을 세는 대가도 있습니다. ⊗, ⅋, &, ⊕, !, ?를 모두 쓰는 명제 선형 논리에서는 어떤 식이 증명되는지 판정하는 알고리즘⁠(algorithm)⁠이 없습니다(패트릭 링컨·존 미첼·안드레 스세드로프·나탈라잔 섕커, 1992). 직관주의 명제 논리⁠(propositional logic)⁠가 PSPACE 완전이지만 결정 가능⁠(decidable)⁠한 것과 대조적입니다. 개수를 셀 수 있게 되자 동전의 개수로 카운터 기계의 수를 적고, &로 갈래를 치고, !로 기계의 명령을 몇 번이든 쓰게 해서 기계의 계산을 흉내 낼 수 있게 된 것입니다. !와 ?를 빼면 PSPACE 완전, ⊗와 ⅋만 남기면 NP 완전입니다. 반대로 &와 ⊕만 빼고 !를 남긴 조각이 결정 가능한지는 아직 널리 받아들여진 답이 없습니다. 흔한 오해 둘. 선형 논리는 '참이 닳는다'고 주장하는 철학이 아니라, 자원처럼 쓰이는 것을 다룰 때 쓰는 더 정밀한 도구입니다. 참처럼 쓰고 싶은 것에는 !를 붙이면 됩니다. 또 러스트가 선형 논리로부터 설계된 것은 아닙니다. 러스트의 소유권은 아핀 타입과 메모리 영역 연구에서 왔고, 선형 논리는 그 계열의 생각을 가장 깨끗하게 적은 논리입니다.

이어지는 곳. 선형 람다 항과 증명의 대응은 커리–하워드 대응의 표에서 ×를 ⊗로, →를 ⊸로 바꾼 것이며, 지라르가 이 논리에 이르기까지의 이야기는 장이브 지라르와 시스템 F⁠(System F)⁠에 있습니다. !로 보통의 논리를 되찾는 번역은 직관주의 논리를 한 번 더 들여다보게 해 줍니다. 끈 그림과 텐서곱을 체계적으로 다루는 틀은 모노이드 범주와 끈 그림이고, 복사와 버리기가 늘 있는 특별한 경우가 데카르트 닫힌 범주입니다. ⊗와 ⊸ 사이의 커링은 수반 함자⁠(adjoint functor)⁠의 한 예이고, !의 구조는 모나드를 뒤집어 보면 보입니다. 프로그램 검증에서 메모리 조각을 자원처럼 나눠 쓰는 분리 논리⁠(separation logic)⁠는 호어 논리⁠(Hoare logic)⁠에 있습니다. 복사가 이차식이라는 관찰은 선형변환의 정의에서 바로 나오며, 선형 논리 전체의 증명 가능성이 결정 불가능하다는 사실은 카운터 기계의 정지 문제⁠(halting problem)⁠를 선형 논리로 옮겨 증명합니다.