Advertisement
Guest User

Untitled

a guest
May 11th, 2015
878
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. 計算体系の数学的性質
  2. 基本的な性質
  3. 11. Church-Rosser性(合流性)
  4. 2.停止性
  5.  
  6. 2は不成立
  7. 停止性 = 実行がとまるか
  8. Ω = (λx.xx)(λx.xx)
  9. Ω -β-> Ω -β-> Ω -β-> ...
  10.  
  11. 今日の目標
  12. Church-Rosser性を示すこと
  13. 平たく言うと計算が合流するか計算順に依存しないか
  14. ・一見簡単に見えるけれど以外に落とし穴あり
  15. ・定義から慎重に考えないといけない
  16.  
  17. β簡約
  18.  
  19. リデックスを書き換える操作
  20.  
  21. リデックスがn箇所に現れたらどれから計算するか
  22.  
  23. M -------β-> P
  24.    |
  25.    ------β-> Q
  26.    
  27. いい加減な合流性の説明:
  28. 分岐した計算パスを合流させられる
  29. ←問題のある説明
  30.  
  31. リデックスが2つ現れるのはどういうケースがありうる
  32.  
  33. 1
  34.  
  35.   M
  36.  +---------------------------------+
  37.  |                                 |
  38.  |  リデックス1           リデックス2       |
  39.  |                                 |
  40.  +---------------------------------+
  41.  
  42. リデックスがオーバーラップしていない時
  43.  
  44. 2
  45.  
  46. オーバーラップする時
  47.  
  48.   M
  49.  +---------------------------------+
  50.  | +-----------+                   |
  51.  |  | リデックス2  |     リデックス1        |
  52.  | +-----------+                   |
  53.  +---------------------------------+
  54.  
  55. 3
  56. 次のような形はない
  57.  
  58.  +----------------+
  59.  |  リデックス1        |
  60.  |           +----|------------+
  61.  +-----------|----+      リデックス2  |
  62.              +-----------------+
  63.  
  64.  
  65. オーバーラップする場合を具体的に描くと
  66.  
  67. (1) (λx . (....(λy.P)Q...))N
  68. (2) (λxM)( ...(λy.P)Q...)
  69.  
  70.  
  71.  
  72.  
  73. (1)のパターンは合流するか?
  74. (λx . (λy.P)Q)N
  75.  
  76. ---λxから---> (λx . (λy.P)Q)[N/x]
  77. ---λyから---> (λx . P[Q/y])N
  78.  
  79. ----両方共次のようになる---> P[Q/y][N/x]
  80.  
  81. (2)のパターンは合流するか?
  82. (λx.M)((λy.P)Q)
  83.  
  84. ----λxから----> M[(λy.P)Q/x]
  85. ----λyから----> (λx.M)(P[Q/y])
  86.  
  87. ----両方共次のようになる---> M[P[Q/y]/x]
  88.  
  89. どちらの場合も2つのリデックスが干渉しないので問題なく合流したように見える
  90. ・この議論には穴がある
  91. 一箇所ささいな嘘をついてる
  92. (2)のほうが問題
  93.  
  94. (λx.M)(P[Q/y]) -β-> M[P[Q/y]/x]
  95. に難あり
  96.  
  97. ・具体的な例を取ると・・・
  98.   Mとしてxxをとる
  99.    xx[(λy.P)Q/x] ---> ((λy.P)Q)((λy.P)Q) --->2ステップ必要---> P[Q/y]P[Q/y]
  100.    
  101. なので(2)のパターンだけはλxから実行した時にはnステップ必要になる。
  102. 一見大した問題はないように見えるが実は大問題
  103.  
  104. o----->o----->o
  105. |      |      |
  106. |      |      |
  107. |      V      V
  108. |      o-->o->o
  109. |      |   v>>o
  110. V      V   vv>
  111. o----->o-->o v>....
  112.  
  113. (n=0-->M) 1/2^n
  114. が必要。。。いつまでも1にならない
  115.  
  116. -----> 有限回の計算で合流させることができない
  117.  
  118. まずはChurch-Rosser性(合流性)の定式化から
  119. 記法 M --*--> N
  120. nステップの簡約でMからNになる(n≧0)
  121.  
  122. 定義
  123. 項書換え系がChurch-Rosser性を満たすとは,
  124. 任意のM(--*-->P, --*-->Q)に対してあるNがあって
  125. P --*-->, Q --*--> N
  126. 全部に*がついてイルことに注意
  127.  
  128. 参考:弱Church-Rosser性
  129. 任意のM(---->P, ---->Q)に対してあるNがあって
  130. P --*-->, Q --*--> N
  131.  
  132. 弱Church-Rosser性はCR性を導くことはできない。・・・上の例のようにこれだけでは不十分
  133.  
  134. 証明を工夫しないとCR性は出てこない
  135. ・アイデアが必要
  136. 並行簡約(パラレル・リダクション)
  137.  
  138. 1ステップで平行に簡約したとみなせるようにしたい
  139. ((λy.P)Q)((λy.P)Q) -->--> P[Q/y]P[Q/y]
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement