튜링상 관련 업적

뚜렷하면서 완벽한 세 가지 성취물이 있다.
1. LCF는 데이나 스콧의 Logic of Computable Functions를 구현한 것으로써 기계의 도움을 받는 증명 방식을 아마도 최초로 이론적 바탕 위에서 구현했다.
2. ML은 타입-안전한 예외 처리를 가지면서 다형적 타입 추론을 포함하는 최초의 언어이다.
3. CCS는 동시성에 관한 일반적 이론이다.
이 외에도 운영 의미론과 표시적 의미론 사이의 관계에 관한 연구를 통해 완벽한 추상화의 틀을 잡고 크게 발전시켰다.

1991년 튜링상 선정 이유

LCF

LCF는 하나의 소프트웨어 시스템이다. 그 목적은 수학적 증명을 도와주기 위함에 있다. 자동으로 증명해 주지는 않는다. 그래서 증명을 검사하는 프로그램proof-checking program이라고 설명되기도 한다.​6​

LCF 시스템은 여러 버전이 있다. 먼저 1972년에 발표된 첫 번째 버전은 스탠퍼드 LCF라고 불린다. 로빈 밀너가 스탠퍼드 대학교에 있을 때 개발했기 때문이다. 그는 에든버러 대학교로 자리를 옮긴 후에 개선된 버전을 발표했다. 그것은 에든버러 LCF라고 불린다. 이후에 그는 더 이상 LCF 개발에 손을 대지 않았지만 다른 연구자들이 새로운 버전을 발표했다. 그중 대표적인 것이 케임브리지 대학교에서 발표한 케임브리지 LCF이다.

한 가지 혼동하지 말아야 할 것이 있다. LCF 시스템은 데이나 스콧의 LCF 이론을 지원하는 도구에서 출발했다. 데이나 스콧의 LCF 이론은, ‘연역적 방법으로 증명을 수행하는 알고리듬’에 관한 것이다.

수학에서 ‘연역적deductive 방법’이란 무엇인가? 이것은 이미 참이라고 확인된 것들에 추론 규칙rule of inference을 적용해서 새로운 정리를 만들어내는 것이다. 이를 다르게 표현한다면, 어떤 정리가 주어졌을 때 이것이 참인지를 증명하기 위해 기존의 참인 명제 혹은 정리들로부터 추론 규칙을 통해 도출해 내는 방식을 말한다.

알고리듬이란 무엇인가? 어떤 결과물을 얻기 위한 과정인데, 이 과정을 따르면 결과물을 반드시 얻을 수 있다. 따라서, 데이나 스콧의 LCF 이론에서 제공하는 알고리듬을 따르기만 하면 수학 정리를 연역적으로 증명할 수 있게 된다.

로빈 밀너는 LCF 이론을 지원하는 소프트웨어를 만들고자 했다. 그는 PDP-10 컴퓨터에서 리스프 언어를 사용했다. 이 LCF 시스템을 실행하면, 명령어를 기다리는 프롬프트가 나타난다. 사용자는 여기에 명령어를 타이핑하여 작업을 지시한다. 여기서 말하는 작업이란, 결국 연역적 증명의 한 단계를 의미한다. 주의할 점이 있다. LCF 시스템이 데이나 스콧의 LCF 이론을 따르기는 하지만, 그렇다고 자동으로 증명을 해주지는 않는다. 증명 과정에서 선택지가 제공되면 어떤 선택을 할지는 사용자의 몫이다.

LCF 시스템에서는 크게 두 종류의 정보를 관리한다. 하나는 목표goal이고 다른 하나는 전제assumption이다.​‡​ 사실상 증명이란 전제들로부터 목표를 끌어내는 일이며, 이 과정은 반드시 추론 규칙에 의거해야만 한다.

LCF 시스템은 ‘전제’에서 출발하지 않고 ‘목표’에서 출발한다. 즉 역방향으로 증명을 수행한다.

주 목표(스콧의 논리식으로 표현)를 선언한 후에 그것을 부 목표들로 쪼갠다. 쪼개는 과정에는 몇 가지 명령어를 사용하게 된다(예를 들어 시작값과 단계를 사용하는 귀납 명령). 부 목표는 단순화 기법simplifier을 사용하여 증명되거나 아니면 전제와 일치할 때까지 계속 더 단순한 부 목표들로 쪼개진다.​6​

단순화 기법simplifier에 주목하자. 이것이 없다면 LCF는 그저 종이를 컴퓨터 화면으로 대치한 정도의 수준에 불과한 것인지도 모른다. 단순화 기법이란, 어떤 목표(하나의 수식이다)가 주어졌을 때, 지금까지 확인된 전제들로부터 연역적으로 도출이 가능한지를 자동으로 확인하는 것이다. 즉, LCF가 수학 정리를 자동으로 증명하지는 못하지만 그 과정의 일부는 자동으로 처리해 줄 수 있다는 것이다.

LCF의 사용 방식

LCF 프로그램이 실행되면 프롬프트prompt가 나타난다. LCF의 프롬프트 표시는 *****이다. 따라서 아래와 같은 상태로 사용자의 입력을 기다리게 된다.

*****
목표 지정
*****GOAL P->X,P->Y,Z ≡ P->X,Z;

A->B,C 는 조건문을 나타내는 수식이다. A가 참(TT)이면 B, A가 거짓(FF)이면 C이고 A가 알 수 없는 값(UU)이면 결과도 알 수 없는 값(UU)이다.

사용자가 위와 같이 입력한 후에 엔터키를 누르면 화면은 다음과 같이 변한다.

*****GOAL P->X,P->Y,Z ≡ P->X,Z;
NEWGOAL #1 P->X,P->Y,Z ≡ P->X,Z

LCF 시스템은 사용자가 지정한 목표를 저장하고 1번이라는 번호를 부여했다. 다른 명령어에서 이 목표를 참조하려 할 때는 이 번호를 사용하게 된다.

증명 시도

LCF 시스템의 목표는 수식의 증명을 도와주는 데 있다. 따라서 주어진 목표에 대한 증명을 시도하기 위한 명령어가 제공된다.

*****TRY 1 SIMPL;

사용자는 TRY라는 명령어를 사용해서 LCF 시스템에게 증명을 시도해보라고 지시할 수 있다. 뒤에 숫자가 오면 해당되는 목표의 번호를 의미한다. 그리고 그 다음에 오는 것이 중요하다. 위의 예에서는 SIMPL이다. 이것은 단순화 기법을 사용하라는 의미이다. LCF 시스템에는 몇 가지 단순화 기법이 구현되어 있어서 이것들이 적용된다. 결과가 성공적이라는 보장은 없다. 실제로 위의 명령을 해보면 실패한다. 그러면 사용자는 다른 방법을 궁리해야 하다. 다음과 같은 옵션들이 있다.

*****TRY 1 CONJ;   <- 수식을 쪼개어서 부 목표로 만들기
*****TRY 1 CASES P;  <- P의 값이 TT, FF, UU인 경우로 나누기
*****TRY 1 INDUCT;  <- 시작값과 단계로 분리하기
*****TRY 1 USE TH1;  <- TH1이라는 이름의 정리를 적용하기
전제 지정

수학적 증명에서는 전제assumption가 따라오는 경우가 많다. 그래서 전제를 지정해주는 명령어가 제공된다.

*****ASSUME F≡[aF.FUN(F)], G≡FUN(G);
1  F≡[aF.FUN(F)]  (1)
2  G≡FUN(G)  (2)

LCF 시스템은 전제들을 각각 저장한 후에 번호를 지정한다. 이 번호는 다른 명령어에서 해당 전제를 참조할 때 사용된다.

수식 다루기

수학 증명을 하다보면 수식의 형태를 변화시키거나 수식들을 결합하는 경우가 종종 발생한다. LCF 시스템은 이를 지원하는 명령어들을 가지고 있다. 다음은 몇 가지 예를 보여주고 있다.

*****CONJ 1, 2;  <- 1번과 2번 전제를 합쳐서 새로운 번호를 부여함.
*****INCL 15, 2;  <- 15번 전제에 있는 수식들 중에서 두 번째 수식만 선택하여 새로운 번호를 부여함.
*****SYM 6;  <- 6번 전제에 있는 수식들 중에서 첫 번째 수식만 선택한 후 순서를 바꾸고 새로운 번호를 부여함.
공리와 정의 다루기

공리는 증명할 필요없이 참인 것을 말한다. 정리는 증명을 통해 참이 확인된 것을 말한다. 이 두 가지를 LCF 시스템은 다르게 취급한다.

*****AXIOM AX1: ..., X≡Y, ...; 
AXIOM AX1
1 ...
2 X≡Y
3 ...
*****THEOREM TH1: 2;
THEOREM(AX1) TH1:X≡Y

정리는 TRY 명령에 사용될 수 있다.

1 2 3 4 5 6