TAPL 読書会@東京 第15回



F が invertible であるとき partial function supportF ∈ U → P(U) は次のように定義される

supportF(x) = { X  if X ∈ Gx and ∀X' ∈ Gx. X ⊆ X'
                ↑ if Gx = 空集合

The support function is lifted to sets as follows

 supportF(x) = {U x ∈x supportF(x) if ∀x ∈ X. supportF(x)↓
                ↑                  otherwise

下向き矢印は何を意味しているの? → 定義域 defined

parial function は数学的には×

Verify that Sf and S,
the genrating functions for the subtyping relations from Definitions 21.3.1 and 21.3.2,
are invertible, and give their support functions

Our goal is to develop algorithms for checking membership
in the least ad greatest fixed points of a generatong function F.
The basic steps in these algorithms will involve "running F backwards":
to check membership for an element x,
we need to ask how x cound have been generated by F.
the advantage of an invertbile F is that there is at most one way to generated by F.
For a non-invertible F, elements can be generated in multiple ways,
leading to a combinatorial explosion in the number of paths that the algorithm must explore.
From now on, we restrict our attention to invertible generating functions.



supoort function とは?


An element x is F-supported if supportF(x)↓;
otherwise, x is F-unsupported.
An F-supported element is called F-ground if supportF(x) = 空集合
最終更新:2012年11月17日 14:36