> 가정(assumption)들의 집합 Γ로부터 타입 σ가 항 M이 가지는 타입들의 집합에 속한다면

다음과 같이 쓰고 "Γ yields M in σ"라고 읽습니다.


Γ ⊢ M : σ.


특정 Curry 타입 할당 체계는 모든 타입들의 집합 T와 타입 할당 규칙에 의존합니다.

오늘은 λ→-Curry 타입 할당 체계를 공부합니다.


1. 정의: 모든 타입들의 집합 T = Type(λ→)는 다음과 같이 귀납적으로 정의됩니다.


α ∈ V ⇒ α ∈ T,

B ∈ B ⇒ B ∈ T,

σ,τ ∈ T ⇒ (σ→τ) ∈ T.


여기서 V = { α, α', α'', ... }는 타입 변수(type variable)들의 집합이고

B는 Int, Bool 같은 기본 타입에 대응하는 타입 상수(type constant)들의 집합입니다.

→는 함수 공간 타입(function space type)을 만듭니다.


표기> σ_1,...,σ_n ∈ T이면 σ_1 → σ_2 → ... → σ_n은 다음과 같습니다.


(σ_1 → (σ_2 → ... → (σ_(n-1) → σ_n)..)).


표기> α,β,γ,...는 임의의 타입 변수를 나타냅니다.


2. 정의:

1) 진술(statement)는 M : σ꼴의 것입니다 - 단, M ∈ Λ and σ ∈ T.

이것을 "M in σ"라고 읽고 M을 이것의 주어, σ를 이것의 술어라고 합니다.

2) 기저(basis)는 변수 그 자체인 서로 다른 람다-항을 주어로 하는 진술들의 집합입니다.

예를 들자면 집합 Γ = { x_1:σ_1, ..., x_n:σ_n }은 기저입니다.


표기> Γ, x:σ = { x_1:σ_1, ..., x_n:σ_n, x:σ }.


3. 정의: λ→ 체계 안에서의 타입 유도(type derivation)은 가정 x:σ들의 집합으로부터 다음 추론 규칙들을 적용하여 세워집니다.


M : σ→τ과 N : σ을 얻으면 M N : τ도 얻습니다.

x:σ라고 가정할 때 M : τ을 얻으면 가정 x:σ은 취소되고 λx. M : σ→τ을 얻습니다.


해설을 달자면 이렇게 달 수 있습니다.

첫 번째 규칙에서 M N은 함수 M에 인자 N이 적용되어 있는 꼴이므로 f(x) ∈ Y이기 때문에 납득할 수 있습니다.

여기서 x는 정의역의 원소이고 Y는 공역입니다.

두 번째 규칙에서 M은 x에 대한 수식 f(x)일 것이고 x를 그 수식에 바운딩시키면 함수 x ↦ f(x)을 얻기 때문에 납득할 수 있습니다.

또한 x는 더 이상 자유 변수가 아니므로 다른 타입 유도에 쓰일 수 없어야 하기 때문에 가정은 취소(cancel)되어야 합니다.


4. 정의: 만약 진술 M : σ의 유도가 모든 취소되지 않은 가정들이 기저 Γ 안에 있는 곳에서 존재한다면

M : σ는 Γ로부터 유도가능하다고 하고 다음과 같이 표기합니다.


Γ ⊢ M : σ.


그리고 ⊢ M : σ는 ∅ ⊢ M : σ의 단축 표기입니다.

한편, 3번을 이용하여 4번을 다음과 같이 재정의할 수 있습니다.

  1. x:σ ∈ Γ임을 알 수 있다면 Γ ⊢ M : σ임을 알 수 있습니다: 공리.

  2. Γ ⊢ M : σ→τ임과 Γ ⊢ N : σ임을 알 수 있다면 Γ ⊢ M N: τ임을 알 수 있습니다: →-제거.

  3. x:σ ∈ Γ임과 Γ ⊢ M : τ임을 알 수 있다면 Γ － { x:σ } ⊢ λx. M : σ→τ임을 알 수 있습니다: →-도입.

5. 예제:


1) σ ∈ T라 하면 ⊢ λf,x. f (f x) : (σ→σ)→σ→σ입니다.

증명)

1.| f : σ→σ. Assumption, cancelled by 6.

2.|| x : σ. Assumption, cancelled by 5.

3.|| f x : σ. →-Elimination 1, 2.

4.|| f (f x) : σ. →-Elimination 1, 3.

5.| λx. f (f x) : σ→σ. →-Introduction 2, 4.

6. λf,x. f (f x) : (σ→σ)→σ→σ. →-Introduction 1, 5.


2) 임의의 σ,τ ∈ T에 대하여 ⊢ K : σ→τ→σ을 얻습니다.


3) 위와 비슷하게 임의의 σ ∈ T에 대하여 ⊢ I : σ→σ을 얻습니다.


4) 기저 Γ = { y:σ }와 임의의 타입 σ에 대하여 Γ ⊢ I y : σ을 얻습니다.


> λ→의 특성: λ→ 체계 안에서의 타입 할당은 몇 가지 특성을 가집니다.


> 첫 번째 특성은 타입 할당을 유도하는 데 얼마나 많은 기저가 필요한지를 분석합니다.


6. 정의: Γ = { x_1:σ_1, ..., x_n:σ_n }을 기저라고 합시다.


1) dom(Γ) = { x_1, ..., x_n }이라 적고 σ_i = Γ(x_i)이라 합니다. 즉, Γ은 부분함수로 간주됩니다.


2) V_0을 변수들의 집합이라 하면 Γ ↑ V_0 = { x:σ | x ∈ V_0 and σ = Γ(x) }이라 합시다.


3) 임의의 타입 σ, τ에 대하여 σ 안의 α의 τ로의 치환을 σ[α := τ]라 적습니다.


7. 기저 보조정리(basis lemma): Γ를 기저라 합시다.


1) 또다른 기저 Γ' ⊇ Γ에 대하여 Γ ⊢ M : σ이면 Γ' ⊢ M : σ입니다.

증명) M : σ의 유도에 대한 귀납법을 적용합시다.

Case 1. M ≡ x이고 x:σ ∈ Γ인 변수 x가 존재해서 Γ ⊢ M : σ인 경우:

x:σ ∈ Γ'이므로 Γ' ⊢ M : σ입니다.

Case 2. M1 : τ→σ이고 M2 : τ이고 M1 M2 ≡ M인 람다-항 M1, M2와 타입 τ가 존재해서 Γ ⊢ M : σ인 경우:

가정에 의하여 Γ' ⊢ M1 : τ→σ이고 Γ ⊢ M2 : τ을 얻습니다.

그러므로 Γ ⊢ (M1 M2) : σ입니다.

Case 3. Γ, x:σ1 ⊢ M1 : σ2이고 M ≡ λx. M1이고 σ ≡ σ1→σ2인 람다-항 M과 변수 x와 타입 σ1, σ2가 존재해서 Γ ⊢ M : σ인 경우:

변수 관례에 의하여 속박 변수 x가 dom(Γ')의 원소가 아님을 가정할 수 있습니다.

그러면 Γ', x:σ1은 Γ, x:σ2를 확장한 기저입니다.

가정에 의하여 Γ', x:σ1 ⊢ M1 : σ2를 얻으므로 Γ' ⊢ (λx. M1) : σ1→σ2입니다.


2) Γ ⊢ M : σ이면 FV(M) ⊆ dom(Γ)입니다.

증명) M : σ의 유도에 대한 귀납법을 적용합시다.

Γ, x:σ1 ⊢ M1 : σ2이고 M : σ가 (λx. M1) : (σ1→σ2)이어서 Γ ⊢ M : σ인 경우에 대해서만 다루겠습니다.

y ∈ FV(λx. M1)이라고 하면 y ∈ FV(M)이고 y ≢ x입니다.

가정에 의하여 y ∈ dom(Γ, x:σ1)을 얻으므로 y ∈ dom(Γ)입니다.


3) Γ ⊢ M : σ이면 Γ ↑ FV(M) ⊢ M : σ입니다.

