TAPL 読書会@東京 第17回


lift についてさらに


1+ という関数があったとする

1+ 2 → 3
1+ 1 → 2


1+ [2 3] → [3 4]
1+ [2 5 6] → [3 6 7]

greatest point of F
least fixed point

generating set for x


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


invertibility をチェックするには
S_f と S の定義を inspect すればよい
G(S,T) の each set が高々一つの (at most) 要素だけを持つこと


support_F(x) が定義されているとき
element x は F-supported である
さもなければ F-unsupported である
F-supported な element は support_F(x) = 空集合
であるとき F-ground と呼ばれる

unsupported と F-ground の違いが良くわからない
 → 21章の頭。集合の話
        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 する


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.


X ⊆ F ( Y ) iff support F ( X ) ↓ and support F ( X ) ⊆ Y .

support_F(X) が定義されていてかつ support_F(X) ⊆ Y のときにのみ
X ⊆ F(Y)


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


最終更新:2012年11月17日 14:43