Open8

ch21 再帰型のメタ理論

def 21.5.5 gfp

X support(X) support(X) \cup X
\{a\} \{b,c\} \{a,b,c\}
\{a,b,c\} \{b,c,e,f,g\} \{a,b,c,e,f,g\}
\{a,b,c,e,f,g\} \{b,c,e,f,g,d\} \{a,b,c,e,f,g,d\}
\{a,b,c,e,f,g,d\} \{b,c,e,f,g,d\} \{a,b,c,e,f,g,d\}

support(X) \subseteq X が成り立つので gfp(\{a\})ture を返す。
よって、\{a\} は最大不動点に含まれる。

Haskell 実装

gfp :: InferRule -> Universe -> Bool
gfp rule setX
  | isNothing setX' = False
  | fromJust setX' `Set.isSubsetOf` setX = True
  | otherwise = gfp rule (fromJust setX' `Set.union` setX)
  where
    setX' = supportSet rule setX

gfp の問題点

余分な再計算が起こる。

def 21.6.1 gfp^{a}

各要素の支持集合を高々1回しか計算しないバージョン。

A X support(X) A \cup X support(X) \setminus (A \cup X)
\emptyset \{a\} \{b,c\} \{a\} \{b,c\}
\{a\} \{b,c\} \{e,f,g\} \{a,b,c\} \{e,f,g\}
\{a,b,c\} \{e,f,g\} \{d,g\} \{a,b,c,e,f,g\} \{d\}
\{a,b,c,e,f,g\} \{d\} \{b\} \{a,b,c,d,e,f,g\} \emptyset
\{a,b,c,d,e,f,g\} \emptyset - - -

X=\emptyset が成り立つので gfp^{a}(\emptyset,\{a\})true を返す。
よって、\{a\} は最大不動点に含まれる。

Haskell 実装

gfpA :: InferRule -> Universe -> Bool
gfpA rule setX = gfpA' rule (Set.empty, setX)

gfpA' :: InferRule -> (Universe, Universe) -> Bool
gfpA' rule (setA, setX)
  | isNothing setX' = False
  | Set.null setX = True
  | otherwise = gfpA' rule (setAX, fromJust setX' `Set.difference` setAX)
  where
    setAX = setA `Set.union` setX
    setX' = supportSet rule setX

def 21.6.3 gfp^{s}

X の要素を1つだけ取り出して計算するバージョン。

A X x support(x) A \cup \{x\} ①\ X \cup support(x) ① \setminus (A \cup \{x\})
\emptyset \{a\} a \{b,c\} \{a\} \{a,b,c\} \{b,c\}
\{a\} \{b,c\} b \{e\} \{a,b\} \{b,c,e\} \{c,e\}
\{a,b\} \{c,e\} c \{f,g\} \{a,b,c\} \{c,e,f,g\} \{e,f,g\}
\{a,b,c\} \{e,f,g\} e \{d\} \{a,b,c,e\} \{e,f,g,d\} \{f,g,d\}
\{a,b,c,e\} \{f,g,d\} f \{g\} \{a,b,c,e,f\} \{f,g,d\} \{g,d\}
\{a,b,c,e,f\} \{g,d\} g \emptyset \{a,b,c,e,f,g\} \{g,d\} \{d\}
\{a,b,c,e,f,g\} \{d\} d \{b\} \{a,b,c,e,f,g,d\} \{d,b\} \emptyset
\{a,b,c,e,f,g,d\} \emptyset - - - - -

X=\emptyset が成り立つので gfp^{s}(\emptyset, \{a\})true を返す。
よって、\{a\} は最大不動点に含まれる。


x の選び方は適当で良いので、例えば上の例で f を選ぶ前に g を選ぶと、次のようになる。

A X x support(x) A \cup \{x\} ①\ X \cup support(x) ① \setminus (A \cup \{x\})
\{a,b,c,e\} \{f,g,d\} g \emptyset \{a,b,c,e,g\} \{f,g,d\} \{f,d\}
\{a,b,c,e,g\} \{f,d\} f \{g\} \{a,b,c,e,g,f\} \{f,d,g\} \{d\}
\{a,b,c,e,g,f\} \{d\} d \{b\} \{a,b,c,e,g,f,d\} \{d,b\} \emptyset
\{a,b,c,e,g,f,d\} \emptyset - - - - -

memo

gfp^{s}(\emptyset, X) のように計算するだけなら if\ x \in A\ then\ gfp^{s}(A, X \setminus \{x\}) は不要になるはず。

Haskell 実装

gfpS :: InferRule -> Universe -> Bool
gfpS rule setX = gfpS' rule (Set.empty, setX)

gfpS' :: InferRule -> (Universe, Universe) -> Bool
gfpS' rule (setA, setX)
  | Set.null setX = True
  | Set.member x setA = gfpS' rule (setA, setX `Set.difference` Set.singleton x)
  | isNothing setX' = False
  | otherwise = gfpS' rule (setAx, (setX `Set.union` fromJust setX') `Set.difference` setAx)
  where
    x = Set.elemAt 0 setX
    setAx = setA `Set.union` Set.singleton x
    setX' = supportSet rule setX

def 21.6.4 gfp^{t}

