수학 개념 지도
인물

토니 호어(Tony Hoare)

퀵정렬⁠(quicksort)⁠을 고안하고, 프로그램이 옳다는 것을 논리로 증명하는 호어 논리⁠(Hoare logic)⁠와 병행 프로세스의 수학을 세운 영국 컴퓨터 과학자.

{P}  C  {Q},{Q[E/x]}  x:=E  {Q}\{P\}\; C\; \{Q\}, \qquad \{Q[E/x]\}\; x := E\; \{Q\}

토니 호어(찰스 앤터니 리처드 호어)는 1934년 실론, 지금의 스리랑카의 콜롬보에서 영국인 부모에게서 태어났습니다. 옥스퍼드에서 고전학과 철학을 공부했고, 해군에서 복무하며 러시아어를 배웠습니다. 1959년 가을 스물다섯 살의 그는 영국 문화원의 교환 학생으로 모스크바 대학에 가서 콜모고로프가 이끌던 모스크바 학파에서 확률론을 공부했습니다. 냉전 속에서 미국과 소련은 서로의 과학 문헌을 기계로 읽으려 경쟁하고 있었고, 그도 러시아어를 영어로 옮기는 기계 번역⁠(machine translation)⁠에 손을 댔습니다. 컴퓨터 과학이라는 분야는 아직 이름도 없던 때였습니다.

굵은 막대가 이 사람의 생애이고, 흰검은 점은 페이지 끝 연표에 적은 일들입니다. 가는 막대는 같은 시대를 산 이 위키의 인물들입니다. 나이를 끌어 보세요.

나이 세 ·

기계 번역은 냉전이 낳은 연구였습니다. 1954년 1월 조지타운 대학과 IBM은 러시아어 문장 60여 개를 영어로 옮기는 시연을 해 몇 년 안에 기계 번역이 해결되리라는 기대를 불러일으켰고, 1957년 스푸트니크 뒤에는 소련의 과학 논문을 빨리 읽어야 한다는 압박이 커졌습니다. 소련 쪽도 외국어 문헌을 러시아어로 옮기는 연구를 서둘렀습니다. 호어가 머문 모스크바 대학의 수학과는 콜모고로프를 중심으로 확률론과 정보 이론과 계산의 이론을 한데 다루던 곳이었고, 그는 이곳에서 얻은 정렬의 착상을 품고 1960년 영국으로 돌아왔습니다.

사전은 자기 테이프⁠(magnetic tape)⁠에 알파벳 순서로 들어 있었고 테이프는 앞에서부터 차례로만 읽을 수 있었으니, 문장의 낱말을 먼저 정렬해 두면 테이프를 한 번만 훑으며 모두 찾을 수 있었습니다. 그가 떠올린 방법은 낱말 하나를 기준(피벗⁠, pivot⁠)으로 골라 그보다 앞서는 것은 왼쪽, 뒤에 오는 것은 오른쪽으로 가르고, 양쪽을 같은 방법으로 정렬하는 것이었습니다(분할 정복⁠(divide and conquer)⁠). 이듬해 런던의 컴퓨터 회사 엘리엇 브라더스에 들어간 그는 멀리 떨어진 원소끼리 먼저 비교해 옮기는 삽입 정렬⁠(insertion sort)⁠의 변형인 셸 정렬⁠(Shellsort)⁠을 구현하라는 일을 받고, 대개는 그보다 빠른 방법을 안다고 말했다가 상사가 건 6펜스 내기에서 이겼다고 회고했습니다. 다만 자기 자신을 부르는 프로시저를 허용한 알골 60을 배우고서야 방법을 깔끔하게 적을 수 있었습니다(재귀⁠(recursion)⁠). 1961년 『ACM 통신』에 실린 「알고리즘⁠(algorithm)⁠ 64: 퀵정렬」은 몇 줄짜리 프로그램이었고, 같은 호에 k번째로 작은 원소⁠(element)⁠를 찾는 짝 「알고리즘 65: 찾기」도 실렸습니다(중앙값⁠(median)⁠).

퀵정렬의 운은 피벗에 달려 있습니다. 매번 가장 작은 원소를 피벗으로 고르면 한 번 가를 때마다 하나씩만 줄어 비교가 n(n−1)/2n(n-1)/2번 듭니다. 그러나 피벗을 무작위로 고르면 어떤 입력에서든 평균⁠(mean)⁠ 비교 횟수가 약 2nln⁡n≈1.39 nlog⁡2n2n\ln n \approx 1.39\,n\log_2 n입니다. i번째와 j번째로 작은 두 원소가 비교되는 것은 그 사이 값의 원소들 가운데 둘 중 하나가 가장 먼저 피벗으로 뽑힐 때뿐이라 그 확률⁠(probability)⁠이 2/(j−i+1)2/(j-i+1)이고, 이것을 모두 더하는 기댓값⁠(expected value)⁠의 선형성이 조화급수⁠(harmonic series)⁠를 낳습니다. 어떤 비교 정렬⁠(comparison sort)⁠도 log⁡2n!\log_2 n!번보다 적게 비교할 수는 없으니(비교 정렬의 하한⁠, comparison sorting lower bound⁠) 그 40% 가까이 위에 있는 셈이지만, 원소를 옮기는 일이 적고 따로 공간이 거의 필요 없어 실제로는 흔히 가장 빠릅니다. 운을 자료가 아니라 알고리즘 안에 두는 무작위 알고리즘⁠(randomized algorithm)⁠의 대표적인 예입니다(무작위성).

엘리엇 브라더스에서 그는 곧 엘리엇 803 컴퓨터의 알골 60 컴파일러⁠(compiler)⁠를 만드는 팀을 이끌었고, 1962년 그 팀의 동료 질 핌과 결혼했습니다. 1963년 완성된 컴파일러는 좋은 평을 받았지만, 뒤이어 맡은 더 야심 찬 운영 체제와 소프트웨어 계획은 약속한 기능을 끝내 내지 못하고 무너졌습니다. 그는 1980년 튜링상⁠(Turing Award)⁠ 강연에서 이 실패를 숨기지 않고 들려주며, 복잡함을 다스리지 못한 설계가 어떻게 무너지는지를 교훈으로 삼았습니다. 1965년에는 스위스의 컴퓨터 과학자 니클라우스 비르트와 함께 알골의 후계 언어를 제안했지만 국제 위원회가 훨씬 복잡한 알골 68을 택하자, 두 사람의 제안은 알골 W라는 이름으로 따로 구현되었습니다. 이 경험이 1968년 데이크스트라 등과 함께 알골 68에 반대하는 소수⁠(prime number)⁠ 의견서에 서명한 배경입니다.

1968년 벨파스트의 퀸스 대학 교수가 된 그는 이듬해 「컴퓨터 프로그래밍의 공리적 기초⁠(basics)⁠」를 발표했습니다. 출발점은 1967년 로버트 플로이드가 순서도의 화살표마다 조건을 붙여 프로그램의 뜻을 정한 논문이었습니다. 호어는 프로그램 조각 C를 실행하기 전에 조건 P가 참이면 실행한 뒤에 조건 Q가 참이라는 주장을 {P} C {Q}\{P\}\,C\,\{Q\}로 적고, 대입문, 순서, 조건문, 반복문마다 이런 주장을 이어 붙이는 추론 규칙을 주었습니다. 핵심은 반복문의 규칙입니다. 반복 조건이 참일 때 한 번 돌고 나서도 참으로 남는 불변식 I를 찾으면, 반복이 끝났을 때 I와 '반복 조건이 거짓'이 함께 성립합니다. 다만 이 규칙은 끝났다면 무엇이 참인지를 말할 뿐이어서, 반복이 언젠가 끝난다는 것은 줄어드는 양을 찾아 따로 보여야 합니다. 수학적 귀납법⁠(mathematical induction)⁠을 프로그램에 옮긴 것이고, 변하는 것 속에서 변하지 않는 것을 찾는 수학의 오랜 방법이기도 합니다(대칭과 불변량⁠(invariant)⁠). 1부터 n까지 더하는 반복문이라면 "s는 1부터 i까지의 합"이 불변식이고, i가 n에 이르러 멈추면 s가 답임을 증명할 수 있습니다. 이 '호어 논리'는 오늘날 프로그램을 기계로 검증하는 도구들의 뿌리가 되었습니다.

1974년 그는 모니터라는 개념을 정리했습니다. 공유 자료와 그것을 다루는 프로시저를 한 덩어리로 묶고, 한 번에 한 프로세스만 그 안에 들어가게 하는 구조입니다. 덴마크의 페르 브린치 한센과 함께 다듬은 이 생각은 데이크스트라의 신호 장치인 세마포어⁠(semaphore)⁠를 프로그램 여기저기에 흩뿌리는 대신 병행 프로그램을 구조적으로 짜게 해 주었고, 오늘날 자바의 동기화 같은 곳에 남아 있습니다. 1977년 그는 1975년 세상을 떠난 크리스토퍼 스트레이치의 뒤를 이어 옥스퍼드 프로그래밍 연구 그룹을 맡았고, 이곳은 프로그램의 뜻을 수학으로 정하는 형식 의미론과 형식 명세 연구의 중심이 되었습니다.

옥스퍼드로 옮긴 이듬해 그는 「통신하는 순차 프로세스」(CSP)에서, 따로 도는 프로세스들이 기억 장치를 함께 건드리는 대신 통로로 메시지를 주고받으며 서로 박자를 맞추는 방식을 수학으로 다루었습니다. 데이크스트라의 세마포어가 연 병행 프로그래밍의 문제를 대수로 옮긴 이 이론은 오캄 언어와 트랜스퓨터 칩을 거쳐 오늘날 Go 언어의 채널에까지 이어졌습니다. 1980년 튜링상 수상 강연 「황제의 낡은 옷」에서 그는, 소프트웨어를 설계하는 방법은 너무 단순해서 결함이 없는 것이 분명하게 만드는 것과 너무 복잡해서 분명한 결함이 없게 만드는 것 두 가지뿐이라고 말했습니다. 2009년에는 1965년 알골 W를 설계하며 아무것도 가리키지 않는 참조값, 곧 '빈 참조'(null)를 넣은 일을 두고 스스로 수십억 달러짜리 실수라 불렀습니다.

