장이브 지라르(Jean-Yves Girard)

장이브 지라르는 1947년 프랑스 리옹에서 태어났습니다. 그가 논리학을 시작한 1960년대 말, 증명 이론에는 큰 숙제가 있었습니다. 괴델은 1958년 자연수⁠(natural number)⁠의 산술이 무모순⁠(consistent)⁠이라는 것을, 자연수에서 자연수로 가는 함수⁠(function)⁠, 그런 함수를 받는 함수 같은 고차 함수들의 단순한 계산 체계(체계 T)로 바꾸어 설명했습니다. 이 '디알렉티카 해석'을, 자연수의 집합⁠(set)⁠까지 다루는 훨씬 강한 2계 산술로 넓힐 수 있을까요? 지라르는 그 답을 찾다가 새로운 프로그래밍 언어 하나를 만들었고, 그것이 오늘날 다형성⁠(polymorphism)⁠ 이론의 표준 모형인 시스템 F입니다.

나이 세 ·

시스템 F는 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠에 '타입을 인자로 받는 함수'를 더한 것입니다. 항등 함수를 생각해 봅시다. 단순 타입 체계에서는 정수⁠(integer)⁠의 항등 함수, 문자열의 항등 함수를 따로 적어야 합니다. 시스템 F에서는 타입 $\alpha$를 먼저 받고 그다음 $\alpha$형의 값을 받아 그대로 돌려주는 함수 하나를 적고, 그 타입을 '모든 타입 $\alpha$에 대해 $\alpha \to \alpha$'로 씁니다(위의 식). 자연수도 함수로 적을 수 있습니다. 수 $n$은 '함수 $f$와 시작값 $x$를 받아 $f$를 $n$번 적용한다'는 함수이고, 그 타입은 $\forall\alpha.\,(\alpha \to \alpha) \to \alpha \to \alpha$입니다. 같은 무렵인 1974년 미국의 존 레이놀즈는 프로그래밍 언어의 관점에서 같은 체계를 독립적으로 만들었습니다(다형성과 시스템 F).

지라르가 1971–72년 증명한 결과는 두 가지입니다. 첫째, 시스템 F에서 타입이 붙은 모든 프로그램은 어떤 순서로 계산해도 반드시 멈춥니다(강정규화⁠, strong normalization⁠). 증명을 위해 그는 타입마다 '잘 멈추는 프로그램들의 후보 모임'을 정하고, 모든 가능한 후보에 대해 한꺼번에 성질을 보이는 '환원 가능성 후보⁠(reducibility candidates)⁠'의 방법을 만들었습니다. 이 방법은 오늘날에도 정규화 증명의 표준 도구입니다. 둘째, 시스템 F로 짤 수 있는 자연수 함수는 정확히 2계 산술이 전체 함수임을 증명할 수 있는 함수들입니다. 재귀⁠(recursion)⁠로 정의되는 아커만 함수는 물론, 그보다 훨씬 빨리 자라는 함수들도 여기 들어 있습니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 보면, 시스템 F의 타입은 2계 명제 논리⁠(propositional logic)⁠의 명제이고, 모든 프로그램이 멈춘다는 정리는 그 논리의 모든 증명을 돌아가는 길 없이 정리할 수 있다는 정리입니다. 그의 증명은 고차 논리의 절단 제거⁠(cut elimination)⁠에 관한 다케우티 가이시의 추측을 새로 증명하는 일이기도 했습니다.

모든 프로그램이 멈춘다는 것은 대가가 있습니다. 시스템 F는 튜링 기계⁠(Turing machine)⁠가 하는 모든 계산을 할 수는 없습니다. 예를 들어 프로그램을 수로 부호화해 받아 그 프로그램을 돌린 값을 내는 보편 함수 $U(n, m)$는 시스템 F 안에서 짤 수 없습니다. 짤 수 있다면 $d(n) = U(n, n) + 1$도 시스템 F의 프로그램이고, 그 부호를 $k$라 하면 $d(k) = U(k, k) + 1 = d(k) + 1$이 되어 모순이기 때문입니다. 대각선 논법⁠(diagonal argument)⁠ 그대로입니다. 같은 논증은 프로그램을 기계적으로 나열할 수 있고 모든 프로그램이 멈추는 언어라면 어디에나 통합니다. 이 맞바꿈, 곧 그런 언어는 자기 자신의 해석기를 담을 수 없고 멈추는 계산 가운데서도 빠뜨리는 것이 생긴다는 사실은 정지 문제⁠(halting problem)⁠의 또 다른 얼굴이고, 오늘날의 증명 보조기⁠(proof assistant)⁠가 멈춤을 보장하는 언어를 쓰는 까닭이기도 합니다.

1972년 그는 또 하나의 부정적인 결과를 냈습니다. 마르틴뢰프의 1971년 타입 이론⁠(type theory)⁠처럼 '모든 타입의 타입' $\mathsf{Type} : \mathsf{Type}$을 허락하면 모순이 생긴다는 것입니다. '모든 서수⁠(ordinal)⁠의 모임'이 서수가 될 수 없다는 부랄리포르티의 역설을 타입으로 옮긴 논증으로, 이 결과 때문에 증명 보조기의 바탕이 되는 오늘날의 타입 이론들은 대부분 우주를 층으로 쌓습니다.

1987년 그는 선형 논리를 발표했습니다. 보통의 논리에서 가정은 몇 번이든 쓸 수 있고, 쓰지 않고 버려도 됩니다. '$A$이면 $A$이고 $A$'가 늘 참인 까닭입니다. 선형 논리는 이 두 규칙(복제와 버리기)을 막고, 가정을 딱 한 번씩 쓰는 자원처럼 다룹니다. $A \multimap B$는 '$A$ 하나를 써서 $B$ 하나를 얻는다'입니다. 그러면 보통의 '그리고'가 둘로 갈라집니다. 커피 한 잔 값의 동전 $A$로 커피 $B$와 차 $C$ 가운데 내가 고른 하나를 살 수 있다면 $A \multimap B \,\&\, C$이고, 자판기가 무엇을 줄지 정한다면 $A \multimap B \oplus C$입니다. 둘 다 받는 $A \multimap B \otimes C$는 동전 하나로는 성립하지 않습니다. 몇 번이든 써도 되는 가정은 따로 $!A$로 표시해, 보통의 논리를 선형 논리 안에 다시 담을 수 있습니다. 이 구분은 계산에서 자원의 흐름을 정확히 적는 도구가 되었고, 값을 한 번만 쓰도록 강제하는 오늘날 언어들의 타입 체계(러스트의 소유권이 대표적인 예입니다)가 같은 계열의 생각에 기대고 있습니다. 가정을 두 번 쓰지 못하게 하면 커리의 역설도 성립하지 않습니다.

그 뒤에도 그는 증명을 도형으로 그리는 증명망⁠(proof net)⁠, 증명의 계산을 연산자⁠(operator)⁠의 대수로 옮긴 상호작용의 기하학(1989), 증명과 반박의 상호작용에서 논리를 다시 세우려는 루딕스(2001)를 내놓았습니다. 1989년 이브 라퐁, 폴 테일러와 함께 쓴 『증명과 타입』은 시스템 F와 정규화를 배우는 표준 교과서이고, 2006–07년의 강의록 『맹점』은 그의 논리관을 거침없는 문체로 담았습니다. 그는 오랫동안 CNRS의 연구 책임자로 마르세유 뤼미니의 수학 연구소에서 일했고, 1983년 CNRS 은메달, 1990년 퐁슬레상을 받았으며 프랑스 과학 아카데미 회원입니다.

이어지는 곳. 타입을 인자로 받는 함수와 그 타입 규칙은 다형성과 시스템 F에서, 그 바탕이 되는 체계는 단순 타입 람다 계산과 람다 계산에서 볼 수 있습니다. 모든 증명이 정리된다는 정리와 모든 프로그램이 멈춘다는 정리가 같은 말인 까닭은 커리–하워드 대응에, 모든 것이 멈추는 언어의 한계는 정지 문제와 대각선 논법에 있습니다. 타입 추론⁠(type inference)⁠이 가능한 범위를 시스템 F보다 좁혀 자동화한 것이 힌들리–밀너 타입 추론이고, 우주를 층으로 쌓는 까닭은 러셀의 역설⁠(Russell's paradox)⁠과 마르틴뢰프의 페이지에 있습니다.

관계.

• 영향을 받음 쿠르트 괴델 — 괴델이 1958년 산술의 무모순성⁠(consistency)⁠을 고차 함수의 계산 체계 T로 해석한 디알렉티카 해석을 2계 산술로 넓히려다 시스템 F를 만들었습니다.
• 영향을 줌 페르 마르틴뢰프 — 마르틴뢰프의 1971년 타입 이론 첫 판에서 모순을 끌어내, 우주를 층으로 나눈 술어적인 판이 나오게 했습니다.

연표.

• 1971년 괴델의 해석을 2계 산술로 넓히는 논문에서 시스템 F를 내놓다
• 1972년 국가 박사 논문을 내고, '모든 타입의 타입'에서 모순을 끌어내다
• 1983년 국립 과학 연구원(CNRS) 은메달을 받다
• 1987년 선형 논리를 발표하다
• 1989년 라퐁, 테일러와 『증명과 타입』을 펴내고, 상호작용의 기하학을 내놓다
• 1990년 프랑스 과학 아카데미의 퐁슬레상을 받다
• 2001년 루딕스를 발표하다
• 2007년 논리학 강의 『맹점』을 완간하다