페르 마르틴뢰프(Per Martin-Löf)

페르 마르틴뢰프는 1942년 스웨덴 스톡홀름에서 태어났습니다. 그는 서로 멀어 보이는 두 곳에 기초⁠(basics)⁠를 놓았습니다. 하나는 '무작위'란 무엇인가라는 확률론의 물음이고, 다른 하나는 증명과 프로그램을 같은 언어로 적는 타입 이론입니다. 두 작업을 잇는 것은 한 가지 태도입니다. 무엇이 있다고 말하려면 그것을 실제로 만들어 보일 수 있어야 한다는 구성주의, 그리고 그 '만들어 보인다'를 계산으로 정확히 하려는 태도입니다.

나이 세 ·

그는 1964–65년 모스크바에서 콜모고로프에게 배웠습니다. 콜모고로프는 막 문자열의 복잡도를 '그 문자열을 출력하는 가장 짧은 프로그램의 길이'로 정의한 참이었습니다(콜모고로프 복잡도⁠, Kolmogorov complexity⁠). 0101…01이 백만 자리 이어지는 문자열은 짧은 프로그램으로 만들 수 있으니 무작위해 보이지 않고, 동전을 던져 얻은 문자열은 대개 그 자체보다 짧게 줄일 수 없습니다. 그러나 무한 수열의 무작위성을 이 방식으로 곧장 정의하려던 시도는 기술적인 난점에 부딪혔습니다. 1966년 마르틴뢰프는 다른 길을 냈습니다. 통계학자가 수열을 의심하는 방식, 곧 '0과 1의 비율이 반반에서 너무 멀다', '특정 무늬가 너무 자주 나온다' 같은 검정을 생각합시다. 공정한 동전을 한없이 던진다는 확률⁠(probability)⁠ 모형에서, 이런 검정은 확률이 0인 사건⁠(event)⁠, 곧 측도 0⁠(measure zero)⁠인 수열들의 모임으로 적을 수 있습니다. 검정에 걸린다는 것은 그 모임에 든다는 뜻입니다. 그는 계산으로 적을 수 있는 모든 검정을 한꺼번에 통과하는 수열을 무작위 수열이라 정의했습니다. 계산으로 적을 수 있는 검정은 셀 수 있을 만큼만 있으므로 그것들을 모두 합쳐도 측도⁠(measure)⁠가 0입니다. 따라서 무작위 수열들의 모임은 확률이 1이고, 이런 뜻에서 거의 모든 수열이 무작위합니다. 또 무작위 수열은 큰 수의 법칙⁠(law of large numbers)⁠ 같은 성질을 저절로 가집니다. 그 법칙을 어기는 수열들을 걸러 내는 것도 계산으로 적을 수 있는 검정이기 때문입니다. 1970년대 초 레오니트 레빈과 클라우스 슈노어는 이 정의가 '알맞게 정의한 복잡도로 재면 앞부분 $n$자리를 $n$비트보다 일정량 넘게 줄일 수 없다'는 복잡도의 정의와 같다는 것을 증명해, 두 길이 한 곳에서 만났습니다.

1970년 스톡홀름 대학에서 박사 학위를 받은 뒤 그는 논리학으로 무게를 옮겼습니다. 하워드가 보인 대로 명제를 타입으로, 증명을 그 타입의 값으로 볼 수 있다면, 수학 전체를 처음부터 이 방식으로 세울 수 있지 않을까요? 1971년의 첫 판은 모든 타입을 담는 타입 하나를 허락했는데, 이듬해 지라르가 그 체계에서 모순을 끌어냈습니다. '모든 집합⁠(set)⁠의 집합'이 러셀의 역설⁠(Russell's paradox)⁠을 낳는 것과 닮은 이치로, 정확히는 '모든 서수⁠(ordinal)⁠의 모임'에 관한 부랄리포르티의 역설을 타입으로 옮긴 논증이었습니다. 마르틴뢰프는 타입들의 모임인 우주를 $U_0 : U_1 : U_2 : \cdots$처럼 층으로 쌓아 어떤 우주도 자기 자신을 담지 않게 한 술어적인 판으로 고쳤고, 1973년 브리스틀 논리학 대회에서 발표했습니다.

이 이론에서 기본이 되는 말은 '판단'입니다. '$A$는 타입이다', '$a$는 $A$의 원소다($a : A$)', '$a$와 $b$는 $A$의 같은 원소다' 같은 것입니다. 타입을 만드는 방법마다 원소⁠(element)⁠를 만드는 규칙과 쓰는 규칙이 짝을 이룹니다. 핵심은 값에 따라 달라지는 타입, 곧 의존 타입⁠(dependent type)⁠입니다. $\prod_{x : A} B(x)$는 '모든 $x$에 대해 $B(x)$'이고 그 원소는 $x$마다 $B(x)$의 원소를 주는 함수⁠(function)⁠이며, $\sum_{x : A} B(x)$는 '어떤 $x$가 있어 $B(x)$'이고 그 원소는 $x$ 하나와 $B(x)$의 원소 하나의 쌍입니다. 위의 식은 '모든 자연수⁠(natural number)⁠보다 큰 자연수가 있다'인데, 이 명제의 증명은 $n$을 받아 $n + 1$과 '$n \lt n + 1$'의 증명을 돌려주는 함수입니다. 증명을 가진다는 것은 곧 $n$에서 더 큰 수를 실제로 계산하는 프로그램을 가진다는 뜻입니다. '존재한다'를 증명하면 증인을 찾는 방법까지 손에 넣는 것, 이것이 직관주의 논리⁠(intuitionistic logic)⁠의 요구이고 브라우어르가 고집한 구성의 뜻을 계산으로 옮긴 것입니다.

같음도 타입입니다. $a, b : A$에 대해 '$a$와 $b$가 같다'는 명제는 타입 $\mathrm{Id}_A(a, b)$이고, 그 원소를 만드는 기본 방법은 자기 자신과의 같음 $\mathrm{refl}_a : \mathrm{Id}_A(a, a)$뿐입니다. 같음을 쓰는 규칙은 '$\mathrm{refl}$인 경우에 성립하는 것은 모든 같음에 대해 성립한다'는 모양입니다. 이 규칙에서 대칭성과 추이성⁠(transitivity)⁠, 같은 것끼리 바꿔 넣기가 모두 나옵니다. 그런데 이 규칙만으로는 같음의 증명이 둘 이상 있을 수 있는지 결정되지 않는다는 것이 1990년대 호프만과 슈트라이허의 모형으로 드러났고, 이 틈에서 2000년대 보예보츠키의 호모토피 타입 이론⁠(homotopy type theory)⁠이 자랐습니다.

1979년 하노버 강연 「구성적 수학과 컴퓨터 프로그래밍」에서 그는 이 이론이 그 자체로 프로그래밍 언어라고 말했습니다. 타입은 프로그램이 지켜야 할 명세이고, 그 타입의 원소를 만드는 일은 명세를 만족하는 프로그램을 짜는 일이며, 타입 검사가 곧 프로그램이 옳다는 증명의 확인입니다. '정렬되어 있고, 받은 목록을 재배열한 것을 돌려준다'는 성질을 타입에 적어 두면, 타입 검사를 통과한 정렬 함수는 그 명세에 관해서는 틀릴 수 없습니다. 다만 명세가 모자라면 보장도 모자랍니다. '재배열' 조건을 빼면 늘 빈 목록을 돌려주는 함수도 통과합니다. 이 생각은 1980–90년대 코넬의 NuPRL, 예테보리의 ALF를 거쳐 2000년대의 아그다로 거의 그대로 구현되었습니다. 록(옛 이름 Coq)과 린은 티에리 코캉과 제라르 위에의 '구성의 계산⁠(calculus of constructions)⁠'이라는 가까운 친척 이론 위에 서 있습니다(증명 보조기). 1980년 파도바 강의를 묶은 1984년 책 『직관주의 타입 이론』이 이 이론의 표준 문헌입니다.

그는 스톡홀름 대학에서 수학과 철학을 함께 맡은 교수로 2009년 은퇴할 때까지 가르쳤습니다. 논리학의 철학에서도 '명제의 뜻을 안다는 것은 무엇이 그 증명으로 인정되는지를 안다는 것'이라는 입장을 일관되게 다듬었습니다. 1990년 스웨덴 왕립 과학원 회원이 되었고, 2020년 롤프 쇼크상을 받았습니다.

이어지는 곳. 값에 따라 달라지는 타입과 $\Pi$, $\Sigma$의 규칙은 의존 타입에서, 그 뜻의 뿌리인 구성적 증명은 직관주의 논리와 커리–하워드 대응⁠(Curry–Howard correspondence)⁠에서 따라갈 수 있습니다. 같음 타입⁠(identity type)⁠의 새로운 해석은 호모토피 타입 이론과 보예보츠키로, 이론을 실제로 돌리는 도구는 증명 보조기로 이어집니다. 무작위 수열의 정의는 콜모고로프 복잡도, 측도 0, 큰 수의 법칙과 한 그림을 이루고, 우주를 층으로 쌓는 까닭은 러셀의 역설과 타입 이론의 출발점에 있습니다.

관계.

• 스승 안드레이 콜모고로프 — 1964–65년 모스크바에서 콜모고로프에게 배우며, 그가 제안한 복잡도로 무작위성을 정의하는 문제를 이어받았습니다.
• 영향을 받음 L. E. J. 브라우어르 — 증명을 구성으로 보는 브라우어르의 직관주의와, 그것을 다듬은 브라우어르–헤이팅–콜모고로프 해석이 그의 타입 이론이 명제의 뜻을 설명하는 방식의 뿌리입니다.
• 영향을 받음 윌리엄 하워드 — 하워드가 1969년 원고에서 술어 논리⁠(predicate logic)⁠로 넓히며 쓴 의존 타입의 생각을, 수학 전체의 기초로 삼을 수 있는 이론으로 세웠습니다.
• 영향을 받음 장이브 지라르 — 1971년 첫 판은 '모든 타입의 타입'을 허락했는데, 지라르가 그 체계에서 모순을 끌어내자 타입의 우주를 층으로 나눈 술어적 판으로 고쳤습니다.
• 영향을 줌 블라디미르 보예보츠키 — 보예보츠키는 마르틴뢰프 타입 이론의 같음 타입을 공간의 경로로 해석하는 모형을 만들고 일가성 공리⁠(univalence axiom)⁠를 더해 호모토피 타입 이론을 열었습니다.

연표.

• 1964년 모스크바에서 콜모고로프에게 배우다(1964–65)
• 1966년 「무작위 수열의 정의」를 발표하다
• 1968년 시카고 대학 조교수가 되다(1968–69)
• 1970년 스톡홀름 대학에서 박사 학위를 받다
• 1971년 직관주의 타입 이론의 첫 판을 내놓다
• 1972년 첫 판에서 지라르의 역설⁠(Girard's paradox)⁠이 발견되어 술어적인 판으로 고치다
• 1973년 브리스틀 논리학 대회에서 술어적 타입 이론을 발표하다
• 1979년 하노버에서 「구성적 수학과 컴퓨터 프로그래밍」을 발표하다
• 1984년 파도바 강의록 『직관주의 타입 이론』을 펴내다
• 1990년 스웨덴 왕립 과학원 회원이 되다
• 2009년 스톡홀름 대학에서 은퇴하다
• 2020년 롤프 쇼크상(논리학·철학)을 받다