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$ の問題点

余分な再計算が起こる。

wado 2020/12/08に更新

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

wado 2020/12/08に更新

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

wado 2020/12/08に更新

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

wado 2020/12/08

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

wado 2020/12/08に更新

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$ 問題点

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

wado 2020/12/08に更新

$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}$ の問題点

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

wado 2020/12/08

def 21.5.1 可逆と $suport$

TODO

def 21.5.5 gfp

Haskell 実装

gfp の問題点

def 21.6.1 gfp^{a}

Haskell 実装

def 21.6.3 gfp^{s}

memo

Haskell 実装

def 21.6.4 gfp^{t}

Haskell 実装

ex 21.5.13 lfp

Haskell 実装

lfp 問題点

lfp^{a}

定義

Haskell 実装

lfp^{a} の問題点

def 21.5.1 可逆と suport

def 21.5.5 $gfp$

$gfp$ の問題点

def 21.6.1 $gfp^{a}$

def 21.6.3 $gfp^{s}$

def 21.6.4 $gfp^{t}$

ex 21.5.13 $lfp$

$lfp$ 問題点

$lfp^{a}$

$lfp^{a}$ の問題点

def 21.5.1 可逆と $suport$