서 론

하향식 타입 유추 알고리즘 M의 속성 증명

(Proofs About a Folklore Let-Polymorphic Type Inference Algorithm M)

이 욱 세     이 광 근

(Oukseh Lee)  (Kwangkeun Yi)

요 약 Hindley/Milner 스타일의 복합형 타입 시스템(let-polymorphic type system)을 구현하는 타입 유추 알고리즘은 두 가지가 있다. 하나는 사실상 표준인 상향식(bottom-up) 알고리즘 W이고, 다른 하나는 하향식(top-down) 알고리즘 M이다. W 알고리즘은 안전성(soundness)과 완전성(completeness)이 수학적으로 검증되어 있고 가장 널리 쓰이기는 하지만, 타입 오류가 있는 입력 프로그램에 대해 때때로 모호한 메시지를 만들어 내는 문제점이 있다. 이에 M 알고리즘이 대안이 될 수 있는지를 확인할 필요가 있다. 하지만, 이 알고리즘은 단지 구현상에서 사용되었을 뿐, 정확하게 정의되어 있지 않고, 타입 시스템을 충실히 구현하는지(sound-and-completeness)도 증명되지 않았으며, W 알고리즘과 다른 점도 정확하게 규명되어 있지 않다. 본 논문에서는 M 알고리즘을 정확하게 기술하고, 복합형 타입 시스템을 충실히 구현함을 증명하며, 타입 오류가 있는 입력에 대해 W 알고리즘보다 신속히 타입 오류를 감지하는 성질을 증명한다. 본 논문에서의 증명은 실제 사용되었던 알고리즘에 대한 이론적인 검증인 것이다.

Abstract The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard W algorithm that is bottom-up or context-insensitive and the other is a folklore algorithm that is top-down or context-sensitive. Because the latter algorithm has not been formally presented with its sound-and-completeness proofs and its relation with the W algorithm has not been rigorously investigated, its use in place of or in combination with W could not be seen appealing.

In this paper, we formally define the context-sensitive, top-down type inference algorithm named M, prove its sound-and-completeness, and show a distinguishing property that M always stops earlier than W if the input program is ill-typed. Our proofs can be seen as theoretical justifications for various type-checking strategies in practice.

□ 본 연구는 한국과학재단 (과제번호 95-0100-54-3), 정보통신부 (과제번호 96151-IT2-12), 삼성전자, LG 정보통신의 지원을 받았음을 밝힙니다.

Hindley/Milner 복합형 타입 시스템(let-polymorphic type system)[1]을 구현하는 표준 타입 유추(type inference) 알고리즘인, W 알고리즘[1,2]은 너무 늦게 타입 오류를 감지하는 경향이 있다. 그림 1의 팩토리얼 함수 선언문의 경우, □fac(n-1)□로 작성해야 하는 곳에 □fac(n=1)□로 잘못 작성했다. 그림 1.(a)에서 W 알고리즘은 전체 프로그램을 오류 장소로 지적한다. W 알고리즘은 함수와 인자가 서로 충돌되는 타입으로 유추되었을 때에만 타입 유추에 실패한다. 즉, 함수와 인자의 타입이 따로 유추가 되고 나서야 타입 오류가 감지되는 것이다. 그러므로, 타입 오류 메시지는 함수와 인자를 모두 포함하는 부분을 지적해서 타입 오류가 있다고 알려 준다. 이러한 오류 메시지는 때때로 프로그램 작성자가 오류를 수정하는데 도움이 되지 못하는 경우가 많다. 함수와 인자가 차지하는 부분이 매우 클 수 있기 때문이다.

이와는 달리 CamlLight 0.61[3]에서 사용되었던 알고리즘(본 논문에서는 M이라 칭함)은 타입 오류를 신속히 감지한다. 그림 1.(b)의 예제와 같은 경우, M 알고리즘은 □=□ 만을 오류 장소로 지적하여 오류를 수정하는데 효과적인 오류 메시지를 제공한다. 그러나, M 알고리즘은 구현상에서만 사용되었을 뿐, 정확하게 정의되지 않았기 때문에, 타입 시스템(type system)을 충실히 구현한 것인지도 증명되어 있지 않다. 본 논문에서는 M 알고리즘이 W 알고리즘과는 어떻게 다른지를 정확하게 규명한다. 이를 위해, 2장에서는 M 알고리즘을 정확하게 정의하고 3장에서는 M 알고리즘이 타입 시스템을 충실히 구현함을 증명한다. 그리고, 4장에서는 타입 오류가 있는 입력 프로그램에 대해 M 알고리즘이 W 알고리즘보다 신속히 오류를 감지함을 증명한다.

M 알고리즘

개요

W 알고리즘은 Hindley/Milner 복합형 타입 시스템의 사실상 표준 알고리즘이다. W 알고리즘은 Hindley/ Milner 복합형 타입 시스템을 기초로 하고 있고 널리 쓰이고 있는, SML/NJ[4], CamlLight 0.71[5], Haskell[6] 등에서 사용하고 있다. W 알고리즘의 원리는 하위 표현식(sub-expression)의 타입을 유추한 정보를 모아서 상위 표현식(super-expression)의 타입을 유추하는 것이다. 예를 들어, 함수 적용문(application) □[eqn: e_1 ~e_2]□의 타입을 유추할 때, [eqn: e_1]과 [eqn: e_2]의 타입을 독립적으로 유추하고 나서, [eqn: e_2]의 타입이 [eqn: e_1]의 타입의 인자 타입이 되도록 동일화(unify)한다. 표현식 □([eqn: lambda]x.x+1) 1□을 보자. W 알고리즘은 우선 ([eqn: lambda]x.x+1)의 타입을 int[eqn: `->``]int 로 유추한다. 그리고 나서, 유추된 타입과 독립적으로 1의 타입을 int 로 유추한다. int 타입이 int[eqn: `->``]int 타입의 인자 타입이 될 수 있으므로, 전체 표현식을 int 타입으로 유추한다. 거시적으로, 각각의 하위 표현식을 독립적으로 유추하고 나서 상위 표현식의 타입을 유추하므로, 상향식(bottom-up) 알고리즘이라 할 수 있다.

#let rec fac n = if n=0 then 1 else n* fac(n=1);;

Toplevel input:

>let rec fac n = if n=0 then 1 else n* fac(n=1);;

>        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This expression has type int -> int,

but is used with type bool -> int.

(a) W 알고리즘 (CamlLight 0.71)

#let rec fac n = if n=0 then 1 else n*(fac(n=1));;

Toplevel input:

>let rec fac n = if n=0 then 1 else n*(fac(n=1));;

>                                           ^

Expression of type 'a -> 'a -> bool

cannot be used with type 'a -> 'a -> int

(b) M 알고리즘 (CamlLight 0.61)

그림 1: W 알고리즘과 M 알고리즘의 오류 메시지

그러나, W 알고리즘은 타입 오류를 늦게 감지한다. 표현식 □([eqn: lambda]x.x+1) true□의 경우를 보자. ([eqn: lambda]x.x+1)과 true를 독립적으로 타입 유추하여 int[eqn: `->``]int 타입과 bool 타입을 유추해 낸다. bool 타입은 int[eqn: `->``]int 타입의 인자 타입이 될 수 없으므로, 전체 표현식에서 오류를 발생한다. 그림 1과 같이 보다 복잡한 표현식에서 때때로 이러한 오류는 사용자가 오류를 수정하는데 도움이 되지 않는다.

W 알고리즘의 늦게 타입 오류를 감지하는 성질은 Hindley/Milner 복합형 타입 시스템을 갖춘 언어로 프로그램을 작성하는데 어려움을 주었고, 이를 해결하기 위하여 여러 방법이 개발되었다. 이러한 방법들로서 타입 유추 과정을 설명하는 방법[7,8,9,10], 타입 정보를 보여 주는 방법[10,11,12], 타입 오류 장소를 경험적으로(heuristic) 찾는 방법[13] 등이 개발되었으나, 근본적인 해결책은 제시하지 못하고 있다.

M 알고리즘은 이러한 문제를 해결할 수 있는 타입 유추 알고리즘으로 CamlLight 0.61[3] 등에서 실제적으로 사용되었다. 원리는 각각의 표현식(expression)이 가져야 할 타입의 조건을 항상 생각하면서, 이를 만족시키도록 타입 유추를 하는 것이다. 예를 들어, 함수 적용문 □[eqn: e_1 ~e_2]□가 int 조건으로 유추되어야 하는 경우, [eqn: e_1]은 [eqn: alpha~ ->`]int 조건 내에 유추되어야 하고, [eqn: e_2]는 [eqn: alpha``]가 [eqn: e_1]을 유추하면서 얻어진 타입 조건으로 유추되어야 한다. 이런 식으로 프로그램 내의 모든 식들에 대해 각각의 타입 조건을 만들어 가며 그 조건을 만족하도록 하는 것이다. 타입 조건을 만들어 간다는 것은 상위 표현식에서 알아낼 수 있는 타입 유추 정보를 최대한 모아서 하위 표현식의 타입 유추에 사용한다는 것이므로, 하향식(top-down) 알고리즘이라 할 수 있다.

M 알고리즘과 W 알고리즘의 근본적인 차이를 이해하기 위해 다음의 예제들을 살펴보자. 타입 오류가 없는 경우 과정은 다르지만 같은 결과를 낸다. 그러나, 타입 오류가 있는 경우 차이가 두각 된다.

예제 1 표현식 □([eqn: lambda]x.if x then 1 else 2) true□의 경우를 보자. W 알고리즘은 ([eqn: lambda]x.…)를 유추하여 bool[eqn: `->``]int 타입을 얻는다. 그리고 나서, true를 유추하여 bool 타입을 얻는다. bool 타입은 bool[eqn: `->``]int 타입의 인자 타입이 될 수 있으므로, 결과로 int 타입을 준다. M 알고리즘은 ([eqn: lambda]x.…)를 함수 조건, 즉 [eqn: alpha~->``beta] 조건으로 유추한다. 성공하여 bool[eqn: `->``]int 타입을 얻으면, 인자 타입인 bool 타입 조건으로 true를 유추한다. 성공하므로, 결과 타입인 int를 준다.

예제 2 표현식 □true false□의 경우를 보자. W 알고리즘은 각각을 타입 유추하여 bool 타입, bool 타입을 얻는다. true가 함수 타입이 아니므로 함수 적용(apply)을 할 수 없다. 그러므로, □true false□에서 오류를 발생한다. M 알고리즘은 true를 함수 조건으로 유추한다. 그러나, true는 함수 타입을 가질 수 없으므로, true에서 실패한다.

예제 3 그림 1의 경우를 보자. □fix f [eqn: lambda]n.if n=0 then 1 else n*f(n=1)□이 주어진 표현식이다. W 알고리즘은 f의 타입과 상관없이 [eqn: lambda]n.…를 유추한다. 그러면, f(n=1)에 의해 f의 타입이 bool[eqn: ->``beta]로 결정된다. 그러나, [eqn: lambda]n.…의 타입은 int[eqn: `->``]int로 유추된다. 두 타입은 동일화 할 수 없으므로, 전체 표현식에서 오류가 발생한다. 반면에 M 알고리즘은 f의 타입을 [eqn: alpha``]라 하고 [eqn: lambda]n.…를 [eqn: alpha``]조건으로 유추한다. [eqn: lambda]n.…를 유추할 때 n의 타입을 [eqn: beta``]라 하면, [eqn: alpha``] 타입으로 유추되어야 하므로 [eqn: alpha=beta~->``gamma``]가 된다. n=0을 유추할 때, [eqn: beta=]int로 결정된다. n=1을 유추할 때, f의 인자 타입인 int 타입 조건으로 유추하지만 □=□는 int를 결과 타입으로 줄 수 없다. 그러므로, □=□에서 오류가 발생한다.

예제를 통하여 볼 수 있듯이 M 알고리즘은 타입 오류를 신속히 감지한다. 신속히 타입 오류를 감지한다는 성질의 정확한 의미는 4장에서 살펴보기로 한다.

수식

사용된 수식은 다음과 같다. 특별한 표시가 없으면 [eqn: alpha``], [eqn: beta``], [eqn: gamma``], [eqn: delta``]는 타입 변수들을, [eqn: tau``], [eqn: rho``]는 타입을, [eqn: sigma``]는 타입 스킴(type scheme)을 [eqn: Gamma``]는 타입 환경(type environment)을, [eqn: P``], [eqn: R``], [eqn: S``]는 타입 치환 함수(substitution)를 의미한다. 벡터 [eqn: vec alpha``]는 [eqn: left{alpha_1 ,cdots,alpha_n right}]을, [eqn: FORALL vec alpha . tau``]는 [eqn: FORALL alpha_1 cdots alpha_n . tau``]를 줄여 표기한 것이다.

타입 환경(type environment)은 변수에서 타입 스킴으로의 매핑으로, [eqn: left{ x_1 ``mapsto`` sigma_1 ,cdots, x_n ``mapsto ``sigma_n right}]과 같이 표기한다. [eqn: Gamma`+x``:`sigma``]는 [eqn: left{ y``mapsto``sigma' ``|``x not= y, ~y ``mapsto`` sigma' in Gamma`` right} ``cup`left{ x``mapsto``sigma`right}]를 의미한다. 즉, 타입 환경 [eqn: Gamma``]에 변수 [eqn: x``]에 대한 이전의 매핑을 잊고 새로운 [eqn: sigma``]로의 매핑을 추가한 타입 환경을 의미한다.

[eqn: ftv``]는 자유 변수(free type variable)의 집합을 주는 함수이다. [eqn: ftv(tau`)]는 [eqn: tau``] 내의 모든 타입 변수들의 집합을 의미한다. [eqn: ftv(sigma`)]는 [eqn: sigma=FORALL vec alpha . tau``]이면 [eqn: ftv(sigma`)=ftv(tau`)\` vec alpha``]이다. [eqn: ftv(Gamma``)]는 [eqn: ``cup`_{x in dom(Gamma`)} `ftv(Gamma`(x))]이다.

타입 치환 함수(substitution)는 타입 변수에서 타입으로의 매핑으로, [eqn: left{ tau_1 / alpha_1 ,cdots, tau_n / alpha_n right}]으로 쓰거나, 줄여서 [eqn: left{ vec tau / vec alpha `right}]로 쓴다. 타입 치환 함수 [eqn: S=left{ vec tau / vec alpha `right}]에 대하여, [eqn: supp(S`)]는 [eqn: S``]의 지원 변수들(support type variable)의 집합을 의미하고, [eqn: left{ alpha``|``S` alpha not= alpha` right}]이다. [eqn: i nv(S`)]는 관련 변수들(involved type variable)의 집합을 의미하고, [eqn: left{ alpha ``|`` beta ``in` supp(S`),][eqn: alpha ``in` left{beta` right}``cup`ftv(S`beta`) right}]이다. 타입 [eqn: tau``]에 대하여 [eqn: S`tau``]는 [eqn: alpha ``in` ftv(tau`)]를 [eqn: S`alpha``]로 치환하여 얻어지는 타입을 의미한다. [eqn: S`sigma``]는 [eqn: vec beta ``cup`(inv(S`)``cup`ftv(sigma))=emptyset]인 어떤 [eqn: vec beta ``]에 대하여 [eqn: FORALL vec beta .S` left{ vec beta / vec alpha ` right}] 이다. [eqn: S`Gamma``]는 [eqn: left{ x``mapsto``S`alpha``|``x``mapsto``alpha``in`Gamma`` right}] 이다. [eqn: RS``]는 [eqn: S``]로 치환하고 나서 [eqn: R``]로 치환하는 타입 치환 함수를 의미한다. [eqn: R` vec alpha``]는[eqn: left{ R`alpha_1 ,cdots, R`alpha_n ` right}]를 줄여 표기한 것이다.

[eqn: Clos_Gamma ``(tau`)]는 Gen([eqn: Gamma``],[eqn: tau``])[2]와 같은 것으로, [eqn: vec alpha =][eqn: ftv(tau`)\` ftv(Gamma`)]라 할 때, [eqn: FORALL vec alpha . tau``]이다. 지네릭 인스턴스(generic instance)와 동일화(unification) 알고리즘 U는 정의 1과 정리 1에 있다.

정의 1 [2] 타입스킴 [eqn: sigma``], [eqn: sigma'``]에 대해 [eqn: sigma=FORALL vec alpha . tau``]이고 [eqn: sigma'=FORALL vec beta . tau'``]라 할 때, [eqn: supp(S`) `subseteq `vec alpha ``]이고 [eqn: tau'=S `tau``]를 만족하는 타입 치환 함수 [eqn: S``]가 존재하고, [eqn: ftv(sigma`) `subseteq` ftv(sigma')]이면, [eqn: sigma'``]를 [eqn: sigma``]의 지네릭 인스턴스라 하고, [eqn: sigma ``succ` sigma'``]로 표기한다. 타입 환경 [eqn: Gamma``], [eqn: Gamma`'`]에 대하여, [eqn: dom(Gamma`)=dom(Gamma`')]이고, [eqn: FORALL x`in`dom(Gamma`)]에 대해, [eqn: Gamma`(x)`succ`Gamma`'(x)]이면, [eqn: Gamma``succ`Gamma`']라 표기한다.

정리 1 [14] 두 개의 타입을 입력으로 받아, 다음 조건을 만족하는 타입 치환 함수을 주는 U 알고리즘은 존재한다.

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

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

정의

그림 2: 기반 언어, 타입 유추 규칙, W 알고리즘

그림 2가 기반 언어와 타입 시스템, 그리고, 기반 언어에 대한 W 알고리즘을 기술한 것이다. 동일화 과정이 함수 적용문에 있음을 주목하라.

그림 3이 그림 2의 타입 시스템에 대한 M 알고리즘을 정의한 것이다.  M 알고리즘은 표현식, 타입 환경, 타입 조건을 입력으로 받아, 타입 치환 함수를 결과로 준다. 타입 조건은 단순히 타입으로 나타낼 수 있다. 표현식의 유추된 결과 타입은 타입 조건에 타입 치환 함수를 적용하여 얻을 수 있다. M 알고리즘은 동일화 알고리즘을 사용하는 곳이 함수 적용문이 아니라, 상수, 변수, 함수 정의문이다. 변수의 경우(M.2), 주어진 타입 조건 [eqn: rho``]와 변수 [eqn: x``]의 타입 [eqn: Gamma`(x)``]가 같은 타입이 될 수 있어야 한다. 함수 정의문의 경우(M.3), 우선 주어진 타입 조건 [eqn: rho``]가 함수 타입인지 검사하여야 한다. 동일화 과정인

그림 3: M 알고리즘

[eqn: U`( rho, beta_1 `->` beta_2 ),~ \new ~ beta_1, beta_2``]	(M.3)

이 검사하는 작업이다. 함수 적용문의 경우(M.5), 주어진 타입 조건 [eqn: rho``]가 [eqn: e_1]의 타입 조건의 치역이 되어야 한다.

[eqn: M`( Gamma, e_1, beta `->` rho), ~\new ~beta``]	(M.5)

그리고, [eqn: beta``]가 [eqn: e_1]의 유추를 통해서 보다 구체적인 타입이 된 [eqn: S_1 `beta``]가 [eqn: e_2]의 타입 조건이 되어야 한다. let-문의 경우(M.7), [eqn: e_1]은 아무 조건 없이 유추된다.

[eqn: M`( Gamma, e_1 , beta), ~\new ~ beta``]	(M.7)

왜냐하면 어떠한 조건도 만들어 낼 수 없기 때문이다. [eqn: e_2]의 타입 조건은 [eqn: rho``]가 [eqn: e_1]의 유추를 통해서 보다 구체적인 타입이 된 [eqn: S_1 `rho``]가 된다. fix-문의 경우(M.9), [eqn: lambda x.e``]의 타입 조건은 주어진 타입 조건 [eqn: rho``]와 같다.

M 알고리즘의 안전성(soundness)과 완전성(completeness)

M 알고리즘은 주어진 타입 유추 규칙(type inference rule)을 충실히 구현(sound and complete)하고 있다. 타입유추 알고리즘이 타입 유추 규칙을 충실히 구현한다는 것은, 안전성과 완전성을 만족한다는 것을 의미한다. 안전성은 타입유추 알고리즘을 통해 얻어진 결과 타입이 타입 유추 규칙을 만족하는 성질을 말한다. 완전성은 타입 유추 규칙을 만족하는 타입을, 타입유추 알고리즘을 통해서도 얻을 수 있는 성질을 말한다.

M 알고리즘의 안전성은 다음과 같이 나타낼 수 있다.

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

안전성의 증명을 위해 보조정리 1과 보조정리 2가 필요하다.

보조정리 1 [2] 타입 치환 함수 [eqn: S``]에 대하여, [eqn: Gamma```vdash`e``:`tau``]이면 [eqn: S `Gamma ```vdash` e``:` S` tau``]이다.

보조정리 2 [15] 타입 치환 함수 [eqn: S``], 타입 환경 [eqn: Gamma``], 타입 [eqn: tau``]에 대하여, [eqn: vec alpha = ftv(tau)\` ftv(Gamma`)]이고, [eqn: vec beta ``]가 새 타입변수들이고, [eqn: S`']가 [eqn: S` left{ vec beta / vec alpha`right}]이면, [eqn: S`'Clos_Gamma `(tau)=Clos_{S`'Gamma}`(S`'tau)]이다.

정리 2의 증명. 표현식 [eqn: e``]의 구조에 대해 귀납적으로 증명할 수 있다.

[eqn: ()]의 경우: [eqn: S `rho=S `iota= iota``]이므로, [eqn: S`Gamma```vdash`()``:`S`rho``]는 (CON)을 만족한다.

[eqn: x``]의 경우: [eqn: S`rho=S`left{vec beta / vec alpha `right}tau``prec` S`Gamma`(x)]. 그러므로, (VAR)에 의하여 [eqn: S`Gamma```vdash` x``:`S`rho``]가 성립한다.

[eqn: lambda x.e``]의 경우:

(M.4)로부터 귀납가정에 의하여

[eqn: S_2 S_1 Gamma ``+` x``:`S_2 S_1 beta_1 `vdash`e``:`S_2 S_1 beta_2``]

가 성립한다. (FN) 규칙에 의하여 [eqn: S_2 S_1 Gamma ```vdash`][eqn: lambda x.e ``:`][eqn: S_2 S_1 beta_1 `->` S_2 S_1 beta_2]가 성립한다. 이것은 즉, (M.3)에 의하여 [eqn: S_2 S_1 Gamma```vdash`lambda x.e ``:`S_2 S_1 rho``]가 성립함을 말한다.

[eqn: e_1 ```e_2``]의 경우:

(M.5)로부터 귀납가정에 의하여 [eqn: S_1 Gamma```vdash` e_1``:`S_1 (beta`->`rho)]가 성립한다. 보조정리 1에 의하여 양쪽에 타입 치환 함수 [eqn: S_2``]를 적용시키면 다음식이 성립한다.

[eqn: S_2 S_1 Gamma```vdash` e_1``:`S_2 S_1 beta`->` S_2 S_1 rho``]

(M.6)으로부터 귀납가정에 의하여

[eqn: S_2 S_1 Gamma```vdash` e_2``:`S_2 S_1 beta``]

이 성립하면, 위 두식으로부터 (APP) 규칙에 의하여 [eqn: S_2 S_1 Gamma```vdash` e_1 ```e_2``:`S_2 S_1 rho``]이 성립한다.

[eqn: \let```x=e_1```\in```e_2``]의 경우:

(M.7)로부터 귀납가정에 의해 [eqn: S_1 Gamma```vdash` e_1``:`S_1 beta``]이 성립한다. [eqn: S_2 '=S_2 left{ vec beta / vec alpha ` right}``]라 하자. 단, [eqn: vec alpha = ftv(S_1 beta)\` ftv(S_1 Gamma`)``]이고 [eqn: vec beta``]는 새로운 타입 변수들이다. 보조정리 1에 의하면 양쪽에 [eqn: S_2 ']를 적용하면 다음 식이 성립한다.

[eqn: S_2 ' S_1 Gamma```vdash` e_1``:`S_2 'S_1 beta``]

(M.8)로부터 귀납가정에 의하여 [eqn: S_2 S_1 Gamma``+`][eqn: x``:`S_2 Clos_{S_1 Gamma}(S_1 beta)``vdash` e_2``:`S_2 S_1 rho``]이 성립한다. 이 식으로부터 보조정리 2와 [eqn: S_2 ' S_1 Gamma=S_2 S_1 Gamma``]라는 사실에 의하여 다음 식이 성립한다.

[eqn: S_2 'S_1 Gamma + x``:`Clos_{S_2 'S_1 Gamma}(S_2 'S_1 beta) ``vdash` e_2``:`S_2 S_1 rho``]

위 두식에 (LET) 규칙을 적용하면 [eqn: S_2 'S_1 Gamma```vdash`][eqn: \let ```x=e_1 ``` \in ```e_2 ``:`S_2 S_1 rho``]이 성립한다. 이것은 즉, 증명하고자 하는 식, [eqn: S_2 S_1 Gamma```vdash` \let```x=e_1``` \in```e_2``:`S_2 S_1 rho``]이 성립함을 말한다.

[eqn: \fix```f```x```e``]의 경우:

[eqn: S= M`(Gamma`+`f``:`rho,lambda x.e,rho)``]라 하자. 귀납가정에 의하여 (M.9)는

[eqn: S Gamma`+`f``:`S rho``vdash`lambda x.e``:`S rho``]

를 의미한다. (FIX)에 의하여 [eqn: S Gamma```vdash` \fix``` f``` x``` e`` :`S rho``]가 성립한다. □

M 알고리즘의 완전성은 다음과 같이 나타낼 수 있다.

정의 2 [eqn: P``□_V ``]는 타입 치환 함수 [eqn: P``], 타입 변수 집합 [eqn: V``]에 대하여, [eqn: P`□_V ``□` left{ tau / alpha ``in` P~|~alpha ``not in` V `right}]로 정의한다.

정리 3 (M 알고리즘의 완전성) 표현식 [eqn: e``], 타입 환경 [eqn: Gamma``]에 대해, [eqn: P Gamma`````vdash`` e````:``P rho``]를 만족하는 타입 [eqn: rho``]와 타입 치환 함수 [eqn: P``]가 존재하면, [eqn: M`(Gamma,e,rho)]가 [eqn: S``]를 결과값으로 성공하며, [eqn: M`(Gamma,e,rho)]에서 사용된 새 타입 변수들의 집합을 [eqn: V``]라 할 때, [eqn: P``□_V =(RS`)□_V ``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다.

완전성의 증명을 위해 보조정리 3-7이 필요하다. 보조정리 4, 6, 7의 증명은 부록에 있다.

보조정리[eqn: ``]3[eqn: ``][2] [eqn: Gamma`' succ Gamma``]이고 [eqn: Gamma```vdash` e``:`tau``]가 존재하면, [eqn: Gamma`'`vdash` e``:`tau``]도 존재한다.

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

보조정리[eqn: ``]5[eqn: ``][1] 타입 [eqn: tau``], [eqn: tau'``]에 대하여 [eqn: S=U`(tau,tau')]이면, [eqn: i nv(S`) `subseteq`][eqn: ftv(tau)``][eqn: cup` ftv(tau')]가 성립한다.

보조정리[eqn: ``]6 [eqn: S=M`(Gamma,e,rho)]이면, [eqn: V``]를 [eqn: M`(Gamma,e,rho)]에서 사용한 새 타입 변수들의 집합이라 할 때, [eqn: i nv(S) ``subseteq`ftv(Gamma`)``cup`ftv(rho)``cup` V``]이 성립한다.

보조정리[eqn: ``]7 [eqn: inv(S)``cap` A = emptyset]이면, [eqn: (RS`)□_A = R``□_A S``]가 성립한다.

정리 3의 증명. 표현식 [eqn: e``]의 구조에 대해 귀납적으로 증명할 수 있다. 새 타입 변수들에 대한 정확한 증명을 위해, M 알고리즘을 통해 사용된 모든 새 타입 변수들은 서로 구별된다고 하고, [eqn: M`(Gamma,e,rho)]에 의해 사용된 새 타입 변수들의 집합을 [eqn: V``]라 할 때, [eqn: V``cap`(ftv(Gamma`)``cup`ftv(rho))=emptyset]을 만족한다고 가정한다.

[eqn: ()``]의 경우:

주어진 가정이 [eqn: P Gamma```vdash`()``:`P rho``]라 하자. (CON)에 의하여 [eqn: P rho= iota``]이다. 즉, [eqn: P iota = iota = P rho``]이므로, [eqn: P``]는 [eqn: iota``]와 [eqn: rho``]의 동일화 함수(unifier)이다. [eqn: iota``]와 [eqn: rho``]의 동일화 함수가 존재하므로, [eqn: M`(Gamma,(),rho)]는 (M.1)에 의하여 [eqn: iota``]와 [eqn: rho``]의 가장 일반적인 동일화 함수 [eqn: S``]를 결과값으로 성공한다. 그러므로, [eqn: P=RS``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다.

[eqn: x``]의 경우:

주어진 가정이 [eqn: P Gamma```vdash`x``:`P rho``]라고 하고, [eqn: vec beta ``]를 (M.2)에서 사용된 새 타입 변수들이라 하자. 먼저, [eqn: rho``]와 [eqn: left{vec beta / vec alpha right} tau``]의 동일화 함수가 존재함을 증명해야 한다. 주어진 가정에 (VAR)를 적용하면

[eqn: P Gamma(x) `succ P rho``]	(1)

가 성립함을 알 수 있다. [eqn: Gamma`(x)] 를 [eqn: FORALL vec alpha . tau``]라 하고, [eqn: vec gamma ``]가 [eqn: ( ftv (Gamma`) ``cup` ftv (rho) ``cup` inv(P) ``cup` vec beta` ) ``cap` vec gamma = emptyset]를 만족하는 타입 변수들이라 하면,

[eqn: P Gamma`(x)= P FORALL vec alpha . tau = FORALL vec gamma .P` left{ vec gamma / vec alpha `right} tau``]	(2)

가 성립한다. (1)과 (2)에 의하여 [eqn: supp(B) ````subseteq`` vec gamma ``]이고

[eqn: BP left{ vec gamma / vec alpha ` right} tau = P rho ``]	(3)

을 만족하는 타입 치환 함수 [eqn: B ``]가 존재한다. (3)의 좌변은 [eqn: vec beta ````cap`` ftv( FORALL vec alpha . tau)= emptyset]이므로,

[eqn: BP left{ vec gamma / vec alpha ` right} tau = BP left{ vec gamma / vec beta ` right} left{ vec beta / vec alpha ` right} tau``]

와 같다. 또한 (3)의 우변은 [eqn: ftv( rho) ``cap`( vec beta ``cup` vec gamma )= emptyset]이고 [eqn: supp(B) `subseteq` vec gamma``]이므로,

[eqn: P rho = BP` left{ vec gamma / vec beta ` right} rho``]

와 같다. 그러므로, [eqn: BP` left{ vec gamma / vec beta ` right}]는 [eqn: rho``]와 [eqn: left{ vec beta / vec alpha ` right} tau ``]의 동일화 함수이다. [eqn: ( ftv (rho)`` cup` ftv( left{ vec beta / vec alpha ` right} tau)) ``cap` vec gamma = emptyset]이므로, [eqn: (BP left{ vec gamma / vec beta ` right})□_{ vec gamma} ``] 또한 [eqn: rho``]와 [eqn: left{ vec beta / vec alpha ` right} tau ``]의 동일화 함수이다. 즉, (M.2)는 [eqn: rho``]와 [eqn: left{ vec beta / vec alpha ` right} tau ``]의 가장 일반적인 동일화 함수 [eqn: S``]를 결과로 성공하며,

[eqn: RS= (BP left{ vec gamma / vec beta ` right})□_{ vec gamma} ``]	(4)

을 만족하는 타입 치환 함수 [eqn: R ``]이 존재한다. 그러므로,

[eqn: (RS)□_{ vec beta} &= (BP left{ vec gamma / vec beta ` right})□_{ vec gamma ``cup` vec beta} # &= (BP`)□_{ vec gamma ``cup` vec beta} # &= ( B□_{vec gamma} ``P`)□_{ vec beta} & ~~inv(P) ``cap` vec gamma = emptyset이고, # &&~~보조정리~ 7에 ~의해 # &= P``□_{ vec beta}& ~~왜냐하면~ supp(B) ``subseteq` vec gamma]

가 성립한다.

[eqn: lambda x.e``]의 경우:

주어진 가정이 [eqn: P Gamma`` `vdash` lambda x.e ``:` tau_1`->` tau_2]라 하자. 여기서, [eqn: tau_1 `->`tau_2]는 [eqn: P rho``]와 같다. [eqn: beta_1], [eqn: beta_2]가 (M.3)에서 사용된 새 타입 변수들이고, [eqn: V_1]를 (M.4)의 [eqn: M`(S_1 Gamma``+`x``:`S_1 beta_1 ,e,S_1 beta_2 )] 에서 사용한 새 타입 변수들의 집합이라 할 때, [eqn: V``]는 [eqn: left{ beta_1 , beta_2 right} ``cup` V_1]이다.

우선, (M.3)의 [eqn: U`( rho, beta_1 `->` beta_2 )]이 성공함을 증명해야 한다. [eqn: P`'= left{ tau_1 / beta_1 , tau_2 / beta_2 right}``cup` P``□_{left{ beta_1 , beta_2 right}}] 라 하자. 그러면,

[eqn: P`' rho &=& P rho & ~왜냐하면~ left{ beta_1, beta_2 right} ``cap` ftv( rho)= emptyset # &=& tau_1 `->` tau_2 # &=& P`'( beta_1 `->` beta_2 )]

이므로, [eqn: P`']은 [eqn: rho``]와 [eqn: beta_1 `->` beta_2]의 동일화 함수이다. 그러므로,

[eqn: P`' = R_1 S_1]	(5)

을 만족하는 타입 치환 함수 [eqn: R_1]은 존재한다. 주어진 가정으로부터 (FN)에 의하여

[eqn: P Gamma``+`x ``:` tau_1 ``vdash` e``:` tau_2]	(6)

이 성립한다.

(6)과 (M.4)의 [eqn: M`(S_1 Gamma``+`x``:`S_1 beta_1 ,e,S_1 beta_2 )]에 귀납 가정을 적용하기 위하여, [eqn: tau_2 =P_1 S_1 beta_2]와 [eqn: P Gamma``+`x ``:`tau_1 =][eqn: P_1 (S_1 Gamma``+`x ``:` S_1 beta_1 )]을 만족하는 타입 치환 함수 [eqn: P_1]이 존재함을 보여야 한다. (5)의 [eqn: R_1]은 [eqn: P_1]의 조건을 만족한다. 왜냐하면

[eqn: R_1 S_1 beta_2 &=&P`' beta_2&~~ (5)에~의해 # &=& tau_2]

이고,

[eqn: & R_1 (S_1 Gamma``+`x ````:`` S_1 beta_1 )# &=P`'( Gamma``+`x ````:`` beta_1 ) # &=P Gamma``+`x ````:`` tau_1&~ 왜냐하면~ left{ beta_1 , beta_2 right} ``cap` ftv( Gamma`)= emptyset]

이기 때문이다.

(M.4)와 (6)으로부터 귀납 가정에 의하여

[eqn: R_1 □_{V_1} = (R_2 S_2 )□_{V_1}]	(7)

을 만족하는 [eqn: R_2``]가 존재한다. [eqn: R=R_2]라 하면,

[eqn: (RS)□_V &=& (R_2 S_2 S_1 )□_V # &=& ((R_2 S_2 S_1 )□_{V_1})□_{ left{ beta_1, beta_2 right}}]

이 성립한다. 보조정리 5에 의해 [eqn: inv(S_1 ) ``subseteq`][eqn: ftv (rho) ``cup` left{ beta_1 , beta_2 right}]이고 [eqn: ( ftv(rho)``cup` left{ beta_1 , beta_2 right}) ``cap` V_1 = emptyset]이므로, [eqn: i nv(S_1 ) ``cap` {V_1}= emptyset]이다. 그러므로, 보조정리 7에 의하여 [eqn: (R_2 S_2 S_1 )□_{V_1} = (R_2 S_2 )□_{V_1} S_1]가 성립한다. 그러므로,

[eqn: (8) &=& ((R_2 S_2 )□_{V_1} S_1 )□_{ left{ beta_1 , beta_2 right}} # &=& ( R_1 □_{V_1} S_1 )□_{ left{ beta_1 , beta_2 right}} &~~ (7)에~의해 # &=& ((R_1 S_1 )□_{V_1})□_{ left{ beta_1 , beta_2 right}} &~~ 보조정리~7에~의해 # &=& (R_1 S_1 )□_V # &=& P`'□_V&~~(5)에~의해 # &=& P``□_V&~~ 왜냐하면~ left{ beta_1 , beta_2 right} ``subseteq` {V}.]

[eqn: e_1```e_2``]의 경우:

주어진 가정이 [eqn: P Gamma ``vdash` e_1 ``e_2 ``:`P rho``]라하고, [eqn: beta``]가 (M.5)에서 사용된 새 타입 변수이고, [eqn: V_1]와 [eqn: V_2]가 각각 (M.5)와 (M.6)의 M 함수 호출시 사용된 새 타입 변수의 집합이라 할 때, [eqn: V = beta ``cup` V_1 ``cup` V_2``]가 된다. 주어진 가정으로부터 (APP)에 의하여,

[eqn: P Gamma ```vdash` e_1``:` tau ```->` P rho]	(9)

[eqn: P Gamma ``vdash` e_2``:` tau``]	(10)

이다. [eqn: P`'= left{ tau / beta right} ``cup` P``□_beta ``]라 하자. [eqn: beta ``not in` ftv(Gamma`)``cup` ftv(rho)]이므로, [eqn: tau```->`P rho=P`'( beta```->`rho)]와 [eqn: P Gamma =P`' Gamma``]가 성립한다. 그러므로, (9)와 (M.5)로부터 귀납가정에 의하여,

[eqn: P`'□_{V_1} = (R_1 S_1 )□_{V_1}]	(11)

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

유사하게

[eqn: tau&=&P`' beta # &=&R_1 S_1 beta&~왜냐하면~ beta ``not in` V_1 이고, (11)에 의해# P Gamma&=&P`' Gamma&~ 왜냐하면~ beta ``not in` ftv (Gamma) # &=&R_1 S_1 Gamma&~ 왜냐하면~ftv(Gamma)``cap` V_1 = emptyset 이고, (11)에 의해]

이므로, (M.6)과 (10)으로부터 귀납가정에 의하여,

[eqn: R_1 □_{V_2}= (R_2 S_2 )□_{V_2}]	(12)

을 만족하는 타입 치환 함수 [eqn: R_2 ``]가 존재함을 증명할 수 있다.

[eqn: R=R_2 ``]라 하면,

[eqn: (RS`)□_V &=& (R_2 S_2 S_1 )□_V # &=& ((R_2 S_2 S_1 )□_{V_2})□_{V_1 ``cup` left{ beta `right}}``]

이 성립한다. 보조정리 6에 의하여 [eqn: i nv(S_1 ) ``subseteq` ftv(Gamma`)``cup` ftv(rho) ``cup` V_1 ``cup` left{ beta right}]이 성립한다. 그런데,[eqn: ( ftv( Gamma`) ``cup` ftv( rho)) ``cap` V_2 ``subseteq`( ftv( Gamma`) ``cup` ftv( rho)) ``cap` V= emptyset]이고, 모든 새 타입 변수들은 구별된다는 가정에 의해 [eqn: (V_1 ``cup`beta) ``cap`V_2 = emptyset]이므로, [eqn: i nv(S_1 ) ``cap` V_2 = emptyset]이 성립함을 알 수 있다. 그러므로, 보조정리 7에 의하여

[eqn: (13) &=& ( (R_2 S_2 )□_{V_2} S_1 )□_{V_1 ``cup` left{ beta right}} # &=& ( R_1 □_{V_2} S_1 )□_{V_1 ``cup` left{ beta right}} & ~~(12)에~의해 # &=& (R_1 S_1 )□_V&~~ 보조정리~ 7에~ 의해 # &=& ( (R_1 S_1 )□_{V_1})□_{V_2 ``cup` left{ beta right}} # &=& P`'□_V& ~~(11)에~ 의해# &=& P``□_V&~~ 왜냐하면~ beta`` in` V]

가 성립한다.

[eqn: \let```x=e_1```\in```e_2``]의 경우:

주어진 가정이 [eqn: P Gamma``vdash` \let```x=e_1 ```\in```e_2 ``:`P rho``]라 하자. [eqn: beta``]가 (M.7) 에서 사용된 새 타입 변수이고, [eqn: V_1], [eqn: V_2 ``]가 (M.7), (M.8)의 M 호출시 사용된 새 타입 변수들의 집합이라 할 때, [eqn: V = left{ beta right} ``cup` V_1 ``cup` V_2 ``]이라 하자.

주어진 가정으로부터 (LET)에 의하여

[eqn: P Gamma ```vdash` e_1``:` tau``]	(14)

[eqn: P Gamma``+`x ``:` Clos_{P Gamma} `tau ``vdash` e_2``:`P rho``]	(15)

이 성립한다.

[eqn: P`'= left{ tau / beta right} ``cup` P``□_{left{ beta `right}} ``]라 하자. [eqn: beta ``not in` ftv (Gamma`)]이므로, [eqn: tau=P`' beta``]이고, [eqn: P Gamma=P`' Gamma``]이다. 그러므로, (M.7)과 (14)로부터 귀납가정에 의하여

[eqn: P`'□_{V_1} = (R_1 S_1 )□_{V_1}]

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

[eqn: & Clos_{P Gamma} `(tau)# &= Clos_{P`' Gamma}`(P`' beta) # &= Clos_{R_1 S_1 Gamma}`(R_1 S_1 beta) & ~ (16)과~ ( ftv(Gamma`) ``cup` left{ beta right}) ``cap` V_1 = emptyset 에#&& ~의해# & prec R_1 Clos_{S_1 Gamma}`(S_1 beta) & ~보조정리~4에~ 의해]

이므로,

[eqn: P Gamma``+`x ``:` Clos_{P Gamma}`(tau) ``prec` R_1 (S_1 Gamma``+`x ``:` Clos_{S_1 Gamma}`(S_1 beta))]

이 성립한다. 보조정리 3과 (15)에 의하여,

[eqn: R_1 (S_1 Gamma``+`x ``:` Clos_{S_1 Gamma}(S_1 beta)) ``vdash` e_2``:`P rho``]

이 성립한다. [eqn: R_1 (S_1 rho)=P`' rho=P rho``]이므로, (M.8)과 (17)로부터 귀납가정에 의하여

[eqn: R_1 □_{V_2} = (R_2 S_2 )□_{V_2}]

를 만족하는 [eqn: R_2 ``]가 존재함을 증명할 수 있다. [eqn: R=R_2 ``]라 하면 □[eqn: e_1```e_2]□의 경우를 증명할 때와 같이, (16)과 (18)로부터

[eqn: P``□_V = (RS)□_V ``]

가 성립함을 증명할 수 있다.

[eqn: \fix```f```x```e``]의 경우:

주어진 가정이 [eqn: P Gamma ``vdash` \fix``` f``` x``` e``:`P rho``]라 하자. (FIX)에 의하여

[eqn: P Gamma``+`f ``:` P rho ``vdash` lambda x.e``:`P rho``]

이 성립한다. 귀납가정에 의하여 [eqn: M`( Gamma``+`f ``:` rho, lambda x.e, rho)]은 [eqn: S``]를 결과로 성공하고, [eqn: P``□_V = (RS)□_V ``]을 만족하는 [eqn: R``]이 존재한다. 여기서, [eqn: V``]는 (M.9)의 [eqn: M`( Gamma``+`f ``:` rho, lambda x.e, rho)]에서 사용한 새 타입 변수들의 집합이다. (M.9)에 의해 [eqn: M`( Gamma, \fix``` f``` x``` e, rho)``] 또한 [eqn: S``]를 결과로 성공하고, [eqn: P``□_V = (RS)□_V ``]가 성립한다. □

M 알고리즘의 신속한 오류 감지

타입 유추 알고리즘의 실행과정을 호출 문자열(call string)로 나타낼 수 있다. 어떤 표현식 [eqn: e``], 타입 환경 [eqn: Gamma``]에 대하여, [eqn: W`( Gamma,e)``]의 호출 문자열을 만드는 과정은 다음과 같다. 처음에 빈 문자열([eqn: epsilon``])으로 시작하여, 알고리즘이 실행되는 과정에서 W를 호출할 때의 인자를 순서대로 추가한다. 호출뿐만 아니라 귀환할 때도 호출할 때의 인자를 순서대로 추가한다. 호출과 귀환을 구별하기 위해 호출할 때는 [eqn: d``]를 귀환할 때는 [eqn: u``]를 위에 붙인다. 알고리즘이 실패하거나 성공할 때까지 계속 추가하고, 더 이상 추가할 수 없을 때, 만들어진 문자열을 호출 문자열이라 한다. 예를 들어 표현식

[eqn: e``]
(	(fn x=>x)	2)
	[eqn: e_1``]

에 대하여 [eqn: W`(Gamma,e)``]의 호출 문자열은

[eqn: ( Gamma,e)^d ( Gamma,e_1 )^d cdots ( Gamma,e_1 )^u ( Gamma,2)^d ( Gamma,2)^u ( Gamma,e)^u]

가 된다. [eqn: M`( Gamma,e, rho)``]의 호출 문자열도 유사한 방법으로 정의한다.

정의 3 [eqn: □W`( Gamma,e)□]은 [eqn: W`( Gamma,e)``]의 호출 문자열을 의미한다. 그리고, [eqn: □M`( Gamma,e, rho)□]는 [eqn: M`( Gamma,e, rho)``]의 호출 문자열을 의미한다.

[eqn: □W`( Gamma,e)□]와 [eqn: □M`( Gamma,e, rho)□]는 항상 유한함을 주목하라. 왜냐하면 각각의 하위 표현식(sub-expression)을 W와 M은 한 번씩만 호출하기 때문이다.

호출 문자열을 이용하여, M 알고리즘이 W 알고리즘보다 신속히 오류를 감지함을 다음과 같이 나타낼 수 있다.

정리 4 (신속한 오류 감지) 타입 환경 [eqn: Gamma``], 표현식 [eqn: e``], 새 타입 변수 [eqn: beta``]에 대하여,

[eqn: | □M`( Gamma,e, beta)□| ``<=` | □W`( Gamma,e)□|]

가 성립한다. 여기서 [eqn: |s|]는 호출 문자열 [eqn: s``]의 튜플의 수를 의미한다.

호출 문자열이 더 짧다는 것은 주어진 입력이 타입 오류를 가지는 경우, 신속히 실패한다는 것을 의미한다. 즉, 신속히 오류를 감지함을 의미한다.

예제 4 표현식 (([eqn: lambda]x.x^"a") true)의 경우를 보자. W 알고리즘은 (([eqn: lambda]x.x ^"a") true)의 하위 표현식들을 유추하고 나서 실패한다. 이에 비해 M 알고리즘은 true에서 실패한다.

예제 5 표현식 (1 (2 3))의 경우를 보자. W 알고리즘은 (2 3)에서 실패한다. M 알고리즘은 일찍 1에서 실패한다. 함수 적용문에서 1이 유추되고 나서 (2 3)이 유추됨을 주목하라.

예제 6 표현식 (([eqn: lambda]x.x+1) [eqn: lambda]y.(1 1))의 경우를 보자. W 알고리즘은 (1 1)에서 실패한다. M 알고리즘은 ([eqn: lambda]y.(1 1))에서 실패하는데, 이것이 호출되고 나서 (1 1)이 호출된다.

정리 4의 증명에서 보조정리 8-11이 사용된다.

보조정리 8 타입 환경 [eqn: Gamma``], [eqn: Gamma`'`], 타입 [eqn: tau``]에 대하여 [eqn: Gamma ``succ` Gamma`'``]이면 [eqn: Clos_Gamma `tau ``succ` Clos_{Gamma`` '} `tau``]이다.

증명 부록 D에 있다.

보조정리 9 [4] 타입 스킴 [eqn: sigma`], [eqn: sigma'], 타입 치환 함수 [eqn: S``]에 대하여, [eqn: sigma ``succ` sigma' ``]이면, [eqn: S sigma ``succ` S sigma'`]가 성립한다.

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

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

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

[eqn: e'``]이 □[eqn: lambdax.e``]□의 [eqn: e``]인 경우:

[eqn: lambda x.e``]가 호출 될 때의 각각의 타입 환경 인자가 [eqn: Gamma^W ``]와 [eqn: Gamma^M ``]라 하자. 우선 귀납가정에 의하여 [eqn: R Gamma^W ``succ` Gamma^M``]이 성립한다. 즉, 보조정리 9에 의하여 [eqn: S_1^M R Gamma^W ``succ` S_1^M Gamma^M ``]이 성립한다.  [eqn: R_1 = S_1^M ( R``□_{left{ beta right}} ``cup` left{beta_1^M / beta^W ``right})]라 하면

[eqn: R_1 ( Gamma^W `+`x``:` beta^W ) &=& S_1^M R Gamma^W `+`x``:`S_1^M beta_1^M # & succ&S_1^{ M} Gamma^{ M} `+`x``:`S_1^{ M} beta_1^{ M}]

가 성립한다.

[eqn: e'``]이 □[eqn: e_1```e_2]□의 [eqn: e_1``]인 경우: [eqn: e_1``]이 호출될 때의 타입 환경은 [eqn: e_1```e_2``]가 호출될 때와 같으므로 조건이 만족한다.

[eqn: e'``]이 □[eqn: e_1```e_2]□의 [eqn: e_2``]인 경우:

M 알고리즘의 안전성에 의하여 (M.5)로부터 다음 식을 이끌어 낼 수 있다.

[eqn: S_1^{ M} Gamma^{ M} ``vdash` e_1``:`S_1^{ M}( beta^{ M} `->` rho^{ M})]

귀납가정에 의하여 [eqn: R Gamma^{ W} ``succ` Gamma^{ M}``]가 성립하므로, 보조정리 9에 의하여 [eqn: S_1^{ M}R Gamma^{ W} ``succ` S_1^{ M} Gamma^{ M} ``]가 성립하고, 보조정리 3에 의하여 다음 식이 성립한다.

[eqn: S_1^{ M}R Gamma^{ W} ``vdash` e_1``:`S_1^{ M}( beta^{ M} `->` rho^{ M})``]

W 알고리즘의 완전성에 의하여 [eqn: R'S_1^{ W} Gamma^{ W} = S_1^{ M}R Gamma^{ W}``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다. 그러므로, [eqn: R' S_1^W Gamma^W = S_1^M R Gamma^W ``succ` S_1^M Gamma^M ``]가 성립하여 [eqn: e_2``]를 방문하는 경우가 증명된다.

[eqn: e'``]이 □[eqn: \let```x=e_1```\in```e_2``]□의 [eqn: e_1``]인 경우: [eqn: e_1``]이 호출될 때의 타입 환경은 [eqn: \let```x=e_1```\in```e_2``]가 호출될 때와 같으므로 조건이 만족한다

[eqn: e'``]이 □[eqn: \let```x=e_1```\in```e_2``]□의 [eqn: e_2``]인 경우:

M 알고리즘의 안전성에 의해 (M.7)로부터 다음 식을 이끌어 낼 수 있다.

[eqn: S_1^{ M} Gamma^{ M} ``vdash` e_1``:`S_1^{ M} beta^{ M}``]

귀납가정에 의하여 [eqn: R Gamma^{ W} ``succ` Gamma^{ M}``]가 성립하므로, 보조정리 9에 의하여 [eqn: S_1^{ M}R Gamma^{ W} ``succ` S_1^{ M} Gamma^{ M}``]가 성립한다. 이 사실과 위 식으로부터 보조정리 3에 의하여 다음 식이 성립한다.

[eqn: S_1^{ M}R Gamma^{ W} ``vdash` e_1``:`S_1^{ M} beta^{ M}``]

W 알고리즘의 완전성에 의하여 [eqn: R' tau_1^{ W} = S_1^{ M} beta^{ M}``]와 [eqn: R'S_1^{ W} Gamma^{ W} = S_1^{ M}R Gamma^{ W}``]을 만족하는 타입 치환 함수 [eqn: R'`]가 존재한다. 그러므로 다음과 같이 식을 전개할 수 있다.

[eqn: R'S_1^{ W} Gamma^{ W}``succ` S_1^{ M} Gamma^{ M}``]

그리고,

[eqn: &R' Clos_{S_1^{ W} Gamma^{ W}}(tau_1^{ W})# & succ ~ Clos_{R'S_1^{ W} Gamma^{ W}}(R' tau_1^{ W}) & 보조정리~4에~의하여# & = ~Clos_{S_1^{ M}R Gamma^{ W}}(S_1^{ M} beta^{ M}) # & succ ~ Clos_{S_1^{ M} Gamma^{ M}}(S_1^{ M} beta^{ M}) & 보조정리~8에~의하여]

위의 전개된 두 식은 [eqn: e_2``]를 방문하는 경우를 증명하고 있다.

[eqn: e'``]이 □[eqn: \fix```f```x```e``]□의 [eqn: e``]인 경우:

귀납가정에 의하여 [eqn: R Gamma^{ W} ``succ` Gamma^{ M} ``]을 만족하는 타입 치환 함수 [eqn: R``]이 존재한다. [eqn: R'= R``□_{ left{ beta^W ``right}} ``cup` left{ rho^M / beta^W ``right}``] 라 하면,

[eqn: R'( Gamma^{ W}`+`f``:` beta^{ W}) &=& R Gamma^{ W}+f``:` rho^{ M} # & succ& Gamma^{ M}``+`f``:` rho^{ M}]

가 성립한다. □

보조정리 11 표현식 [eqn: e``], 타입 환경 [eqn: Gamma``], 새 타입 변수 [eqn: beta``]에 대하여, [eqn: □W`(Gamma,e)□]에 [eqn: ( Gamma^W ,e' )^d ``]가 있고, [eqn: □M`( Gamma,e, beta)□]에 [eqn: ( Gamma^M ,e', rho)^d ``]가 있을 때, [eqn: □W`(Gamma^W ,e')□]가 실패하면, [eqn: □M`( Gamma^M ,e', rho)□]도 실패한다.

증명. [eqn: M`( Gamma^{ M},e', rho) ``]가 어떤 타입 치환 함수 [eqn: S``]를 결과로 성공한다고 가정하자. 그러면,  M 알고리즘의 안전성에 의해 다음 규칙이 성립한다.

[eqn: S Gamma^{ M} ``vdash` e'``:`S rho``]

보조정리 10에 의해, [eqn: R Gamma^{ W} ``succ` Gamma^{ M}``]을 만족하는 타입 치환 함수 [eqn: R``]이 존재한다. 보조정리 9에 의해 [eqn: SR Gamma^{ W} ``succ`` S Gamma^{ M}``]이 성립한다. 보조정리 3에 의해,

[eqn: SR Gamma^{ W} ``vdash` e'``:`S rho``]

이 성립하므로, W 알고리즘의 완전성에 의해, [eqn: W`( Gamma^{ W},e')``]가 성공한다. 이는 주어진 조건에 모순된다. 그러므로, [eqn: M`( Gamma^{ M},e', rho)``]는 실패한다. □

정리 4의 증명. [eqn: e``]에 타입 오류가 없을 때는 쉽게 증명된다. [eqn: |□W`(Gamma,e)□| = |□M`(Gamma,e,beta)□|]임이 명백하기 때문이다.

[eqn: e``]에 타입 오류가 있을 경우를 보자. [eqn: W`( Gamma,e) ``]가 [eqn: (e_1```e_2 )``]에서 실패한다고 하자. 그러면, [eqn: W`( Gamma,e)``]의 호출 문자열은 다음과 같은 형태이다.

[eqn: □W`( Gamma,e)□ = cdots ( Gamma_1^{ W},e_1```e_2 )^d cdots( Gamma_2^{ W},e_2 )^u``]

왜냐하면 W 알고리즘은 함수 적용문의 피연산자로부터 귀환하자마자 실패하기 때문이다.

다음을 가정하자.

[eqn: |□W`(Gamma,e)□| □ |□M`(Gamma,e,beta)□|]

그러면,

[eqn: □M`( Gamma,e, beta)□ = cdots( Gamma_1^{ M},e_1```e_2 , rho_1 )^d cdots( Gamma_2^{ M},e_2 , rho_2 )^u cdot kappa # ~ (단,~ kappa not= epsilon )]

와 같은 형태를 갖는다. 왜냐하면 하위 표현식을 방문하는 순서는 W나 M이나 같고, [eqn: e_2``]로부터 귀환한 다음 순서는 [eqn: e_1```e_2``]로부터 귀환하는 것이기 때문이다. 그러므로, [eqn: kappa``]는 [eqn: ( Gamma_1^{ M},e_1```e_2 , rho_1 )^u cdot kappa'``]의 형태이다. 이것은, 즉 [eqn: M`( Gamma_1^{ M},e_1```e_2 , rho_1 )``]이 성공함을 뜻한다. 그러나, [eqn: W`( Gamma_1^{ W},e_1```e_2 )``]가 실패하기 때문에, 보조정리 11에 의해, [eqn: M`( Gamma^{ M},e_1```e_2 , rho_1 )``]은 실패한다. 그러므로, 가정은 사실이 아니다.

결론

Hindley/Milner 타입 시스템의 표준 타입 유추 알고리즘인 W 알고리즘은 때때로 넓은 범위를 지적하는 오류 메시지를 준다. 이 문제를 해결하기 위한 한 방법으로, W 알고리즘과 다른 오류 메시지를 주는 타입 유추 알고리즘 M이 두각되었다. 그러나, M 알고리즘은, 정확하게 정의되지 않았고, 따라서 타입 시스템을 충실히 구현하는지 증명되지 않았고, W 알고리즘과 어떠한 다른 성질을 갖고 있는지 조사되지 않았다.

본 논문에서는 타입 유추 알고리즘 M을 정확하게 정의하고, 타입 시스템을 충실히 구현함을 증명하며, M 알고리즘이 W 알고리즘보다 신속히 타입 오류를 감지함을 증명하였다. 신속히 타입 오류를 감지한다는 것이 항상 오류 수정에 도움이 되는 오류 메시지를 제공한다고 말할 수 없다. 그러나, M 알고리즘이 W 알고리즘의 순서를 따르면서 보다 신속히 타입 오류를 감지한다는 성질로부터, 두 알고리즘의 오류 메시지의 조합이 어느 한쪽의 오류 메시지를 항상 보완한다는 것을 확인할 수 있다. M과 W를 조합해서 오류 메시지를 만들어 내는 프로그래밍 환경이 이미 구현되고 있고[10], 이 논문의 증명을 통해 그 방법의 효용성이 엄밀하게 입증된 셈이다.

부록

보조정리 4의 증명

[eqn: vec alpha = ftv(tau)\` ftv( Gamma`)``]이고, [eqn: vec beta``]를 [eqn: vec beta ``cap`( i nv(S) ``cup` ftv (tau))= emptyset]와 [eqn: | vec alpha | = | vec beta |``]를 만족하는 타입 변수들이라 하자. 그러면,

[eqn: S Clos_Gamma`(tau)= FORALL vec beta .S left{ vec beta / vec alpha right} tau]

가 성립한다. [eqn: R= left{ S vec alpha / vec beta right}``]라 하면, [eqn: S tau = RS left{ vec beta / vec alpha right} tau``]이고 [eqn: supp(R) ``subseteq` vec beta``]이다. 이것은 지너릭 인스턴스의 첫번째 조건을 만족하는 것이다. 두 번째 조건은 다음과 같이 전개하여 증명할 수 있다.

[eqn: ftv(S Clos_Gamma`(tau)) &=& bigcup_{ gamma`` in` ftv (tau) ``cap` ftv( Gamma`)} ftv(S gamma`) # & ``subseteq`& left( bigcup_{ gamma`` in` ftv(tau)} ftv(S gamma`) right) ``cap` left( bigcup_{ gamma ``in` ftv( Gamma`)} ftv(S gamma`) right) # &=& ftv(S tau) ``cap` ftv(S Gamma) # &=& ftv( Clos_{S Gamma}(S tau)).]

□

보조정리 6의 증명

증명을 위해 보조정리 12가 필요하다.

보조정리 12 [1] 타입 치환 함수 [eqn: R], [eqn: S], 타입 [eqn: tau``]에 대하여 다음이 성립한다.

[eqn: i nv(RS) ``subseteq` i nv(R) ``cup` i nv(S)]

[eqn: ftv(S tau) ``subseteq` ftv(tau) ``cup` i nv(S)]

표현식 [eqn: e``]의 구조에 대해 귀납적으로 증명한다.

()의[eqn: ``]경우: 보조정리 5에 의해 [eqn: i nv(U`( rho, iota)) ``subseteq`][eqn: ftv( rho )``cup` ftv( iota )``subseteq` ftv( rho)``]가 성립한다.

[eqn: x``]의 경우:

[eqn: &i nv(U`( rho,left{ vec beta / vec alpha right} tau)) # & subseteq`` ftv (rho) ``cup` ftv( left{ vec beta / vec alpha right} tau) &~~ 보조정리~ 5에~ 의해# & subseteq`` ftv( rho) ``cup`( ftv( tau)\`vec alpha ) ``cup` vec beta# &= `ftv( rho) ``cup` ftv( FORALL vec alpha . tau) ``cup` vec beta # &= `ftv( rho )``cup` ftv( Gamma(x)) ``cup` vec beta# & subseteq ``ftv( rho )``cup` ftv( Gamma`) ``cup` left{V right}.]

[eqn: lambda x.e``]의 경우: 보조정리 5에 의해

[eqn: i nv(S_1 ) ``subseteq` ftv( rho )``cup` ftv( beta_1 `->` beta_2 )]

가 성립한다. 귀납가정과 보조정리 12에 의하여

[eqn: i nv(S_2 ) & subseteq& ftv(S_1 Gamma``+`x ``:` S_1 beta_1 ) ``cup` ftv(S_1 beta_2 ) ``cup` left{V_1 right}# & subseteq& i nv(S_1 ) ``cup` ftv( Gamma`) ``cup` left{V_1 right} ``cup` left{ beta_1 , beta_2 right}]

가 성립한다. 그러므로,

[eqn: i nv(S_2 S_1 ) &subseteq& i nv(S_1 ) ``cup` i nv(S_2 ) #&subseteq& ftv (Gamma`) ``cup` ftv( rho) ``cup` left{V_1 right} ``cup` left{ beta_1 , beta_2 right}]

가 성립한다.

나머지 경우에도 비슷하게 증명할 수 있다. □

보조정리 7의 증명

모든 [eqn: alpha``]에 대해 [eqn: (RS)□_A alpha= R``□_A S alpha``]가 성립함을 보이면 된다.

[eqn: alpha`` in` A``]인[eqn: ``]경우: [eqn: (RS)□_A alpha = alpha``]이고, [eqn: i nv(S) ``cap` A= emptyset]이므로 [eqn: R``□_A S alpha = R``□_A alpha = alpha``]이다.

[eqn: alpha`` not in` A``]인[eqn: ``]경우: [eqn: (RS)□_A alpha = RS alpha``]이고, [eqn: ftv(S alpha) ``cap` A ``subseteq`][eqn: ( i nv(S) ``cup` left{ alpha right}) ``cap` A = emptyset]이므로 [eqn: R``□_A S alpha = RS alpha``]이다.

□

보조정리 8의 증명

정의에 따르면 [eqn: FORALL x ``in` dom( Gamma`) ``]에 대해 [eqn: Gamma`(x) succ` Gamma`'(x)``]이다. 이것은 [eqn: FORALL x ``in` dom( Gamma`) ``]에 대해 [eqn: ftv(Gamma`(x)) ``subseteq` ftv(Gamma`'(x))``]가 성립함을 말한다. 즉, [eqn: ftv(Gamma`) ``subseteq` ftv( Gamma`') ``]이므로,

[eqn: ftv( Clos_Gamma(tau)= ftv( tau) ``cap` ftv( Gamma`) ``subseteq` ftv( tau) ``cap` ftv( Gamma`') = ftv( Clos_{ Gamma`'}( tau))]

가 성립한다. □

참고 자료

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

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

[3]	Xavier Leroy. The caml light system, release 0.6, 1993.

[4]	David B. MacQueen and Andrew W. Appel. Standard ML of New Jersey. Technical memorandum, AT&T Bell Labs., 1993.

[5]	Xavier Leroy. The caml light system, release 0.7, 1995.

[6]	Paul Hudak, Simon L. Peyton-Jones, and Philip Wadler. Reports on the functional programming haskell.  ACM SIGPLAN Notices, 27(5), 1992.

[7]	Mitchell Wand. Finding the source of type errors. In Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 38-43, 1986.

[8]	Mike Beaven and Ryan Stansifer. Explaining type errors in polymorphic languages. In ACM Letters on Programming Languages and Systems, volume 2, pages 17-30, March-December 1993.

[9]	Dominic Duggan and Frederick Bent. Explaining type inference. Technical Report UW TR CS-94-14, University of Waterloo, Waterloo, Ontario N2L 3G1, Canada, 1994.

[10]	Laurence Rideau and Laurent Th□ry. Interactive programming environment for ML. Technical Report 3139, Institut National de Recherche en Informatique et en Automatique, March 1997.

[11]	Karen L. Bernstein and Eugene W. Stark. Debugging type errors (full version). Technical report, State University of New York at Stony Brook, 1995.

[12]	편기현. Standard ML 프로그램 식들의 유추된 타입들을 보여주는 도구의 개발. 석사 논문, 한국과학기술원, 1997.

[13]	Gregory F. Johnson and Janet A. Walz. A maximal-flow approach to anomaly isolation in unification-based incremental type inference. In Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 44-57, 1986.

[14]	J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23-41, January 1965.

[15]	Xavier Leroy. Polymorphic Typing of An Algorithmic Language. PhD thesis, Institut National de Recherche en Informatique et en Automatique, 1992.