서 론

일반화된 Let-다형성 타입 유추 알고리즘

(A Generalized Let-Polymorphic Type Inference Algorithm)

이 욱 세     이 광 근

(Oukseh Lee)  (Kwangkeun Yi)

요 약 본 연구에서는 일반화된 let-다형성(let-polymorphic) 타입 유추 알고리즘을 제시하고, 이로부터 얻어지는 모든 예 알고리즘들은 Hindley/Milner 타입 체계를 안전하고 완전하게 (sound and complete) 구현하고 있음을 증명하며, 일반화된 알고리즘의 두 예 알고리즘들간에 어느 한쪽이 항상 오류를 더 신속히 감지하게 되는 조건을 제시한다.

일반화된 알고리즘으로부터 이론적으로 검증된 두 타입 유추 알고리즘, 즉, 상향성 표준 타입 유추 알고리즘 W와 하향성 알고리즘 M 뿐만 아니라 두 알고리즘의 혼성 알고리즘(hybrid algorithm)을 만들 수 있다. 만들어진 예 알고리즘들의 안전성, 완전성, 상대적인 신속한 오류 감지 성질들은 본 논문의 증명에 의해 자동적으로 유추된다. 본 논문에서 제시하는 알고리즘으로부터 만들어 낼 수 있는 예 알고리즘에는 SML/NJ와 Objective Caml 컴파일러에서 채택한 알고리즘을 포함하고 있다.

Abstract We present a generalized let-polymorphic type inference algorithm, prove that any of its instances is sound and complete with respect to the Hindley/Milner let-polymorphic type system, and present a condition that one instance algorithm always detects type errors earlier than the other.

By instantiating the generalized algorithm with different parameters, we can obtain not only the two opposite algorithms (the bottom-up standard algorithm W and the top-down folklore algorithm M) but also other various hybrid algorithms that avoid their extremities in type-checking (W fails too late, while M fails too early). Such hybrid algorithms' soundness, completeness, and their relative earliness in detecting type-errors can be obtained automatically. The set of hybrid algorithms that come from the generalized algorithm is a superset of those used in the two most popular ML compilers, SML/NJ and OCaml.

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

Hindley/Milner let-다형성 타입 체계(let-polymorphic type system)[1]의 서로 다른 타입 유추 알고리즘, 즉, 상향성 표준 타입 유추 알고리즘 [eqn: W``][1,2,3]와 하향성 타입 유추 알고리즘 [eqn: M``][4,5]은 타입 유추에 있어 극단적이다. [eqn: W``] 알고리즘은 프로그램의 문맥에 영향 받지 않고(context-insensitive) 타입을 유추하므로 타입 오류를 늦게 감지한다. 반면에 [eqn: M``] 알고리즘은 최대한 문맥에 따라(context-sensitive) 타입을 유추하므로 신속히 오류를 감지한다. [eqn: W``] 알고리즘은 함수 적용(application)시 함수와 인자의 타입을 독립적으로 유추하고 나서 서로 충돌이 일어나는지 검사한다. 그렇기 때문에, 타입 오류가 있는 프로그램에 대해 실제 타입 오류가 있는 지점을 성공적으로 유추한 뒤 나중에 오류를 감지하게 되는 경우가 많다. 반면에, [eqn: M``] 알고리즘은 프로그램의 문맥을 보고 최대한의 정보를 실은 타입 조건(type constraint) 또는 기대 타입(expected type)을 만들어서 유추한다. 만들어진 기대 타입을 만족하지 않는 지점에서 멈추므로 때로 타입 오류가 있는 지점보다 일찍 오류를 감지하게 된다. 예를 들어, 함수 적용 □1 2□를 [eqn: W``]로 유추하면 1, 2를 각각 유추하고 나서 1에다 2를 적용할 수 없으므로 실패하고, [eqn: M``]으로 유추하면 1을 유추할 때 함수 타입을 기대하였는데 그렇지 않아 실패하게 된다.

실제 컴파일러 시스템에서는 극단적이지 않은 타입 유추 알고리즘이 필요한데, 이러한 혼성 알고리즘을 고안하는 체계적인 방법이 없다. 이미 SML/NJ[6]와 Objective Caml(이하 OCaml)[7]에서는 혼성 알고리즘(hybrid algorithm)을 사용하고 있는데, 이러한 알고리즘들의 안전성(soundness)과 완전성(completeness)도 증명되지 않았고, 또한 두 알고리즘이 어떻게 다른지도 알려지지 않았다. [eqn: M``] 알고리즘의 수행 속도 개선을 위해 제시한 [eqn: H``] 알고리즘[8,9]의 경우에도 일일이 안전성과 완전성을 증명해야 했고 또한 [eqn: M``]보다는 늦게 [eqn: W``]보다는 신속히 오류를 감지하는 성질을 증명해야 했다.

이러한 혼성 알고리즘을 체계적으로 고안하고 증명하기 위해서 (1) 어떻게 두 알고리즘을 섞어서 혼성 알고리즘을 고안하는지, (2) 고안된 알고리즘이 여전히 안전하고 완전한지, (3) 그리고 가능하다면 상대적으로 타입 오류를 신속히(또는 늦게) 감지하는지를 찾아낼 수 있는 체계가 필요하다.

본 연구에서는 일반화된 타입 유추 알고리즘을 제시하고, 이로부터 만들어 낼 수 있는 예 알고리즘이 항상 안전하고 완전함을 증명하고, 두 예 알고리즘 사이에 어느 한쪽이 항상 더 신속히 오류를 감지하는 조건을 제시한다. 제시된 일반화된 타입 유추 알고리즘으로부터 [eqn: W``], [eqn: M``]뿐만 아니라 여러 혼성 알고리즘을 만들어 낼 수 있으며, 이들의 안전성과 완전성은 자동적으로 증명된다. 또한, 간단한 조건만 증명함으로써 상대적으로 신속히 오류를 감지하는 성질도 자동적으로 이끌어진다. 일반화된 알고리즘으로부터 만들 수 있는 혼성 알고리즘에는 현재 널리 사용되고 있는 SML/NJ와 OCaml의 타입 유추 알고리즘과 [eqn: H``]도 포함하고 있다.

수식

사용된 수식은 다음과 같다. 특별한 표시가 없으면 [eqn: alpha``], [eqn: beta``], [eqn: gamma``]는 타입 변수(type variable)를, [eqn: tau``], [eqn: rho``], [eqn: theta``]는 타입을, [eqn: sigma``]는 타입 스킴(type scheme)을 [eqn: Gamma``]는 타입 환경(type environment)을, [eqn: P``], [eqn: Q``], [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 FORALL alpha_n .tau``]를, [eqn: R vec alpha``]는 [eqn: left{ R alpha_1 , cdots,R alpha_n right}``]를 줄여 표기한 것이다.

두 타입 스킴이 같다는 것은 구속 변수(bound variable)의 이름을 바꾸어 같아질 수 있음을 말한다. 자유 타입 변수(free type variable)는 구속되지 않은 타입 변수들로, 타입 스킴 [eqn: FORALL vec alpha . tau``]의 자유 타입 변수 집합 [eqn: ftv(FORALL vec alpha . tau)``]는 [eqn: ftv(tau)\ vec alpha ``]로 정의된다. 여기서 [eqn: ftv(tau)``]는 타입 [eqn: tau``]에 나타난 모든 자유 타입 변수들의 집합을 말한다.

타입 환경은 각 변수의 타입 스킴을 저장하고 있는 것으로 [eqn: left{ x_1 `` mapsto `sigma_1 , cdots x_n ``mapsto` sigma_n right}``]과 같이 표기한다. [eqn: Gamma``+`x``:`sigma``]는 타입 환경 [eqn: Gamma``]에서 변수 [eqn: x``]에 대한 이전의 타입 스킴을 버리고 새로운 [eqn: sigma``]로 바꾼 타입 환경을 의미하고, [eqn: left{ y ``mapsto` sigma' ``|`` x not=y,``y ``mapsto sigma' ``in`Gamma`` right} ``cup` left{ x ``mapsto` sigma right}]로 정의된다. 타입 환경 [eqn: Gamma``]의 자유 타입 변수 집합 [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``]에 대해, [eqn: supp(S)``]는 지원 변수(support)의 집합으로 [eqn: left{ alpha~|~S alpha not= alpha right}``]로 정의하고, [eqn: i tv(S)``]는 연루된 타입 변수의 집합으로 [eqn: left{ alpha ~|~beta in supp(S) , alpha in left{ beta right}``cup`` ftv (S beta) right}]로 정의된다. 타입 [eqn: tau``]에 대해 [eqn: S tau``]는 [eqn: tau``]에 있는 [eqn: S``]의 지원 변수 [eqn: alpha_i ``]를 [eqn: S(alpha_i )``]로 치환한 타입을 말하고, 타입 스킴 [eqn: sigma``]에 대해 [eqn: S sigma ``]는 자유 타입 변수만 치환하여 얻는 것을 말한다. 즉, [eqn: sigma``]가 [eqn: FORALL vec alpha . tau``]일 때 [eqn: vec beta ``cap`( i tv(S )``cup` ftv (sigma) )= emptyset``]를 만족하는 [eqn: vec beta ``]에 대해 [eqn: S sigma= FORALL vec beta . S left{vec beta / vec alpha right} tau ``]로 정의된다. 타입 환경 [eqn: Gamma``]에 대해 [eqn: S Gamma``]는 [eqn: left{ x ``mapsto `S sigma ~|~ x ``mapsto` sigma ``in` Gamma`` 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``]와 타입 변수 집합 [eqn: V``]에 대해 [eqn: P``□_V ``]는 [eqn: P``]와 같되 [eqn: V``]를 지원하지 않는 타입 치환 함수를 말하는 것으로 [eqn: left{ tau/alpha ``in` P~|~ alpha ``not in` V ``right}]로 정의된다.

타입 [eqn: tau``], 타입 스킴 [eqn: FORALL vec alpha . tau'``]에 대해 [eqn: S tau' = tau ``]이고 [eqn: supp (S) ``subseteq`` vec alpha``]를 만족하는 [eqn: S``]가 존재하면, [eqn: tau``]가 [eqn: FORALL vec alpha . tau'``]의 예(instance)라 하고 [eqn: FORALL vec alpha . tau ' ``succ` tau``]로 표기한다. 타입스킴 [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`]의 일반예(generic instance)라 하고 [eqn: sigma ``succ` sigma'``]로 표기한다. 또한 타입 환경 [eqn: Gamma``], [eqn: Gamma`'`]에 대해 [eqn: dom(Gamma`)=dom(Gamma`')]이고, 모든[eqn: x`in`dom(Gamma`)]에 대해 [eqn: Gamma`(x)`succ`Gamma`'(x)]일 때 [eqn: Gamma``succ`Gamma`']라 표기한다. [eqn: Clos_Gamma (tau)``]는 [2]의[eqn: rm G en(Gamma,tau)``]와 같은 것으로 [eqn: vec alpha = ftv (tau) □ ftv (Gamma)``]일 때 [eqn: FORALL vec alpha . tau``]로 정의된다.

타입 유추 알고리즘에는 다음 성질을 만족하는 동일화(unification) 알고리즘 [eqn: U``]가 사용된다.

정리 1 (동일화 알고리즘 [eqn: U``])[10]. 두 개의 타입을 입력으로 받아, 다음과 같은 타입 치환 함수를 주는 [eqn: 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)라 한다.

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

일반화된 타입 유추 알고리즘 G

개요

언어와 Hindley/Milner 타입 체계는 그림 1에 있고 타입 유추 알고리즘 [eqn: W``]와 [eqn: M``]은 그림 2에 있다.

일반화된 알고리즘은 하향성이고 문맥에 따라 유추하는 [eqn: M``] 알고리즘을 기반으로 한다. 핵심은 [eqn: M``] 알고리즘에서 두 가지 요소를 변경시킬 수 있도록 하는 것이다. 하나는 타입 조건에 실을 정보의 양이고 또 하나는 동일화 알고리즘의 위치이다. [eqn: M``] 알고리즘은 타입 조건에 가능한 많은 정보를 실어 보내고 각 상수, 변수, 함수에서 동일화한다. [eqn: W``] 알고리즘은 타입 조건에 정보를 실어 보내지 않으며 함수 적용과 재귀 함수 정의에서만 동일화한다. 이 두 가지 요소를 변경시킴으로써 여러 전략의 타입 유추 알고리즘을 만들 수 있다. 반면에 [eqn: W``] 알고리즘을 기반으로 하면 타입 조건을 입력으로 받지 않기 때문에 변경시킬 여지가 없다.

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

예제 1. 다음 프로그램의 타입을 유추하여 보자.

(IsOne 2) : bool

여기서 IsOne은 인자가 1인지 검사하는 함수로 타입이 [eqn: rm i nt ``->`bool ``]이다. 타입 조건을 점점 느슨하게 해 가면서 여러 방법으로 타입 유추해 보자.

□IsOne을 최대 조건인 [eqn: beta`` ->`rm bool``]로 타입 유추한다. 이 유추가 성공하고 나면 IsOne의 인자 타입은 int임을 알게 된다. 그러면, 2를 int 조건으로 유추한다. ([eqn: M``])

□보다 느슨한 조건인 [eqn: beta_1 ``-> `beta_2 ``]로 IsOne을 타입 유추한다. 여기서 [eqn: beta_1 ``], [eqn: beta_2 ``]는 새 타입 변수로 IsOne을 함수 조건으로 유추한다는 의미이다. 즉, 인자 타입이나 결과 타입은 상관없이 IsOne이 함수이기만 기대한다는 의미이다. 이 유추가 성공하고 나서 IsOne의 결과 타입이 bool인지 검사한다. 그리고 나서 IsOne의 인자 타입 int 조건으로 2를 유추한다. ([eqn: H``])

□이번에는 IsOne을 조건 없이 유추한다. 성공한 뒤 IsOne의 타입이 [eqn: rm beta ``->` bool``]인지 검사한다. 그리고 나서 IsOne의 인자 타입 int 조건으로 2를 유추한다. (OCaml)

그림 . 타입 유추 알고리즘 [eqn: W``]와 [eqn: M``]. 모든 새 타입 변수들은 서로 구별된다. 각 재귀 호출 [eqn: W(Gamma,e)``]에서 발생한 새 타입 변수의 집합 [eqn: V``]는 [eqn: V``cap`ftv(Gamma)=emptyset``]을 만족한다. 마찬가지로 각 재귀 호출 [eqn: M(Gamma,e,rho)``]에서 발생한 새 타입 변수의 집합 [eqn: V``]는 [eqn: V``cap`(ftv(Gamma)``cup`ftv(rho))=emptyset``]을 만족한다.

□IsOne을 조건 없이 유추한다. 성공한 뒤 IsOne의 타입이 함수인지 검사한다. 그리고, 2를 int 조건으로 유추한다. 그리고, IsOne의 결과 타입이 bool 인지 검사한다.

□마찬가지로 IsOne을 조건 없이 유추하고 IsOne의 타입이 함수인지 검사한다. 그러나, 2를 조건 없이 유추한다. 그리고 나서, IsOne의 인자 타입이 2의 타입인지, 그리고, IsOne의 결과 타입이 bool 인지 검사한다.

□IsOne을 조건 없이 유추한다. 그러나, IsOne의 타입을 검사하지 않는다. 2 또한 조건 없이 유추한다. 모든 유추가 성공하고 나서 IsOne의 인자 타입이 2의 타입인지 그리고, IsOne의 결과 타입이 bool인지 검사한다. ([eqn: W``])	□

위 예제에서 모든 타입 유추 방법들은 동일한 형태를 가지고 있다. 하위 프로그램의 타입을 유추하기 전 타입 조건을 느슨하게 만들고 그 유추가 성공하고 나면 느슨한 타입 조건을 보상해 준다. 즉, 느슨한 타입 조건으로 유추한 결과를 원래의 최대 조건으로 검사해 준다.

제시할 일반화된 타입 유추 알고리즘은 타입 조건을 느슨하게 만들 수 있도록 하고, 느슨하게 만들어진 타입 조건으로 유추된 결과를 나중에 보상하도록 하였다. 각 타입 유추 과정에서 하위 프로그램을 유추하기 전에 타입 조건을 느슨하게 만들 수 있다. 하위 프로그램의 유추가 끝난 후 느슨한 타입 조건을 동일화를 통하여 보상해 준다. 모든 하위 프로그램의 유추가 끝난 후에는 이전의 보상이 완전하지 않을 수도 있기 때문에 현재 프로그램의 유추가 끝나기 직전에 완전히 보상해 준다. 예를 들어 함수 적용문 [eqn: e_1 ~e_2 ``]를 [eqn: rho``] 조건으로 유추할 때, [eqn: e_1 ``]을 [eqn: beta ``->` rho``]보다 느슨한 조건으로 유추할 수 있다. 예를 들면 아무 조건 없이 유추할 수 있다. [eqn: e_1 ``]의 유추가 끝난 뒤 보상해 주는데 완전히 보상해 줄 필요는 없다. 예를 들면 결과가 함수인지만 검사한다. [eqn: e_2 ``]를 유추할 때도 역시 [eqn: e_1``]의 인자 타입보다 느슨한 조건으로 유추한다. 이 모든 과정이 끝난 후 느슨한 조건들을 모두 두 동일화를 통해 보상해 준다. 즉, [eqn: e_2 ``]의 타입이 [eqn: e_1``]의 인자 타입이 되는지 검사하고, [eqn: e_1``] 타입의 결과 타입이 [eqn: rho``]인지 검사해 준다.

그림 . 일반화된 타입 유추 알고리즘 [eqn: G``]. 각각의 [eqn: theta``>=`rho``]의 [eqn: ftv(theta)□ftv(rho)``]에 속하는 모든 타입 변수들은 새 타입 변수이다. 모든 타입 변수들은 서로 구별된다. 각 재귀 호출 [eqn: G(Gamma,e,rho)``]에서 발생한 새 타입 변수의 집합 [eqn: V``]는 [eqn: V``cap`(ftv(Gamma)``cup`ftv(rho))=emptyset``]을 만족한다.

알고리즘 정의

일반화된 타입 유추 알고리즘 [eqn: G``]는 그림 3에 있다. [eqn: M``]의 경우와 같이 프로그램, 타입 환경, 타입 조건을 입력으로 받아 타입 치환 함수를 결과로 준다. [eqn: G``]의 결과로 얻어진 타입 치환 함수를 입력으로 준 타입 조건에 적용하여 얻어지는 타입이 입력 프로그램의 타입이 된다.

[eqn: G``]에서 (1)에서 (6)까지 [eqn: theta``>=`rho``] 형식으로 표기한 곳이 타입 조건을 느슨하게 만드는 과정이다. 각 과정에서 가능한 최대 타입 조건 [eqn: rho``]로부터 느슨한 [eqn: theta``] 조건을 만들어 하위 프로그램에 넘겨준다. [eqn: rho``]로부터 얻어지는 느슨한 타입 조건 [eqn: theta``]란 [eqn: theta``]에 있는 타입 변수를 치환하여 [eqn: rho``]를 얻을 수 있는 타입 조건을 말한다.

정의 1 ([eqn: theta`` >=` rho``]). 두 타입 [eqn: theta``], [eqn: rho``]에 대해 [eqn: Q theta= rho``]와 [eqn: supp(Q) ``subseteq`` ftv (theta)□ftv(rho)``]를 만족하는 타입 치환 함수 [eqn: Q``]가 존재하면, [eqn: theta``]가 [eqn: rho``]보다 느슨한 타입이라고 하고 [eqn: theta``>=`rho``]라고 표기한다. 또한, 타입 [eqn: theta_1 ``], [eqn: theta_2 ``], [eqn: rho``]에 대하여 [eqn: Q theta_1 = Q theta_2 = rho``]이고 [eqn: supp(Q) ``subseteq` (ftv(theta_1 )``cup` ftv (theta_2 )) □ ftv (rho)``]를 만족하는 타입 치환 함수 [eqn: Q``]가 있을 때 [eqn: theta_1 ``wedge` theta_2 ``geq` rho``]라 표기한다.

변수의 경우(G.2), 변수 타입 [eqn: Gamma(x)``]는 주어진 타입 조건 [eqn: rho``]를 만족하여야 한다: [eqn: U(rho, left{ vec beta /vec alpha right} tau)``]. 상수의 경우(G.1)도 비슷하다.

함수 [eqn: lambda x.e``]의 경우를 살펴보자. 주어진 타입 조건이 [eqn: rho``]일 때, 먼저 함수의 내용(function body) [eqn: e``]를 유추할 타입 조건을 정해야 한다. 주어진 타입 조건 [eqn: rho``]와 같거나 느슨한 타입을 고른 후, 결정된 타입의 인자 타입과 결과 타입을 동일화를 통하여 얻는다.

[eqn: S_1 = U( beta_1 ``->` beta_2, theta)``], new [eqn: beta_1 ,~ beta_2 ``] (1) [eqn: theta ``geq` rho``]	(G.3)

얻어낸 타입의 결과 타입을 함수 내용의 타입 조건으로 넘겨준다.

[eqn: S_2 = G(S_1 Gamma+x` `:` S_1 beta_1 ,e,S_1 beta_2 )``]	(G.4)

예를 들어, [eqn: theta``]를 새 타입 변수로 결정하면, (G.3)의 동일화는 효과가 없어 결국 함수 내용의 타입은 아무 조건 없이 유추된다. 만약, [eqn: theta``]를 [eqn: rho``]로 결정하면 (G.3)는 주어진 조건 [eqn: rho``]가 함수인지 검사한 후 [eqn: rho``]의 결과 타입을 조건으로 하여 함수 내용을 유추한다. [eqn: e``]에 대한 유추가 끝난 뒤 느슨하게 만든 타입 조건을 보상해 주어야 한다. 유추의 마지막 과정은 느슨한 타입 조건으로 유추한 타입이 원래의 타입 조건을 만족하는지 검사하는 것이다.

[eqn: S_3 = U(S_2 S_1 theta, S_2 S_1 rho)]	(G.5)

함수 적용(application) [eqn: e_1 ~e_2 ``]의 경우를 살펴보자. 주어진 타입 조건이 [eqn: rho``]일 때, 우선 함수 부분 [eqn: e_1 ``]을 유추할 타입 조건을 결정해야 한다. 가장 정보가 많은 타입 조건 [eqn: beta ``->` rho``]보다 느슨한 타입이면 된다. 여기서, [eqn: beta``]는 새 타입 변수이다.

[eqn: S_1 = G( Gamma,e, theta_1 )], new [eqn: beta``], (2) [eqn: theta_1 ``geq` beta``->`rho``]	(G.6)

함수 부분의 타입이 성공적으로 유추되고 나서 인자 부분의 타입을 유추하기 전에 타입 조건을 느슨하게 한 것을 보상해준다. 그러나, 완전히 보상해 줄 필요는 없다. 이 보상은 함수 부분의 유추된 타입에 기대하는 정도를 조정할 수 있도록 하여 이루어진다. 최대 기대 타입인 [eqn: beta ``->` rho``]로 검사할 수도 있고 아무 것도 검사하지 않을 수도 있다. 이러한 조정 가능한 보상도 역시 [eqn: S_1 ( beta ``->` rho)``]보다 느슨한 타입 [eqn: theta_2 ``]를 골라서 [eqn: e_1 ``]의 타입과 동일화하여 이루어진다.

[eqn: S_2 = U(S_1 theta_1 , theta_2 ), ~~~~ (3)~ theta_2 ``geq` S_1 ( beta ``->` rho)``]	(G.7)

다음 순서로 인자 부분 [eqn: e_2 ``]의 타입을 유추하기 위한 타입 조건을 결정한다. [eqn: e_1 ``]의 인자타입인 [eqn: beta``]보다 느슨한 타입 [eqn: theta_3``]을 타입 조건으로 [eqn: e_2 ``]를 유추한다.

[eqn: S_3 = G(S_2 S_1 Gamma,e_2 , theta_3 ), ~~~~(4)~ theta_3 ``geq` S_2 S_1 beta]	(G.8)

마지막으로 모든 느슨함을 두 번의 동일화를 통하여 보상해 준다. 하나는 느슨하게 만든 타입 조건 [eqn: theta_1 ``]을 원래의 최대 타입 조건 [eqn: beta``->`rho``]로 검사하여 준다.

[eqn: S_4 = U(S_3 S_2 S_1 theta_1 ,S_3 S_2 S_1 ( beta ``->` rho))]	(G.9)

또 하나는 느슨하게 만든 타입 조건 [eqn: theta_3 ``]을 원래의 타입 조건, 즉, [eqn: e_1 ``]의 인자 타입으로 검사한다.

[eqn: S_5 = U(S_4 S_3 theta_3 ,S_4 S_3 S_2 S_1 beta)]	(G.10)

[eqn: theta_2 ``]는 이미 [eqn: theta_1 ``]과 (G.7)에서 동일화했고 (G.9)에서 [eqn: theta_1 ``]을 완전히 보상하였으므로 보상해 줄 필요가 없다.

[eqn: {rm let}~x = e_1 {rm i n}~e_2 ``]의 경우를 살펴보자. [eqn: e_1 ``]에 줄 수 있는 타입 조건은 없으므로 조건 없이 [eqn: e_1 ``]의 타입을 유추한다.

[eqn: S_1 = G( Gamma,e_1 , beta), {rm n ew} ~ beta]	(G.11)

다음으로 [eqn: e_2 ``]를 유추하기 위한 타입 조건을 결정한다. 주어진 타입 조건보다 느슨한 타입이면 된다.

[eqn: S_2 = G(S_1 Gamma+x ``:` Clos_{S_1 Gamma} (S_1 beta) ,e_2 , theta), ~ (5)~ theta ``geq` S_1 rho]	(G.12)

마지막으로 느슨한 타입 조건 [eqn: theta``]를 원래의 타입 조건으로 보상해 준다.

[eqn: S_3 = U(S_2 theta,S_2 S_1 rho) ``]	(G.13)

재귀 함수(recursive function) [eqn: rm fix it``f ~lambda x.e ``]의 경우를 살펴보자. 먼저 [eqn: lambda x.e ``]를 유추하기 위한 타입 조건과 [eqn: f``]의 타입을 결정해야 한다. 두 타입 모두 주어진 타입 조건 [eqn: rho``]보다 느슨한 타입이면 된다.

[eqn: S_1 = G( Gamma+f ``:` theta_1 , lambda x.e, theta_2 ), ~~~~ (6)~ theta_1 wedge theta_2 ``geq` rho``]	(G.14)

유추에 성공하고 나서 느슨한 타입들을 원래의 타입 조건으로 보상해 준다.

그림 . [eqn: G``]의 다섯 예 알고리즘. [eqn: beta_i``]는 모두 새 타입 변수이다.

[eqn: S_2 = U(S_1 theta_1 ,S_1 theta_2 ,S_1 rho)]	(G.15)

예 알고리즘

[eqn: G``]에서 느슨한 타입 조건을 결정함으로써 다양한 타입 유추 알고리즘을 얻을 수 있다. 예 알고리즘에는 표준 알고리즘 [eqn: W``], 하향성 알고리즘 [eqn: M``], 혼성 알고리즘 [eqn: H``], 그리고 SML/NJ와 OCaml에서 사용된 혼성 타입 유추 알고리즘을 모두 포함한다.

□모든 [eqn: theta``]를 새 타입 변수로 결정하면 [eqn: W``] 알고리즘이 된다.

□모든 [eqn: theta``]를 느슨하게 만들지 않으면, 즉, 최대 타입 조건으로 결정하면 [eqn: M``] 알고리즘이 된다.

□(G.6)의 (2)에서 타입 조건을 새 함수 타입([eqn: beta_1 ``->` beta_2 ``], 단, [eqn: beta_1 ``], [eqn: beta_2 ``]는 새 타입 변수)으로 하고 나머지는 느슨하게 하지 않으면 [eqn: H``] 알고리즘이 된다.

□(G.6)의 (2)에서 타입 조건을 새 타입 변수로 하고 나머지는 느슨하게 하지 않으면 OCaml의 타입 유추 알고리즘이 된다.

□SML/NJ의 타입 유추 알고리즘은 다음과 같다. (G.3)의 (1)에서 함수가 재귀 함수일 때는 최대 타입 조건으로 결정하고, 아니면 새 타입 변수로 결정한다. (G.14)의 (6)에서 [eqn: theta_1 ``], [eqn: theta_2 ``]를 같은 새 타입 변수로 결정한다. 나머지는 새 타입 변수로 결정한다.

위의 다섯 예 알고리즘의 타입 조건 [eqn: theta``]를 그림 4에 요약하였다.

안전성과 완전성

[eqn: G``]의 모든 예 알고리즘은 Hindley/Milner 타입 체계에 대해 안전하고 완전하다.

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

증명. 부록 A에 있음.

안전성은 프로그램 [eqn: e``]를 타입 조건 [eqn: rho``]로 [eqn: G``]에 의해 타입 유추하였을 때 성공하여 결과 [eqn: S``]를 주면, 타입 유추 규칙을 통하여 [eqn: e``]가 타입 [eqn: S rho``]를 가진다는 것을 말한다.

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

증명. 부록 B에 있음.

완전성은 프로그램 [eqn: e``]가 타입 조건 [eqn: rho``]를 만족하는 타입 [eqn: tau``]를 가지면(즉, [eqn: exists P. P rho = tau ``]), [eqn: G``] 알고리즘이 성공하고 결과로 [eqn: S``]를 주는데 [eqn: S rho``]가 [eqn: tau``]보다 일반적이라는 의미이다(즉, [eqn: exists R. RS rho = tau``]).

덜 느슨한 알고리즘이 신속히 오류를 감지한다

타입 조건에 실리는 정보의 양이 알고리즘이 얼마나 신속히 오류를 감지하는지를 결정한다. 보다 느슨한 타입 조건으로는 하위 프로그램을 성공적으로 타입 유추할 가능성이 높아지기 때문에 오류를 감지하는 시점이 연기된다.

[eqn: G``]의 두 예 알고리즘의 어느 한쪽이 항상 느슨한 타입 조건으로 결정할 때 보다 느슨한 알고리즘이라고 한다. □항상□의 의미는 각각의 느슨한 타입 조건을 결정하는 과정에서, 최대 기대 타입이 더 느슨하다면 결정된 타입 조건 또한 더 느슨하다는 뜻이다. 즉, [eqn: A``]의 타입 조건을 결정하는 [eqn: theta_i ``geq` rho_i``]와 이에 상대되는 [eqn: A'``]의 [eqn: theta_i ' ``geq` rho_i '``]에 대해 [eqn: rho_i '``]가 [eqn: rho_i``]보다 느슨하다면 [eqn: theta_i '``] 또한 [eqn: theta_i ``]보다 느슨하게 할 때 [eqn: A'``]를 보다 느슨한 알고리즘이라고 한다.

정의 2([eqn: A``sqsubseteq`A'``]). [eqn: A``], [eqn: A'``]이 [eqn: G``]의 예 알고리즘이라고 하자. [eqn: A( Gamma,e, rho)``] 도중의 [eqn: theta_i ``geq` rho_i ``]와 이에 상대되는 [eqn: A'( Gamma,e, rho)``] 도중의[eqn: theta_i ' ``geq` rho_i ' ``] 사이에, 만약 [eqn: rho_i =R rho_i '``]인 [eqn: R``]이 존재할 때, [eqn: theta_i = (R`□_supp(P) ``cup` P) theta_i '``]이고 [eqn: supp (P ) ``subseteq` ftv (theta_i ') □ ftv( rho_i ')``]를 만족하는 [eqn: P``]가 존재하면, [eqn: A'``]이 [eqn: A``]보다 느슨한 알고리즘이라 하고 [eqn: A``sqsubseteq`A'``]라고 표기한다.

그러면, 앞에 제시한 다섯 예 알고리즘들 사이에 느슨한 정도로 순서가 생긴다. [eqn: W``]가 가장 느슨하고 [eqn: M``]이 가장 느슨하지 않다.

보조정리 1. [eqn: M``sqsubseteq``H``sqsubseteq`rm OCaml] 알고리즘[eqn: ``sqsubseteq`{rm SML/NJ}] 알고리즘[eqn: ``sqsubseteq` W``].

증명. 부록 D에 있음.

타입 오류를 감지하는 시점은 호출 문자열(call string)[4]에 의해 엄밀히 살펴 볼 수 있다. [eqn: G( Gamma,e, rho)``]의 호출 문자열은, [eqn: □G( Gamma, e, rho)□]로 표기하며, 공백 문자열에서 시작해서, 매번 [eqn: G( Gamma_1 ,e_1 , rho_1 )]를 호출할 때는 [eqn: ( Gamma_1 ,e_1 , rho_1 )^ d ``]를 붙이고, 귀환할 때는 [eqn: ( Gamma_1 ,e_1 , rho_1 )^u ``]를 붙여 만든 문자열을 의미한다. 위첨자 [eqn: d``]와 [eqn: u``]는 각각 스택 포인터가 아래쪽으로(downward) 또는 위쪽으로(upward) 이동하는 것을 의미한다. [eqn: G``]의 모든 예 알고리즘의 호출 문자열은 유한함을 주목하라. 왜냐하면, [eqn: G``]의 모든 예 알고리즘은 각 하위 프로그램을 단 한 번만 호출하기 때문이다. [eqn: G``]의 모든 예 알고리즘의 호출/귀환 순서는 같다.

두 [eqn: G``]의 예 알고리즘 [eqn: A``], [eqn: A'``]에 대해 [eqn: A``]가 [eqn: A'``]보다 덜 느슨하면 타입 오류를 더 신속히 감지한다.

정리 4(상대적인 오류 감지의 신속성). [eqn: G``]의 두 예 알고리즘 [eqn: A``], [eqn: A'``]에 대해 [eqn: A``sqsubseteq` A'``]이면, 타입 환경 [eqn: Gamma_0 ``], 프로그램 [eqn: e_0 ``], 타입 [eqn: rho_0 ``]에 대해 [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]에 [eqn: ( Gamma,e, rho)^ d/u ``]가 있으면 [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□]에 [eqn: ( Gamma``',e, rho')^ d/u ``]가 있고, [eqn: R Gamma`' ``succ` Gamma``]이고 [eqn: R rho'= rho``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다.

증명. 부록 E에 있음.

하위 프로그램을 호출하고 귀환하는 순서는 같으므로 위의 정리는 즉, [eqn: A'``]가 [eqn: A``]보다 느슨하면 [eqn: A``]의 호출 문자열이 항상 같거나 짧다는 것을 의미한다. 호출 문자열이 짧다는 것은 더 일찍 멈춘다는 것을 의미하므로, 즉, 오류를 신속히 감지한다는 것이다.

보조정리 1과 정리 4에 의해, 제시된 다섯 예 알고리즘들 간에 오류를 신속히 감지하는 순서가 증명된다.

따름정리 1. 타입 환경 [eqn: Gamma``], 프로그램 [eqn: e``], 타입 [eqn: rho``]에 대해

[eqn: |□ M( Gamma,e, rho) □| &leq& | □ H( Gamma,e, rho)□ | # &leq& | □rm OCaml' rm s it ( Gamma,e, rho)□ | # &leq& | □rm SML/NJ' rm s it ( Gamma,e, rho)□ |# &leq& | □W( Gamma,e, rho)□ |]

가 성립한다. 여기서 |s|는 호출 문자열 [eqn: s``]의 길이이다.

결론

두 알고리즘 [eqn: W``]와 [eqn: M ``]은 Hindley/Milner let-다형성 타입 체계의 극단적 타입 유추 알고리즘이다. 사실상 표준인 [eqn: W``] 알고리즘은 문맥에 상관없이 타입을 검사하므로 타입 오류를 늦게 감지한다. 반면에 하향성 [eqn: M``] 알고리즘은 가능한 문맥을 모두 참고하여 타입을 검사하므로 타입 오류를 신속히 감지한다. 실제 컴파일러 시스템에서는 이러한 극단적인 행태를 피한 혼성 알고리즘이 필요하게 되는데 이를 위한 체계적인 방법론이 아직 연구되지 않았다.

본 연구에서는 타입 유추시 문맥을 참고하는 정도를 조절할 수 있도록 하여 일반화된 타입 유추 알고리즘을 제시하였다. [eqn: W``], [eqn: M``] 뿐만 아니라 다양한 혼성 알고리즘을 제시된 알고리즘의 예로 만들어 낼 수 있고, 예 알고리즘은 모두 타입 체계를 안전하고 완전하게 구현함을 증명하였다. 또한 예 알고리즘이 다른 예 알고리즘보다 상대적으로 신속히 오류를 감지하는 조건을 제시하였다. 결국 예 알고리즘의 안전성, 완전성, 상대적인 오류 감지의 신속성이 자동적으로 이끌어 낼 수 있게 되었다. [eqn: G``] 알고리즘의 예 알고리즘은 현재 널리 쓰이는 SML/NJ와 OCaml 컴파일러의 혼성 타입 유추 알고리즘까지 포함한다.

보다 일반화된 알고리즘을 만드는 방법은 타입 조건만 느슨하게 하는 것뿐만 아니라 타입 환경이나 타입 치환 함수까지 느슨하게 하는 방법이 있을 수 있다. McAdam의 알고리즘[11]은 [eqn: G``]의 예 알고리즘이 아닌데, 하위 프로그램들의 타입 유추 중 결과로 발생하는 타입 치환 함수를 누적하지 않고 타입 유추를 하다가 모든 하위 프로그램들의 유추가 끝나야만 비로소 타입 치환 함수들이 일관성이 있는지 검사한다. [eqn: G``] 알고리즘에서 그랬듯이 타입을 느슨하게 하는 것뿐만 아니라 누적되는 타입 치환 함수를 조절하게 하면 McAdam의 타입 유추 알고리즘까지 포함하는 일반화된 유추 알고리즘을 만들 수 있다. 이렇게 느슨한 타입 치환 함수는 [eqn: G``]가 그랬듯이 반드시 나중에 보상을 해 주어야만 한다.

보다 일반적인 방법[12,13,14,15,16]으로 타입 유추 알고리즘을 두 단계를 나누어서 생각하는 방법이 있다. (1) 동일화 조건들을 이끌어 내는 단계와 (2) 그 조건들을 푸는 단계를 따로 생각하는 방법이다. 그 관점에서 보면, [eqn: G``] 알고리즘은 동일화 조건을 푸는 순서를 정할 수 있는 조절 방법을 제시한 것이다. 타입 조건을 느슨하게 함으로써 동일화 조건을 푸는 것을 연기시키고 연기된 과정은 결국 나중에 보상 과정에서 풀도록 한 것이다.

부록

A. 정리 2의 증명

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

다음의 보조정리들을 사용한다.

보조정리 2[2]. [eqn: Gamma ``vdash` e``:` tau ``]이면 [eqn: S Gamma ``vdash` e``:`S tau``]이다.

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

보조정리 4[1]. 타입 [eqn: tau``], 타입 환경 [eqn: Gamma``], 타입 치환 함수 [eqn: S``]에 대해,[eqn: vec alpha =ftv(tau)□ftv(Gamma)``], [eqn: vec beta ``]는 새 타입 변수, [eqn: S'=S left{ vec beta / vec alpha right}``]라 하면, [eqn: S Clos_Gamma` ( tau) = Clos_S'Gamma` (S'tau)``]이다.

정리 2의 증명. [eqn: e``]의 구조에 대한 귀납법으로 증명한다.

□()의 경우: [eqn: S rho=S iota= iota``]. 그러므로 (CON) 규칙에 의해 [eqn: S Gamma ``vdash` () ``:`S rho ``]이 성립한다.

□[eqn: x``]의 경우: 보조정리 3에 의해 [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``]의 경우: 귀납 가정에 의해 (G.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` lambda x.e``:`S_2 S_1 ( beta_1 ``->` beta_2 )``]가 성립한다. 보조정리 2에 의해 양변에 [eqn: S_3 ``]를 적용하면

[eqn: S_3 S_2 S_1 Gamma ``vdash` lambda x.e``:`S_3 S_2 S_1 ( beta_1 ``->` beta_2 )]

가 성립한다. (G.3)에 의해 [eqn: S_1 ( beta_1 ``->` beta_2 )=S_1 theta ``]이고 (G.5)에 의해 [eqn: S_3 S_2 S_1 theta = S_3 S_2 S_1 rho``]이므로, [eqn: S_3 S_2 S_1 Gamma ``vdash``][eqn: lambda x.e``:`S_3 S_2 S_1 rho``]가 성립한다.

□[eqn: e_1 ~e_2 ``]의 경우: 귀납 가정에 의해 (G.6)은 [eqn: S_1 Gamma ``vdash`][eqn: e_1 ``:`S_1 theta_1]을 의미한다. 보조정리 2에 의해 [eqn: S_5 S_4 S_3 S_2 ``]을 양변에 취하면

[eqn: S_5 S_4 S_3 S_2 S_1 Gamma ``vdash` e_1 ``:`S_5 S_4 S_3 S_2 S_1 theta_1 ``]

가 성립한다. (G.9)에 의해 [eqn: S_4 S_3 S_2 S_1 theta_1 = S_4 S_3 S_2 S_1 (beta ``->][eqn: rho)``]이고, (G.10)에 의해 [eqn: S_5 S_4 S_3 S_2 S_1 beta =][eqn: S_5 S_4 S_3 theta_3 ``]이므로,

[eqn: S_5 S_4 S_3 S_2 S_1 Gamma ``vdash` e_1``:`S_5 S_4 S_3 ( theta_3 ``->` S_2 S_1 rho)``]	(7)

가 성립한다. 귀납 가정에 의해 (G.8)은 [eqn: S_3 S_2 S_1 Gamma ``vdash`][eqn: e_2 ``:`S_3 theta_3 ``]을 의미한다. 보조정리 2에 의해 양변에 [eqn: S_5 S_4 ``]를 적용하면

[eqn: S_5 S_4 S_3 S_2 S_1 Gamma ``vdash` e_2 ``:`S_5 S_4 S_3 theta_3]	(8)

가 된다. 그러므로 (7)과 (8)에 (APP)를 적용하면

[eqn: S_5 S_4 S_3 S_2 S_1 Gamma ``vdash` e_1 ~e_2 ``:`S_5 S_4 S_3 S_2 S_1 rho``]

가 성립한다.

□[eqn: {rm let}~ x=e_1 {rm i n}~ e_2]의 경우: [eqn: vec alpha = ftv(S_1 beta) □ ftv (S_1 Gamma)]이고 [eqn: vec beta``]는 (G.11)에서 발생한 새 타입 변수들일 때, [eqn: S_2 ' = S_2 left{ vec beta / vec alpha right}``]라 하자. 귀납 가정에 의해 (G.11)은 [eqn: S_1 Gamma ``vdash` e_1 ``:`S_1 beta``]이 성립한다. 보조정리 2에 의해 양변에 [eqn: S_2 '``]를 적용하면

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

가 성립한다. 귀납 가정에 의해 (G.12)는

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

를 의미한다. [eqn: S_2 '``]와 [eqn: S_2 ``]는 [eqn: S_1 Gamma ``]의 자유 타입 변수가 아닌 경우에만 다르므로 [eqn: S_2 S_1 Gamma = S_2 ' S_1 Gamma``]이고, 보조정리 4에 의해 [eqn: S_2 Clos_{S_1 Gamma``} (S_1 beta) = Clos_{ S_2 'S_1 Gamma``} (S_2 'S_1 beta)``]가 성립한다. 그러므로, (10)은

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

가 된다. (9)와 (11)에 (LET) 규칙을 적용하면 [eqn: S_2 'S_1 Gamma ``vdash{rm let} ~x=e_1 {rm i n}~ e_2 ``:`S_2 theta``]가 성립한다. 즉, [eqn: S_2 S_1 Gamma ``][eqn: vdash{rm let} ~x= e_1 {rm i n} ~e_2 ``:`S_2 theta``]가 성립한다. 보조정리 2에 의해 양변에 [eqn: S_3 ``]를 적용하면, [eqn: S_3 S_2 S_1 Gamma ``vdash`rm let~it x= e_1 {rm i n}~e_2 ``:][eqn: S_3 S_2 theta``]가 성립한다. (G.13)은 [eqn: S_3 S_2 theta = S_3 S_2 S_1 rho``]을 의미하므로

[eqn: S_3 S_2 S_1 Gamma ``vdash{rm let}~ x =e_1 {rm i n}~ e_2 ``:`S_3 S_2 S_1 rho``]

가 성립한다.

□[eqn: rm fix ``it f ~lambda x.e ``]의 경우: 귀납 가정에 의해 (G.14)는 [eqn: S_1 Gamma + f ``:` S_1 theta_1 ``vdash` lambda x.e``:`S_1 theta_2 ``]을 의미한다. 보조정리 2에 의해 양변에 [eqn: S_2 ``]를 적용하면

[eqn: S_2 S_1 Gamma + f ``:` S_2 S_1 theta_1 ``vdash` lambda x.e``:`S_2 S_1 theta_2 ``]

가 성립한다. (G.15)에 의해 [eqn: S_2 S_1 theta_1 =S_2 S_1 theta_2 =S_2 S_1 rho ``]이므로

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

가 성립한다. 여기에 (FIX) 규칙을 적용하면 [eqn: S_2 S_1 Gamma ``vdash` {rm fix}~ f~lambda x.e``:`S_2 S_1 rho``]가 성립한다. □

B. 정리 3의 증명

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

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

보조정리 5[4]. [eqn: S Clos_Gamma`` (tau) succ Clos_{S Gamma`` }(S tau)].

보조정리 6[2]. [eqn: Gamma``succ`Gamma``'``]인 타입 환경 [eqn: Gamma``], [eqn: Gamma``']에 대해 [eqn: Gamma``' ``vdash` e``:` tau``]이면 [eqn: Gamma ``vdash` e``:` tau``]이다.

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

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

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

보조정리 8. [eqn: S= G( Gamma,e, rho)]이면 [eqn: i tv(S) ``subseteq` ftv(Gamma )``cup` ftv (rho )``cup`][eqn: V``]이다. 단,[eqn: V``]는 [eqn: G(Gamma,e,rho)``]에서 발생한 새 타입 변수의 집합이다.

증명. 부록 C에 있음. □

보조정리 9[4]. [eqn: i tv(S) ``cap` V= emptyset``]이면 [eqn: (RS)□_V = R`□_V S``]이다.

정리 3의 증명. [eqn: e``]의 구조에 대한 귀납법으로 증명한다. 새 타입 변수에 대해 엄밀히 증명하기 위해 다음을 가정한다. [eqn: G``] 알고리즘에서 발생한 모든 새 타입 변수는 다르다. 각각의 호출 [eqn: G(Gamma,e,rho)``]에서 발생한 새 타입 변수들의 집합 [eqn: V``]는[eqn: V ``cap` ( ftv (Gamma) ``cup` ftv (rho))= emptyset``]를 만족한다. [eqn: theta ``>=` rho``]를 사용할 때마다 발생하는 [eqn: Q theta = rho``]를 만족하는 타입 치환 함수 [eqn: Q``]의 지원 변수 [eqn: supp(Q) =][eqn: ftv (theta)□ftv(rho)``]는 모두 새 타입 변수이다.

□[eqn: ()``]와 [eqn: x``]의 경우: [eqn: M``]의 증명과 같다. [4,5]

□[eqn: lambda x.e``]의 경우: 주어진 가정이 [eqn: P Gamma ``vdash` lambda x.e``:` tau_1 ``->` tau_2 ``]라 하자. 여기서, [eqn: tau_1 ``->` tau_2 =P rho ``]이다. 그리고, [eqn: V = left{ beta_1, beta_2 right} ``cup`][eqn: supp( Q) ``cup` V_1 ``]라 하자. 여기서, [eqn: beta_1 ``], [eqn: beta_2 ``]는 (G.3)의 새 타입 변수이고, [eqn: Q``]는 (G.3)의 [eqn: theta ``geq` rho``]에 대한 타입 치환 함수이며, [eqn: V_1 ``]은 (G.4)의 [eqn: G(S_1 Gamma+x ``:` S_1 beta_1 ,e,S_1 beta_2 ) ``]에서 발생한 새 타입 변수의 집합이다.

(G.3)의 [eqn: U( beta_1 ``->` beta_2 , theta)``]가 성공함을 증명하여야 한다. [eqn: P`' = (PQ)□_{left{ beta_1 , beta_2 right}} ``cup` left{ tau_1 / beta_1 , tau_2 / beta_2 right}``]라 하자. 그러면, [eqn: P`'``]은 [eqn: beta_1 ``->` beta_2 ``]와 [eqn: theta``]를 동일화한다. 왜냐하면,

[eqn: P`' theta & = & PQ theta & beta_1, beta_2 not in ftv( theta) 이므로 # & = & P rho & Q의~ 정의에 ~의해 # &=& tau_1 ``->` tau_2 & 가정에 ~의해 # &=& P`'( beta_1 ``->` beta_2 ) ~~ & P`'의~ 정의에 ~의해.]

이기 때문이다. 그러면 정리 1에 의해 (G.3)의 동일화는 성공하여 결과 [eqn: S_1 ``]을 주며

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

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

(FN) 규칙에 의해 주어진 가정은

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

를 의미한다. (G.4)의 [eqn: G(S_1 Gamma+x ``:` S_1 beta_1 ,e,S_1 beta_2 )``]과 (13)에 귀납 가정을 적용하기 위해 [eqn: tau_2 =P_1 (S_1 beta_2 )``]와 [eqn: P Gamma+x ``:` tau_1 =P_1 (S_1 Gamma+x ``:` S_1 beta_1 )``]를 만족하는 [eqn: P``]가 존재함을 보여야 한다. 그러한 [eqn: P_1 ``]은 (12)의 [eqn: R_1 ``]이다. 왜냐하면,

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

[eqn: &R_1 (S_1 Gamma+x ``:` S_1 beta_1 )~~ # &=~ P`'( Gamma+x ``:` beta_1 ) & (12)에~ 의해 # &=~ PQ Gamma+x ``:` tau_1 & beta_1, beta_2 not in ftv (Gamma)이므로 # &=~ P Gamma + x ``:` tau_1 & supp (Q) ``cap` ftv (Gamma) = emptyset이므로#]

이기 때문이다. 그러면 귀납 가정에 의해 (G.4)의 [eqn: G(S_1 Gamma + x ``:` S_1 beta_1 , e, S_1 beta_2 )]는 [eqn: S_2 ``]를 결과로 성공하며 다음을 만족하는 [eqn: R_2 ``]가 존재한다.

[eqn: (R_2 S_2 )□_V_1 = R_1 □_V_1 ``]	(14)

그러면,

[eqn: &i tv(S_1 ) # &subseteq` left{ beta_1 , beta_2 right}``cup` ftv (theta) & 정리~1에 ~의해# & subseteq` left{ beta_1 , beta_2 right}``cup` ftv (rho) ``cup`supp(Q)~& supp (Q) = ftv (theta) □ ftv (rho) # &&이므로]

가 성립하므로 [eqn: G``]의 정의에 의해

[eqn: V_1 ``cap` i tv( S_1 ) = emptyset``]	(15)

가 성립한다. 그러므로,

[eqn: &(R_2 S_2 S_1 )□_V_1 # &=`` (R_2 S_2 )□_V_1 S_1 & 보조정리 ~9와~ (15)에~ 의해 # &=`` R_1 □_V_1 S_1 & (14)에 ~의해 # &=`` (R_1 S_1 )□_V_1 & 보조정리 ~9와~ (15)에~ 의해# &=`` P`'□_V_1 & (12)에~의해]	[eqn: ##(16)]

가 성립한다.

이제 (G.5)의 동일화 [eqn: U(S_2 S_1 theta,S_2 S_1 rho)``]가 성공함을 증명할 차례이다.

[eqn: R_2 (S_2 S_1 theta) &=& P`' theta & (16)과 ~ftv (theta)`` cap` V_1 = emptyset 이므로 # &=& PQ theta & beta_1 , beta_2 not in ftv (theta) # &=& P rho & Q의 ~정의에 ~따라 # &=& PQ rho & ftv (rho) ``cap` supp(Q) = emptyset이므로# &=& P`' rho & beta_1 , beta_2 not in ftv (rho) # &=& R_2 (S_2 S_1 rho) & (16)과~ ftv (theta)`` cap` V_1 = emptyset 이므로]

이므로, [eqn: R_2``]는 [eqn: S_2 S_1 theta``]와[eqn: S_2 S_1 rho``]을 동일화한다. 그러므로, (G.5)의 동일화는 [eqn: S_3 ``]를 결과로 성공하며

[eqn: R_3 S_3 = R_2 ``]	(17)

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

결국, [eqn: G( Gamma, lambda x.e, rho)]는 [eqn: S_3 S_2 S_1 ``]를 결과로 성공하며 [eqn: (R_3 S_3 S_2 S_1 )□_V = P`□_V ``]이다. 왜냐하면,

[eqn: &(R_3 S_3 S_2 S_1 )□_V # & = `` (R_2 S_2 S_1 )□_V & (17)에 ~의해 # & = `` P`'□_V & (16)에~ 의해 # & = `` P`□_V & supp (Q) ``cup` left{ beta_1 , beta_2 right}``subseteq` V``이므로]

가 성립하기 때문이다.

□[eqn: e_1 ~e_2 ``]의 경우: 주어진 가정이 [eqn: P Gamma ``vdash` e_1 ~e_2``:`P rho``]이고

[eqn: V = left{ beta right} ``cup` supp( Q_1 )``cup` supp( Q_2 )``cup` supp( Q_3 )``cup`V_1 ``cup` V _2 ``]

라 하자. 여기서 [eqn: beta``]는 (G.6)의 새 타입 변수이고, [eqn: Q_1 ``], [eqn: Q_2 ``], [eqn: Q_3 ``]는 각각 (G.6)의 [eqn: theta_1 geq beta ``->` rho``], (G.7)의 [eqn: theta_2 ``geq` S_1 ( beta ``->` rho)``], (G.8)의 [eqn: theta_3 ``geq` S_2 S_1 beta``]의 타입 치환 함수이고, [eqn: V _1 ``], [eqn: V_2 ``]는 (G.6)의 [eqn: G( Gamma,e_1 , theta_1 )``]와 (G.8)의 [eqn: G(S_2 S_1 Gamma, e_2 , theta_3 )``]에서 발생한 새 타입 변수들의 집합이다. (APP) 규칙을 적용하면 어떤 타입 [eqn: tau``]에 대해

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

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

가 성립한다.

먼저 귀납 가정에 의해 (G.6)의 [eqn: G( Gamma,e_1 , theta_1 )``]이 성공함을 증명한다. [eqn: P`'= P`□_{left{ beta right}}``cup` left{ tau/ beta right}``]라 하자. 그러면

[eqn: P`'Q_1 theta_1 &=& P`'( beta ``->` rho) & Q_1 의~정의에~따라 # &=& tau ``->` P rho & beta ``not in` ftv (rho)]

이고, [eqn: ftv (Gamma )``cap`( supp (Q_1 )``cup` beta ) = emptyset``]이므로 [eqn: P`'Q_1 Gamma = P Gamma``]가 성립한다. 그러므로, (G.6)의 [eqn: G( Gamma,e_1 , theta_1 )``]과 (18)에 귀납 가정을 적용하면

[eqn: (R_1 S_1 )□_V_1 = (P`'Q_1 ) V_1 ``]	(20)

가 성립한다.

그러면 [eqn: R_1 Q_2 ``]가 (G.7)의 [eqn: S_1 theta_1 ``]와 [eqn: theta_2 ``]을 동일화한다. 왜냐하면,

[eqn: &ftv (S_1 theta_1 )``cap` supp (Q_2 ) # &subseteq ( i tv(S_1 ) `cup ftv( theta_1 )) ``cap` supp (Q_2 ) & 보조정리`` 7에`` 의해 # & subseteq ( ftv (Gamma) `cup V _1 `cup ftv (theta_1 )) `cap supp (Q_2 ) & 보조정리`` 8에`` 의해 # &= emptyset&~~~~~~~~~~~~~~~~(21)]

이므로

[eqn: &R_1 Q_2 (S_1 theta_1 ) # &=`` R_1 S_1 theta_1 & (21)에 ~의해 # &=`` P`'Q_1 theta_1 & ftv (theta_1 )``cap` V _1 = emptyset 이므로~ (20)에~ 의해# &=`` P`'( beta ``->` rho) & Q_1 의~정의에~따라 # &=`` P`'Q_1 ( beta ``->` rho) & ftv (beta ``->` rho)`` cap` supp (Q_1 ) = emptyset 이므로# &=`` R_1 S_1 ( beta ``->` rho) & ftv (beta ``->` rho )``cap` V _1 = emptyset 이므로 ~(20)에~ 의해 # &=`` R_1 Q_2 ( theta_2 ) & Q_2 의 ~정의에 ~따라]

가 성립하기 때문이다. 그러므로, 정리 1에 의해, (G.7)의 동일화는 [eqn: S_2 ``]를 결과로 성공하며 [eqn: R_2 S_2 = R_1 Q_2 ``]를 만족하는 [eqn: R_2 ``]가 존재한다. 그러면,

[eqn: &(R_2 S_2 S_1 )□_{supp(Q_2 ) ``cup` V_1 } # &= (R_1 Q_2 S_1 )□_{ supp (Q_2 ) ``cup` V_1 } # &= (R_1 S_1 )□_{ supp (Q_2 )``cup` V_1 } & supp (Q_2 )`` cap` i tv(S_1 )= emptyset``이므로 # &&보조정리~ 8에 ~의해 # &= (P`'Q_1 )□_{ supp (Q_2 )``cup` V_1 } & (20)에 ~의해~~~~~~~~~~~~~~~~~(22)]

가 성립한다.

(G.8)의 [eqn: G(S_2 S_1 Gamma,e_2 , theta_3 )``]와 (19)에 귀납 가정을 적용하기 위하여, [eqn: P_1 (S_2 S_1 Gamma)=P Gamma``]와 [eqn: P_1 theta_3 = tau``]를 만족하는 [eqn: P_1 ``]이 존재함을 보여야 한다. [eqn: R_2 Q_3 ``]가 그러한 [eqn: P_1 ``]이다. 이에 대한 증명은 다음과 같다. 우선,

[eqn: &ftv (S_2 S_1 Gamma` )# & subseteq`` i tv(S_2 )``cup` i tv( S_1 )``cup` ftv (Gamma`) & 보조정리~7에~ 의해 # & subseteq`` ftv (theta_2 )`cup ftv( theta_1 )`cup V _1 `cup ftv( Gamma `) & 정리 ```1과``` 보조정리 ``8에``` 의해]

이므로

[eqn: supp (Q_3 )``cap` ftv (S_2 S_1 Gamma )= emptyset``]	(23)

가 성립한다. 그러면,

[eqn: &R_2 Q_3 (S_2 S_1 Gamma) # &=`` R_2 S_2 S_1 Gamma & (23)에~ 의해# &=`` P`'Q_1 Gamma & ftv (Gamma )``cap`( supp (Q_2 )``cup` V _1 )= emptyset``이므로# && (22)에~ 의해 # &=`` P Gamma & ftv (Gamma)`` cap`(left{ beta right}``cup` supp( Q_1 ))= emptyset이므로 ## &R_2 Q_3 ( theta_3 ) # &=`` R_2 S_2 S_1 beta & Q_3 ``의~ 정의에~ 따라# &=`` P`'Q_1 beta & beta not in supp (Q_2 ) ``cup` V _1 이므로 ~(22)에~ 의해 # &=`` P`' beta & beta not in supp (Q_1) # &=`` tau & P`'의~ 정의에~ 따라]

가 성립한다. 그러면 귀납 가정에 의해 (G.8)은 [eqn: S_3 ``]를 결과로 성공하며

[eqn: (R_3 S_3 )□_V_2 = (R_2 Q_3 )□_V_2 ``]	(24)

를 만족하는 [eqn: R_3 ``]가 존재한다. 게다가

[eqn: (R_3 S_3 )□_{V_2 ``cup` supp (Q_3 )} = R_2 □_{V_2 ``cup` supp (Q_3 )}``]	(25)

를 만족한다.

그러면 [eqn: R_3 ``]가 (G.9)의 [eqn: S_3 S_2 S_1 theta_1 ``]과 [eqn: S_3 S_2 S_1 ( beta ``->` rho)``]를 동일화한다.

[eqn: & R_3 S_3 S_2 S_1 theta_1 # &= R_2 S_2 S_1 theta_1 & ftv( theta_1 )``cap`( V _2 ``cup` supp ( Q_3 ))= emptyset 이므로# && (25)에~ 의해 # &= P`'Q_1 theta_1 & ftv (theta_1 )``cap`( V _1 ``cup` supp (Q_2 ))= emptyset이므로 # &&(22)에~ 의해 # &= P`'( beta ``->` rho) & Q_1 의 ~정의에~따라 # &= P`'Q_1 ( beta ``->` rho) & ftv( beta ``->` rho )``cap` supp (Q_1 )= emptyset 이므로# &= R_2 S_2 S_1 ( beta ``->` rho) & ftv( beta ``->` rho )``cap`( V _1 ``cup` supp( Q_2 ))= emptyset이므로 #&&(22)에~ 의해# &= R_3 S_3 S_2 S_1 ( beta ``->` rho) & ftv (beta ``->` rho )``cap`( V _2 ``cup` supp( Q_3 ))= emptyset이므로# && (25)에~ 의해.]

그러므로, 정리 1에 의해, (G.9)의 동일화는 [eqn: S_4 ``]를 결과로 성공하며

[eqn: R_4 S_4 = R_3 ``]	(26)

를 만족하는 [eqn: R_4 ``]가 존재한다.

마지막으로 [eqn: R_4 ``]는 (G.10)의 [eqn: S_4 S_3 theta_3 ``]와 [eqn: S_4 S_3 S_2 S_1 beta``]를 동일화한다:

[eqn: &R_4 (S_4 S_3 theta_3 )# &=`` R_3 S_3 theta_3 & (26)에~ 의해# &=`` R_2 Q_3 theta_3 & ftv (theta_3 )``cap` V _2 = emptyset이므로~(24)에~의해# &=`` R_2 S_2 S_1 beta & Q_3 의~ 정의에 ~따라 # &=`` R_4 (S_4 S_3 S_2 S_1 beta) & beta not in V _2 ``cup` supp( Q_3 )이므로#&& (25), (26)에 ~의해.]

그러므로, (G.10)의 동일화는 [eqn: S_5 ``]를 결과로 성공하고

[eqn: R_5 S_5 =R_4 ``]	(27)

를 만족하는 [eqn: R_5 ``]가 존재한다. 결론적으로 [eqn: G( Gamma,e_1 ~e_2 , rho)``]는 [eqn: S_5 S_4 S_3 S_2 S_1 ``]를 결과로 성공한다.

이제 남은 것은 [eqn: (R_5 S_5 S_4 S_3 S_2 S_1 )□_V = P`□_V ``]를 증명하는 것이다. 보조정리 7, 8과 정리 1에 의해 [eqn: i tv( S_2 S_1 ) ``subseteq` ftv (Gamma )``cup` ftv( theta_1 )``cup` ftv( theta_2 )``cup` V _1 ``]가 성립하므로 알고리즘의 정의에 의해

[eqn: i tv(S_2 S_1 ) ``cap`( V _2 ``cup` supp (Q_3 ) )= emptyset``]	(28)

가 성립한다. 그러므로,

[eqn: &(R_5 S_5 S_4 S_3 S_2 S_1 )□_V # &=`` (R_4 S_4 S_3 S_2 S_1 )□_ V & (27)에~의해# &=`` (R_3 S_3 S_2 S_1 )□_V & (26)에 ~의해 # & =`` ((R_3 S_3 )□_{V_2 ``cup` supp (Q_3 )} S_2 S_1 )□_V & 보조정리~9와 ~(28)에~의해 # &=`` ( R_2 □_{V_2 ``cup` supp (Q_3 )} S_2 S_1 )□_V & (25)에~의해# &=`` (R_2 S_2 S_1 )□_V & 보조정리~9와~(28)에 ~의해# & =`` (P`'Q_1 )□_V & (22)에~의해# & = ``P`□_V & left{ beta right}``cup` supp (Q_1 ) ``subseteq` V``이므로]

가 성립한다.

□[eqn: rm let it~ x=e_1 ~rm i n ~it e_2 ``]의 경우: 주어진 가정이 [eqn: P Gamma ``vdash` rm let][eqn: x=e_1 ~rm i n ~it e_2 ``:` P rho``]이고, [eqn: V = left{ beta right}``cup` supp (Q) ``cup` V _1 ``cup` V _2 ``]라 하자. 여기서 [eqn: beta``]는 (G.11)의 새 타입 변수이고 [eqn: Q``]는 (G.12)의 [eqn: theta ``geq` S_1 rho``]의 타입 치환 함수이고, [eqn: V _1 ``], [eqn: V _2 ``]는 각각 (G.11)의 [eqn: G( Gamma,e_1 , beta)``]와 (G.12)의 [eqn: G(S_1 Gamma +][eqn: x ``:` Clos_{ S_1 Gamma }( S_1 beta) , e_2 , theta)``]에서 발생한 새 타입 변수의 집합이다. (LET) 규칙에 의해 어떤 타입 [eqn: tau``]에 대해

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

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

가 성립한다. [eqn: P`'= P`□_{left{ beta right}} ``cup` left{ tau/ beta right}``]라 하자. 그러면, [eqn: beta ``not in` ftv( Gamma )``]이므로 [eqn: P`' beta = tau``]이고 [eqn: P`' Gamma = P Gamma``]이다. 그러므로 (G.11)의 [eqn: G( Gamma,e_1 , beta)``]와 (29)에 귀납 가정을 적용하면

[eqn: (R_1 S_1 )□_V_1 = P`'□_V_1 ``]	(31)

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

[eqn: &R_1 Q(S_1 Gamma) # &=`` R_1 S_1 Gamma ~~& supp (Q)`` cap` ftv( S_1 Gamma )= emptyset이므로#&& 보조정리~ 7, 8에~ 의해# &=`` P`' Gamma & ftv (Gamma)`` cap` V _1 = emptyset이므로~(31)에~의해# &=`` P Gamma & beta not in ftv (Gamma) 이므로# # &R_1 Q( Clos_{ S_1 Gamma}( S_1 beta )) # & succ`` Clos_{ R_1 QS_1 Gamma}( R_1 QS_1 beta) & 보조정리~ 5에~ 의해# &=`` Clos_{ P Gamma} (R_1 S_1 beta) & supp(Q)``cap` ftv( S_1 beta) = emptyset 이므로#&& 보조정리~7, 8에~의해# &=`` Clos_{ P Gamma} ( P`' beta) & beta not in V _1 이므로 ~(31)에~의해# &=`` Clos_{ P Gamma} (tau) & P`'의 ~정의에 ~따라]

가 성립한다. 즉, [eqn: R_1 Q(S_1 Gamma+x ``:` Clos_{ S_1 Gamma} (S_1 beta )) ``succ` P Gamma +][eqn: x ``:` Clos_{ P Gamma }( tau)``]가 성립한다. 그러면, 보조정리 6과 (30)에 의해

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

가 성립한다.

(G.12)의 [eqn: G(S_1 Gamma + x ``:` Clos_{S_1 Gamma} (S_1 beta) , e_2 , theta)``]과 (32)에 귀납 가정을 적용하기 위하여 [eqn: R_1 Q theta = P rho ``]을 증명하여야 한다:

[eqn: R_1 Q( theta) &=& R_1 S_1 rho & Q의~ 정의에 ~의해# &=& P`' rho & ftv( rho)`` cap` V _1 = emptyset 이므로~(31)에~의해 # &=& P rho & beta not in ftv( rho)이므로.]

그러므로, 귀납 가정에 의하여 (G.12)의 [eqn: G(S_1 Gamma +][eqn: x ``:` Clos_{S_1 Gamma} (S_1 beta) , e_2 , theta)``]는 [eqn: S_2 ``]를 결과로 성공하고

[eqn: (R_2 S_2 )□_V_2 = (R_1 Q)□_V_2 ``]	(33)

를 만족하는 [eqn: R_2 ``]가 존재한다. 게다가 [eqn: R_2 ``]는 다음을 만족한다.

[eqn: (R_2 S_2 )□_{ supp( Q) ``cup` V_2 } = R_1 □_{ supp (Q) ``cup` V_2 }]	(34)

그러면, [eqn: R_2 ``]는 (G.13)의 [eqn: S_2 theta``]와 [eqn: S_2 S_1 rho``]를 동일화한다:

[eqn: R_2 (S_2 theta) &=& R_1 Q theta & ftv (theta) ``cap` V _2 = emptyset이므로 #&&& (33)에~ 의해# &=& R_1 S_1 rho & Q의~정의에~따라 # &=& R_2 (S_2 S_1 rho) & 보조정리 ~7, 8에 ~의해 #&&&ftv (S_1 rho) ``cap`( supp(Q) ``cup` V _2 )= emptyset #&&&이므로 ~(34)에 ~의해.]

그러므로 (G.13)의 동일화는 [eqn: S_3 ``]를 결과로 성공하며

[eqn: R_3 S_3 = R_2 ``]	(35)

를 만족하는 [eqn: R_3 ``]가 존재한다. 결론적으로 [eqn: G( Gamma,][eqn: rm let~ it x = e_1 ~rm i n~it e_2 , rho)``]는 [eqn: S_3 S_2 S_1 ``]를 결과로 성공한다.

마지막으로 [eqn: (R_3 S_3 S_2 S_1 ) □_V = P`□_V ``]만 증명하면 된다. 보조정리 8에 의해 [eqn: i tv( S_1 )``subseteq` ftv( Gamma )``cup` beta ``cup` V _1 ``]이므로 [eqn: Q``]의 정의에 따라

[eqn: i tv(S_1 ) ``cap`( supp (Q) ``cup` V _2 )= emptyset``]	(36)

가 성립한다. 그러므로,

[eqn: &(R_3 S_3 S_2 S_1 )□_V # &=`` (R_2 S_2 S_1 )□_V & (35)에~의해# &=`` ((R_2 S_2 )□_{ supp(Q) ``cup` V_2 } S_1 )□_V & 보조정리~9와 ~(36)에~ 의해# &=``(R_1 □_{ supp(Q) ``cup` V_2 } S_1 )□_V & (34)에~의해# &=``(R_1 S_1 )□_V & 보조정리~9와 ~(36)에~ 의해# &=`` P`'□_V & (31)에~ 의해# &=`` P`□_V & beta in V ``이므로]

가 성립한다.

□[eqn: rm fix ``it f ~lambda x.e]의 경우: 주어진 가정이 [eqn: P Gamma ``vdash` rm fix ``it f~lambda x.e``:][eqn: P rho ``]이고 [eqn: V = supp(Q) ``cup` V `'``]이라 하자. 여기서 [eqn: Q``]는 (G.14)의 [eqn: theta_1 ``wedge` theta_2 ``geq` rho``]의 타입 치환 함수이고, [eqn: V` '``]은 (G.14)의 [eqn: G( Gamma+f ``:` theta_1 , lambda x.e, theta_2 )``]에서 발생한 새 타입 변수의 집합이다. (FIX) 규칙에 의해 [eqn: P Gamma+f ``:` P rho ``vdash`][eqn: lambda x.e``:`P rho``]가 성립한다. [eqn: supp (Q) ``cap` ftv (Gamma)= emptyset``]이므로

[eqn: PQ Gamma+f ``:` PQ theta_1 ``vdash` lambda x.e``:`PQ theta_2 ``]

가 성립한다. (G.14)의 [eqn: G( Gamma+f ``:` theta_1 , lambda x.e, theta_2 )``]에 귀납 가정을 적용하면 [eqn: S_1 ``]을 결과로 성공하며

[eqn: (R_1 S_1 )□_{V`'} = (PQ)□_{V`'} ``]	(37)

를 만족하는 [eqn: R_1 ``]이 존재한다. 그러면, [eqn: R_1 ``]이 (G.15)의 [eqn: S_1 theta_1 ``], [eqn: S_1 theta_2 ``], [eqn: S_1 rho``]를 동일화한다:

[eqn: &R_1 (S_1 rho) # & = `` PQ rho & ftv (rho) ``cap` V` '= emptyset 이므로~(37)에~의해# & = ``P rho & ftv (rho)`` cap` supp (Q)= emptyset이므로 # & = `` PQ( theta_1 `` 또는 `` theta_2 ) & Q의~ 정의에~ 따라# & = `` R_1 (S_1 theta_1 `` 또는 ``S_1 theta_2 )& ( ftv (theta_1 )``cup` ftv (theta_2 )) ``cap` V `'= emptyset 이므로# && (37)에 ~의해.]

그러므로 (G.15)의 동일화는 [eqn: S_2 ``]를 결과로 성공하고

[eqn: R_2 S_2 = R_1 ``]	(38)

를 만족하는 [eqn: R_1 ``]이 존재한다. 결론적으로 [eqn: G( Gamma,][eqn: rm fix ``it f~lambda x.e, rho) ``]는 [eqn: S_2 S_1 ``]을 결과로 성공하고 [eqn: (R_2 S_2 S_1 )□_V][eqn: = P`□_V ``]를 만족한다. 왜냐하면,

[eqn: (R_2 S_2 S_1 )□_V &=& (R_1 S_1 )□_V & (38)에 ~의해 # &=&(PQ)□_V & (37)에~의해 # &=& P `□_V & supp (Q) ``subseteq` V ``이므로]

이기 때문이다. □

C. 보조정리 8의 증명

[eqn: e``]의 구조에 대한 귀납법으로 증명한다.

□[eqn: ()``]의 경우: 정리 1에 의해 [eqn: i tv( U( rho, iota) ) ``subseteq` ftv (rho) ``cup`][eqn: ftv( iota)= ftv (rho )]가 성립한다.

□[eqn: x``]의 경우:

[eqn: &i tv(U ( rho, left{ vec beta / vec alpha right} tau)) # & ``subseteq`` ftv (rho) ``cup` ftv( left{ vec beta / vec alpha right} tau) & 정리 ~1에~의해 # & 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 & Gamma(x)= FORALL vec alpha . tau ``이므로# & subseteq`` ftv( rho) ``cup` ftv( Gamma )``cup` vec beta .]

[eqn: vec beta``]는 [eqn: G( Gamma,x, rho)``]에서 발생한 새 타입 변수이다.

□[eqn: lambda x.e``]의 경우: [eqn: Q``]를 (G.3)의 [eqn: theta ``geq` rho``]의 타입 치환 함수라 하자. 가정에 의해 [eqn: supp( Q )``]는 모두 새 변수이다.

[eqn: i tv(S_1 )& subseteq & ftv (theta) ``cup` ftv (beta_1 ``->` beta_2 ) # &&~~~~~~~~정리~ 1에~ 의해# & subseteq & ftv (rho) ``cup` supp (Q) ``cup` left{ beta_1 , beta_2 right} # & &~~~~~~~~supp (Q)= ftv( theta)□ftv (rho)이므로,## i tv(S_2 ) & subseteq& ftv ( S_1 Gamma` )``cup` ftv( S_1 beta_1 )``cup` ftv (S_1 beta_2 )``cup` V _1 # &&~~~~~~~~ 귀납 ~가정에 ~의해# & subseteq& i tv( S_1 ) ``cup` ftv (Gamma`) ``cup` left{ beta_1 , beta_2 right} ``cup` V _1 # &&~~~~~~~~ 보조정리~ 7 에~의해]

가 성립한다. 여기서, [eqn: V_1``]은 (G.4)의 [eqn: G(S_1 Gamma+x ``:` S_1 beta_1 ,][eqn: e,S_1 beta_2 )``]에서 발생한 새 타입 변수이다. 그리고,

[eqn: &i tv(S_3 ) # & subseteq`` ftv (S_2 S_1 theta )``cup` ftv( S_2 S_1 rho ) & 정리~1에~의해# &subseteq`` i tv(S_2 )``cup` i tv( S_1 )``cup` ftv( theta )``cup` ftv( rho )& 보조정리~ 7에 ~의해# & subseteq`` i tv(S_2 ) ``cup` i tv( S_1 ) ``cup` supp (Q) ``cup` ftv( rho)]

가 성립한다. 그러므로, [eqn: i tv( S_3 S_2 S_1 ) ``subseteq` ftv( Gamma `)``cup` ftv( rho )``cup`][eqn: ( supp( Q) ``cup` left{ beta_1 , beta_2 right}``cup` V _1 )``]가 성립한다. 여기서, [eqn: supp (Q)][eqn: cup`left{ beta_1 , beta_2 right}``cup` V _1]은 [eqn: G( Gamma, lambda x.e, rho)]에서 발생한 새 타입 변수이다.

다른 경우도 비슷하게 증명된다. □

D. 보조정리 1의 증명

보조정리 1. [eqn: M``sqsubseteq``H``sqsubseteq`rm OCaml] 알고리즘[eqn: ``sqsubseteq`{rm SML/NJ}] 알고리즘[eqn: ``sqsubseteq` W``].

증명. 바로 인접한 예 알고리즘들간에 증명하면 된다.

□[eqn: M``sqsubseteq` H ``]의 증명: 두 알고리즘은 (G.6)의 (2)에서만 다르다. [eqn: M``]은 [eqn: beta ``->` rho``geq`` beta ``->` rho``]이고 [eqn: H``]는 [eqn: beta' ``->` beta_2 ' ``geq`][eqn: beta' ``->` rho'``]이다. [eqn: R( beta' ``->` rho') = beta ``->` rho``]를 만족하는 [eqn: R``]이 존재한다고 가정하자. 그러면, [eqn: (R`□_{left{ beta_2 ' right}}``cup` left{rho/ beta_2 'right})][eqn: ( beta' ``->` beta_2 ') = R beta' ``->` rho = beta ``->` rho``]가 성립한다.

□[eqn: H ``sqsubseteq`]OCaml 알고리즘의 증명: 두 알고리즘은 (G.6)의 (2)에서만 다르다. [eqn: H``]는 [eqn: beta ``->` beta_2 ``geq` beta ``->` rho``]이고, OCaml의 알고리즘은 [eqn: beta_1 ' geq beta' ``->` rho'``]이다. 어떤 타입 치환 함수 [eqn: R``]에 대해서도 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ beta ``->` beta_2 / beta_1 ' right} )beta_1 ' =][eqn: beta ``->` beta_2]이 성립한다.

□OCaml 알고리즘[eqn: ``sqsubseteq`]SML/NJ 알고리즘의 증명:

- (G.3)의 (1)의 경우: OCaml 알고리즘은 [eqn: rho ``>=` rho``]이고 SML/NJ 알고리즘은 [eqn: beta_1 ' ``geq` rho'``] 또는 [eqn: rho'``geq`rho'``]이다. [eqn: R rho'= rho``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다고 가정하자. 그러면, [eqn: (R`□_{left{beta_1 ' right}} ``cup` left{ rho / beta_1 ' right} )beta_1 '= rho``] 또는 [eqn: (R ``cup` left{ right}) rho'= rho``]가 성립한다.

- (G.6)의 (2)의 경우: OCaml 알고리즘은 [eqn: beta_1 ``geq` rho``]이고 SML/NJ 알고리즘은 [eqn: beta_1 ' ``geq` rho'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ beta_1 / beta_1 ' right} )beta_1 '= beta_1 ``]이 성립한다.

- (G.7)의 (3)의 경우: OCaml 알고리즘은 [eqn: S_1 ( beta ``->` rho)][eqn: geq` S_1 ( beta ``->` rho)``]이고 SML/NJ 알고리즘은 [eqn: beta_2 ' ``geq`][eqn: S_1 '( beta' ``->` rho')``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{beta_2 ' right}} ``cup][eqn: left{ S_1 ( beta ``->` rho) / beta_2 'right}) beta_2 ' = S_1 ( beta ``->` rho)``]을 만족한다.

- (G.8)의 (4)의 경우: OCaml 알고리즘은 [eqn: S_2 S_1 beta ``geq`][eqn: S_2 S_1 beta``]이고 SML/NJ 알고리즘은 [eqn: beta_3 ' ``geq` S_2 'S_1 ' beta'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_3 ' right}}``cup` left{S_2 S_1 beta / beta_3 'right}) beta_3 ' = S_2 S_1 beta``]를 만족한다.

- (G.12)의 (5)의 경우: OCaml 알고리즘은 [eqn: S_1 rho ``geq` S_1 rho``]이고 SML/NJ 알고리즘은 [eqn: beta_1 ' ``geq` S_1 ' rho'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ S_1 rho / beta_1 'right}) beta_1 ' = S_1 rho``]를 만족한다.

- (G.14)의 (6)의 경우: OCaml 알고리즘은 [eqn: rho ``wedge` rho ``geq` rho``]이고 SML/NJ 알고리즘은 [eqn: beta_1 ' ``wedge` beta_1 ' ``geq` rho'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ rho / beta_1 ' right}) beta_1 ' = rho``]를 만족한다.

□SML/NJ 알고리즘[eqn: ``sqsubseteq`W``]의 증명:

- (G.3)의 (1)의 경우: SML/NJ 알고리즘은 [eqn: beta_1 ``geq` rho``] 또는 [eqn: rho ``geq` rho``]이고, [eqn: W``]는 [eqn: beta_1 ' ``geq` rho'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ beta_1 / beta_1 ' right}) beta_1 ' = beta_1 ``] 또는 [eqn: (R`□_{left{ beta_1 ' right}} ``cup` left{ rho / beta_1 'right})][eqn: beta_1 ' = rho``]를 만족한다.

- (G.14)의 (6)의 경우: SML/NJ 알고리즘은 [eqn: beta_1 ``wedge` beta_1][eqn: geq` rho``]이고 [eqn: W``]는 [eqn: beta_1 '`` wedge` beta_2 ' ``geq` rho'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_1 ',beta_2 ' right}} ``cup` left{ beta_1 / beta_1 ', beta_1 / beta_2 ' right}) ( beta_1 '~ 또는 ~beta_2 ') = beta_1]을 만족한다.

- 나머지 경우: SML/NJ 알고리즘은 어떤 타입 [eqn: tau``]에 대해 [eqn: beta_i ``geq` tau``]이고 [eqn: W``]는 어떤 타입 [eqn: tau'``]에 대해 [eqn: beta_i ' ``geq` tau'``]이다. 어떤 [eqn: R``]이든 [eqn: (R`□_{left{ beta_i ' right}} ``cup` left{ beta_i / beta_i 'right}) beta_i ' =][eqn: beta_i``]을 만족한다. □

E. 정리 4의 증명

정리 4(상대적인 오류 감지의 신속성). [eqn: G``]의 두 예 알고리즘 [eqn: A``], [eqn: A'``]에 대해 [eqn: A``sqsubseteq` A'``]이면, 타입 환경 [eqn: Gamma_0 ``], 프로그램 [eqn: e_0 ``], 타입 [eqn: rho_0 ``]에 대해 [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]에 [eqn: ( Gamma,e, rho)^ d/u ``]가 있으면 [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□]에 [eqn: ( Gamma``',e, rho')^ d/u ``]가 있고, [eqn: R Gamma`' ``succ` Gamma``]이고 [eqn: R rho'= rho``]를 만족하는 타입 치환 함수 [eqn: R``]이 존재한다.

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

보조정리 10[4]. [eqn: Gamma ``succ` Gamma``'``]이면 [eqn: Clos_Gamma (tau)`` succ` Clos_{ Gamma``'}( tau)``]이다.

보조정리 11. [eqn: G``]의 두 예 알고리즘 [eqn: A``], [eqn: A'``], 타입 환경 [eqn: Gamma``], [eqn: Gamma``'``], 타입 [eqn: rho``], [eqn: rho'``]에 대해 [eqn: R Gamma``' ``succ` Gamma``]와 [eqn: R rho'= rho``]를 만족하는 [eqn: R``]이 존재한다고 하자. [eqn: A( Gamma,e, rho)``]가 [eqn: S``]를 결과로 성공한다면, [eqn: A'( Gamma``',e, rho')] 또한 [eqn: S`'``]을 결과로 성공하며 [eqn: (R'S`')□_V = (SR)□_V ``]를 만족하는 [eqn: R'``]이 존재한다. 여기서, [eqn: V``]는 [eqn: A( Gamma,e, rho)``]가 사용한 새 타입 변수들의 집합이다.

증명. [eqn: A( Gamma,e, rho)``]가 [eqn: S``]를 결과로 성공했으므로 안전성에 의해 [eqn: S Gamma ``vdash` e``:`S rho``]가 성립한다. 보조정리 3에 의해 [eqn: SR Gamma``' ``succ` S Gamma``]이고 [eqn: S rho=SR rho'``]이므로, 보조정리 6에 의해 [eqn: SR Gamma``' ``vdash` e``:`SR rho'``]가 성립한다. 그러면 완전성에 의해 [eqn: A'( Gamma``',e, rho')``]은 [eqn: S`'``]를 결과로 성공하며 [eqn: (R'S`')□_V =][eqn: (SR)□_V ``]를 만족하는 [eqn: R'``]이 존재한다. □

정리 4의 증명. 호출 문자열 [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]의 접두 문자열(prefix)의 길이에 대해 귀납적으로 증명한다. [eqn: A'(Gamma_0 ,e_0 ,rho_0 )``]에서 사용된 모든 이름에 위첨자 [eqn: '``]를 붙인다.

□접두 문자열의 길이가 1인 경우: 처음 호출인 경우이다. 항등 타입 치환 함수가 조건을 만족한다. 즉, [eqn: left{ right} Gamma_0 ``succ` Gamma_0 ``]이고 [eqn: left{right} rho_0 = rho_0 ``]이다.

이제 문자열의 길이가 1보다 큰 경우를 증명한다. 먼저 접두 문자열이 귀환([eqn: u``])으로 끝나는 경우를 보자.

□[eqn: e``]로부터 귀환한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이 [eqn: ( Gamma,e, rho)^d][eqn: cdots( Gamma,e, rho)^u ``]를 포함한 경우이다. 귀납 가정에 의하여 [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□``] 또한 [eqn: ( Gamma``',e, rho')^d``]를 포함하고, [eqn: R rho'= rho``]이고 [eqn: R Gamma``' ``succ` Gamma``]를 만족하는 [eqn: R``]이 존재한다. 보조정리 11에 의해 [eqn: A'( Gamma``',e, rho')``]은 성공한다. 즉, [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□``]이 [eqn: ( Gamma``',e, rho')^u``]를 포함한다.

이제 접두 문자열이 호출로 끝나는 경우를 증명한다: [eqn: ( Gamma_0 ,e_0 , rho_0 ) cdots( Gamma,e, rho)^d ``].

□[eqn: lambda x.e``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: ( Gamma, lambda x.e, rho)^d (S_1 Gamma + x ``:` S_1 beta_1 ,e,S_1 beta_2 )^d``]

를 포함한 경우이다. 여기서 [eqn: S_1 ``]은 (G.3)의 [eqn: U ( beta_1 ``->` beta_2 , theta)``]의 결과이고, [eqn: beta_1 ``], [eqn: beta_2 ``]는 (G.3)의 새 타입 변수들이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□``] 또한 [eqn: ( Gamma``', lambda x.e, rho')^d``]를 포함하고,

[eqn: R Gamma``'`` succ` Gamma``]	(39)

와 [eqn: R rho'= rho``]를 만족하는 [eqn: R``]이 존재한다.

[eqn: A'( Gamma``', lambda x.e, rho')``]가 [eqn: e``]를 호출하기 위해서는 (G.3)의 동일화가 성공해야 한다. [eqn: A``sqsubseteq`A'``]이므로

[eqn: theta = (R`□_supp(P) ``cup` P`) theta'``]	(40)

와 [eqn: supp(P)``subseteq`ftv(theta') □ftv(rho')``]을 만족하는 [eqn: P``]가 존재한다. [eqn: G``]의 정의에 의해

[eqn: supp( P) ``cap` ftv (Gamma``') = emptyset]	(41)

임을 주목하라. [eqn: R_0 = R`□_{left{ beta_1 ', beta_2 ' right} ``cup` supp( P )}``cup` P ``cup` left{ beta_1 / beta_1 ', beta_2 / beta_2 ' right}``]라 하자. 여기서 [eqn: beta_1 '``], [eqn: beta_2 '``]는 [eqn: A'``]에서 사용된 (G.3)의 새 타입 변수이다. 그러면 [eqn: S_1 R_0 ``]이 (G.3)의 [eqn: beta_1 ' ``->` beta_2 '``]과 [eqn: theta'``]을 동일화한다:

[eqn: S_1 R_0 ( theta') &=& S_1 (R`□_supp(P) ``cup` P`) theta' & beta_1 ', beta_2 ' not in ftv (theta')이므로 # &=& S_1 theta & (40)에 ~의해 # &=& S_1 ( beta_1 ``->` beta_2 ) & (rm G.3)에~의해 # &=& S_1 R_0 ( beta_1 ' ``->` beta_2 ') & R_0 의~ 정의에 ~의해]

그러므로, [eqn: A'``]의 (G.3)에 동일화는 [eqn: S_1 '``]을 결과로 성공한다. [eqn: □A'(Gamma_0 ,e_0 ,rho_0 )□``]는 [eqn: (S_1 ' Gamma``'+x ``:` S_1 ' beta_1 ',e,S_1 ' beta_2 ')^d ``]를 포함한다.

남은 것은 [eqn: R`'(S_1 ' Gamma``' + x ``:` S_1 ' beta_1 ') ``succ` (S_1 Gamma+x ``:` S_1 beta_1 )``]와 [eqn: R`'(S_1 ' beta_2 ') = S_1 beta_2 ``]를 만족하는 [eqn: R`'``]이 존재함을 증명하는 것이다. (G.3)가 [eqn: S_1 '``]을 결과로 성공했으므로 정리 1에 의해

[eqn: S_1 R_0 = R_1 S_1 '``]	(42)

를 만족하는 [eqn: R_1``]이 존재한다. 그러면 [eqn: R_1``]이 그러한 [eqn: R`'``]이다. 왜냐하면,

[eqn: &R_1 (S_1 ' Gamma``'+x ``:` S_1 ' beta_1 ')# &= S_1 R_0 ( Gamma``'+x ``:` beta_1 ') & (42)에~ 의해# &= S_1 ((R`□_supp(P) `cup P`) Gamma`'+x `: R_0 beta_1 ') & beta_1' , beta_2 ' not in ftv (Gamma`')이므로# &= S_1 (R Gamma``'+x ``:` beta_1 ) & (41)과 ```R_0 의 ``정의에 ``의해# & succ S_1 ( Gamma + x ``:` beta_1 ) & (39)와 ```보조정리`` 3에 ```의해]

[eqn: R_1 (S_1 ' beta_2 ') &=& S_1 R_0 beta_2 ' & (42)에~ 의해# &=& S_1 beta_2 & R_0 의 ~정의에 ~따라]

이기 때문이다.

□[eqn: e~e_2``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: ( Gamma,e~e_2 , rho)^d ( Gamma,e, theta_1 )^d ``]

를 포함한 경우이다. 여기서 [eqn: theta_1``]는 (G.8)의 [eqn: beta ``->` rho``]로부터 느슨해진 타입 조건이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``] 또한 [eqn: ( Gamma``',e~e_2 , rho')^d``]를 포함하고

[eqn: R Gamma``' ``succ` Gamma ``]	(43)

와 [eqn: R rho'= rho``]를 만족하는 [eqn: R``]이 존재한다. 그러므로, [eqn: G``]의 정의에 따라 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: ( Gamma``',e, theta_1 ')^d ``]를 포함하고 있다. 여기서, [eqn: theta_1 '``]은 (G.8)의 [eqn: beta' ``->` rho'``]로부터 느슨해진 타입 조건이다.

남은 것을 증명하자. [eqn: R_0 = R`□_{left{ beta' right}} ``cup` left{ beta/ beta' right}``]라 하자. 여기서, [eqn: beta``], [eqn: beta'``]은 각각 (G.6)에 있는 [eqn: A``], [eqn: A'``]의 새 타입 변수이다. [eqn: A``sqsubseteq`A'``]이고

[eqn: R_0 ( beta' ``->` rho') &=& beta ``->` R rho' & beta' not in ftv( rho')이므로# &=& beta ``->` rho]

이므로 정의 2에 따라

[eqn: (R_0 □_supp(P) ``cup` P`)theta_1 '= theta_1]

와 [eqn: supp (P) ``subseteq` ftv (theta_1 ') □ ftv( beta' ``->` rho')``]를 만족하는 [eqn: P``]가 존재한다. [eqn: G``]의 정의에 의해 [eqn: supp (P)`` cap` ftv (Gamma``') = emptyset``]이 성립하므로,

[eqn: &(R_0 □_supp(P) ``cup` P`)( Gamma``') # &=`` R Gamma``' & ( left{ beta right}``cup` supp( P)) ``cap` ftv (Gamma``') = emptyset이므로# & succ`` Gamma& (43)에~ 의해]

가 성립한다.

□[eqn: e_1 ~e``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: ( Gamma,e_1 ~e, rho)^d ( Gamma,e_1 , theta_1 )^d cdots ( Gamma,e_1 , theta_1 )^u (S_2 S_1 Gamma,e, theta_3 )^d ``]

를 포함한 경우이다. 여기서 [eqn: theta_1``], [eqn: theta_2``], [eqn: theta_3``]는 각각 (G.6), (G.7), (G.8)의 느슨한 타입 조건이고, [eqn: S_1``]은 (G.6)의 [eqn: G( Gamma,e_1 , theta_1 )``]의 결과이고, [eqn: S_2``]는 (G.7)의 [eqn: U(S_1 theta_1 , theta_2 )``]의 결과이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: ( Gamma``',e_1 ~e, rho')^d``]를 포함하고

[eqn: R Gamma``' ``succ` Gamma``]	(44)

와 [eqn: R rho' = rho``]를 만족하는 [eqn: R``]이 있다.

[eqn: A'( Gamma``',e_1 ~e, rho')``]이 [eqn: e``]를 호출하기 위해서는 (G.6)의 [eqn: e_1``] 호출이 성공하고 (G.7)의 동일화가 성공해야 한다.

- (G.6)의 [eqn: A'( Gamma``',e_1 , theta_1 ')``]이 성공한다: [eqn: R_0 = R`□_{left{ beta' right}} ``cup`][eqn: left{ beta/ beta' right}``]라 하자. 여기서, [eqn: beta``], [eqn: beta'``]는 각각 [eqn: A``], [eqn: A'``]의 (G.6)에서의 새 타입 변수이다. [eqn: A``sqsubseteq`A'``]이고

[eqn: R_0( beta' ``->` rho') &=& beta ``->` R rho' & beta' not in ftv (rho')이므로# &=& beta ``->` rho]	[eqn: #(45)]

이므로, 정의 2에 의해

[eqn: theta_1 = (R_0 □_{supp(P_1 )} ``cup` P_1 ) theta_1 '``]	(46)

와 [eqn: supp(P_1 ) ``subseteq ftv(theta_1 ')□ftv(beta ' ``->` rho')``]를 만족하는 타입 치환 함수 [eqn: P``]가 존재한다. [eqn: G``]의 정의에 의해

[eqn: supp (P_1 )``cap`( ftv (Gamma``' )``cup` ftv( beta' ``->` rho') )= emptyset``]	(47)

이므로

[eqn: ~~&(R_0 □_{supp(P_1 )} `cup` P_1 ) Gamma`' # &=`` R Gamma``' & (47)과 ```beta' not in ftv( Gamma`')이므로 # & succ`` Gamma &(44)에~ 의해~~~~~~~~~~~~~~~(48)]

이다. 결국,[eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]는 [eqn: ( Gamma,e_1 , theta_1 )^u]를 포함하고 있고 [eqn: (R_0 □_{supp(P_1 )} ``cup` P_1 ) Gamma``' ``succ` Gamma``] 이고 [eqn: (R_0 □_{supp(P_1 )} ``cup` P_1 ) theta_1 '= theta_1 ``]이다. 그러므로, 보조정리 11에 의해 [eqn: A'( Gamma``',e_1 , theta_1 ')``]는 [eqn: S_1 '``]을 결과로 성공하며,

[eqn: (R_1 S_1 ')□_V_1 = (S_1 (R_0 □_{supp(P_1 )} ``cup` P_1 ) )□_V_1 ``]	(49)

를 만족하는 [eqn: R_1``]이 존재한다. 여기서 [eqn: V _1]은 [eqn: A'( Gamma``',e_1 , theta_1 ')``]에서 발생한 새 타입 변수들의 집합이다.

- (G.7)의 [eqn: U(S_1 ' theta_1 ', theta_2 ')``]는 성공한다: [eqn: A``sqsubseteq`A'``]이고

[eqn: ~~~&R_1 (S_1 '( beta' ``->` rho')) # &= S_1 (R_0 □_{supp(P_1 )} ``cup` P_1 ) ( beta' ``->` rho')# &~~~~~~~~~ (49)와 ~ ftv( beta' ``->` rho' )``cap` V _1 = emptyset이므로# &= S_1 R_0 ( beta' ``->` rho') ~~~~~~~~~~~~~~~~ (47)에~의해# &= S_1 ( beta ``->` rho) ~~~~~~~~~~~~~~~~~~~~ (45)에~의해~~~~(50)]

이므로, 정의 2에 의해

[eqn: theta_2 = (R_1 □_{supp(P_2 )} ``cup` P_2 ) theta_2 ']	(51)

와 [eqn: supp(P_2 ) ``subseteq ftv(theta_2 ')□ftv(S_1 '(beta ' ``->` rho'))``]를 만족하는 [eqn: P_2``]가 존재한다.

[eqn: &ftv (S_1 ' theta_1 ' )``cup` ftv (S_1 ' beta' )``cup` ftv (S_1 ' Gamma``' )# & ``subseteq` i tv(S_1 ') ``cup` ftv( theta_1 ') ``cup`left{ beta'right} ``cup` ftv (Gamma``') & 보조정리~ 7 에 ~의해# & ``subseteq` V _1 ``cup` ftv( theta_1 ') ``cup`left{ beta' right}``cup` ftv (Gamma``') & 보조정리~ 8에 ~의해]

이므로, [eqn: G``]의 정의에 의해

[eqn: supp( P_2 )``cap`( ftv (S_1 ' theta_1 ') ``cup` ftv( S_1 ' beta' )``cup` ftv( S_1 ' Gamma``' ))= emptyset``]	(52)

가 성립한다. 그러면 [eqn: S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 )``]가 (G.7)의 [eqn: S_1 ' theta_1 '``]과 [eqn: theta_2 '``]를 동일화한다:

[eqn: &S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 ) (S_1 ' theta_1 ') # &= S_2 R_1 S_1 ' theta_1 ' & (52)에~ 의해# &= S_2 S_1 (R_0 □_{supp(P_1 )} ``cup` P_1 ) theta_1 ' & (49)와``ftv( theta_1 ') cap V _1 = emptyset 이므로# &= S_2 S_1 theta_1 & (46)에~ 의해# &= S_2 theta_2 & (rm G.7)에~ 의해# &= S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 ) ( theta_2 ') & (51)에~ 의해]

그러므로 [eqn: A'``]의 (G.7)에서의 동일화는 [eqn: S_2 '``]를 결과로 성공한다.

결과적으로 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: (S_2 'S_1 ' Gamma``',e, theta_3 ')^d``]를 포함한다.

남은 증명은 [eqn: R' theta_3 ' = theta_3``]와 [eqn: R'(S_2 'S_1 ' Gamma``')`` succ` S_2 S_1 Gamma``]를 만족하는 [eqn: R'``]을 찾는 것이다. (G.7)이 [eqn: S_2 '``]을 결과로 성공했으므로 정리 1에 의해

[eqn: R_2 S_2 ' = S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 )``]	(53)

를 만족하는 [eqn: R_1``]이 존재한다. [eqn: A``sqsubseteq`A'``]이고

[eqn: R_2 (S_2 'S_1 ' beta') &=& S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 ) S_1 ' beta' & (53)에~의해# &=& S_2 R_1 S_1 ' beta' & (52)에~ 의해 # &=& S_2 S_1 beta & (50)에~의해]

이므로, 정의 2에 의해

[eqn: theta_3 = (R_2 □_{supp(P_3 )} ``cup` P_3 ) theta_3 '``]

와 [eqn: supp(P_3 ) ``subseteq` ftv(theta_3 ')□ftv(S_2 'S_1 ' beta')``]를 만족하는 [eqn: P_3``]가 존재한다. 보조정리 7, 8, 정리 1에 의해,

[eqn: &ftv( S_2 'S_1 ' Gamma``') # &subseteq`` ftv (theta_1 ) ``cup` ftv( theta_2 )``cup` V _1 ``cup` ftv( Gamma``')# & subseteq`` supp( P_1 ) ``cup` ftv( beta ``->` rho )``cup` supp( P_2 )``cup` V _1 ``cup` ftv( Gamma``')``]

이므로 [eqn: G``]의 정의에 의해

[eqn: supp (P_3 ) ``cap` ftv( S_2 'S_1 ' Gamma``') = emptyset``]	(54)

가 성립한다. 그러므로 [eqn: (R_2 □_{supp(P_3 )} ``cup` P_3 )``]이 그러한 [eqn: R'``]이 된다:

[eqn: &(R_2 □_{supp(P_3 )} ``cup` P_3 ) (S_2 'S_1 ' Gamma``') # &= R_2 S_2 'S_1 ' Gamma``' & (54)에~의해# &= S_2 (R_1 □_{supp(P_2 )} ``cup` P_2 ) S_1 ' Gamma``' & (53)에~의해# &= S_2 R_1 S_1 ' Gamma``' & (52)에~의해# &= S_2 S_1 (R_0 □_{supp(P_1 )} ``cup` P_1 ) Gamma``' & (49)와 ``ftv (Gamma`') cap V _1 = emptyset이므로# & succ S_2 S_1 Gamma & (48)과~ 보조정리~ 3에~ 의해.]

□[eqn: rm let ``it x=e rm ```i n``it e_2 ``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: ( Gamma, rm let ``it x=e rm ```i n``it e_2 , rho)^d ( Gamma,e, beta)^d``]

를 포함한 경우이다. 여기서 [eqn: beta``]는 (G.11)의 새 타입 변수이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``] 또한 [eqn: ( Gamma``', rm let ``it x=e rm ```i n``it e_2 , rho')^d``]를 포함하고 [eqn: R Gamma``' ``succ` Gamma``]와 [eqn: R rho'= rho``]를 만족하는 [eqn: R``]이 존재한다. [eqn: G``]의 정의에 따라 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: ( Gamma``',e_1 , beta')^d``]를 포함하고 있다. 여기서 [eqn: beta'``]는 [eqn: A'``]의 (G.11)에서의 새 타입 변수이다. [eqn: R_0 =R`□_{left{ beta' right}} ``cup` left{ beta/ beta' right}``]라 하면 [eqn: R_0 Gamma``' = R Gamma``' ``succ` Gamma ``]와 [eqn: R_0 beta' = beta ``]를 만족한다.

□[eqn: rm let ``it x=e_1 rm ```i n``it e ``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: &( Gamma, rm let ``it x=e_1 rm ```i n``it e, rho)^d ( Gamma,e, beta)^d cdots #&( Gamma,e, beta)^u (S_1 Gamma+x ``:` Clos_{ S_1 Gamma `}(S_1 beta) ,e, theta)^d``]

포함한 경우이다. 여기서 [eqn: beta``]는 (G.11)의 새 타입 변수이고, [eqn: theta``]는 (G.12)의 느슨한 타입 조건이고, [eqn: S_1``]는 (G.11)의 [eqn: G( Gamma,e_1 , beta)``]의 결과이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: ( Gamma``', rm let ``it x=e_1 rm ```i n``it e , rho')^d``]를 포함하고

[eqn: R Gamma``' ``succ` Gamma``]	(55)

와 [eqn: R rho' = rho``]를 만족하는 [eqn: R``]이 존재한다. [eqn: R_0 = R`□_{left{ beta' right}}``cup` left{ beta/ beta' right}``]라 하자. 여기서 [eqn: beta'``]은 [eqn: A'``]의 (G.11)에서의 새 타입 변수이다. 그러면,

[eqn: R_0 Gamma``' &=& R Gamma``' & beta' not in ftv (Gamma``')# & succ & Gamma &(55)에~ 의해]	[eqn: #(56)]

와 [eqn: R_0 beta'= beta``]가 성립한다. 그러면, 보조정리 11에 의해 (G.11)의 [eqn: A'( Gamma``',e_1 , beta')``]는 [eqn: S_1 '``]를 결과로 성공한다. 그러므로[eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: (S_1 ' Gamma`'+x `: Clos_{ S_1 ' Gamma`'}( S_1 ' beta') ,][eqn: e_2 , theta')^d ``]를 포함한다.

남은 것은 [eqn: R' theta'= theta``]와 [eqn: R'(S_1 ' Gamma``' + x ``:` Clos_{ S_1 ' Gamma``'}( S_1 ' beta' )) ``succ][eqn: S_1 Gamma+x ``:` Clos_{ S_1 Gamma }(S_1 beta )``]를 만족하는 [eqn: R`'``]이 존재함을 증명하는 것이다. (G.11)이 [eqn: S_1 '``]을 결과로 성공하므로 보조정리 11에 의해

[eqn: (R_1 S_1 ')□_V_1 = (S_1 R_0 )□_V_1]	(57)

를 만족하는 [eqn: R_1``]이 존재한다. 여기서, [eqn: V _1``]은 [eqn: A'( Gamma``',e_1 , beta')``]에서 발생한 새 타입 변수의 집합이다. [eqn: A``sqsubseteq`A'``]이고

[eqn: R_1 (S_1 ' rho') &=& S_1 R_0 rho' & (57)과 ~ ftv (rho')`` cap` V _1 = emptyset``이므로# &=& S_1 R rho' & beta' not in ftv( rho')# &=& S_1 rho]

이므로, 정의 2에 의해

[eqn: (R_1 □_supp(P) ``cup P) theta' = theta]

와 [eqn: supp(P)``subseteq`ftv(theta')□ftv(S_1 'rho' )``]를 만족하는 [eqn: P``]가 존재한다.

[eqn: &ftv (S_1 ' Gamma``') ``cup` ftv (S_1 ' beta') # & subseteq`` i tv(S_1 ') ``cup` ftv (Gamma``') ``cup` left{ beta' right} & 보조정리~ 7에~의해 # & subseteq `` V _1 ``cup` ftv( Gamma``' )``cup` left{ beta' right} & 보조정리~8에~ 의해]

이므로, [eqn: G``]의 정의에 의해

[eqn: supp (P) ``cap`( ftv (S_1 ' Gamma``') ``cup` ftv( S_1 ' beta') )= emptyset``]	(58)

가 성립한다. 그러므로, [eqn: (R_1 □_supp(P) ``cup P)``]가 그러한 [eqn: R`'``]이다. 왜냐하면,

[eqn: &(R_1 □_supp(P) ``cup P)(S_1 ' Gamma``') # &=`` R_1 (S_1 ' Gamma``') &(58)에 ~의해# &=`` S_1 R_0 Gamma``' &(57)과 ~V _1 ``cap` ftv (Gamma``') = emptyset# & succ`` S_1 Gamma &(56)과~ 보조정리~ 3에~의해 ~~~~ (59)]

[eqn: &(R_1 □_supp(P) ``cup P)( Clos_ S_1 ' Gamma``' S_1 ' beta' ) # &= R_1 Clos_{S_1 ' Gamma``'} ( S_1 ' beta') & (58)에~ 의해 # & succ Clos_{ R_1 S_1 ' Gamma``' }(R_1 S_1 ' beta') & 보조정리 ~5에~ 의해 # & succ Clos_{ S_1 Gamma}( R_1 S_1 ' beta') & (59)과~보조정리~ 10 에~의해 # &= Clos_{ S_1 Gamma}( S_1 R_0 beta') & (57)와 ~beta' not in V _1 이므로 # &= Clos_{ S_1 Gamma }(S_1 beta) & R_0 의~정의에~따라]

이기 때문이다.

□[eqn: rm fix ``it f~lambda x.e ``]의 [eqn: e``]를 호출한 경우: [eqn: □A(Gamma_0 ,e_0 ,rho_0 )□]이

[eqn: ( Gamma, rm fix ``it f~lambda x.e, rho)^d ( Gamma+f ``:` theta_1 , lambda x.e, theta_2 )^d``]

를 포함하는 경우이다. 여기서, [eqn: theta_1``], [eqn: theta_2``]는 (G.14)에서의 느슨한 타입 조건이다. 귀납 가정에 의해 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``]는 [eqn: ( Gamma``', rm fix ``it f~lambda x.e, rho')^d``]를 포함하고

[eqn: R Gamma``' ``succ` Gamma``]	(60)

와 [eqn: R rho'= rho``]를 만족하는 [eqn: R``]이 존재한다. [eqn: G``]의 정의에 따라 [eqn: □A'(Gamma_0 , e_0 , rho_0 )□``] 또한 [eqn: ( Gamma``'+f ``:` theta_1 ', lambda x.e, theta_2 ')^d``]를 포함한다.

남은 것을 증명하자. [eqn: A``sqsubseteq`A'``]이고 [eqn: R rho'= rho``]이므로, 정의 2에 의해

[eqn: theta_1 = (R`□_supp(P) ``cup` P) theta_1 '``]	(61)

와 [eqn: theta_2 = (R□_supp(P) ``cup` P) theta_2 '``]를 만족하는 [eqn: P``]가 존재한다. 그러므로,

[eqn: &(R□_supp(P) ``cup` P)( Gamma``'+f ``:` theta_1 ') # &= R Gamma``' + f ``:` theta_1 ~~~~~~ (61)과 ~ ftv (Gamma``')`` cap` supp( P )= emptyset이므로# & succ Gamma + f ``:` theta_1 ~~~~~~~~~ (60)에~의해]

가 성립한다. □

참고 자료

[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 Proceedings of  the 9th Annual ACM Symposium on Principles of Programming Languages, pages 207-212, New York, 1982. ACM Press.

[3]	Luis Manuel Martins Damas. Type assignment  in programming Languages. Ph. D. Thesis, University of Edinburgh, 1984.

[4]	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.

[5]	이욱세, 이광근. 하향식 타입 유추 알고리즘 [eqn: M``]의 속성 증명. 정보과학회 논문지, 25(8):1281-1292,  August 1998.

[6] The Standard ML of New Jersey, release 110.0.6. Bell Labs, Lucent Technologies, November 1999. http://cm.bell-labs.com/cm/cs/what/smlnj.

[7] Xavier Leroy, Didier R□my, J□r□me Vouillon, and Damien Doligez. The objective caml system release 2.04. Institut National de Recherche en Informatique et en Automatique, November 1999. http://caml.inria.fr.

[8]	주상현, 이욱세, 이광근. 복합형 타입 유추 알고리즘 [eqn: M``]의 병목을 해소하기 위한 알고리즘 [eqn: H``]. 정보과학회 논문지, 2000. (심사완료)

[9]	주상현. [eqn: M``]의 병목을 해소하는 타입유추 알고리즘. 석사논문, 한국과학기술원, 2000.

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

[11]	Bruce J. McAdam. On the unification of substitutions in type inference. In Kevin Hammond, Anthony J. T. Davie, and Chris Clack, editors, Proceedings of The International Workshop on Implementation of Fuctional Languages, volume 1595 of Lecture Notes in Computer Science, pages 139-154. Springer-Verlag, September 1998.

[12]	Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253-289, April 1993.

[13]	Kenta Cho and Kazunori Ueda. Diagnosing non-well-moded concurrent logic programs. In Joint  International Conference on Logic Programming, pages 215-229. MIT Press, 1996.

[14]	Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Proceedings of Functional Programming Languages  and Computer Architecture, pages 31-41, 1993.

[15]	Satish R. Thatte. Type inference with partial types. Theoretical Computer Science, 124(1):127-148, February 1994.

[16]	Didier R□my. Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992.