그의 이론은 산업으로도 건너갔습니다. 영국의 반도체 회사 인모스는 CSP를 바탕으로 병렬 처리 언어 오캄과 트랜스퓨터 칩을 만들었고, 옥스퍼드 연구진이 인모스와 함께 형식 방법으로 트랜스퓨터의 부동소수점⁠(floating point)⁠ 장치를 검증한 일은 1990년 영국 여왕상을 받았습니다. 1999년 옥스퍼드에서 은퇴한 뒤에는 마이크로소프트 연구소 케임브리지로 옮겨, 2000년대 초 검증된 소프트웨어를 컴퓨터 과학의 '큰 도전'으로 삼자고 제안했습니다. 호어 논리는 2000년대 초 포인터와 공유 기억 장치를 다루는 분리 논리⁠(separation logic)⁠로 확장되었고, 이 논리를 쓰는 도구들이 지금은 큰 회사들의 코드에서 오류를 자동으로 찾아냅니다.

그는 2000년 기사 작위와 교토상을 받았고, 2026년 3월 세상을 떠났습니다.

이어지는 곳. 정렬된 두 목록을 합치는 병합 정렬⁠(merge sort)⁠은 1945년 폰 노이만이 적었고, 최악에도 nlog⁡nn\log n을 지키는 힙 정렬⁠(heapsort)⁠은 우선순위 큐⁠(priority queue)⁠로 달립니다(정렬 알고리즘⁠(sorting algorithm)⁠, 점근 표기법⁠(asymptotic notation)⁠). 정렬해 둔 목록에서는 이진 탐색⁠(binary search)⁠으로 빨리 찾을 수 있습니다. 모든 프로그램의 옳고 그름을 기계가 스스로 가려낼 수는 없다는 것은 튜링의 정지 문제⁠(halting problem)⁠가 보장하므로, 검증 도구들은 사람이 준 불변식에 기댑니다. 모스크바의 스승 콜모고로프의 이름은 콜모고로프 복잡도⁠(Kolmogorov complexity)⁠에 남아 있습니다.

관계.

가운데가 이 사람, 둘레가 이어진 인물들입니다. 선의 색은 관계의 종류(초록 스승·제자, 파랑 함께 연구, 보라 편지, 빨강 논쟁, 주황 영향)이고, 다른 인물의 페이지에 적힌 관계도 함께 모았습니다.

  • 스승 안드레이 콜모고로프 — 1959–60년 모스크바 대학의 교환 학생으로 콜모고로프의 학파에서 확률론을 공부했고, 그곳에서 기계 번역을 궁리하다 퀵정렬을 떠올렸습니다.

연표.

  • 1956년 해군에서 복무하며 러시아어를 배우다
  • 1959년 모스크바 대학의 교환 학생으로 기계 번역을 하다 퀵정렬을 떠올리다
  • 1960년 런던의 엘리엇 브라더스에 들어가다
  • 1961년 「알고리즘 64: 퀵정렬」을 발표하다
  • 1963년 엘리엇 803 컴퓨터의 알골 60 컴파일러를 완성하다
  • 1965년 알골 W를 설계하며 빈 참조를 넣다
  • 1968년 벨파스트의 퀸스 대학 교수가 되다
  • 1969년 「컴퓨터 프로그래밍의 공리적 기초」를 발표하다
  • 1974년 병행 프로그램의 모니터 개념을 발표하다
  • 1977년 옥스퍼드 대학 교수가 되다
  • 1978년 「통신하는 순차 프로세스」를 발표하다
  • 1980년 튜링상을 받고 「황제의 낡은 옷」을 강연하다
  • 1985년 『통신하는 순차 프로세스』를 책으로 펴내다
  • 1999년 옥스퍼드에서 은퇴하고 마이크로소프트 연구소 케임브리지로 옮기다
  • 2000년 기사 작위와 교토상을 받다
  • 2009년 빈 참조를 스스로 '수십억 달러짜리 실수'라 부르다
관련된 시대와 장소모스크바 수학 학파
이 개념이 나오는 큰 생각대칭과 불변량무작위성

이 인물이 나오는 긴 글

그래프 이론 일곱 다리의 도시 쾨니히스베르크의 일곱 다리를 한 번씩만 건너 산책할 수 있을까? 오일러는 지도를 지우고 점과 선만 남겼다. 계산언어학 말을 세는 기계 문법은 규칙일까, 확률일까? 파니니의 문법에서 촘스키의 위계, 섀넌의 영어 엔트로피, 오늘날의 언어 모델까지. 알고리즘과 복잡도 줄 세우기의 한계 카드 천 장을 가장 빨리 줄 세우는 방법은? 인구조사의 천공 카드에서 퀵정렬까지, 그리고 어떤 방법도 넘을 수 없는 n log n의 벽.

이 인물을 언급하는 페이지

이 페이지가 가리키는 개념