TaPL_exercise_11_4 RSSPLAIN

Related pages: TaPL_exercise
551155545444554445551111051112000111110111011101055111101015000000030111111111115
5

演習 11.4.1 (page 93)

5

 

1
問(1)
1

型指定を派生形式として形式化せよ。「公式」の型付け規則および評価規則が、その形式化に何らかの適切な意味で対応することを証明せよ。

5

 

5
前提条件
5
評価規則                                      t → t'
4
v1 as T → v1             (E-ASCRIBE)
5

 

4
    t1 → t1'
4
--------------------      (E-ASCRIBE1)
4
t1 as T → t1' as T
5

 

5
型付け規則                                   Γ ⊢ t : T
4
   Γ ⊢ t1 : T
4
--------------------      (T-ASCRIBE)
4
 Γ ⊢ t1 as T : T
5

 

5

 

5
回答
1
考えかた
1
 t as T  →  (λx:T.x) t
1

を e(省略化関数) として定義し、型指定部分(as T)を脱糖衣する。

1

それを、評価規則と型付け規則の両面からラムダ抽象と適用に関する規則を使って導出する。

0

e を導入しても、これまでの評価規則が問題なく適用可能どうかを見る。

5

 

1
評価規則
1
v1 as T → v1             (E-ASCRIBE) 
1

E-ASCRIBEは脱糖衣は v1 そのままなので導出完了。

2

 

0

仮定

0

t1 → t1' が存在するとき、t1 as T → t1' も成り立つか?

0

 

1
    t1 → t1'
1
--------------------      (E-ASCRIBE1)
1
t1 as T → t1' as T
1

↓e

1
    t1 → t1'
0
-------------------- 
1
(λx:T.x) t1 → (λx:T.x) t1'
1

↓ (λ:T11.t12) v2 → [x ↦ v2] t12      (E-APPABS)

1
    t1 → t1'
0
--------------------
1
[x ↦ t1] x → [x ↦ t1'] x
1

1
    t1 → t1'
0
--------------------
1
    t1 → t1'
0

となり、全ての t についても同様に成り立つ。

5

 

5

 

1
型付規則
1
   Γ ⊢ t1 : T
1
--------------------      (T-ASCRIBE)
1
 Γ ⊢ t1 as T : T
0

↓eによる書き換え

1
   Γ ⊢ t1 : T
0
--------------------
1
 Γ ⊢ (λx:T.x) t1 : T
5

 

0
   Γ ⊢ x:T, t1:T 
0
   ---------------- (T-VAR)
0
   Γ,x:T ⊢ t1:T
0
   -------------------------- (T-ABS) 
0
      ⊢ (λx:T.x) : T → T   Γ ⊢ t1 : T
0
  ---------------------------------------------------  (T-APP)
0
                        Γ ⊢ (λx:T.x) t1 : T
3

 

0

 

1
問(2)
1

以下の先行的(egaer) な規則が与えられたとする。

1
   t1 as T → t1                 (E-ASCRIBEEAGER)
1

この規則は、型指定に到達し次第、型指定を除去する。この場合にも、型指定を派生形式として扱うことはできるか。

1

 

1
回答
1

(ペンディング)

1

書籍の答えのページに以下のような注意が書かれていますが、そこまで考えきれていません…

1
 t as T の脱糖衣をする際に、 tの評価を遅延させるような、改良された脱糖
1
 衣を採用する必要がある。
1

 

5

...comment disabled...