수학 증명과 컴퓨터 프로그램을 동일시하는 딥링크 | 콴타 매거진

일부 과학적 발견은 DNA의 이중 나선 구조나 블랙홀의 존재와 같은 새로운 것을 밝혀주기 때문에 중요합니다. 그러나 일부 계시는 한때 별개로 여겨졌던 두 가지 오래된 개념이 실제로는 동일하다는 점을 보여주기 때문에 심오합니다. 전기와 자기가 단일 현상의 두 가지 측면, 즉 중력과 휘어진 시공간을 연결하는 일반 상대성 이론을 보여주는 제임스 클러크 맥스웰(James Clerk Maxwell)의 방정식을 살펴보세요.

Curry-Howard 서신은 동일하지만 더 큰 규모로 한 분야 내의 개별 개념뿐만 아니라 전체 분야를 연결합니다. 컴퓨터 과학 및 수학적 논리. 커리-하워드 동형성(두 가지 항목 사이에 일종의 일대일 대응이 존재함을 의미하는 용어)이라고도 알려진 이는 수학적 증명과 컴퓨터 프로그램 사이의 연결을 설정합니다.

간단히 말해서 Curry-Howard 서신은 컴퓨터 과학의 두 가지 개념(유형 및 프로그램)이 각각 명제 및 증명, 즉 논리 개념과 동일하다고 가정합니다.

이 서신의 한 가지 결과는 프로그래밍(종종 개인 기술로 간주됨)이 이상적인 수학 수준으로 승격된다는 것입니다. 프로그램을 작성하는 것은 단순한 "코딩"이 아니라 정리를 증명하는 행위가 됩니다. 이는 프로그래밍 행위를 공식화하고 프로그램의 정확성에 대해 수학적으로 추론하는 방법을 제공합니다.

이 서신은 그것을 독립적으로 발견한 두 연구자의 이름을 따서 명명되었습니다. 1934년에 수학자이자 논리학자인 하스켈 커리는 수학 함수와 두 명제 사이의 "if-then" 진술 형태를 취하는 논리학의 함축 관계 사이의 유사성을 발견했습니다.

Curry의 관찰에 영감을 받아 수리 논리학자인 William Alvin Howard는 1969년에 계산과 논리 사이의 더 깊은 연관성을 발견하여 컴퓨터 프로그램을 실행하는 것이 논리적 증명을 단순화하는 것과 매우 유사하다는 것을 보여주었습니다. 컴퓨터 프로그램이 실행되면 각 줄은 "평가"되어 단일 출력을 생성합니다. 마찬가지로, 증명에서는 결론에 도달할 때까지 단순화할 수 있는 복잡한 진술(예: 중복 단계를 제거하거나 복잡한 표현을 더 간단한 표현으로 대체)로 시작합니다. 즉, 많은 중간 진술에서 파생된 보다 압축되고 간결한 진술입니다. .

이 설명은 대응에 대한 일반적인 의미를 전달하지만, 이를 완전히 이해하려면 컴퓨터 과학자들이 "유형 이론"이라고 부르는 것에 대해 좀 더 배울 필요가 있습니다.

유명한 역설부터 시작해 보겠습니다. 한 마을에는 스스로 면도하지 않는 모든 남자, 오직 그들만 면도하는 이발사가 살고 있습니다. 이발사는 스스로 면도를 합니까? 대답이 '예'라면 그는 자신의 면도를 해서는 안 됩니다. (왜냐하면 그는 스스로 면도를 하지 않는 남자만 면도하기 때문입니다.) 대답이 그렇지 않으면 그는 스스로 면도해야 합니다. 왜냐하면 그는 스스로 면도하지 않는 모든 사람을 면도하기 때문입니다. 이는 집합이라는 개념을 사용하여 수학의 기초를 확립하려고 시도하는 동안 Bertrand Russell이 발견한 역설의 비공식 버전입니다. 즉, 모순에 부딪치지 않고 자신을 포함하지 않는 모든 집합을 포함하는 집합을 정의하는 것은 불가능합니다.

이러한 역설을 피하기 위해 Russell은 "유형"을 사용할 수 있음을 보여주었습니다. 대략적으로 말하면 이는 특정 값을 객체라고 부르는 범주입니다. 예를 들어, 자연수를 뜻하는 “Nat”이라는 타입이 있다면 그 객체는 1, 2, 3 등이 됩니다. 연구자들은 일반적으로 콜론을 사용하여 개체의 유형을 나타냅니다. 정수형의 숫자 ​​7은 “7:Integer”로 쓸 수 있습니다. A 유형의 개체를 가져와서 B 유형의 개체를 뱉어내는 함수가 있을 수도 있고, A 유형과 B 유형이었던 개체 쌍을 결합하여 "A × B"라는 새로운 유형으로 결합하는 함수가 있을 수도 있습니다.

따라서 역설을 해결하는 한 가지 방법은 이러한 유형을 계층 구조로 배치하여 자신보다 "낮은 수준"의 요소만 포함할 수 있도록 하는 것입니다. 그러면 유형은 자신을 포함할 수 없으므로 역설을 만드는 자기 참조성을 피할 수 있습니다.

유형 이론의 세계에서는 진술이 참이라는 것을 증명하는 것이 우리가 익숙했던 것과 다르게 보일 수 있습니다. 정수 8이 짝수임을 증명하려면 8이 실제로 "짝수"라는 특정 유형의 객체라는 것을 보여주는 문제가 있습니다. 여기서 소속 규칙은 2로 나누어집니다. 8이 나누어떨어지는지 확인한 후 2에 의해 우리는 8이 실제로 Even 유형의 "거주자"라는 결론을 내릴 수 있습니다.

Curry와 Howard는 유형이 논리적 명제와 근본적으로 동일하다는 것을 보여주었습니다. 함수가 유형에 "거주"할 때, 즉 해당 유형의 객체인 함수를 성공적으로 정의할 수 있을 때 해당 명제가 참이라는 것을 효과적으로 보여주는 것입니다. 따라서 A 유형의 입력을 받아 B 유형의 출력을 제공하는 함수(A → B 유형으로 표시)는 "A이면 B입니다."라는 의미와 일치해야 합니다. 예를 들어, "비가 오면 땅이 젖어 있다"는 명제를 생각해 보세요. 유형 이론에서 이 명제는 "Raining → GroundIsWet" 유형의 함수로 모델링됩니다. 다르게 보이는 공식은 실제로 수학적으로 동일합니다.

이러한 연결이 추상적으로 들릴 수도 있지만, 이는 수학과 컴퓨터 공학 실무자들이 자신의 작업에 대해 생각하는 방식을 변화시켰을 뿐만 아니라 두 분야 모두에서 몇 가지 실제 적용으로 이어졌습니다. 컴퓨터 과학의 경우 소프트웨어 검증, 즉 소프트웨어의 정확성을 보장하는 프로세스에 대한 이론적 기반을 제공합니다. 프로그래머는 논리적 명제 측면에서 원하는 동작을 구성함으로써 프로그램이 예상대로 동작한다는 것을 수학적으로 증명할 수 있습니다. 또한 보다 강력한 함수형 프로그래밍 언어를 설계하기 위한 강력한 이론적 기반을 제공합니다.

그리고 수학의 경우, 서신은 다음과 같은 탄생으로 이어졌습니다. 증명 보조원, 대화형 정리 증명자라고도 합니다. 이는 Coq 및 Lean과 같은 형식 증명을 구성하는 데 도움이 되는 소프트웨어 도구입니다. Coq에서 증명의 각 단계는 본질적으로 프로그램이며, 증명의 유효성은 유형 확인 알고리즘을 통해 확인됩니다. 수학자들은 또한 증명 보조 도구를 사용해 왔습니다. 린 정리 증명자 — 엄격한 컴퓨터 검증 형식으로 수학적 개념, 정리 및 증명을 표현하는 수학을 공식화합니다. 이를 통해 때때로 비공식적인 수학 언어를 컴퓨터로 확인할 수 있습니다.

연구자들은 여전히 ​​수학과 프로그래밍 사이의 이러한 연관성의 결과를 탐구하고 있습니다. 커리-하워드의 원래 서신은 프로그래밍을 직관주의적 논리라고 불리는 일종의 논리와 융합했지만, 더 많은 유형의 논리도 그러한 통합에 적용될 수 있다는 것이 밝혀졌습니다.

“커리의 통찰 이후 세기에 일어난 일은 우리가 '논리 시스템 X가 계산 시스템 Y에 대응하는' 사례를 점점 더 많이 발견한다는 것입니다."라고 말했습니다. 마이클 클락슨, 코넬 대학교의 컴퓨터 과학자. 연구자들은 이미 "자원"이라는 개념을 포함하는 선형 논리와 가능성과 필요성의 개념을 다루는 모달 논리와 같은 다른 유형의 논리에 프로그래밍을 연결했습니다.

그리고 이 서신에는 커리와 하워드의 이름이 적혀 있지만, 그것을 발견한 사람은 결코 그들만이 아닙니다. 이는 서신의 기본 특성을 입증합니다. 사람들은 계속해서 이를 알아차립니다. Clarkson은 “계산과 논리 사이에 깊은 연관성이 있다는 것은 우연이 아닌 것 같습니다.”라고 말했습니다.