TaPL_exercise_11_3 RSSPLAIN

Related pages: TaPL_exercise
55555555555555555555555555555555555555555555555535000000055554500050000100500500555000000500000000005055022520005000000005000000000000005
5

演習 11.3.1 (page 91)

5

 

5
t1 = (λx : Unit.x) unit
5

 

5
t_i+1 = (λf:Unit → Unit.f(f(unit)))
5
        (λx:Unit.t_i)
5

 

5

 

5

演習 11.3.2 にあたって

5

 

5
';'(逐次実行)の規則を引用
5

 

5
評価規則
5
    t1 → t1'
5
--------------------    (E-SEQ)
5
t1;t2 → t1' ; t2
5

 

5
v1;t2 → t2             (E-SEQNEXT)
5

 

5
型付規則
5
Γ ⊢ t1:Unit   Γ  ⊢ t2:T2
5
--------------------    (T-SEQ)
5
Γ ⊢ t1;t2 : T2
5

 

5

 

5
 _(ワイルドカード)の回答
5

追加すべき型付け規則と評価規則は以下の通り。

5

 

5
Γ ⊢ t2:T1
5
-------------------------    (T-WILDCARD)
5
Γ ⊢ λ_:T1.t2:T1 → T2
5

 

5
(λ_:T11.t12)v2 →  t12      (E-WILDCARD)
5

 

5
比較参考用: ※ 前章で出てきた T-ABSの型付け規則。
5
    x:T1 ⊢ t2:T2
5
------------------------     (T-ABS)
5
 ⊢ λx:T1.t2:T1 → T2
5

 

5

 

5

 

5

演習 11.3.1 の証明 (page 91)

5

 

5

演習 11.3.2 で _(ワイルドカード)の規則を入れても同様の証明でOK。

5

 

5
回答
5
考えかた1
5

t1;t2 は 「(λx:Unit.t2) t1」 の略記(省略化)であるため、いつでも書き換え可能。

3

よって次の変換経路はどれも適用可能。「→e」 は e(省略化関数)を適用という意味。

5

 

0
考えかた2
0

eは再帰的定義とする必要がある。eを再起にしないとうまく証明できない。

0

 

0

定理1.1

0
 t → E t' のとき e(t) → I e(t') である。
0

 

0

構造的帰納法の仮定を以下と置く。

5
     t             →             t'
5
              E(外部言語のまま)
5
     ↓e ↑e(逆)                 ↓e ↑e(逆)
5
     e(t)           →            e(t')
4
              I(内部言語のまま)
5

 

0

上記のうち、右回りの経路、左回りの経路の二つの経路で、同じ結果になることを証明する。

0
t →  t' → e(t')
0
t → e(t) → e(t')
5

 

0
評価規則の証明。E-SEQを使った評価導出による。
0
 t=t1;t2の形について、
0
t1;t2                      →             t1';t2
0
                       E-SEQを適用
1
   ↓e ↑e(逆)                               ↓e ↑e(逆)
0
 (λx:Unit.e(t2)) e(t1)     →             (λx:Unit.e(t2)) e(t1')
0
                        I内部言語まま
5

 

0

E-SEQを適用した評価導出においても右回りの経路と、左回りの経路で同じ結果になる。

0

構造的帰納法により 全ての t においても成り立つ。

5

 

0

 

0
もうひとつの定理
5

定理1.2

5
 e(t) → I u  であれば λE の項 t' が存在して、u = e(t') かつ t → E t' 
5

 

0

構造的帰納法の仮定

0
t             →               E t'    
0
                               ↑e(逆) 
0
e(t)          →               e(t')   
0
     ↓                        ↑e(逆) 
0
            u = e(t')                  
5

 

0
評価規則の証明。E-SEQを使った評価導出による。
0

t=t1;t2の場合 → t'=t1';t2 のとき。

0
 t = t1;t2                 →            t' = t1';t2
0
                      E-SEQを適用
0
  ↓e                                     ↑e(逆)
0
e(t) = e(t1;t2)             →           e(t') = e(t1';t2) 
0
  ↓                                      ↑
0
 (λx:Unit.e(t2)) e(t1)                   ↑e(逆)
0
  ↓                                      ↑
0
         u = (λx:Unit.e(t2)) e(t1')   
5

 

0

構造的帰納法により、全ての t においても成り立つ。

5

 

5

 

0
型付け規則の証明
2

定理2.1

2
 Γ ⊢ E t:T のとき、かつそのときに限り Γ ⊢ I e(t) : T
5

 

2

以下のように型付け導出して証明する。

0
仮定1
0
 t=t1;t2の場合
0
 Γ ⊢ E t:T のとき Γ ⊢ I e(t) : T
5

 

0

型付導出による証明

0
         Γ ⊢ t2:T2                                                    
0
 --------------------------------------------------------- (T-ABS)     
0
         Γ ⊢ λx:Unit.e(t2) : Unit → T2      Γ ⊢ t2:T2            
0
      ------------------------------------------ (T-APP)
0
        Γ ⊢ λx:Unit.e(t2) e(t1) : T2                               
0
      ------------------------------------------ (関数eによる書き換え)
0
        Γ ⊢ t1;t2 : T2
5

 

0
仮定2
0
 t=t1;t2の場合
0
 Γ ⊢ I e(t) : Tのとき、Γ ⊢ E t:T
0

 

0

型付導出による証明

0
        Γ ⊢ t1:Unit    Γ ⊢ t2:T2                                    
0
 ------------------------------------------------------- (T-SEQ)              
0
        Γ ⊢ t1;t2 : T2                                              
0
      ------------------------------------------ (関数e(逆)による書き換え)
0
        Γ ⊢ λx:Unit.e(t2) e(t1) : T2                               
0
      ------------------------------------------ (関数eによる書き換え)
0
        Γ ⊢ e(t1;t2) : T2                                           
0

 

0

 

5

...comment disabled...