커리–하워드–드 브라윈 대응에 대한 기초적 소개

URL: https://patternatlas.com/v0/curry-howard-de-bruijn/

Title: An Elementary Introduction to the Curry Howard de Bruijn Correspondence

PartITypes as Propositions

이 글은 내가 커리–하워드–드 브라윈 대응(Curry Howard de Bruijn Correspondence)을 어떻게 이해하게 되었는지에 대한 기록이다. 이것은 논리 체계와 컴퓨터 프로그램 사이의 깊은 대응 관계로, 최초로는 1940년대 무렵에 식별되었다. 나는 그동안 주워 들은 밑바탕 아이디어들을 엮어, 이 대응을 이해하기 위한 입문서로 만들고자 했다. 개념을 설명하는 데 필요한 만큼의 기술 용어만 쓰는, 비교적 편안한 톤의 글로 유지했다.

전체적으로는, “프로그램은 증명의 다른 얼굴(그리고 그 반대도 마찬가지!)”라는 매혹적인 생각을 처음 배울 때 내가 갖고 싶었던 안내서를 목표로 구성했다. 당시 나는 사용자 인터페이스 디자이너/개발자였고, 이 아이디어들을 파악하는 데 기초가 되는 조밀한 형식적 자료들을 이해할 역량이 없었다.

처음 이 대응을 접했을 때는 어디서부터 읽어야 할지 막막했다. 제한된 수학 경험으로는 도무지 감을 잡기 어려웠다. 아이디어들이 놓이고 전달되는 전체 기호적 전통이, 무엇이 말해지고 있는지 꿰뚫어 보기 어렵게 만들었다.

하지만 어느 정도 끈기 있게 파고들고 나니, 더 깊이 들어가 이 자료들을 이해하기 시작할 수 있는 지점에 도달한 것 같다. 나는 이 탐구를 기록하는 저널 시리즈로 이어가고 싶다. 이 여정을 걷는 다른 학습자들에게, 지금까지 배운 것들을 가능한 한 접근하기 쉬운 방식으로 공유하려 한다. 실무 프로그래머에게 이 아이디어가 주는 실용적 장점이나 함의를 강조하는 데 도움이 된다고 생각해, 설명은 전통적인 프로그래밍 관용구에 가깝게 유지했다. 다만 이 글은 초보 프로그래머를 대상으로 하지는 않는다. 타입이 있는 언어로 프로그래밍을 해 본 경험과, 논리에 대한 기본적인 노출이 있다는 것을 전제로 한다. 또한 이 분야를 탐험하고 배우는 과정에서 흥미롭게 읽은 작업들을 일부 링크해 두었다.

이런 서론을 마쳤으니, 이제 커리–하워드–드 브라윈 대응을 이루는 아이디어들을 펼쳐 보며 탐구를 시작해 보자!

이게 뭐지? 왜 신경 써야 하지?

커리–하워드–드 브라윈 대응 같은 거창해 보이는 개념을 처음 들으면 자연스레 이런 질문이 떠오를 것이다. “왜 이걸 배워야 하지?” 특히 이미 배울 것이 산더미인데, 이렇게 추상적이고 이론적인 것을 말이다. 이 글을 다 읽고 나면, 고효율 이론을 배우는 데 집중하는 프로그래머에게 왜 이것이 유용한 무기가 될 수 있는지 그 함의를 보게 되기를 바란다.

커리–하워드–드 브라윈은, 이전에는 서로 무관하다고 여겨졌던 수학의 형식 체계들 사이의 깊은 대응이다. 약간의 형식적 엄밀함을 희생하고 단순하게 말하자면, 수학적 대상에 대한 증명은 데이터에 대한 계산과 쌍대(dual) 관계에 있다. 이 의미에서 증명은 우리가 계산에 사용하는 수학적 대상의 존재에 대한 증거/증인 역할을 하고, 프로그램은 구체적 데이터로 이 대상을 “실현”하는 방식이다. 설명 자료를 읽다 보면 보통 “타입은 명제(types as propositions), 증명은 프로그램(proofs as programs)” 사이의 대응으로 요약된다. 또한 “증명의 단순화는 컴퓨터 프로그램의 평가(evaluation)와 동등하다”는 점이 강조된다. 처음 접하면 상당히 밀도 높은 주장들이다. 이제 여기서 무슨 일이 벌어지는지 풀어 보자.

