프로그래머인 내가 논리학을 공부하는 이유
직관적 타입 이론은 "타입과 명제가 일대일 대응된다"는 사상(커리-하워드 대응)과 의존적 타입 시스템을 바탕으로 수학의 토대를 쌓은 것이다. 나는 프로그래밍 잘 하려고 타입을 썼을 뿐인데 어느새 수학의 근본에 가깝게 와 있다는 점이 재밌다.
내가 관심 있는 논리학은 수리 논리학이다. 그 중에서도 타입 이론과 증명 언어를 공부하고 있다.
수학하는 놈들
수학적인 얘기를 하기 전에 우선, 주제에서 약간 벗어나서, 프로그래머와 수학의 관계에 대해 먼저 말하고 싶다. 요즘 여러 종류의 사람들이 완전히 다른 관점에서 "프로그래머의 역량"을 정의하곤 하는데, 그 중에서 자주 포함되는 역량이 수학이더라.
그래서 비전공자 분들은 수학적인 걸 경험해 본 적이 없다고 FOMO를 가지시기도 하는 것 같다.
나는 수학으로 게이트키핑을 하고 싶은 생각이 전혀 없다. 그리고 한국에 있는 컴퓨터학과들 중에 수학과 그렇게 친한 곳이 별로 없어 보인다. 웹상에 나오는 컴퓨터학과에 대한 이미지는 매우 과장되어 있다.
컴퓨터공학과는 슬프게도 수학과가 아니다. 물론 딥러닝처럼 누가 봐도 특정 수학이 필요할 것 같은 과목은 수학 문제가 나오지만, 그런 과목들을 모두 피해도 프로그래밍을 하는 데 문제가 없다. 모든 것은 과목 선택에 달린 것이다.
결론적으로, 나는 모든 프로그래머가 본인이 즐거운만큼만 수학을 하면 된다고 생각한다. 그렇다면 재밌는 수학을 하는 게 중요하므로, 정말 재밌는 수학 갈래 하나를 소개하고자 한다.
왜 논리학인가?
"근본"에 집착하는 이들이 있다. 라이브러리를 그냥 조립해서 프로그램을 만드는 것에는 만족하지 못하고, 무한히 그 구현을 파고들어 CPU 속 회로의 전압 변화까지 이해해야 직성이 풀리는 사람들이다.
나도 어릴 적부터 그 일원이었다. 밑바닥에 있는 단일한 원리를 알고 싶었다. 컴퓨터를 공부할 때는 NAND 게이트의 범용성만 알면 되는 거였고, 과학을 공부할 때는 양자 역학과 상대성 이론만 궁금하고 나머지는 통계적 사족에 불과하다 생각했다.
그러면 수학의 근본은 어디에 있는가? 우리가 배우는 모든 개념과 증명 아래에, 어떤 부정할 수 없는 토대가 존재할 터이다. 19세기부터 수학자들이 수학의 토대를 다지기 위해 노력한 결과, 지금은 수학을 나름 단순하고 근본적인 토대 위에 세우는 방법이 알려져 있다. 문제는, 수학자들이 쓰는 토대가 하나가 아니라는 점이다.
현재까지 가장 널리 쓰이는 토대는 집합론이다. 고등학교에서 "집합과 명제"라는 단원으로 묶어서 다루는 것에서 알 수 있듯, 집합은 논리적으로 상당히 근본에 가까운 대상이다.
집합은 다른 대상과의 관계가 "포함한다"와 "포함하지 않는다" 두 가지의 경우밖에 없으므로 조건을 나타내는 데 적합하다. 또한, 집합은 그 속에 다른 집합을 포함할 수 있다는 점에서 단순한 "모임"과 구별된다. 집합 속에 집합 속에 집합 속에 집합을 넣을 수 있는 재귀적인 구조 덕에, 온갖 복잡한 수학적 대상을 집합의 형태로 나타낼 수 있게 되었다.
그러나 집합론보다, 프로그래머에게 더 흥미를 돋구는 도구가 있다. 직관적 타입 이론이다.
직관적 타입 이론은 "타입과 명제가 일대일 대응된다"는 사상(커리-하워드 대응)과 의존적 타입 시스템을 바탕으로 수학의 토대를 쌓은 것이다.
여기서 타입 시스템은 우리가 아는 그 타입 시스템이 맞다. 타입 시스템이 어떻게 수학의 토대가 될 수 있는지 알아보자. 위에서 말한 "타입과 명제가 일대일 대응된다"는 것을 실제로 보이는 것이다.
먼저, "a의 타입이 A다"라는 말은 "a는 A에 대한 증명이다"라는 말과 동등하다. 즉, 우리는 증명을 값으로, 명제를 타입으로 본다. 그리고, 명제에 대한 연산을 타입에 대한 연산으로 바꿔 말하기만 할 수 있으면 된다.
"A 그리고 B"의 증명은 무엇일까? A의 증명과 B의 증명이 둘 다 있으면 "A 그리고 B"를 증명할 수 있다. 따라서 순서쌍 타입 Pair<A, B>는 "A 그리고 B"에 대한 증명을 담는다. 줄여 말하면, "A 그리고 B"는 Pair<A, B>다.
같은 원리로 "A 또는 B"는 A의 증명이나 B의 증명 중 하나를 요구하므로 Either<A, B>다. "A이면 B"는 A의 증명으로부터 B의 증명을 만들어내면 되므로 함수 타입 A -> B에 해당한다.
이런 방식으로 모든 명제를 타입으로 표현할 수 있고, 그 타입에 속하는 값(증명)을 하나라도 찾아낼 수 있다면 우리는 증명에 성공한 것이 된다. 그리고 그 증명이 맞는지 검증하는 것은 타입 체커를 돌려서 오류가 나는지만 보면 된다.
이런 방식은 컴퓨터를 이용한 증명 검증에 적합했기 때문에, 직관적 타입 이론을 바탕으로 Coq, Agda, Lean과 같은 증명 언어들이 나오게 되었다. 이 언어들은 프로그래밍 언어로도 사용 가능하지만, 수학 명제를 증명하는 데에도 쓸 수 있다는 중요한 가치가 있다. 또, 프로그램을 만들면서 그 프로그램에 버그가 없는지 증명해 버릴 수도 있다!
이렇게 타입 이론에 익숙해지고 나니, 집합론이 너무 하이레벨 프레임워크로 느껴진다. 물론 집합론을 바탕으로 타입 이론을 인코드(구현)할 수도 있고 그 반대도 가능하니 필연적인 것은 아니기는 하지만, 집합론은 기저에 깔린 논리와 층위가 너무 구분되어 상대적으로 본질적이지 못하게 느껴진다.
그리고 나는 프로그래밍 잘 하려고 타입을 썼을 뿐인데 어느새 수학의 근본에 가깝게 와 있다는 점이 재밌다.
타입 이론 친구들
직관적 타입 이론 자체는 잘 정립된 개념이지만, 이 안에서도 여러 가지 변주가 있다. 이론적 타입 이론만으로 증명을 써내기에는 편의 기능이 부족하기 때문으로 이해하고 있다.
가장 어려운 부분은 identity type이다. "a와 b가 같다"라는 명제는 수학에서 매우 유용하고, 수학적으로 매우 다양한 방식으로 정의되어 사용된다. 그런데 이 모든 용례를 편리하게 지원할 수 있는 시스템을 만들 수 있는가? 어디까지 지원했을 때 가장 바람직한 성질들이 도출되는가? 이런 점에서 Coq, Lean, Agda, HoTT 등 시스템들이 서로 차이를 보인다.
아직 지식이 부족하여 어떤 차이가 본질적이고 어떤 차이가 부수적인지 제대로 구별하지 못하고 있는데, 그래도 읽을수록 약간씩 개념들의 지도가 선명해지고 있다는 느낌이 든다.
지금 노력하고 있는 부분은 Coq과 Lean의 타입 시스템 차이를 이해하는 것이다. 나 같은 프로그래머에게 언어 선택은 매우 중요한 문제다. 제대로 알고 선택해야 종교 전쟁에 참전할 수 있으므로, Lean의 몫 타입 문제(링크)를 비롯하여 여러 가지를 공부하고 있다.
한편, 타입 이론을 공부한다고 하여도 정확히 타입 이론만 공부할 수는 없는 것 같다. 우선 타입 이론 기반 시스템은 카테고리와 양면성을 가지고 있어, 카테고리 이론의 관점에서 보았을 때 더 이해가 잘 되는 경우가 있다. 또, 다른 논리계도 배워야 타입 이론과 비교도 하고 러스트의 linear type 같은 것들을 이해할 수 있다.
공부 자료들
타입 이론을 위주로 논리학을 공부하고자 하는 프로그래머라면 다음과 같은 자료를 보면 도움이 될 것이다.
- 학부 수준 이산 수학 (선택)
- 보통 대학 1학년 전공필수 과목으로 배우게 되는데, 불 대수부터 lattice 같은 기초적인 대수 구조까지 교양으로 알고 있으면 좋다. 어려운 내용들은 아니라 어차피 필요할 때 잘 배우게 될 것이기는 하다.
- 기초 알고리즘, 확률론 등등은 논리학에는 필요 없다.
- 함수형 프로그래밍 경험 (선택)
- 함수 뒤에 인수를 괄호가 아니라 공백으로 구분해서 전달하는 구문에 익숙해지는 정도면 충분하다. 거기다 algebraic data type 정도.
- 전혀 경험이 없으면 그냥 아래에 있는 Lean documentation 읽으면서 함수형 프로그래밍을 배우자.
- Software Foundations
- 증명 언어인 Coq으로 증명하면서 논리학 및 프로그래밍 언어론을 배울 수 있다.
- 문제가 많고, 답안으로 올바른 택틱을 적어넣으면 "더 이상 목표 없음"을 띄우면서 증명 완료되는 것이 쾌감이 있다. 개발자 친구들한테 한 번씩 영업하면 다들 재밌게 하더라.
- Lean documentation
- Coq보다 모던한 신택스와 개발 환경을 가진 Lean으로 함수형 프로그래밍과 증명을 배울 수 있다.
- vscode와 연동된 개발 환경이 정말 좋다. 개발 환경 설계에 관심이 있다면 경험해 볼만하다.
- The Type Theory of Lean
- Lean의 타입 시스템에 대한 논문이다.
- Homotopy Type Theory
- 수학 이론에 관한 책이므로 난이도가 좀 있지만, 그래도 내용을 시작부터 다루기는 하므로 공부하기에 위키백과나 nLab보다는 좀 더 낫다.
- https://homotopytypetheory.org/book/ (무료)