로빈 밀너(Robin Milner)

로빈 밀너는 1934년 영국 데번주 얠럼턴에서 태어났습니다. 이튼 칼리지와 케임브리지 킹스 칼리지에서 수학과 철학을 공부한 그는 박사 학위를 받지 않았습니다. 학교 교사와 페란티 사의 프로그래머를 거쳐 1968년 스완지 대학에서 연구를 시작했을 때, 그의 물음은 프로그램이 옳다는 것을 어떻게 믿을 수 있는가였습니다. 사람이 짠 프로그램은 틀리고, 사람이 쓴 증명도 틀립니다. 밀너는 기계가 증명을 확인하게 하는 도구, 틀린 프로그램을 돌리기 전에 걸러 내는 타입 체계, 동시에 돌아가는 프로그램들을 다루는 수학을 차례로 만들었고, 1991년 이 세 가지 업적으로 튜링상⁠(Turing Award)⁠을 받았습니다.

나이 세 ·

1971–73년 매카시가 세운 스탠퍼드 인공지능⁠(artificial intelligence)⁠ 연구소에서 그는 데이나 스콧의 '계산 가능한 함수⁠(function)⁠의 논리'로 프로그램의 성질을 증명하는 도구 LCF를 만들었고, 1973년 에든버러 대학으로 옮겨 그것을 다시 설계했습니다. 에든버러 LCF의 발상은 단순하고 강력합니다. 정리를 나타내는 값의 타입 thm을 따로 두되, 그 타입의 값을 만드는 방법은 논리의 추론 규칙에 해당하는 몇 개의 함수뿐이게 합니다. 사용자는 증명을 찾는 전략을 마음껏 프로그램으로 짤 수 있지만, 어떤 전략을 짜든 thm형의 값은 추론 규칙을 거쳐서만 나오므로 틀린 정리가 만들어질 수 없습니다. 믿어야 할 것은 작은 핵심 부분뿐입니다. 이 설계는 오늘날 HOL, 이자벨 같은 증명 보조기의 기본 원리가 되었습니다. 그 전략을 짜는 언어로 만든 것이 메타 언어, 곧 ML이었습니다.

ML은 처치의 람다 계산⁠(lambda calculus)⁠에 타입을 붙인 언어인데, 프로그래머가 타입을 적지 않아도 컴파일러⁠(compiler)⁠가 알아서 찾아 줍니다. 목록의 모든 원소⁠(element)⁠에 함수를 적용하는 map을 보겠습니다. map f [] = [], map f (x :: xs) = f x :: map f xs라고만 적으면, 컴파일러는 이렇게 추론합니다. 둘째 인자는 목록 모양으로 쪼개지므로 어떤 타입 $d$에 대해 $d\ \mathrm{list}$이고 x는 $d$형입니다. f x라고 썼으니 f는 $d$를 받는 함수이고, 돌려주는 타입을 $e$라 하면 $f : d \to e$입니다. 결과는 f x를 앞에 붙인 목록이므로 $e\ \mathrm{list}$입니다. 재귀⁠(recursion)⁠ 호출 map f xs도 같은 타입이어야 하는데 모순이 없습니다. $d$와 $e$에는 아무 제약도 걸리지 않았으므로, 답은 위의 식처럼 모든 $\alpha$, $\beta$에 대한 타입입니다. 모르는 타입마다 변수를 두고, 쓰임새에서 나온 등식들을 1965년 앨런 로빈슨의 단일화⁠(unification)⁠ 알고리즘⁠(algorithm)⁠으로 푸는 것이 1978년 논문의 알고리즘 W입니다.

이 알고리즘이 찾는 타입은 '주 타입⁠(principal type)⁠'입니다. 그 프로그램에 붙일 수 있는 다른 모든 타입이 주 타입의 변수에 무언가를 넣어 얻어진다는 뜻입니다. 1969년 로저 힌들리가 조합 논리⁠(combinatory logic)⁠에서 같은 결과를 먼저 얻었습니다. 1982년 밀너는 루이스 다마스와 함께, let이 들어간 언어에서도 알고리즘 W가 언제나 주 타입을 찾는다는 정리를 발표했습니다(자세한 증명은 1985년 다마스의 박사 논문에 실렸습니다). 그래서 이 체계를 힌들리–밀너 타입 추론⁠(type inference)⁠이라 부릅니다. 1978년 논문에는 오래 인용되는 문장도 있습니다. "타입이 잘 맞는 프로그램은 잘못될 수 없다." 정확히는, 타입 검사를 통과한 프로그램이 돌다가 정수⁠(integer)⁠에 함수를 적용하는 식의 타입 오류를 일으키는 일은 없다는 정리입니다. 무한히 도는 일이나 0으로 나누는 일까지 막아 주는 것은 아닙니다.

힌들리–밀너 체계의 절묘함은 어디까지를 자동으로 할지 고른 데 있습니다. let id = fn x => x in (id 3, id true)에서 id는 정수에도 참거짓 값에도 쓰이는데, let으로 이름 붙인 값은 타입을 일반화해 두기 때문에 괜찮습니다. 그러나 같은 id를 함수의 인자로 받아 두 가지 타입에 쓰는 것은 허락되지 않습니다. 그것까지 허락하면 지라르의 시스템 F⁠(System F)⁠가 되는데, 시스템 F에서는 타입 추론이 결정 불가능하다는 것이 1990년대에 증명되었습니다(다형성⁠(polymorphism)⁠과 시스템 F). 한편 힌들리–밀너의 추론도 최악의 경우에는 프로그램 길이에 대해 지수 시간이 걸린다는 것이 1990년 증명되었지만, 사람이 실제로 쓰는 프로그램에서는 거의 선형 시간에 끝납니다. 이론의 최악과 실제의 보통이 크게 다른 예입니다. ML의 이 설계는 OCaml, 하스켈, F#으로 이어졌고, 러스트와 스위프트의 타입 추론에도 영향을 주었습니다.