이것은 관련된 세 분야 사이의 삼자 대응으로 설명할 수 있다. 다이어그램에서 보듯, 서로 다른 목적을 위해 사용되는 세 가지 프레임워크가 이 결절점에서 상호 보완적인 삼각관계로 묶인다. 덕분에 두 세계씩 짝지은 세 쌍 사이를 오가며 사고할 수 있다.

I Type ↔ Computation

타입과 계산의 세계에서, 계산에서 타입으로 가는 방향은 코드베이스로부터 타입을 추론할 수 있게 해 준다. 반대 방향에서는 타입 정보로부터 코드 합성(code synthesis)을 얻는다.

II Computation ↔ Logic

계산과 논리의 세계에서는, 프로그램을 증명하고 증명을 프로그래밍할 수 있게 된다!

III Logic ↔ Type

논리와 타입의 세계에서는, 논리의 기계를 타입에 적용해 작업할 수 있고, 타입은 논리가 특정한 이율배반(antinomies)에서 벗어나는 데 도움을 준다.

이 에세이의 목적을 위해, 나는 이 프레임워크들 사이의 상호작용 특징을 비추는 네 번째 짝을 도입한다. 그것은 데이터라는 범주인데, 타입의 서로 다른 논리적 정식화가 컴퓨터 프로그램의 구조/프로세스를 어떻게 독특하게 조직하도록 결정하는지를 조명한다. 이 연결은 진행하면서 설명하겠다.

이런 방식으로 다이어그램을 조직하면, 두 쌍으로 분해할 수 있다: 1) Type ↔ Computation 쌍과 2) Logic ↔ Data 쌍. 위에서 쌍색(dual colors)로 표시했듯이 type/logic과 computation/data 사이에는 대략적인 상보성이 있다.

이는 위 다이어그램에서 가능한 여섯 가지 상호작용 쌍 중 두 가지일 뿐이다. 내가 이 둘을 따로 집어낸 이유는, 첫째로 이것들이 이 글을 쓰게 만든 직접적 동기이기 때문이다. 둘째로, 이 쌍들이 주는 통찰이 실무 프로그래머에게 이 아이디어가 갖는 실용적 함의를 더 또렷하게 해 준다고 느꼈다. 이론을 배우고 그 함의를 끌어내는 데는 큰 시간 투자가 든다. 나는 실천 지향의 프로그래머에게 공명할 수 있는 관점을 보여 주고 싶었다. 이것이 일상의 실무에 어떤 영향을 줄 수 있는지 동기 부여가 되기를 바란다. 셋째로, 이 쌍들은 한 차원에서의 쌍대성이 다른 차원에서의 상호작용에 어떻게 반영되는지를 붙잡을 손잡이를 제공한다. 즉 type ↔ computation 상호작용이 logic ↔ data 상호작용으로 어떻게 비친다는 점이다.

Type ↔ Computation Interaction

위로 향하는 방향에서는 타입 추론(type inference)이 있다. Algorithm W 같은 알고리즘이, 계산을 수행하는 함수들이 어떤 타입을 사용하고 있는지 추론하게 해 준다. 아래 방향에서는 타입에 대한 기술(description)로부터 코드 합성을 얻는다.

Logic ↔ Data Interaction

논리에서 데이터로 가는 방향에서는, 같은 계산을 서로 다른 논리로 표현하는 방식이 그 내용으로서의 데이터 구조를 독특하게 결정한다. 이는 계산 프로세스가 실행되는 존재론(ontology)을 바꾸는 것으로 생각할 수 있다. 반대로 데이터에서 논리로 가는 방향에서는, 예컨대 텍스트 검색에서 트리 대신 트라이(trie)를 선택하는 것처럼 다른 데이터 구조를 선택하는 일이, 프로그램에서 전개되는 증명의 형태를 결정한다. 이는 프로그램의 타입으로 직접 반영된다.

A Leitmotif

나는 위의 네 가지 개념을 네 개의 원형 핀으로 압축해 보드 위에 나타냈고, 이를 이 에세이 전반에 걸쳐 반복되는 모티프로 사용할 것이다. 이는 에세이의 특정 절이 대응의 어느 부분을 다루는지 표시하는 데 도움이 된다.

다음은 이 에세이에서 다룰 네 가지 상이한 주제에 대응하는 네 가지 구성이다. CHD 대응의 그 측면을 건드릴 때마다 적절한 아이콘을 사용하겠다.

Type

Logic

Computation

Data

이 글의 전개 과정에서 우리는 이 조합들을 네 번 순환할 것이다. 네 번째에 이르면(내가 일을 잘했다면) 이 개념들 사이의 의미와 상호작용이 더 분명해질 것이다.

이 글을 다 읽고 나면 최소한, 겉보기에는 서로 동떨어져 보이는 이상한 수학/컴퓨터 과학 아이디어들 사이에 얼마나 깊은 숨은 통일성이 있는지 이해하려는 사람에게, 여러 형식주의를 가로지르는 이런 대응이 왜 매혹적인지 드러나기를 바란다.

Synopsis

이 절에서는 글 전체를 짧게 조망하는 파놉티콘(panopticon)으로서, 이 글을 쓰게 된 계기 뒤의 이야기를 다시 떠올려 보려 한다. 내가 이런 연결을 만들어 가며 느낀 핵심을, 이 회고 속에 담아내고 싶다.

이 짧은 회고 뒤에는, 이 에세이의 두 번째와 세 번째 절에서 계산 함수의 타입이 어떻게 논리 명제로 보일 수 있는지, 그리고 이 논리적 조직이 어떻게 조합적 대상(combinatorial objects)으로 구체적으로 이해될 수 있는지를 보게 될 것이다. 요약 부분에서는 반대로, 서로 다른 데이터 구조를 선택하는 일이 프로그램의 서로 다른 리팩터링 스타일로 이해될 수 있고, 이것이 타입의 논리로 어떻게 반영되는지를 보여 주겠다.

이 글 아이디어를 어떻게 떠올리게 되었는지 이야기해 보자:

Logic

논리 능력을 다듬기 위해 Harold Halvorson의 입문서 How Logic Works를 공부하던 중, 다음 공식들 사이의 동치성을 보게 되었다:

P -> (Q -> R) <=> (P ∧ Q) -> R

논리적으로 말하면, 이는 두 개의 동치인 명제를 갖고 있다는 뜻이다. 좌변은 명제 $P$가 또 다른 함의 $(Q -> R)$를 함의하는 형태이고, 우변은 두 명제 $P$와 $Q$의 연언(conjunction)이 $R$을 함의하는 형태다.

Type

나는 이전에 커리–하워드–드 브라윈 대응을 접했던 경험과, Chris Taylor의 “The Algebra of Algebraic Data Types”라는 강연 및 함께 읽을 수 있는 블로그 시리즈를 떠올렸다. 그 글에서는 X imply Y가 타입 이론에서 지수 타입(exponential type)으로, X and Y가 곱 타입(product type)으로 볼 수 있다고 말한다.

그 글의 핵심은, 이런 타입들이 그 거주자(inhabitants)의 개수를 나타낸다는 점이다. P -> Q가 있으면 지수 타입이고, P * Q가 있으면 곱 타입이라는 뜻이다.

P -> (Q -> R) <=> (P * Q) -> R

구체적 대상으로 생각해 보면, 지수 타입에서는 가능한 함수의 수를 세는 것으로, 곱 타입에서는 대상들의 동시 발생(co-occurrences)을 세는 것으로 볼 수 있다. 이게 무슨 뜻일까? 산술적 대응물로 번역해 보면 더 명확해진다. 지수 타입을 거듭제곱 연산으로, 곱 타입을 곱셈으로 나타내면, 이는 수를 거듭제곱하는 다음 산술 항등식과 매우 흡사한 모습을 보인다:

(XM)N = X(M×N)Example(21)3 = 21×3

수의 경우엔 이해하기 쉽지만, 이것이 계산의 경우와는 어떻게 연결될까? 원소가 각각 3개와 2개인 두 타입 $X$와 $Y$를 생각해 보자. 사상 $X -> Y$는 예를 들어 “2가지 색의 자동차 3대”, “2종의 식물 3개”, 심지어 “2개의 꿈을 가진 3개의 이야기” 같은 것일 수 있다.

