「TAPL 読書会＠東京 第17回」の編集履歴（バックアップ）一覧はこちら
「TAPL 読書会＠東京 第17回」(2012/11/17 (土) 14:43:45) の最新版変更点
追加された行は緑色になります。
削除された行は赤色になります。
2012/10/14
lift
モナドってなんなのよ
21.5.1
問題文
lift
1+ という関数があったとする
1+ 2 → 3
1+ 1 → 2
この関数を「lift」して元の集合に対して扱えるようにする
1+ [2 3] → [3 4]
1+ [2 5 6] → [3 6 7]
greatest point of F
least fixed point
generating set for x
21.5.1
定義
G_x = {X⊆U | x ∈ F(X)}
関数が invertible
F が invertible で
partial function support_F ∈ U → P(U) が次のように定義されているとき
support_F(x) = { X if X ∈ G_x and ∀X' ∈ G_x.X⊆X'
↑ if G_x = 空集合
その support function は次のように lift される
support_F(X) = { Ux∈X support_F(x) if ∀x ∈ X.support_F(x) ↓
↑ otherwise
x → X
2012/10/14
lift についてさらに
→ [[モナドって何なのよ>http://dl.dropbox.com/u/7687891/join_to_Monad/join_to_Monad.html]]
21.5.1
問題文
lift
1+ という関数があったとする
1+ 2 → 3
1+ 1 → 2
この関数を「lift」して元の集合に対して扱えるようにする
1+ [2 3] → [3 4]
1+ [2 5 6] → [3 6 7]
greatest point of F
least fixed point
generating set for x
21.5.1
定義
G_x = {X⊆U | x ∈ F(X)}
関数が invertible
F が invertible で
partial function support_F ∈ U → P(U) が次のように定義されているとき
support_F(x) = { X if X ∈ G_x and ∀X' ∈ G_x.X⊆X'
↑ if G_x = 空集合
その support function は次のように lift される
support_F(X) = { Ux∈X support_F(x) if ∀x ∈ X.support_F(x) ↓
↑ otherwise
x → X
21.5.2
solution:
invertibility をチェックするには
S_f と S の定義を inspect すればよい
G(S,T) の each set が高々一つの (at most) 要素だけを持つこと
21.5.3
定義
support_F(x) が定義されているとき
element x は F-supported である
さもなければ F-unsupported である
F-supported な element は support_F(x) = 空集合
であるとき F-ground と呼ばれる
unsupported と F-ground の違いが良くわからない
→ 21章の頭。集合の話
21.3
three-element universe U = {a, b, c}
E1(空集合) = {c} ← ground
Figure 21-2
i は唯一の unuspported element
g は唯一の ground element
h が (ここでの定義に従えば) supported element であることに注意
a given x に対して
set support_E(x) が arrow from x to y が存在する every y を contain する
21.5.5
定義
gfp(X) = if support(X)↑, then false support(X) が undeined のとき false
else if support(X)⊆X, then true support(X) ⊆ X のとき true
otherwise gfp(support(X) U X)
f(x)↑ or f(x) = ↑ mean "f is undefined on x"
f(x)↓ mean "f is defined on x"
2.1.9 definition
gfp を extend
indivisula elements by taking gfp(x) = gfp({x})
2.1.8 definition
partial function
21.5.6 Exercise [ ? ]
Another observation that can be made from Figure 21-2 is that an element x of vF is not a member
of μF if x participates in a cycle in the support graph (or if there is a path from x to an
element that participates in a cycle). Is the converse also true that is, if x is a member of vF
but not μF , is it necessarily the case that x leads to a cycle?
The remainder of the section is devoted to proving the correctness and termination of gfp .
(First-time readers may want to skip this material and jump to the next section.) We start by
observing a couple of properties of the support function.
21.5.7
lemma
X ⊆ F ( Y ) iff support F ( X ) ↓ and support F ( X ) ⊆ Y .
support_F(X) が定義されていてかつ support_F(X) ⊆ Y のときにのみ
X ⊆ F(Y)
21.5.13
exercise
Suppose F is an invertible generating function.
Define the function lfp_F (or just lfp) as follows:
lfp(X) = if support(X)↑, then false
else if X = O, then true
else lfp(support(X)).
Intuitively, lfp works by starting with a set X and using the support relation to reduce it
until it becomes empty. Prove that this algorithm is partially correct, in the sense that
If lfp_F(X) = true, then X ⊆ μF.
If lfp_F(X) = false, then X ? μF.
Can you find a class of generating functions for which lfp_F is guaranteed to terminate on
all finite inputs?
finite な入力全てに対して lfp_F のterminate が保証される
generating functions の class とは?
21.6 More Efficient Algorithms
gfp^s
gfp^t
メモを持ち回る感じ
一度みつかったものを何回も探しに行くことをしない