증명) M1 : τ→σ이고 M2 : τ인 타입 τ가 존재하고 M : σ이 (M1 M2) : σ이어서 Γ ⊢ M : σ인 경우에 대해서만 다루겠습니다.

가정에 의하여 Γ ↑ FV(M1) ⊢ M1 : τ→σ와 Γ ↑ FV(M2) ⊢ M2 : τ을 얻습니다.

이때 1)에 의하여 Γ ↑ FV(M1 M2) ⊢ M1 : τ→σ이고 Γ ↑ FV(M1 M2) ⊢ M2 : τ이므로 Γ ↑ FV(M1 M2) ⊢ (M1 M2) : σ입니다.


> 두 번째 특성은 특정 형태의 항들이 어떻게 타입을 얻는지 분석합니다.

이 특성은 어떤 항이 타입을 가질 수 없음을 보이는 데 유용합니다.


8. 생성 보조정리(generation lemma):


1) Γ ⊢ x : σ이면 x:σ ∈ Γ입니다.

증명) 유도들의 구조에 대한 귀납법으로 증명하면 됩니다.


2) Γ ⊢ M N: τ일 때, Γ ⊢ M : σ→τ이고 Γ ⊢ N : σ인 타입 σ가 존재합니다.

증명) 1)과 비슷하게 하면 됩니다.


3) Γ ⊢ λx. M : ρ일 때, Γ, x:σ ⊢ M : τ이고 ρ ≡ σ→τ인 타입 σ, τ가 존재합니다.

증명) 1)과 비슷하게 하면 됩니다.


9. 하위항들의 타입가능성(typability of subterms): M'가 M의 하위항일 때 어떤 기저 Γ'와 어떤 타입 σ'에 대하여


Γ ⊢ M : σ ⇒ Γ' ⊢ M' : σ'.


즉, M이 타입을 가진다면 M의 모든 하위항들 또한 타입을 가집니다.

증명) M의 생성에 대한 귀납법으로.


10. 치환 보조정리(substitution lemma):


1) Γ ⊢ M : σ이면 Γ[α := τ] ⊢ M : σ[α := τ]입니다.

증명) M : σ의 유도에 대한 귀납법으로 증명합니다.


2) Γ, x:σ ⊢ M : τ임과 Γ ⊢ N : σ임을 가정하면 Γ ⊢ M[x := N] : τ입니다.

증명) Γ, x:σ ⊢ M : τ을 보이는 유도에 대한 귀납법으로 증명합니다.


> 다음 결과는 특정 타입을 갖는 람다-항들의 집합은 소거에 대해 닫혀있음을 진술합니다.


11. 주어 소거 정리(Subject Reduction Theorem): M ⇒β M'임을 가정하면


Γ ⊢ M : σ ⇒ Γ ⊢ M' : σ.


증명) 생성 보조정리와 치환 보조정리를 이용하며 ⇒β의 발생에 대한 귀납법으로 증명합시다.

M ≡ (λx. P) Q이고 M' ≡ P[x := Q]인 경우에 대해서만 다루겠습니다.

만약 Γ ⊢ (λx. P) Q : σ이라면 생성 보조정리에 의하여 Γ, x:τ ⊢ P : σ이고 Γ ⊢ Q : τ인 타입 τ가 존재합니다.

이때 치환 보조정리에 의하여 Γ ⊢ P[x := Q] : σ입니다.


> 어떤 타입을 가지는 항들은 확장에 대하여 닫혀있지 않습니다. 예를 들어, 항 λx. x x은 타입을 가지지 않으므로, ⊢ I : σ→σ이지만


⊬ K I (λx. x x) : σ→σ.


12. 관찰: 어떤 람다-항 M, M'와 어떤 타입 σ, σ'가 존재하여 M' ⇒β M이고 ⊢ M : σ이고 ⊢ M' : σ'이지만 ⊬ M' : σ입니다.


증명) M ≡ λx,y. y, M' ≡ S K, σ ≡ α→β→β 그리고 σ' ≡ (β→α)→β→β을 택하면 됩니다.


> 모든 타입가능한 항들로부터 출발하는 모든 소거는 유한합니다. 즉 타입가능하면 strong nomalization 특성이 성립합니다.