![Image 13: Exponential Type

                    X with 2 elements {a, b} → Y with 3 elements {1, 2, 3}
                    
                    A tree organized with two leaves X and Y with subscript 2 and 3 respectively, conjoined by → as the parent node. It is labelled Type Level (External View). This is compared against another equivalent visualization with the internal contents of X and Y, {a, b} and {1, 2, 3} visualized as nested capsules contained inside a box with the operator label →. It is labelled Inhabitant Level (Internal View).](https://patternatlas.com/v0/curry-howard-de-bruijn/img/exponential-type-intro.svg)

이 상황은 두 가지 관점에서 볼 수 있다. 바깥/외부 관점에서는, 지수 타입을 수의 거듭제곱처럼 생각할 수 있다. 3 -> 2는 $2^3$처럼 대응한다. 즉 외부적으로는, 타입이 거듭제곱 형태로 거주자 수를 추적한다고 볼 수 있다. 하지만 안쪽/내부 관점으로 들어가면, 정말 흥미로운 일이 벌어진다!

![Image 14: Inhabitants of Exponential Type

                        Visualization of possible functions between { a, b } → {1, 2, 3}
                        
                        {<a,1>,<b,3>}
                        {<a,1>,<b,2>}
                        {<a,2>,<b,3>}
                        {<a,3>,<b,1>}
                        {<a,2>,<b,1>}
                        {<a,3>,<b,2>}
                        {<a,1>,<b,1>}
                        {<a,2>,<b,2>}
                        {<a,3>,<b,3>}](https://patternatlas.com/v0/curry-howard-de-bruijn/img/inhabitants-of-exponential-type-intro.svg)

타입의 거듭제곱이 내부에서 하는 일은, 두 영역 사이의 잠재적 함수들을 추적하는 것이다! 우리는 두 도메인 사이의 함수의 개수, 즉 왼쪽(정의역)의 것들이 오른쪽(공역)의 것들로 사상될 때 부여될 수 있는 다대일 이름짓기의 경우의 수를 세고 있는 셈이다. 이것이 X -> Y 형태의 지수 타입이 의미하는 바다.

이제 곱 타입에서 무슨 일이 벌어지는지 보자. 곱에서는 두 타입을 곱할 때, 외부 수준에서 그 거주자들이 함께 나타날 수 있는 모든 경우의 수를 추적한다!

![Image 15: Exponential Type

                X with 2 elements {a, b} → Y with 3 elements {1, 2, 3}
                
                A tree organized with two leaves X and Y with subscript 2 and 3 respectively, conjoined by → as the parent node. It is labelled Type Level (External View). This is compared against another equivalent visualization with the internal contents of X and Y, {a, b} and {1, 2, 3} visualized as nested capsules contained inside a box with the operator label →. It is labelled Inhabitant Level (Internal View).](https://patternatlas.com/v0/curry-howard-de-bruijn/img/product-type-intro.svg)

다음은 데카르트 곱(cartesian product) 연산을 계산했을 때의 시각화다. 외부 관점에서의 타입의 연언은 내부적으로 함께 나타날 수 있는 모든 원소 쌍의 컬렉션을 만들어내는 것으로 생각할 수 있다.

![Image 16: Inhabitants of Product Type

                    Visualization of product of X := {a, b} * Y := {1, 2, 3}
                    
                    [a, 1]
                    [a, 2]
                    [a, 3]
                    [b, 1]
                    [b, 2]
                    [b, 3]](https://patternatlas.com/v0/curry-howard-de-bruijn/img/inhabitants-of-product-type-intro.svg)

Computation

타입은 내부 계산 내용에 대한 바깥 관점이다. 지수 타입은 함수를 기술하는 방식이고, 곱 타입은 연언된 타입들에서 가능한 모든 원소의 데카르트 곱을 포착한다. 이런 생각의 흐름을 따르면, 타입으로 표현되는 논리는 컴퓨터 프로그램에 대한 두 가지 다른 형태의 기술로 볼 수 있다.

이것이 “타입은 명제” 해석이다. 타입은 합성되어 명제문을 이룬다. 이 명제들을 증명하려면, 우리의 증명 시스템 성질과 조화를 이루는 평가 규칙(evaluation rules)을 도입해야 한다. 시각을 돌려 계산의 관점에서 보면, 이 명제들을 증명하는 과정은 타입을 존중하는 프로그램을 작성하는 방식과 평행을 이룬다! 이런 의미에서 대략적으로, 타입은 형식(form)이고 계산은 그 내용(content)이라고 볼 수 있다.

curriedFunction :: P -> (Q -> R)
                    curriedFunction = pThing => qThing => rThing

<=>

uncurriedFunction :: (P * Q) -> R
                    uncurriedFunction = (pThing, qThing) => rThing

계산의 관점에서 지수 타입은 커리잉(currying)이라고 불리는 프로그램 조직 방식을 나타낸다. 이 표현에서는 매개변수를 한 번에 하나씩 함수에 전달한다. 즉 먼저 타입 $P$의 값을 넘기고, 그러면 타입 $Q$의 값을 넘겨야 하는 새 함수가 “열리고”, 그렇게 해서 $R$을 얻는다. 반면 곱 타입 $P * Q$는 매개변수의 연언, 즉 $P$와 $Q$를 함께 $(P, Q)$로 묶어 전달하는 것을 뜻한다. $P$를 먼저, 그다음 $Q$를 넘겨 $R$을 얻는 타입/명제의 사슬 대신, 두 값을 동시에 인자로 넘기는 것이다.

Sergei가 타입의 논리를 활용해 계산적 내용을 추출하는 방법을 설명한 아주 좋은 발표가 있다. 내게는 타입이 계산으로 어떻게 사상되는지 이해하는 데 큰 도움이 되었다!

Data

나는 한편으로는 이산 미적분과 조합론도 조금씩 파고 있었는데, 이 노력들이 타입이 기술하는 분할/조합이 그 거주자 계산 프로세스를 추적하는 방식의 서로 다른 모습으로서, 밑바탕 구조를 어떻게 볼 수 있는지 비추어 주었다. 이 조각들이 맞물리면서 이 글을 쓰게 되었다.

조합론적으로 무슨 일이 일어나는지 보이기 위해, $P$가 원소 2개, $Q$가 1개, $R$이 3개인 예를 들겠다. 이렇게 하면 구조에서 벌어지는 일을 해석할 구체적 맥락이 생긴다. 많은 교과서에서 이 부분은 대수식으로 다뤄진다. 하지만 조합론 속에는 정말 맛있는 시각적 아이디어가 많다고 생각한다. 나는 개인적으로, 대수적(내포적, intensional) 텍스트 설명은 그에 대응하는 시각적 기하학적(외연적, extensional) 설명으로 보완되어야 밑바탕 아이디어를 더 풍부하게 하고 밝혀 준다고 느낀다.

나는 점점 더 확신하게 된다. 대수가 어떤 형식을 구획하고 그 내용을 연구하기 위해 사용될 때마다(기저 대상이 아무리 추상적이거나 복잡하더라도), 그 대수식에 대응하는 기하학을 붙여 시각적 형태와 전달 가능한 구조를 부여할 수 있다는 것을. 우리가 그것들을 시각화하는 방식은, 서로가 어떻게 연결되는지/구분되는지를 볼 수 있는 구체적 장을 제공한다. 이는 대수로 마음의 눈 속에서 수학적 대상의 형식/내용을 보고, 몸의 눈으로 가능한 기하학적 구현을 보는 길을 열어 준다. 대수와 기하의 결합은, 동료들과 수학을 기호적으로도 촉각적으로도 인지하고 소통하게 해 준다.

![Image 19: P -> (Q -> R) and (P * Q) -> R and their visualizations at the Type Level (External View) and Inhabitant Level (Internal View). P has 2, Q has 1, and R 3 elements.

                At the Type Level for P -> (Q -> R), a tree visualization is shown with P on the left paired with the pair Q and R, all with the -> operator. At the Inhabitant level, nested boxes are shown with 3 orange triangles inside P, a yellow circle inside Q, and 2 purple squares inside R. Q and R are nested inside a box with an -> operator on top. It is nested inside another container with P on the left and another -> operator on top.
                
                At the Type Level for (P * Q) -> R, a tree is shown with P and Q on the left paired with the * operator, which is paired with R using ->. At the inhabitant level, nested boxes with internal details of the types are exposed in the same manner as above, but with * on top of the container of P and Q. This is nested inside another box with R on the right with -> on the top.](https://patternatlas.com/v0/curry-howard-de-bruijn/img/data-type-inhabitants-intro.svg)

바깥에서 보면 사상은 이렇게 생겼다. 이제 여기에 내재한 관계를 평가하고, 이들 사이에 성립하는 가능한 함수의 수를 세어 보자. 타입 절에서 준 직관을 이용하면, 전개해 보며 이들이 잠재적으로 생성할 수 있는 조합의 수를 확인할 수 있다.

위 관계를 전개하는 방법은 많다. 가능성 중 어떤 방식을 택하느냐에 따라 특정한 전개 형태가 나온다. 나는 이항 트리(binary trees) 형태를 유지하면서도, 거듭제곱 과정이 단계적 전개로 이어지고 각 레벨이 지수의 거주자에 의해 점진적으로 인덱싱되는 모습을 드러낼 수 있는 방식을 하나 선택했다.

여기서의 전개 패턴은 {a, b}를 세 번 곱해 생성된 8개의 노드로 볼 수 있지만, 각 레벨은 특정 레벨에 대응하는 (P * Q)의 거주자 중 하나에 의해 인덱싱된다. 이를 산술로 생각하면 더 쉬울 수 있다. $P$와 $Q$는 각각 3개와 1개의 원소를 가지므로 $3×1$ = 3개의 노드가 나온다. 이는 원소가 2개인 $R$의 지수가 되어 $2^{(3×1)}$ = 8개의 노드를 만든다.

곧바로 눈에 띄는 점 하나는, 전개의 각 레벨에서 가지치기하는 트리를 얻는다는 것이다. 2를 나타내는 {a, b} 쌍만 보면, 각 레벨에서 이분(bifurcating)하며 형식적 수열 $2^1, 2^2, 2^3$을 만든다. 즉 $R$의 거주자인 {a, b}가, 3개의 원소를 가진 지수 $P * Q$의 거주자에 의해 각 레벨에서 인덱싱되며(전개 단계마다 하나씩) 전개된다. 각 레벨을 보면, 이는 (a, b) * (a, b) * (a, b)의 표현인데, 각 레벨이 3개 원소를 가진 (P * Q) 쌍에서 하나의 원소를 소비하며 인덱싱된다.

타입 거주자들 사이의 대수적 관계를 완전히 전개하면, 다음의 정규화(normalized) 결과를 얻는다. 이는 트리를 바닥까지 완전히 펼쳤을 때 얻는 대상들이라고 생각할 수 있다.

![Image 20: An Unfolding Pattern of (P * Q) -> R

                    Shows the tree of unfolding the inhabitants of the types (P * Q) -> R which can be described using S-expressions as:
                    
                    (+
                        (*
                            (-> (* 1 I) a)
                                    (+
                                    (* (-> (* 2 I) a)
                                        (+ (-> (* 3 I) a) (-> (* 3 I) b))
                                    )
                                    (* (-> (* 2 I) b)
                                        (+ (-> (* 3 I) a) (-> (* 3 I) b))
                                            )
                                    )
                        )
                            (*
                            (-> (* 1 I) a)
                                    (+
                                    (* (-> (* 2 I) a)
                                        (+ (-> (* 3 I) a) (-> (* 3 I) b))
                                    )
                                    (* (-> (* 2 I) b)
                                        (+ (-> (* 3 I) a) (-> (* 3 I) b))
                                            )
                                    )
                        )
                    )
                    
                    At each level (* 1 I), (*2 I), and (* 3 I) are extracted out of the common pairs to highlight they are recurring and put around a common container of (+ a b). Thus there is only a single (* 1 I), two (* 2 I)s, and 4 (* 3 I)s at each unfolding level of the tree.](https://patternatlas.com/v0/curry-howard-de-bruijn/img/unfolding-pattern-of-uncurried-intro.svg)![Image 21: The normalized results of unfolding the uncurried function (P * Q) -> R with 2, 1, and 3 inhabitants respectively.

                    Shows a grid of the results:
                    
                    ((1 * I) -> a) * ((2 * I) -> a) * ((3 * I) -> a)
                    ((1 * I) -> a) * ((2 * I) -> a) * ((3 * I) -> b)
                    ((1 * I) -> a) * ((2 * I) -> b) * ((3 * I) -> a)
                    ((1 * I) -> a) * ((2 * I) -> b) * ((3 * I) -> b)
                    ((1 * I) -> b) * ((2 * I) -> a) * ((3 * I) -> a)
                    ((1 * I) -> b) * ((2 * I) -> a) * ((3 * I) -> b)
                    ((1 * I) -> b) * ((2 * I) -> b) * ((3 * I) -> a)
                    ((1 * I) -> b) * ((2 * I) -> b) * ((3 * I) -> b)](https://patternatlas.com/v0/curry-howard-de-bruijn/img/uncurried-version-normalized-results-intro.svg)

이제 P -> (Q -> R)의 경우를 보자. 여기서의 전개 패턴은 (P * Q) -> R의 경우와 거의 같아 보인다. 하지만 자세히 보면, 각 레벨에서 전개를 인덱싱하고 잎을 표시하는 라벨이 다르다. 이제 전개되는 것은 (Q -> R)의 거주자들이고, 각 레벨은 이전 사례처럼 $P * Q$를 지수로 하는 $R$의 거주자가 아니라, 각 레벨에서 $P$의 거주자에 의해 인덱싱된다.

![Image 22: An Unfolding Pattern of P -> (Q -> R)

                        Shows a tree of unfolding the inhabitants of the types P -> (Q -> R) which can be described using S-expressions as:
                        
                        (+
                            (*  (-> 1 (-> I a))
                                (+
                                    (* (-> 2 (-> I a))
                                        (+
                                            (-> 3 (-> I a))
                                            (-> 3 (-> I b))
                                        )
                                    )
                                    (* (-> 2 (-> I b))
                                        (+
                                            (-> 3 (-> I a))
                                            (-> 3 (-> I b))
                                        )
                                    )
                                )
                            )
                            (*  (-> 1 (-> I b))
                                (+
                                    (* (-> 2 (-> I a))
                                        (+
                                            (-> 3 (-> I a))
                                            (-> 3 (-> I b))
                                        )
                                    )
                                    (* (-> 2 (-> I b))
                                        (+
                                            (-> 3 (-> I a))
                                            (-> 3 (-> I b))
                                        )
                                    )
                                )
                            )
                        )
                        
                        At each level, the indices 1, 2, and 3 are extracted out of the common pairs of (-> I a) and (-> I b) to highlight they are repetitive and put around a common container of (+ (-> I a) (-> I b)). Thus there is only a single 1, two 2s, and 4 3s at each unfolding level of the tree.](https://patternatlas.com/v0/curry-howard-de-bruijn/img/unfolding-pattern-of-curried-intro.svg)

여기서의 분석만 보면, 두 정식화의 전개 패턴이 거주자의 구성과 무관하게 항상 같을 것처럼 보일 수 있다. 하지만 이 예에서 같아 보인 것은 $Q$가 거주자 1개를 가진 경우였기 때문이다. 뒤의 절에서는, 이 언커리드/곱의 지수를 사용하는 버전이 커리드/연쇄 지수 버전보다 더 깊은 트리를 만드는 예를 보게 될 것이다.

다음은 트리를 완전히 펼쳐 노드들을 얻은 결과다. 개별 구성 요소들이 공유하는 패턴에서도 P -> (Q -> R)의 연쇄 지수 형태가 드러난다는 점에 주목하라.

![Image 23: The normalized results of unfolding the curried function P -> (Q -> R) with 2, 1, and 3 inhabitants respectively.

                        Shows a grid of the results:
                        
                        (1 -> (I -> a)) * (2 -> (I -> a)) * (3 -> (I -> a))
                        (1 -> (I -> a)) * (2 -> (I -> a)) * (3 -> (I -> b))
                        (1 -> (I -> a)) * (2 -> (I -> b)) * (3 -> (I -> a))
                        (1 -> (I -> a)) * (2 -> (I -> b)) * (3 -> (I -> b))
                        (1 -> (I -> b)) * (2 -> (I -> a)) * (3 -> (I -> a))
                        (1 -> (I -> b)) * (2 -> (I -> a)) * (3 -> (I -> b))
                        (1 -> (I -> b)) * (2 -> (I -> b)) * (3 -> (I -> a))
                        (1 -> (I -> b)) * (2 -> (I -> b)) * (3 -> (I -> b))](https://patternatlas.com/v0/curry-howard-de-bruijn/img/curried-version-normalized-results-intro.svg)

이제 표현식의 전개 형태와 정규화 결과를 함께 놓아 보자. 왼쪽은 두 개의 연쇄 지수를 갖는 커리드 버전이고, 오른쪽은 곱 타입을 지수 타입과 연결한 언커리드 버전이다. 타입이 추적하는 “프로세스”로서의 가능한 계산을, 이 카운팅을 수행하기 위한 데이터 구조로 물질화(reify)하고 있음을 보라.

![Image 24: The juxtaposition of Unfolding Pattern and Normalized Results of P -> (Q -> R) and (P * Q) -> R

                        Unfolding pattern of P -> (Q -> R) shows {I, a}, and {I, b} unfolding as two trees with either of them as the root node and then doubling and finally quadrupling resulting in 2 of them at the first stage, 4 of them in the second stage, and 8 of them in the third and last stage. Each of these stages are tracked by 1, 2, and 3 respectively.
                        
                        The Normalized Results of this unfolding pattern is shown as described in: https://patternatlas.com/v0/curry-howard-de-bruijn/img/uncurried-version-normalized-results-intro.svg
                        
                        Unfolding pattern of (P * Q) -> R shows {a, b} unfolding as two trees with either of them as the root node and then doubling and finally quadrupling resulting in 2, 4, and 8 of them per stage. Each of these stages are tracked by 1 * I, 2 * I, 3 *I respectively.
                        
                        The Normalized Results of this unfolding pattern is shown as described in: https://patternatlas.com/v0/curry-howard-de-bruijn/img/curried-version-normalized-results-intro.svg](https://patternatlas.com/v0/curry-howard-de-bruijn/img/curried-uncurried-juxtaposition-intro.svg)

여기서 내가 강조하고 싶은 핵심은, 두 표현식이 구조로서 서로 다른 전개 패턴을 갖고 있음에도 불구하고, 정규화(즉 더는 단순화될 수 없는 항으로 평가)하면 결과가 동일해진다는 점이다.

여기에는 연산자가 다르다는 작은 주름(wrinkle)이 있다. 하지만 정규화된 원소 수준에서는 11이 1 × 1과 같은 것이라는 항등성이 있다. 즉 어떤 것을 1로 거듭제곱하는 것은 1번 곱하는 것과 동일하다. 이를 이용해 한 형태를 다른 형태로 바꿀 수 있다. 이런 대수적 변환은 뒤의 절에서 다루겠다. 지금은 큰 윤곽만 전달하려 한다.

이 둘을 조직하는 전역 구조는 매우 다르지만, 그 지역적 거주자들은 완전히 펼쳐 보면 의미론적으로 동일한 것으로 드러난다. 최종 결과의 이 동형(isomorphism)은 타입들 사이의 논리적 동치가 추적한다. 논리 영역에서 성립하는 동치는, 거주자 데이터 구조의 기수(cardinality)의 동일성으로 번역된다. 이는 프로그램을 논리적으로 조직하는 방식이, 우리가 프로그램을 생각하는 방식뿐 아니라 기계가 공간과 시간 위에서 이를 실행하는 방식에도 영향을 준다는 것을 보여 준다. 이것은 매우 기초적인 예일 뿐이고, 그 밑바탕 이론은 훨씬 더 풍부하고 깊으며 더 많은 꼬임과 뒤틀림, 땋임과 매듭을 갖고 있다.

만약 이 아이디어들을 처음 접했다면, 걱정하지 말라. 지금 이 지점에서 이 에세이를 따라가기 위해 필요한 것은, 타입 수준에서 프로그램을 조직하는 두 가지 방식이 서로 다른 전개 패턴을 만든다는 기본 요지뿐이다. 전개 패턴이 구조적으로 같아 보이더라도, 각 레벨에서의 내용(인덱스와 잎의 거주자)은 크게 다르다는 흥미로운 사실에 주목하라. 나는 이것이 데이터베이스 아키텍처 결정이나 알고리즘 설계에서 우리가 내리는 선택을 비추는 중요한 아이디어가 될 수 있다고 느낀다. 이것이 일반적인 프로그래밍과 시스템에서 데이터를 다루는 일에 갖는 더 넓은 함의는 앞으로 탐구해 보고 싶다. 하지만 초점을 분명한 문제에 맞추기 위해, 다음 절들에서는 구체적 예로 평범한 프로그래밍 과업에 대한 함의를 전개해 보겠다.

A Brief History of the Correspondence

계산과 논리 체계의 이 연결은, Nicolaas G. de Bruijn이 AUTOMATH를 설계할 때(명제를 람다 계산 항의 “범주(categories)”로, 증명을 항으로) 계산적 맥락에서 인식되었다. 그는 Heyting의 작업에서 지수(exponentials) 아이디어를 빌려왔다고 언급하는데, 이를 보는 것도 흥미롭다. 다음은 AUTOMATH에 대한 자신의 작업을 되돌아보는 그가 쓴 좋은 논문이다.

하지만 이 대응의 최초 식별은(당시에는 컴퓨터 프로그램이 없었음에도) Haskell Curry가 자신의 조합 논리(combinatory calculus)로 논리 체계를 연구하던 중에 이루어졌다. 이는 1934년의 “Functionality in Combinatory Logic”라는 논문에 기록되어 있다. 다만 이 노력은 약 30년 동안 충분히 발전되지 못했고, William Howard가 이를 알아보고 확장할 때까지 그러했다!

William Howard는 Haskell Curry의 작업에 영향을 받아, 1969년 원고에서 독립적으로 이 대응을 진술했다. 이 글은 널리 회람되었고 1980년에 출판되었다. 이때쯤 이 아이디어는 연구 문화 속으로 삼투(osmosized)되었고, 그 이후로 계속 연구되고 발전해 왔다!

이것으로, 네 갈래 대응을 매우 빠르고 간단히 훑어 보았다. 이것만으로도 왜 이 아이디어가 흥미로운지 어느 정도 빛을 비춘다고 생각한다! 하지만 미리 이런 것들을 알고 있지 않았다면 너무 빠르게 느껴졌을 것이다. 이제 원래 방정식의 각 변을 하나씩, 더 느린 속도로 풀어 보자.

❖ ❖ ❖

다음 절은 정말 정말 곧 이어질 예정이다. 계속 지켜봐 달라.

Follow us on Twitter — PatternAtlas