シャドーイングの問題
シャドーイングは、現実的には頭の痛い問題で、認める/認めないの判断(決断)が必要だ。が、理論的には特に問題ない。
シャドーイングは入れ子スコープで起こるが、「入れ子にすること」を指標のマージだと解釈する。マージは余ファイバー和と解釈する。余ファイバー和は、スパンに対して定義されるが、スパンは入れ子の可視性によって定義される。
Σ | Δ で、Σの内側に入った指標Δを意味するとき、シャドーイングがないなら、Σ←Σ→(Σ+Δ) というスパンが入れ子を表す。シャドーイングがあるとき、Σ'⊆Σ をシャドーで削られた指標とする。そして、Σ←Σ'→(Σ'+Δ) を作ればいいので、何の問題も起きない。
- シャドーイングは現実的には難しい問題だが、理論的には何ら問題にならない。
で、現実的な話をする。
Σが外側のスコープで、Δが内側のスコープとする。外側のΣ自体に名前sがあるとき、Δ内からs.fooとすれば、Σ内のfooにアクセスできる。sは大域名で、sはシャドーされてないとする。Σに名前がなかったり、名前を使いたくないときは、ΣとΔの相対位置に注目して、Δ内から (upper foo)とする。upperは修飾子で、ひとつ外のスコープにいって見ることを意味する。(upper upper)foo とかしてもよい。
foo = (upper foo) のとき、fooはシャドーされてない。foo ≠ (upper foo) のときfooはシャドーされている。すべての名前fooに関して、foo = (upper foo) か foo ≠ (upper foo) かを決めると、それは貼り合わせデータとなるから、スパンになり、余ファイバー和を定義できる。
スパン(余ファイバー)と余ファイバー和が定義できれば、後はなんとでもなる。