Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 計算体系の数学的性質
- 基本的な性質
- 11. Church-Rosser性(合流性)
- 2.停止性
- 2は不成立
- 停止性 = 実行がとまるか
- Ω = (λx.xx)(λx.xx)
- Ω -β-> Ω -β-> Ω -β-> ...
- 今日の目標
- Church-Rosser性を示すこと
- 平たく言うと計算が合流するか計算順に依存しないか
- ・一見簡単に見えるけれど以外に落とし穴あり
- ・定義から慎重に考えないといけない
- β簡約
- リデックスを書き換える操作
- リデックスがn箇所に現れたらどれから計算するか
- M -------β-> P
- |
- ------β-> Q
- いい加減な合流性の説明:
- 分岐した計算パスを合流させられる
- ←問題のある説明
- リデックスが2つ現れるのはどういうケースがありうる
- 1
- M
- +---------------------------------+
- | |
- | リデックス1 リデックス2 |
- | |
- +---------------------------------+
- リデックスがオーバーラップしていない時
- 2
- オーバーラップする時
- M
- +---------------------------------+
- | +-----------+ |
- | | リデックス2 | リデックス1 |
- | +-----------+ |
- +---------------------------------+
- 3
- 次のような形はない
- +----------------+
- | リデックス1 |
- | +----|------------+
- +-----------|----+ リデックス2 |
- +-----------------+
- オーバーラップする場合を具体的に描くと
- (1) (λx . (....(λy.P)Q...))N
- (2) (λxM)( ...(λy.P)Q...)
- (1)のパターンは合流するか?
- (λx . (λy.P)Q)N
- ---λxから---> (λx . (λy.P)Q)[N/x]
- ---λyから---> (λx . P[Q/y])N
- ----両方共次のようになる---> P[Q/y][N/x]
- (2)のパターンは合流するか?
- (λx.M)((λy.P)Q)
- ----λxから----> M[(λy.P)Q/x]
- ----λyから----> (λx.M)(P[Q/y])
- ----両方共次のようになる---> M[P[Q/y]/x]
- どちらの場合も2つのリデックスが干渉しないので問題なく合流したように見える
- ・この議論には穴がある
- 一箇所ささいな嘘をついてる
- (2)のほうが問題
- (λx.M)(P[Q/y]) -β-> M[P[Q/y]/x]
- に難あり
- ・具体的な例を取ると・・・
- Mとしてxxをとる
- xx[(λy.P)Q/x] ---> ((λy.P)Q)((λy.P)Q) --->2ステップ必要---> P[Q/y]P[Q/y]
- なので(2)のパターンだけはλxから実行した時にはnステップ必要になる。
- 一見大した問題はないように見えるが実は大問題
- o----->o----->o
- | | |
- | | |
- | V V
- | o-->o->o
- | | v>>o
- V V vv>
- o----->o-->o v>....
- ∑(n=0-->M) 1/2^n
- が必要。。。いつまでも1にならない
- -----> 有限回の計算で合流させることができない
- まずはChurch-Rosser性(合流性)の定式化から
- 記法 M --*--> N
- nステップの簡約でMからNになる(n≧0)
- 定義
- 項書換え系がChurch-Rosser性を満たすとは,
- 任意のM(--*-->P, --*-->Q)に対してあるNがあって
- P --*-->, Q --*--> N
- 全部に*がついてイルことに注意
- 参考:弱Church-Rosser性
- 任意のM(---->P, ---->Q)に対してあるNがあって
- P --*-->, Q --*--> N
- 弱Church-Rosser性はCR性を導くことはできない。・・・上の例のようにこれだけでは不十分
- 証明を工夫しないとCR性は出てこない
- ・アイデアが必要
- 並行簡約(パラレル・リダクション)
- 1ステップで平行に簡約したとみなせるようにしたい
- ((λy.P)Q)((λy.P)Q) -->--> P[Q/y]P[Q/y]
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement