서 론

Let-다형성 타입 유추 알고리즘 [eqn: M``]의 병목을 해소하기 위한 혼성 알고리즘 [eqn: H``]

(Hybrid Algorithm H that Fixes the Bottleneck of Let-Polymorphic Type-Inference Algorithm M)

주 상 현      이 욱 세     이 광 근

(Sanghyun Joo)   (Oukseh Lee)  (Kwangkeun Yi)

요 약  Hindley/Milner let-다형성 타입체계(let-polymorphic type system)에는 두 가지 타입 유추(type-inference) 알고리즘이 있다: 하나는 표준으로 알려진 [eqn: W``] 알고리즘으로 프로그램의 문맥에 상관없이 상향식으로 유추하는 알고리즘이고, 다른 하나는 프로그램의 문맥에 따라 하향식으로 유추하는 [eqn: M``] 알고리즘이다. 본 연구에서는 함수 적용(application)이 중첩되는 경우, [eqn: M``] 알고리즘에 병목현상이 발생함을 보이고, 이러한 병목현상이 발생하지 않는 혼성 알고리즘 [eqn: H``]를 제시한다. [eqn: H``] 알고리즘은 [eqn: M``] 알고리즘을 함수 적용 부분만 [eqn: W``] 알고리즘으로 변형한 알고리즘으로, [eqn: W``]보다는 일찍 [eqn: M``]보다는 늦게 오류를 감지함을 보인다.

Abstract The Hindley/Milner let-polymorphic type system has two different type inference algorithms: one is em de facto standard algorithm [eqn: W``] that is context-insensitive, and the other is context-sensitive algorithm [eqn: M``]. We present the bottleneck of the [eqn: M``] algorithm in the case of repeated applications, and propose a hybrid algorithm, named [eqn: H``], for its remedy. The [eqn: H``] algorithm is made out of [eqn: M``] adopting [eqn: W``] on the application part. We show that [eqn: H``] stops still earlier than [eqn: W``] but later than [eqn: M``] when the input program has type errors.

□ 본 연구는 과학기술부 창의적 연구진흥사업 추진으로 얻어진 결과임을 밝힙니다.

Hindley/Milner let-다형성 타입체계(let-polymorphic type system)에는 타입 유추(type inference) 알고리즘으로 [eqn: W``] 알고리즘[1, 2]과 [eqn: M``] 알고리즘[3]이 있다. [eqn: W``] 알고리즘은 Hindley/Milner 타입체계를 처음으로 충실히 구현한(sound and complete) 타입 유추 알고리즘으로 표준으로 사용되어 왔고, [eqn: M``]은 Caml 6.0[4]에서 이론적 검증 없이 사용되다가, [eqn: W``]의 오류 보고를 개선하기 위해서 타입 유추 알고리즘을 고안하던 Lee와 Yi에 의해 그 안전성(soundness)과 완전성(completeness)이 증명되었다[3]. [eqn: W``] 알고리즘과 [eqn: M``] 알고리즘은 타입 유추 방식에서 차이를 나타낸다. [eqn: W``]는 상향식(bottom-up) 알고리즘으로 프로그램의 문맥에 영향을 받지 않고 (context-insensitive) 타입을 유추하고, [eqn: M``]은 이와는 반대로 하향식(top-down)으로 프로그램의 문맥에 따라 (context-sensitive) 타입을 유추한다.

[eqn: M``] 알고리즘은 오류를 일찍 감지하는 장점이 있는 반면, 함수 적용(application)이 중첩되는 경우 병목현상이 생긴다. 항등 함수(identity function)가 중첩 적용된 프로그램에서:

[eqn: M``]은 문맥에 따라서 타입을 유추하므로, 전체 항등 함수의 개수가 n이라고 하면 첫 번째 항등 함수의 인자의 개수는 n-1 개이고 두 번째는 n-2 개라는 정보를 이용하여 각 항등 함수의 타입을 자신의 인자의 개수만큼의 큰 타입으로 강요한다. 결국 [eqn: M``] 알고리즘은 각 항등 함수에서 인자의 개수에 비례하는 작업을 하고, 이를 합하면 (n-1)+(n-2)+…+2+1 에 비례하는, 즉 프로그램 길이의 제곱에 비례하는 작업을 한다([eqn: O(n^2 )]). 이와는 달리 [eqn: W``]는 각 항등 함수의 타입을 개별적으로 유추하기 때문에 프로그램 길이에 비례하는 작업만이 필요하다([eqn: O(n)]).

본 연구에서는 이와 같은 [eqn: M``]의 병목을 해소하는 타입 유추 알고리즘 [eqn: H``]를 제안한다. [eqn: H``]  알고리즘은 [eqn: W``]와 [eqn: M``]을 선택적으로 병행하는(hybrid) 알고리즘이다. [eqn: M``]의 병목현상이 함수 적용(application)부분에 있으므로 [eqn: H``] 알고리즘은 함수 적용시 [eqn: W``]와 유사하게 유추한다. 즉, 함수 적용 □[eqn: e_1 ~ e_2 ``]□의 경우, [eqn: H``]는 [eqn: e_1 ``]의 타입을 단지 함수라고만 강요함으로써 병목을 해소하게 된다. [eqn: e_1 ``]의 타입을 온전히 유추한 뒤 [eqn: e_1 ~e_2 ``]에 강요된 타입에 비추어서 검사를 하게 된다. 이렇게 늦게 검사를 하게 되므로 [eqn: M``] 보다는 늦게 오류를 감지하게 된다. 그렇지만, [eqn: H``]는 [eqn: M``]으로부터 만들어졌기 때문에 [eqn: W``] 보다는 일찍 오류를 감지한다.

타입 유추 알고리즘 [eqn: H``]는 [eqn: W``]와 [eqn: M``]과는 다르게 오류를 보고한다. 그림 1에서 타입 오류가 있는 프로그램에 대해 세 알고리즘이 다르게 오류를 보고한다. fac은 재귀 호출 함수(recursive function)로, 함수정의 내부에서 □fac(n-1)□라고 써야하는 것을 □fac(n=1)□로 틀리게 작성하였다. [eqn: W``]로 타입을 유추하면, 함수 전체의 유추된 타입 int→int와 함수정의 내부에서 사용된 fac의 유추된 타입 bool→int를 동일화(unification) 할 수 없어 전체 프로그램을 오류로 보고한다. 반면에 [eqn: M``]에서는 강요된 타입을 □=□에서 더 이상 동일화 할 수 없다고 보고한다. [eqn: H``]에서는 이와는 달리 n=1에 강요된 타입 int (fac은 int 타입을 인자로 받는다.)와 n=1에서 유추된 타입 bool을 동일화 할 수 없다고 보고한다.

그림 1: 서로 다른 오류 보고.

W 알고리즘과 M 알고리즘의 정의

그림 2는 언어와 Hindley/Milner 다형성 타입체계이고 그림 3은 [eqn: W``]와 [eqn: M``]이다. 그림에서 사용된 수식들은 다음과 같다.

그림 2: 언어와 타입 유추 규칙.

[eqn: vec alpha ``]는 타입 변수의 집합 [eqn: left{alpha_1 , cdots, alpha_n right}``]을 나타내고, 타입스킴(type scheme) [eqn: FORALL vec alpha . tau ``]는 [eqn: FORALL alpha_1 cdots alpha_n. tau ``]를 나타낸다. 타입스킴이 같다는 것은 구속 변수들(bound variables)의 이름 변화에 영향 받지 않고 같다는 것을 뜻한다. 즉, [eqn: FORALL alpha.alpha```->``iota``]와 [eqn: FORALL beta. beta ``->` iota ``]는 같은 타입스킴이다.

자유 타입 변수(free type variable)는 타입스킴의 한정기호(quantifier)에 의해 묶이지 않는(unbounded) 타입 변수들을 의미한다. 자유 타입 변수를 구하는 함수 [eqn: ftv``]는 다음과 같이 정의할 수 있다.

이 때, [eqn: dom( Gamma )``subseteq` Var``]는 타입 환경(type environment) [eqn: Gamma``]의 정의역(domain)을 의미한다.

타입 치환 함수(substitution) [eqn: S``]([eqn: in TypeVar ````-> ``Type ``]) 는 타입 변수를 다른 타입으로 치환해 주는 함수로 정의역이 확장되어 사용된다.

이 때, 집합 [eqn: supp (S)]는 [eqn: S``]로 인해 치환되는 타입 변수의 집합 [eqn: left{alpha~|~S alpha not= alpha right}]이고, 집합 [eqn: i tv (S)]는 [eqn: S``]에 연루된 타입 변수(involved type variable)의 집합 [eqn: left{ alpha ~|~beta ``in` supp (S) , alpha ``in` ftv (S beta) right}``cup` supp (S)]이다. 그리고, [eqn: left{ vec tau / vec alpha right}]는 타입 치환 함수 [eqn: left{ tau_i / alpha_i ~|~ 1 ``<=` i``<=` n right}]를, [eqn: R vec alpha``]는 [eqn: left{ R alpha_1, cdots, R alpha_n right}]를 줄여 쓴 것이다. 타입 치환 함수 [eqn: S``]에 [eqn: R``]을 중첩한 타입 치환 함수 [eqn: RS``]는 [eqn: left{ R(S alpha)/alpha ~|~alpha``in`supp (S)right} ``cup`left{R alpha/alpha~|~alpha``in`supp(R)\supp(S)right}]를 의미한다. 타입 치환 함수 [eqn: S ``]와 [eqn: R``]이 같다는 것은 모든 [eqn: alpha``in`supp(S)``cup`supp(R)``]에 대해서 [eqn: S alpha=R alpha ``]를 의미한다.

[eqn: P``□_V ``]는 [eqn: P``]와 같되 [eqn: V``]에 속하는 타입 변수를 지원하지 않는 타입 치환 함수이다:

□[eqn: Gamma+x ``: sigma``]□는 타입 환경(type environment) [eqn: Gamma``]에 [eqn: x``]의 항만을 [eqn: sigma ``]로 대치시킨 타입 환경 [eqn: left{ y``mapsto`sigma``|``x not= y,] [eqn: (y ``mapsto` sigma') ``in` Gamma ``right} ``cup` left{ x ``mapsto `sigma right}]를 말한다.

구체화(instantiation) [eqn: sigma ````succ`` tau ``]는 타입 [eqn: tau``]가 타입스킴 [eqn: sigma``]로부터 얻어지는 하나의 구체적인 타입임을 말한다:

그림 3: W 알고리즘과 M 알고리즘. 매번 새로 만들어지는 타입 변수들은 서로 다르다. 그리고, 각각의 [eqn: W(Gamma,e)``]를 재귀 호출하는 경우, 새로 만들어지는 타입 변수들의 집합 [eqn: V``]는 [eqn: V``cap`ftv(Gamma)=emptyset]을 만족한다. 마찬가지로 각각의 [eqn: M(Gamma,e,rho)]을 재귀 호출하는 경우도 [eqn: V``cap`(ftv(Gamma)``cup`ftv(rho))=emptyset]을 만족한다.

예를 들면, [eqn: FORALL alpha. alpha ``->` alpha ````succ`` rm i nt ``->` i nt]이다. 일반화(generalization) [eqn: Clos_Gamma (tau)]는 Damas와 Milner의 Gen[eqn: ( Gamma , tau )][2]와 같이, 타입에 한정자를 붙여 일반적인 타입을 만드는 것으로 [eqn: vec alpha = ftv (tau)\ ftv (Gamma)]일 때 [eqn: FORALL vec alpha . tau``]로 정의된다.

동일화 알고리즘 [eqn: U``( ``in` Type times Type ``->` Subst`` )]는 입력된 두 타입을 동일화하는 함수로 다음 성질을 만족한다.

정리 1[5]. 두 타입을 입력으로 받아 다음을 만족하는 타입 치환 함수를 주는 [eqn: U``] 알고리즘은 존재한다.

□[eqn: U ( tau, tau')]가 성공하여 [eqn: S``]를 결과로 주면 [eqn: S ``]는 [eqn: tau``]와 [eqn: tau' ``]을 같은 타입으로 만들어 준다. 즉, [eqn: S tau=S tau' ``]이다.

□[eqn: tau``]와 [eqn: tau']을 같은 타입으로 만드는 타입 치환 함수 [eqn: S' ``]이 존재하면, [eqn: U ( tau, tau')]은 성공하고, 결과 [eqn: S``]에 대해 [eqn: S'=RS]인 타입 치환 함수 [eqn: R ``]이 존재한다. 이러한 [eqn: S``]를 가장 일반적인 동일화 함수(most general unifier)라 한다.

게다가 [eqn: U ( tau, tau')]는 [eqn: tau``]와 [eqn: tau'``]의 자유 타입 변수에만 연루되어 있다.

M의 병목

그림 4: 항등 함수를 4개 중첩 적용했을 때의 타입 유추 과정.

[eqn: M``] 알고리즘은 함수 적용이 중첩되는 경우 병목현상이 발생한다. 항등 함수를 중첩 적용한 다음의 예를 살펴보자:

항등 함수의 개수가 n이라 하면, [eqn: M``]은 첫 번째 항등 함수를 유추할 때 n-1 개의 인자를 갖는다고 강요한다. 두 번째 항등 함수를 유추할 때 n-2 개, 세 번째 항등 함수는 n-3 개의 인자를 갖는다고 강요한다. 이와 같이 모든 함수들에 대해서 인자의 개수를 알고 있어 인자의 개수 크기의 타입으로 강요를 하게 되어, 결국 전체 타입 유추에 드는 비용은 [eqn: O(n^2 )]이 된다. 반면에 [eqn: W``]는 각 항등 함수를 독립적으로 유추하므로 각각의 함수의 타입 유추 비용은 일정하게 된다. 결국 [eqn: O(n)]의 비용만이 든다.

병목현상의 원인은 함수 적용(application) 부분에 있다:

(M.5)

현재 강요된 타입 [eqn: rho``]를 함수 부분 [eqn: e_1 ``]에 증가된 형태인 [eqn: beta ``->` rho``]로 강요한다. 함수 적용이 계속 되게 되면 강요 타입은 계속 증가되어서 실행비용이 증가한다.

항등 함수를 중첩 적용한 프로그램의 자세한 타입 유추 과정을 살펴보자(그림 4). 첫 번째 열은 입력 프로그램이고 밑줄 친 부분은 각 재귀 호출에서 현재 처리되고 있는 부분이다. 두 번째 열은, [eqn: M``]에서는 현재 처리되고 있는 부분에 강요된 타입이고, [eqn: W``]에서는 결과 타입이다. 세 번째 열은 각 타입 유추 과정에서 불려지는 동일화 알고리즘의 인자를 보여준다. 우선, 4.(a)의 [eqn: M``]의 유추 과정을 살펴보자. (a.1-4)에서, [eqn: M``]은 강요 타입을 [eqn: delta ``]에서 [eqn: alpha ``->` beta ``->` gamma ``->` delta``]로 증가시킨다. (a.5) 에서 함수 내용(function body)에 강요된 타입은 [eqn: beta ``->` gamma ``->` delta``]가 되고 이렇게 커진 강요 타입은 (M.2) 에 의해 [eqn: alpha``]와 동일화된다. 왜냐하면, 항등 함수의 인자 타입과 결과 타입은 같아야 하기 때문이다. 인자 타입 [eqn: alpha ``]가 결과 타입 [eqn: beta ``->` gamma ``->` delta``]로 동일화되었으므로, 두 번째 항등 함수에는 [eqn: beta ``->` gamma ``->` delta``]가 강요된다(a.6). 나머지 과정은 위의 과정과 비슷하게 동작한다. 이와 같이 동일화가 다루는 타입의 크기는 항등 항수의 개수로부터 점차로 줄어들게 된다. 이제 [eqn: W``]의 과정(그림 4.(b))을 살펴보자. (b.1), (b.2), (b.4) 에서 보면, [eqn: W``]는 각 항등 함수의 타입을 [eqn: alpha ``->` alpha``]와 같은 모양으로 유추한다. 이는 [eqn: W``]가 프로그램의 문맥에 상관없이 타입을 유추하기 때문이다. 이와 같이 일정한 모양의 타입으로 (b.3), (b.5) 에서 동일화한다.

그림 5의 실험결과로부터 [eqn: M``]의 실행비용이 프로그램의 크기가 n이라 했을 때 [eqn: O(n^2 )]으로 증가하는 것을 확인할 수 있다. 반면에 [eqn: W``]는 [eqn: O(n)]으로 증가한다. 여기서 측정한 실행비용은 동일화가 처리하는 타입의 총 크기와 실제 타입 유추 알고리즘의 실행시간이다.

그림 5: 항등 함수를 중첩 적용했을 때, M이 W보다 빨리 증가한다. (X: 항등 함수의 개수, Y: 측정치)

H 알고리즘

[eqn: M``]의 병목을 해소하기 위해 함수 적용 부분을 변경시켜 [eqn: H``] 알고리즘을 고안하였다. 그림 6은 [eqn: H``] 알고리즘의 정의이다.

[eqn: H``]는 [eqn: M``]의 함수 적용 부분에서 발생하는 병목을 해결한다. (H.5)를 보면,

(H.5)

[eqn: H``]는 함수 부분 [eqn: e_1 ``]의 타입을 단지 함수라고만 즉, [eqn: beta_1 ``->` beta_2 ``]로 강요한다. 이렇게 [eqn: H``]는 [eqn: M``]과는 달리 함수 적용 전체에 강요된 타입 [eqn: rho``]를 전달하지 않는다.

[eqn: H``]는 [eqn: M``]보다 늦게 오류를 감지한다. [eqn: H``]는 함수부분에 덜 구체적인 타입으로 강요하므로 만들어진 구체적인 타입을 늦게 검사하기 때문이다. (H.6)을 보면,

(H.6)

[eqn: e_1 ``]의 구체적인 결과 타입인 [eqn: S_1 beta_2 ``]를 현재 강요된 타입 [eqn: rho ``]에 비추어 검사한다.

그림 6: H의 정의. 새로 만들어지는 타입 변수들은 서로 다르다. 그리고, 각 [eqn: H(Gamma,e,rho)]의 재귀 호출에서 만들어지는 타입 변수들의 집합 [eqn: V``]는 [eqn: V``cap`(ftv(Gamma)``cup`ftv(rho))=emptyset]을 만족한다.

그림 7: H에서는 M의 병목현상이 일어나지 않는다. (X: 항등 함수의 개수, Y: 측정치)

여전히 [eqn: H``]는 [eqn: W``]보다 일찍 오류를 감지한다. [eqn: M``]과 같이, [eqn: H``]는 함수 부분에서 만들어진 타입을 인자 부분에 전달하여 이를 상수와 변수까지 흘려보내기 때문이다. (H.7)을 보면,

(H.7)

함수 부분 [eqn: e_1 ``]의 인자 타입 [eqn: S_2 S_1 beta_1 ``]으로 인자 부분 [eqn: e_2 ``]를 강요한다.

항등 함수를 중첩 적용한 프로그램을 가지고 실험한 결과(그림 7)를 볼 때, [eqn: H``]에서는 [eqn: M``]의 병목현상이 일어나지 않는다. [eqn: H``]에서 실행비용은 [eqn: W``]와 같이 항등 함수의 개수에 대해 [eqn: O(n)]으로 증가하는 것을 볼 수 있다.

H의 성질

[eqn: H``] 알고리즘은 Hindely/Milner let-다형성 타입체계를 충실히 즉, 안전(sound)하고 완전(complete)하게 구현한다. 안전성(soundness)이란 타입 유추 알고리즘이 프로그램의 타입을 유추한 결과가 타입 유추 규칙에 맞다는 것이고, 완전성(completeness)이란 타입 유추 규칙에 맞는 타입을 타입 유추 알고리즘이 유추해 낼 수 있다는 것이다. 안전성과 완전성이 보장되는 타입 유추 알고리즘이란, 그 타입 유추 규칙을 충실히 즉, 제대로 구현한 알고리즘이란 뜻이다.

정리 2 ([eqn: H``]의 안정성). 프로그램 [eqn: e``], 타입 환경 [eqn: Gamma ``], 타입 [eqn: rho ``]에 대해, [eqn: H`` ( Gamma,e, rho)]가 성공하여 결과 [eqn: S``]를 주면, [eqn: S Gamma ``vdash` e``:`S rho``]가 성립한다.

증명. 다음 보조정리를 사용하여 증명한다:

보조정리 1[2]. [eqn: Gamma ``vdash` e``:` tau ``]이면, [eqn: S Gamma ``vdash` e``:`S tau``]가 성립한다.

[eqn: e``]의 구조에 대한 귀납법으로 증명한다. 여기서는 함수 적용의 경우만 증명한다. 나머지 경우는 [eqn: M``]의 안전성 증명[3]과 같다.

귀납 가정(induction hypothesis)에 의해 (H.5)로부터 가 성립한다. 보조정리 1에 의해 양변에 [eqn: S_3 S_2 ``]를 적용하면

(1)

가 성립한다. (H.6)에 의해 가 성립하므로, (1)로부터

(2)

가 성립한다. 귀납 가정에 의해 (H.7)로부터

(3)

가 성립한다. (APP) 규칙에 의해 (2)와 (3)으로부터 가 성립한다. □

정리 3 ([eqn: H ``]의 완전성). 프로그램 [eqn: e ``], 타입 환경 [eqn: Gamma ``], 타입 [eqn: rho``]에 대해, [eqn: P Gamma ``vdash` e``:`P rho``]이면, [eqn: H ( Gamma,e, rho)]가 성공하고, 그 결과를 [eqn: S``]라 하면, [eqn: P``□_V = (RS)□_V ``]를 만족하는 타입 치환 함수 [eqn: R ``]이 존재한다. 여기서 [eqn: V ``]는 [eqn: H ( Gamma,e, rho)]에서 사용된 새 타입 변수들의 집합이다.

증명. 이 증명은 다음 보조정리들을 사용한다.

보조정리 2. [eqn: S= H ( Gamma,e, rho)]이면  [eqn: i tv(S) ``subseteq`ftv(Gamma)``cup``ftv(rho)][eqn: cup` V ``]이다. 이 때, [eqn: V``]는 [eqn: H ( Gamma,e, rho)]에서 사용된 새 타입 변수들의 집합이다.

증명. Lee와 Yi의 보조정리 6의 증명[3]과 유사하게 증명된다. □

보조정리 3 [3]. [eqn: i tv (S) ``cap` A= emptyset]이면 [eqn: (RS)□_A = R``□_A S``]이다.

[eqn: e``]의 구조에 대해 귀납법으로 증명한다. 안전성 증명과 마찬가지로 함수 적용의 경우에 대해서만 증명한다.

주어진 가정이 [eqn: P Gamma ``vdash` e_1 ~ e_2 ``:`P rho ``]이고 새 타입 변수들의 집합 [eqn: V= left{ beta_1 , beta_2 right}``cup` V_1 ``cup` V_2 ``]이라고 하자. 여기서 [eqn: beta_1 ``]과 [eqn: beta_2 ``]는 (H.5)의 새 타입 변수를 가리키고, [eqn: V_1 ``]는 (H.5)의 [eqn: H ( Gamma,e_1 , beta_1 ``->` beta_2 )]에서, 그리고 [eqn: V_2]는 (H.7)의 [eqn: H (S_2 S_1 Gamma,e_2 ,S_2 S_1 beta_1 )]에서 쓰인 새 타입 변수들의 집합이다.

(APP) 규칙에 의해 다음을 만족하는 타입 [eqn: tau``]가 존재한다:

,	(4)

.	(5)

라 두면, [eqn: beta_1 , beta_2 ``not in` ftv (Gamma )]이기 때문에 [eqn: tau ``->` P rho = P'( beta_1 ``->` beta_2 )]이고 [eqn: P Gamma=P' Gamma ``]이다. 그러므로, 귀납 가정에 의해 (4)와 (H.5)로부터

(6)

을 만족하는 타입 치환 함수 [eqn: R_1 ``]이 존재한다.

[eqn: R_1 S_1 beta_2 = R_1 S_1 rho ``]이다. 왜냐하면,

그러므로, (H.6)의 동일화 [eqn: U (S_1 beta_2 ,S_1 rho)]는 성공한다. 그 결과를 [eqn: S_2 ``]라 하면 [eqn: R_2 S_2 = R_1 ``]를 만족하는 [eqn: R_2 ``]가 존재한다. 그러면, (6)으로부터 다음이 만족된다:

(7)

(5)와 (H.7)의 [eqn: H (S_2 S_1 Gamma,e_2 ,S_2 S_1 beta_1 )]로부터 귀납 가정에 의해

(8)

를 만족하는 타입 치환 함수 [eqn: R_3 ``]가 존재한다. 왜냐하면,

.

그리고

이제 끝으로 [eqn: P``□_V = (R'S_3 S_2 S_1 )□_V ``]를 만족하는 타입 치환 함수 [eqn: R' ``]이 존재함을 보이면 된다. [eqn: R' = R_3 ``]라고 하면,

(9)

가 성립한다. 여기서 [eqn: ( i tv (S_1 )``cup` i tv (S_2 )) ``cap` V_2 = emptyset]임을 주목하라. 왜냐하면, 정리 1과 보조정리 2에 의해 [eqn: i tv (S_1 )``cup` i tv (S_2 )``subseteq` ftv (Gamma) ``cup` left{ beta_1, beta_2 right} ``cup` V_1 ``cup` ftv (rho)]이고, 모든 새로 만들어진 타입 변수들은 서로 다르다고 가정했으므로 [eqn: ( ftv (Gamma )``cup` ftv (rho)) ``cap` V_2 ``subseteq` ( ftv (Gamma) ``cup` ftv( rho)) ``cap` V= emptyset]이고 [eqn: (V_1 ``cup` left{ beta_1 , beta_2 right}) ``cap` V_2 = emptyset]이기 때문이다. 결국, 보조정리 3으로부터 (9)는 다음과 같다:

□

[eqn: H``] 알고리즘은 [eqn: W``] 알고리즘보다 일찍, [eqn: M``] 알고리즘보다는 늦게 오류를 감지한다. 호출 문자열(call string)[3]을 사용하여 이를 엄밀하게 살펴보자. [eqn: W``( Gamma ,e)]의 호출 문자열 는 공백문자열로부터 시작해서 [eqn: W``( Gamma_1 , e_1 )]이 호출될 때마다 [eqn: ( Gamma_1 ,e_1 )^d]의 정보를, 그리고 유추를 끝내고 돌아갈 때 [eqn: ( Gamma_1 , e_1 )^u]의 정보를 붙여 만든 문자열이다. 타입 유추 알고리즘이 동일화 실패로 인해 멈추었을 때, □[eqn: W``]가 [eqn: e``]에서 실패했다□는 것은 다음과 같이 정의된다.

정의 1 [3]. 타입 환경 [eqn: Gamma ``]과 프로그램 [eqn: e``]에 대해, □[eqn: W ( Gamma,e)]가 [eqn: e'``]에서 실패했다□는 것은 호출 문자열 에서 짝이 맞지 않는 정보 중에 오른쪽 끝에 있는 것이 [eqn: ( Gamma``',e')^d ``]라는 뜻이다.

이와 유사하게 [eqn: M``]과 [eqn: H``]의 호출 문자열은 정의된다. [eqn: H``]의 호출 문자열은 [eqn: W``]보다 길지 않고 [eqn: M``]보다 짧지 않다. 그림 8의 예를 보면, [eqn: W``]는 [eqn: e_2 ``]를 성공적으로 타입 유추하고 나서 실패하고, [eqn: M``]은 [eqn: e_2 ``]의 not을 유추하던 도중에 실패하고, [eqn: H``]는 not을 성공적으로 타입 유추하고 나서 실패한다.

정리 4. 타입 환경 [eqn: Gamma``], 프로그램 [eqn: e ``], 새 타입 변수 [eqn: beta ``]에 대해,

이다. 이 때, [eqn: |`s`|``]는 호출 문자열의 길이이다.

증명. [eqn: e``]에 오류가 없으면 호출 문자열의 길이가 같다. [eqn: e``]에 오류가 있을 때를 생각해 보자. 이 증명은 다음의 보조정리들을 사용한다.

그림 8: H의 호출 문자열은 W보다 짧고 M보다 길다.

보조정리 4. 프로그램 [eqn: e``], 타입 환경 [eqn: Gamma ``], 새 타입 변수 [eqn: beta ``]에 대해, 에 [eqn: ( Gamma ^W ,e')^d ``]가 있고 에 [eqn: ( Gamma ^H ,e', rho ^H )^d ``]가 있을 때, [eqn: W ( Gamma ^W ,e')]가 실패하면 [eqn: H ( Gamma ^H ,e', rho ^H )]도 실패한다.

증명. 부록 A에 있음. □

보조정리 5. 프로그램 [eqn: e``], 타입 환경 [eqn: Gamma``], 새 타입 변수 [eqn: beta ``]에 대해, 에 [eqn: ( Gamma ^M ,e', rho ^M )^ d/u ``]가 있으면,  에 [eqn: ( Gamma ^H ,e', rho ^H )^ d/u ``]가 있으며 [eqn: R Gamma ^H ````succ`` Gamma ^M ``]와 [eqn: R rho ^H = rho ^M ``]를 만족하는 타입 치환 함수 [eqn: R ``]이 존재한다.

증명. 부록 B에 있음. □

보조정리 5는 을 직접적으로 증명한다. 왜냐하면, [eqn: H``]와 [eqn: M``]의 호출 문자열의 순서는 같은데 [eqn: M``]에 있으면 해당하는 호출 또는 귀환이 [eqn: H``]에 있다는 것은 [eqn: H``]의 호출 문자열이 항상 더 길거나 같다는 것을 의미하기 때문이다.

이제 을 귀류법으로 증명하겠다. 가 맞다고 가정하자. [eqn: W ( Gamma,e)``]는 함수 적용 [eqn: (e_1 ~e_2 )``]과 재귀 함수정의 (fix[eqn: f~ lambda x.e``]) 에서만 실패할 수 있다. 즉, (W.6)과 (W.10)에서만 실패 할 수 있다.

□(W.6)의 경우: [eqn: e_1 ~e_2 ``]에서 [eqn: W``]가 실패하였다고 하자. 그러면, [eqn: W``]와 [eqn: H ``]의 호출 기록은

와 같다. 왜냐하면, [eqn: H``]의 호출 문자열이 [eqn: W``]보다 길다고 가정했고, [eqn: e_2 ``]의 타입 유추가 끝난 뒤에 [eqn: e_1 ~e_2 ``]가 끝나기 때문이다. 이것은 [eqn: W ( Gamma_1 ^W ,e_1 ~e_2 )]가 실패했을 때 [eqn: H ( Gamma_1 ^H ,e_1 ~e_2 , rho_1 ^H )]가 성공적으로 유추된다는 것인데, 보조정리 4에 의해 불가능하다. 결국 가정에 모순된다.

□(W.10)의 경우: 위의 경우와 비슷하게 가정으로부터 [eqn: W ( Gamma ^W , {rm fix} f~lambda x. e' )]가 실패했을 때 [eqn: H ( Gamma ^H ,{rm fix} f ~lambda x. e' , rho ^H )]가 성공한다고 이끌어 낼 수 있다. 그러나, 보조정리 4에 의해 불가능하다. 결국 가정에 모순된다. □

토론

Obejective Caml에서의 타입 유추 알고리즘

OCaml 2.02[6]는 [eqn: H``]와 유사한 타입 유추 알고리즘을 사용한다. 차이는 함수 적용 부분에 있다. OCaml은 함수 적용에서 함수 부분 [eqn: e_1 ``]의 타입을 함수라고 강요하지 않는다:

그리고 함수 부분의 결과 타입을 현재 함수 적용 전체에 강요된 타입 [eqn: rho ``]에 비추어 검사를 한다:

그리고 인자 부분 [eqn: e_2``]의 타입을 [eqn: H``], [eqn: M``]과 같이 강요한다:

OCaml은 몇몇 예에서 [eqn: W``], [eqn: M ``], [eqn: H ``]와 다르게 오류를 보고한다:

(+ 1 true) 3.

[eqn: M``]은 + 에서, [eqn: H``]는 true를 유추하기 직전에, OCaml은 true에서, [eqn: W``]는 true를 유추한 직후에 실패한다. 즉, OCaml은 [eqn: H``]보다 늦게, [eqn: W``]보다 일찍 오류를 감지한다.

실험 결과

일반적인 프로그램을 입력으로 실험한 결과 [eqn: H``] 알고리즘은 [eqn: W``], [eqn: M``]과 비슷한 성능을 보인다(그림 9). [eqn: M``]과 [eqn: H``]는 Caml 6.0[4] 컴파일러에, [eqn: W``]는 Caml 7.4[7] 컴파일러에 구현되었다. 이 실험은 SUN UltraSparc 2 (400MHz)에서 수행되었다.

let-indent의 경우 [eqn: W``]의 결과가 나쁜 이유는 ML의 패턴구조 때문이다. [eqn: W``]에서는 let-묶음의 좌변 패턴의 타입과 우변의 타입에 동일화 과정이 필요하다. 반면에, [eqn: M``]과 [eqn: H``]에서는 이와 같은 과정이 필요 없다. 다음이 let-indent 경우인데:

let x0 = fun x -> (x,x) in

let x1 = fun y -> x0 (x0 y) in

let x2 = fun y -> x1 (x1 y) in

□

그림 9: 실험 결과

x0;;

이 경우에서는 프로그램의 크기를 n이라 할 때 타입의 크기가 [eqn: O(2^2^n )]로 증가하는 예이다[9]. 이렇게 거대한 타입을 [eqn: W``]는 매번 let-묶음마다 동일화 과정을 해야한다. 그래서 실행비용이 많이 악화된 것이다.

결론

Hindley/Milner의 let-다형성 타입체계의 표준 타입 유추 알고리즘 [eqn: W``]의 오류 보고를 개선하기 위해서 고안된 [eqn: M``]은 함수를 중첩으로 사용된 경우 유추에 소요되는 시간이 프로그램 크기의 제곱으로 증가함을 발견하였다.

본 연구에서는 이러한 [eqn: M``]의 병목을 해소하기 위해 [eqn: H``] 알고리즘을 고안하였다. [eqn: H``]는 [eqn: M``] 알고리즘이 갖고 있는 장점을 모두 갖고 있음을 증명하였다. 즉, [eqn: H``]는 let-다형성 타입체계를 충실히 구현하였고 [eqn: W``] 보다 일찍 오류를 감지한다. 또한 [eqn: M``] 보다는 오류를 늦게 감지하므로 [eqn: W``]와 [eqn: M``]과는 다른 오류 보고가 가능하다. 실험을 통하여 [eqn: H``] 알고리즘은 [eqn: W``] 알고리즘과 [eqn: M``] 알고리즘에서 발생할 수 있는 병목현상이 없음을 보였다.

부록

A. 보조정리 4의 증명

보조정리 4의 증명은 Lee와 Yi의 [eqn: M``] 알고리즘에 대한 보조정리 11의 증명[3]과 같다. 단지, 사용되는 보조정리 8만 다른 뿐이다. 그러므로, 여기서는 보조정리 8만 증명한다. 증명을 위하여 다음의 보조정리들이 필요하다.

보조정리 6 [2]. [eqn: sigma ``succ` sigma' ``]이면 [eqn: S sigma ``succ` S sigma' ``]이다.

보조정리 7 [2]. [eqn: Gamma``' ``vdash` e``:` tau ``]가 성립하고, [eqn: Gamma ``succ` Gamma``' ``]이면, [eqn: Gamma ``vdash` e``:` tau``]가 성립한다.

정리 5 ([eqn: W``] 알고리즘의 완전성) [2]. 타입 환경 [eqn: Gamma ``], 프로그램 [eqn: e``]에 대해, [eqn: Gamma``' ``vdash` e``:` sigma ``]를 만족하는 [eqn: Gamma ``]의 예(instance) [eqn: Gamma``'], 타입스킴 [eqn: sigma ``]가 존재하면, [eqn: W``( Gamma,e)]는 성공한다. 그 결과를 [eqn: (S, tau)]라 하면 [eqn: Gamma``'=RS Gamma ``]이고 [eqn: R Clos_{S Gamma }(tau) ``succ` sigma ``]를 만족하는 타입 치환 함수 [eqn: R ``]이 존재한다.

보조정리 8. 표현식 [eqn: e ``], 타입 환경 [eqn: Gamma ``], 새 타입 변수 [eqn: beta ``]에 대하여, 에 [eqn: ( Gamma ^W ,e')^d ``]가 있고 에 [eqn: ( Gamma ^H ,e', rho ^H )^d ``]가 있으면, [eqn: R Gamma ^W ``succ` Gamma ^H ``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다.

증명. 와 의 접두 문자열(prefix), [eqn: ( Gamma,e)^d cdots( Gamma ^W ,e')^d ``]과 [eqn: ( Gamma,e, beta)^d cdots( Gamma ^H ,e', rho ^H )^d ``]의 길이에 대해 귀납적으로 증명한다. 두 알고리즘은 같은 순서로 표현식을 검색하므로 같은 길이의 접두 문자열을 갖는다. 수식 혼동을 막기 위해 두 알고리즘에서 사용되는 기호들은 위첨자(super-scription)로 구별하기로 한다.

□초기 경우: 접두 문자열의 길이가 1일 때, 즉, 처음 호출했을 때, [eqn: Gamma ^W ``]와 [eqn: Gamma ^H ``]는 같다. [eqn: R ``]을 [eqn: emptyset]로 두면 조건을 만족한다.

함수 적용의 경우를 제외하고는 Lee와 Yi의 보조정리 10의 증명[3]과 같으므로 생략한다.

□[eqn: e' ``]이 [eqn: ( e'~e_2 )]에 있을 경우: [eqn: e'``]을 호출할 때와 [eqn: e'~e_2 ``]를 호출할 때의 타입 환경이 같으므로, 귀납 가정에 의해 조건이 만족한다.

□[eqn: e' ``]이 [eqn: ( e_1 ~e' )]에 있을 경우: [eqn: H``] 알고리즘의 안전성에 의해 (H.5)로부터 [eqn: S_1 ^H Gamma ^H ``vdash` e_1 ``:` S_1 ^H ( beta_1 ^H ``->` beta_2 ^H )]가 성립함을 알 수 있다. 보조정리 1에 의해 [eqn: S_2 ^H]을 양변에 적용할 수 있다. 그러면,

(10)

이 성립한다. 귀납 가정에 의해 [eqn: R_1 Gamma ^W ``succ` Gamma ^H ``]이 성립하고, 보조정리 6에 의해

(11)

가 성립한다. 보조정리 7에 의해 (10)은

을 뜻하고, [eqn: W``] 알고리즘의 완전성에 의해 [eqn: R'S_1 ^W Gamma ^W = S_2 ^H S_1 ^H R_1 Gamma ^W ``]을 만족하는 [eqn: R'``]이 존재한다. 그러면, (11)에 의해 다음이 성립한다.

□

B. 보조정리 5의 증명

다음의 보조정리들과 [eqn: M``]의 안전성이 증명에 사용된다.

보조정리 9 [3]. 타입 치환 함수 [eqn: S``], 타입 환경 [eqn: Gamma ``], 타입 [eqn: tau``]에 대하여, [eqn: S Clos_Gamma (tau) ``succ` Clos_{S Gamma}( S tau)]이다.

보조정리 10 [3]. 타입 환경 [eqn: Gamma``], [eqn: Gamma``'``], 타입 [eqn: tau``]에 대하여 [eqn: Gamma ``succ` Gamma``' ``]이면, [eqn: Clos_Gamma (tau) ``succ` Clos _{Gamma``'} (tau)]이다.

정리 6 ([eqn: M``] 알고리즘의 안전성) [3]. 표현식 [eqn: e``], 타입 환경 [eqn: Gamma``]에 대하여, [eqn: M``( Gamma,e, rho)``=`S ``]인 타입 [eqn: rho``]가 존재하면 [eqn: S Gamma ``vdash` e``:`S rho ``]가 성립한다.

의 접두 문자열의 길이에 대한 귀납법으로 증명된다.

□초기 경우: 접두 문자열 길이가 1일 때, 즉, 처음 호출했을 때는 [eqn: Gamma ^H = Gamma ^M ``]이고 [eqn: rho ^H = rho ^M ``]이다. 고로, [eqn: R``]을 [eqn: emptyset]로 두면 조건을 만족한다.

먼저, [eqn: e'``]에 대한 유추를 끝냈을 때, 즉, 접두 문자열이 [eqn: ( Gamma,e, beta) cdots( Gamma ^M ,e', rho ^M )^u ``]인 경우에 대해 증명한다.

□[eqn: e' ``]으로부터 귀환한 경우: 접두 문자열이 어떤 [eqn: Gamma ^M ``], [eqn: rho ^M ``]에 대해

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M , e', rho ^M )^u ``]이 있다는 것은 [eqn: M ( Gamma ^M , e', rho ^M )``]이 성공한다는 것을 뜻한다. [eqn: M ( Gamma ^M , e', rho ^M )``]이 성공적으로 유추되어 결과로 [eqn: S ^M ``]를 낸다 하면, [eqn: M``] 알고리즘의 안전성에 의해

가 성립한다. 접두 문자열에 [eqn: ( Gamma ^M , e', rho ^M )^d ``]가 있으므로, 귀납 가정에 의해, 에 [eqn: ( Gamma ^H , e', rho ^H )^d ``]가 있고, 또한, [eqn: R rho ^H = rho ^M ``]와 [eqn: R Gamma ^H ``succ` Gamma ^M ``]을 만족하는 [eqn: R ``]이 존재한다. [eqn: R Gamma ^H ``succ` Gamma ^M ``]가 성립하므로 보조정리 6에 의해 [eqn: S ^M R Gamma ^H ``succ` S ^M Gamma ^M ``]가 성립한다. 그러면, 보조정리 7에 의해

가 성립한다. 결국, [eqn: H``]의 완전성에 의해 [eqn: H ( Gamma ^H , e', rho ^H ) ``]가 성공한다. 이는 즉, 에 [eqn: ( Gamma ^H , e', rho ^H )^u ``]이 있음을 말한다.

이제 [eqn: e'``]을 호출하는 경우, 즉, 접두 문자열이 [eqn: ( Gamma,e, beta) cdots( Gamma ^M ,e', rho ^M )^d ``]인 경우를 증명하자. [eqn: e'``]의 위치에 따라 여러 경우로 나누어 증명한다.

□[eqn: lambda x. e'``]의 [eqn: e'``]를 호출하는 경우: 접두 문자열이 어떤 [eqn: Gamma ^M ``], [eqn: rho ^M ``]에 대해

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M , lambda x. e', rho ^M )^d ``]이 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H , lambda x. e', rho ^H )^d ``]가 있고, 또한,

(12)

와 [eqn: R Gamma ^H ``succ` Gamma ^M ``]을 만족하는 [eqn: R``]이 존재한다. 이는 즉, 보조정리 6에 의해

(13)

를 의미한다. [eqn: R'``]을 라 하자. 그러면, [eqn: S_1 ^M R' ``]는 [eqn: rho ^H ``]와 [eqn: beta_1 ^H ``->` beta_2 ^H ``]를 동일화한다. 왜냐하면,

고로, 동일화에 성공하고 [eqn: S_1 ^M R'=R_1 S_1 ^H ``]를 만족하는 [eqn: R_1 ``]이 존재한다. 그러면,

가 성립하고, 또한

가 성립한다.

□[eqn: e'~e_2 ``]의 [eqn: e'``]를 호출한 경우: 접두 문자열이

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M , e'~e_2 , rho ^M )^d ``]가 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H , e'~e_2 , rho ^H )^d ``]가 있고, [eqn: R Gamma ^H ``succ` Gamma ^M ``]와 [eqn: R rho ^H = rho ^M ``]를 만족하는 [eqn: R ``]이 존재한다. [eqn: e'~e_2 ``]를 호출한 후 [eqn: e'``]를 호출하기까지 동일화 알고리즘을 사용 않으므로, 에 [eqn: ( Gamma ^H , e', beta_1 ^H ``->` beta_2 ^H )^d ``]가 있다. [eqn: R' ``]을 라 하면 [eqn: R'( beta_1 ^H ``->` beta_2 ^H ) = beta ^M ``->` rho ^M ``]가 성립하고, [eqn: beta_1 ^H , beta_2 ^H ``not in` ftv (Gamma ^H )]이므로 [eqn: R' Gamma ^H = R Gamma ^H ``succ` Gamma ^M ``]가 성립한다.

□[eqn: e_1 ~e' ``]의 [eqn: e'``]를 호출한 경우: 접두 문자열이

인 경우이다. 여기서 [eqn: beta ^M ``]은 (M.5)에서 생성한 새 타입 변수이다. 접두 문자열에 [eqn: ( Gamma ^M ,e_1, beta ^M ``->` rho ^M )^u ``]이 있으므로, [eqn: M ( Gamma ^M ,e_1, beta ^M ``->` rho ^M )]는 성공한다. [eqn: M``]의 안전성에 의해

(14)

가 성립한다. 접두 문자열에 [eqn: ( Gamma ^M ,e_1 e', rho ^M )^d ``]가 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H ,e_1 e', rho ^H )^d ``]가 있고

(15)

와 [eqn: R Gamma ^H ``succ` Gamma ^M ``]을 만족하는 [eqn: R``]이 존재한다. 이는 보조정리 6에 의해

(16)

임을 뜻한다. [eqn: R'``]을 로 두면, [eqn: S_1 ^M R'( beta_1 ^H ``->` beta_2 ^H )=S_1 ^M ( beta ^M ``->` rho ^M ) ``]이고 [eqn: S_1 ^M R' Gamma ^H =S_1 ^M R Gamma ^H ``][eqn: succ` S_1 ^M Gamma ^M ``]가 성립한다. 그러므로, 보조정리 7에 의해 (14)로부터

를 이끌어 낼 수 있다. 그러므로, [eqn: H``]의 완전성에 의해 [eqn: H ( Gamma ^H ,e_1, beta_1 ^H ``->` beta_2 ^H ) ``]에서 발생한 새 타입 변수의 집합을 [eqn: V``]라 할 때

(17)

을 만족하는 [eqn: R_1 ``]이 존재한다. 바로 이 [eqn: R_1 ``]이 (H.6)의 [eqn: S_1 ^H rho ^H ``]와 [eqn: S_1 ^H beta_2 ^H ``]를 동일화한다. 왜냐하면,

그러므로, [eqn: R_2 S_2 ^H = R_1 ``]인 [eqn: R_2 ``]가 존재하고 (17)로부터

(18)

를 이끌어 낼 수 있다. 그러면,

와

이 성립한다.

□[eqn: {rm let} ``x =e'``{rm i n}`` e_2 ``]의 [eqn: e'``]를 호출한 경우: 접두 문자열이 (M.7)에서 생성된 새 타입 변수를 [eqn: beta ^M ``]이라 할 때

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M , {rm let} ``x =e'``{rm i n}`` e_2 , rho ^M )^d ``]가 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H , {rm let} ``x =e'``{rm i n}`` e_2 , rho ^H )^d ``]가 있고, [eqn: R Gamma ^H ``succ` Gamma ^M ``]와 [eqn: R rho ^H = rho ^M ``]를 만족하는 [eqn: R``]이 존재한다. [eqn: H ``] 알고리즘은 [eqn: e'``]를 호출하기까지 동일화 알고리즘을 사용하지 않으므로, 에 [eqn: ( Gamma ^H , e', beta ^H )^d ``]가 있다. [eqn: R'``]을 라 두면, [eqn: R' beta ^H = beta ^M ``]이고, [eqn: beta ^H ``not in` ftv (Gamma ^H )]이므로 [eqn: R' Gamma ^H = R Gamma ^H ``succ` Gamma ^M ``]이다.

□[eqn: {rm let}``x=e_1 ``{rm i n}``e'``]의 [eqn: e'``]를 호출한 경우: 접두 문자열이

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M ,e_1 , beta ^M )^u ``]가 있으므로 [eqn: M ( Gamma ^M ,e_1 , beta ^M )``]는 성공한다. 그러므로, [eqn: M``] 알고리즘의 안전성에 의해

(19)

가 성립한다. 접두 문자열에 [eqn: ( Gamma ^M , {rm let} ``x =e'``{rm i n}`` e_2 , rho ^M )^d ``]가 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H , {rm let} ``x =e'``{rm i n}`` e_2 , rho ^H )^d ``]가 있고,

(20)

와 [eqn: R Gamma ^H ``succ` Gamma ^M ``]을 만족하는 [eqn: R ``]이 존재한다. 이는 즉, 보조정리 6에 의해

(21)

임을 뜻한다. [eqn: R'``]을 라 두면, [eqn: S_1 ^M R' beta ^H = S_1 ^M beta ^M ``]가 성립하고, [eqn: beta ^H `` not in ` ftv(Gamma ^H )``]이므로 (21)에 의해 [eqn: S_1 ^M R' Gamma ^H = S_1 ^M R Gamma ^H ``succ` S_1 ^M Gamma ^M ``]가 성립한다. 그러면, 보조정리 7에 의해 (19)로부터

를 이끌어 낼 수 있다. [eqn: H``] 알고리즘의 완전성에 의해

(22)

을 만족하는 [eqn: R_1 ``]이 존재한다. 그러면,

이고,

이다. 게다가

이다.

□[eqn: {rm fix} ``f ~lambda x.e'``]에 있는 [eqn: lambda x. e'``]를 호출한 경우: 접두 문자열이

인 경우이다. 접두 문자열에 [eqn: ( Gamma ^M , {rm fix} ``f ~lambda x.e', rho ^M )^d ``]가 있으므로, 귀납 가정에 의해 에 [eqn: ( Gamma ^H , {rm fix} ``f ~lambda x.e'`` , rho ^H )^d ``]가 있고, [eqn: R Gamma ^H ``succ` Gamma ^M ``]와 [eqn: R rho ^H = rho ^M ``]를 만족하는 [eqn: R``]이 존재한다. 그러면,

이 성립한다. □

참고 문헌

[1]	Robin Milner. A theory of type polymorphism in programming. Journal of Computer System Science, 17:348-375, 1978.

[2]	Luis Damas and Robin Milner. Principal type-scheme for functional programs. In  Proceedings of the 9th Annual ACM Symposium on Principles of Programming Languages, pages 207-212, New York, 1982. ACM.

[3]	Oukseh Lee and Kwangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):707--723, July 1998.

[4]	Xavier Leroy. The Caml Light system, release 0.6. Institut National de Recherche en Informatique et en Automatique, 1993.

[5]	J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of ACM, 12(1):23-41, January 1965.

[6]	Xavier Leroy. The Objective Caml system, release 2.02. Institut National de Recherche en Informatique et en Automatique, 1999.

[7]	Xavier Leroy. The Caml Light system, release 0.74. Institut National de Recherche en Informatique et en Automatique, 1997.

[8]	Michel Mauny. Functional programming using Caml Light, January 1995.

[9]	Paris C. Kanellakis, Harry G. Mairson, and John C. Mitchell. Unification and ML type reconstruction. In Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 382--401, 1990.