引数を集合では無く候補となる要素1つだけを取るようにしたバージョン。

変更点

  • 末尾再帰ではなくなる
  • 返り値が仮定の集合
A x x \in A support(x) A_{0} A_{1} A_{2}
gfp^{t}(\emptyset, a) \emptyset a false \{b,c\} \{a\} gfp^{t}(A_{0}, b) gfp^{t}(A_{1}, c)
gfp^{t}(A_{0}, b) \{a\} b false \{e\} \{a,b\} gfp^{t}(A_{0}, e) -
gfp^{t}(A_{0}, e) \{a,b\} e false \{d\} \{a,b,e\} gfp^{t}(A_{0}, d) -
gfp^{t}(A_{0}, d) \{a,b,e\} d false \{b\} \{a,b,e,d\} gfp^{t}(A_{0}, b) -
gfp^{t}(A_{0}, b) \{a,b,e,d\} b true - - - -

この段階で gfp^{t}(A_{0}, b) = \{a,b,e,d\} が得られる。

A x x \in A support(x) A_{0} A_{1} A_{2}
gfp^{t}(A_{1}, c) \{a,b,e,d\} c false \{f,g\} \{a,b,e,d,c\} gfp^{t}(A_{0}, f) gfp^{t}(A_{1}, g)
gfp^{t}(A_{0}, f) \{a,b,e,d,c\} f false \{g\} \{a,b,e,d,c,f\} gfp^{t}(A_{0}, g) -
gfp^{t}(A_{0}, g) \{a,b,e,d,c,f\} g false \emptyset \{a,b,e,d,c,f,g\} - -

ここで gfp^{t}(A_{0}, f) = \{a,b,e,d,c,f,g\} が得られる。

A x x \in A support(x) A_{0} A_{1} A_{2}
gfp^{t}(A_{1}, c) \{a,b,e,d\} c false \{f,g\} \{a,b,e,d,c\} \{a,b,e,d,c,f,g\} gfp^{t}(A_{1}, g)
gfp^{t}(A_{1}, g) \{a,b,e,d,c,f,g\} g true - - - -

ここで gfp^{t}(A_{1}, g) = \{a,b,e,d,c,f,g\} が得られる。
よって gfp^{t}(A_{1}, c) = gfp^{t}(\emptyset, a) = \{a,b,e,d,c,f,g\} が得られる。

gfp^{t}(\emptyset, a) が成功したため、\{a\} は最大不動点に含まれる。

Haskell 実装

gfpT :: InferRule -> Element -> Bool
gfpT rule x = isJust $ gfpT' rule (Just Set.empty, x)

gfpT' :: InferRule -> (Maybe Universe, Element) -> Maybe Universe
gfpT' rule (mSetA, x) = do
  setA <- mSetA

  if Set.member x setA
    then mSetA
    else do
      xs <- Set.toList <$> support rule x
      let a0 = setA `Set.union` Set.singleton x
          go = flip $ curry $ gfpT' rule
      foldr go (Just a0) xs

TODO: BNF, (可逆な)生成関数, 推論規則, 支持関数 の繋がりについてまとめる

ex 21.5.13 lfp

最大不動点ではなく、最小不動点の所属性検査を行う関数。

  • 与えられた要素が循環に含まれるか、循環に含まれる要素に依存している場合に無限ループになり、実行が止まらなくなる
X support(X)
\{c\} \{f,g\}
\{f,g\} \{g\}
\{g\} \emptyset
\emptyset -

X=\emptyset が成り立つので lfp(\{c\})true を返す。
よって \{c\} は最小不動点に含まれる。


循環の場合は以下のように無限ループする。

X support(X)
\{b\} \{e\}
\{e\} \{d\}
\{d\} \{b\}
\{b\} \{e\}

Haskell 実装

lfp :: InferRule -> Universe -> Bool
lfp rule setX
  | isNothing setX' = False
  | Set.null (fromJust setX') = True
  | otherwise = lfp rule (fromJust setX')
  where
    setX' = supportSet rule setX

lfp 問題点

  • 余分な再計算が起こる。
  • 循環や無限列が含まれる場合に停止しない

lfp^{a}

  • gfp^{a} のように lfp に対しても仮定の集合を持つようにしたバージョン
  • 循環を扱えるようになる

定義

TODO

lfp^{a}(A, X) ={\rm if\ } support(X)\uparrow {\rm then\ } false \\ {\rm else\ if\ } A = X = \emptyset {\rm \ then\ } true \\

Haskell 実装

lfpA :: InferRule -> Universe -> Bool
lfpA rule setX = lfpA' rule (Set.empty, setX)

lfpA' :: InferRule -> (Universe, Universe) -> Bool
lfpA' rule (setA, setX)
  | isNothing setX' = False
  | setA == (setA `Set.union` setX) = Set.null setX -- 循環チェック
  | otherwise = lfpA' rule (setA `Set.union` (setX `Set.difference` fromJust setX'), fromJust setX')
  where
    setX' = supportSet rule setX

lfp^{a} の問題点

  • 余分な再計算が起こる
  • 無限列に対しては停止しない

def 21.5.1 可逆と suport

TODO

ログインするとコメントできます