> 타입 할당의 결정가능성: 타입 할당 체계에 대한 몇 가지 질문이 있습니다. Γ = { x_1:σ_1, ..., x_n:σ_n }에 대하여


(Γ ⊢ M : σ) ⟺ (⊢ λx_1,...,x_n. M : σ1→...→σ_n→σ)

을 얻으므로 공집합인 기저에 대하여 논합시다. 다음과 같은 문제들이 있습니다.

  1. 타입 확인(type checking): M과 σ가 주어졌을 때, ⊢ M : σ임을 알 수 있는가?
  2. 타입가능성(typability): M이 주어졌을 때, ⊢ M : σ인 σ가 존재하는가?
  3. 거주(inhabitation): σ이 주어졌을 때, ⊢ M : σ인 M이 존재하는가?

> 타입 확인과 타입가능성은 결정가능합니다 - Curry(1969), Hindley(1969), Milner(1978).


13. 정리:


1) λ→에서 항이 타입가능한지는 결정가능합니다.


2) M이 λ→에서 타입가능하다면 M은 주요 타입 스킴을 가집니다.

즉, 타입 σ가 존재하여 M에 대한 모든 가능한 타입들이 σ의 타입변수를 치환한 인스턴스입니다.

게다가 주요 타입 스킴 σ은 M으로부터 계산가능합니다.


14. 따름정리: λ→에 대한 타입 확인은 결정가능합니다.

증명) M이 타입가능한지 확인하고 τ가 M의 주요 타입의 인스턴스인지 확인하면 M : τ인지를 알 수 있기 때문입니다.


> 다형성: 이제 2계 람다 대수 λ2를 소개하겠습니다. λ→에서는


⊢ I : σ→σ, for all σ ∈ T


이지만 λ2에서는


⊢ I : ∀α.α→α.


15. 정의: λ2의 타입들의 집합 T = Type(λ2)은 다음 문법에 의하여 명시됩니다.


T = V | B | T→T | ∀V.T.


16. 정의: λ2의 타입 할당 규칙은 λ→의 그것에 다음 두 가지 규칙을 더한 것입니다.


M : ∀α.σ을 얻으면 M : σ[α := τ]도 얻습니다.

M : σ을 얻으면 M : ∀α.σ도 얻습니다.


단, 후자에서 전제 M : σ가 의존하는 어떤 가정에도 타입 변수 α가 나타나면 안 됩니다.

위 두 규칙을 다음과 같이 나타낼 수도 있습니다.

  1. Γ ⊢ M : ∀α.σ임을 알 수 있다면 Γ ⊢ M : σ[α := τ]임을 알 수 있습니다: ∀-제거.

  2. Γ ⊢ M : σ임을 알 수 있고 α ∉ FV(Γ)이면 Γ ⊢ M : ∀α.σ임을 알 수 있습니다: ∀-도입.

17. 예제:


1) λ2에서는 ⊢ λx. x x : ∀α.(∀β.β)→α입니다.


2) 처치 수 c_n에 대하여 Nat ≡ ∀α.(α→α)→α→α이라 두면 ⊢ c_n : Nat입니다.


18. 정리 - Girard(1972):


1) 주어 소거 특성이 λ2에서도 성립합니다.


2) λ2는 strong nomalizing합니다.


> λ2는 결정가능하지 않습니다 - Wells(1994).


> 연습문제: λ→에서 다음이 성립하게 하는 람다-항 M과 N을 찾으세요:

  1. ⊢ M : (α→β)→(β→γ)→(α→γ).
  2. ⊢ N : (((α→β)→β)→β)→(α→β).

답) M ≡ λf,g,x. g (f x), N ≡ λf,x. (λa. K (f (a (λg. g x))) (a (f (λh. h x)))) I.


> 마치며: 요새 제가 ㅈ밥이라는 것을 느끼고 있습니다. 엄청나게 큰 수리논리학과 컴퓨터과학의 세계를 돌아다니면서 자존감이 많이 낮아졌지만

그래도 천 리 길도 한 걸음부터라는 격언을 마음에 세기고 열심히 공부하겠습니다.