1970년대 후반 그의 관심은 동시에 돌아가며 서로 메시지를 주고받는 프로그램들로 옮겨 갔습니다. 1980년 책 『통신하는 시스템의 계산(CCS)』은 프로세스를 대수식으로 적습니다. $a.P$는 '$a$를 한 뒤 $P$처럼 움직인다', $P + Q$는 '$P$나 $Q$ 가운데 하나로 움직인다'입니다. 핵심 물음은 두 프로세스가 언제 같은가입니다. 자판기 두 대를 생각합시다. 첫째 $a.(b + c)$는 동전을 넣으면($a$) 커피($b$)와 차($c$) 단추가 둘 다 켜집니다. 둘째 $a.b + a.c$는 동전을 넣는 순간 기계가 몰래 한쪽을 골라, 커피 단추만 켜지거나 차 단추만 켜집니다. 일어날 수 있는 동작의 순서(ab 또는 ac)는 똑같지만 둘째 기계 앞의 손님은 원하는 것을 못 얻을 수 있습니다. 데이비드 파크가 1981년 정식화하고 밀너가 CCS의 중심에 놓은 '쌍모의(bisimulation)'는 한쪽이 하는 모든 동작을 다른 쪽이 따라 하고, 그 뒤의 상태들도 계속 그러하다는 관계이고, 이 기준으로 두 기계는 다릅니다. 같은 시기 호어는 CSP라는 다른 대수를 만들었고, 두 이론은 서로 자극하며 자랐습니다. 1992년 요아힘 패로, 데이비드 워커와 발표한 π 계산은 통신 채널의 이름 자체를 메시지로 주고받게 해, 연결 구조가 바뀌는 시스템까지 적을 수 있게 했습니다.

그는 1986년 에든버러에 컴퓨터 과학 기초⁠(basics)⁠ 연구소(LFCS)를 함께 세웠고, 1990년 매즈 토프테, 로버트 하퍼와 함께 언어 전체의 뜻을 수학적으로 정의한 『스탠더드 ML의 정의』를 펴냈습니다. 1995년 케임브리지 대학으로 옮겨 컴퓨터 연구소를 이끌었고, 말년에는 곳곳에 퍼진 컴퓨터와 장치들의 연결과 위치를 함께 적는 '바이그래프' 이론을 연구했습니다. 1988년 영국 왕립학회 회원이 되었고, 2010년 케임브리지에서 세상을 떠났습니다.

이어지는 곳. 모르는 타입을 변수로 두고 등식을 푸는 과정은 타입 추론: 힌들리–밀너에서 한 걸음씩 따라가 볼 수 있고, 그 바탕의 체계는 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠입니다. let의 일반화가 어디서 멈추는지는 다형성과 시스템 F와 지라르에서, 목록과 트리⁠(tree)⁠ 같은 타입을 짜는 방법은 대수적 자료형⁠(algebraic data type)⁠에서 볼 수 있습니다. LCF의 설계를 이어받은 도구들은 증명 보조기에 있습니다. 두 자판기를 유한 오토마톤⁠(finite automaton)⁠으로 보면 받아들이는 동작 순서가 같아 구별되지 않는데, 쌍모의가 오토마톤⁠(automaton)⁠의 같음보다 더 섬세한 기준인 까닭이 여기 있습니다. 동시성의 다른 대수를 만든 사람은 호어입니다.

관계.

• 영향을 받음 알론조 처치 — ML의 뼈대는 처치의 타입 붙은 람다 계산이고, 밀너의 타입 추론은 그 위에 '타입을 적지 않아도 찾아 주는' 층을 얹은 것입니다.
• 영향을 받음 존 매카시 — 1971–73년 매카시가 세운 스탠퍼드 인공지능 연구소에서 일하며 프로그램의 성질을 기계로 증명하는 도구 LCF를 처음 만들었습니다.

연표.

• 1957년 케임브리지 킹스 칼리지를 졸업하다
• 1968년 스완지 대학에서 프로그램 검증을 연구하기 시작하다
• 1971년 스탠퍼드 인공지능 연구소에서 증명 도구 LCF를 만들다
• 1973년 에든버러 대학으로 옮겨 에든버러 LCF와 그 메타 언어 ML을 만들다
• 1978년 「프로그래밍에서 타입 다형성의 이론」을 발표하다
• 1980년 『통신하는 시스템의 계산(CCS)』을 펴내다
• 1982년 다마스와 주 타입 스킴의 정리를 발표하다
• 1986년 에든버러에 컴퓨터 과학 기초 연구소(LFCS)를 함께 세우다
• 1988년 영국 왕립학회 회원이 되다
• 1990년 토프테, 하퍼와 『스탠더드 ML의 정의』를 펴내다
• 1991년 튜링상을 받다
• 1992년 패로, 워커와 π 계산을 발표하다
• 1995년 케임브리지 대학으로 옮겨 컴퓨터 연구소를 이끌다