full abstraction
full abstraction ... λ計算とかπ計算とか表示的意味論のお話ではよく出てくる概念なんですが、未だによくわからないなーとつぶやいていたら id:sumii さんに教えていただいた。 もったいないのでここに残しておきます。
full abstraction の私的な説明
計算体系Aと計算体系(もしくはモデル)B があるとして、 その間の変換を C[・] : A -> B、 〜A と 〜B をそれぞれの計算体系(かモデル)における等価性とします。
すべてのAの項 ta1とta2について
- C[ta1] 〜B C[ta2] ならば ta1〜A ta2 ... adequacy(soundness)
- ta1 〜A ta2 ならば C[ta1] 〜B C[ta2] ... completeness
この両方が成り立つとき、 変換は fully abstract であるといいます。
たとえば プログラミング言語(PCF)の操作的意味定義と そのモデル(表示的意味)を対応づけたり、他には 高階π計算 とπ計算の表現能力を云々したりするときに使っているのを見たことがあります。
full abstractionを使えば、ふつうのPCFの操作的意味は 表示的意味に対して fully abstractじゃないので parallel or 構文を追加しますよーとか、 高階π計算はπ計算で表現可能ですよー、とかそういう議論ができるようになります。
参考 (よりわかりやすい or きっちりとした説明)
twitterログ
 | keigoi | full abstractionが未だにわからん。。completenessは分かる、すげーよくわかる… 変換前のequivalenceが変換後も成り立つってことだからな… 変換後の項で意味を議論するなら必須だろう… だが何だsoundnessって! という程度の能力 | link |
| keigoi | 何がわからんのかわからん。 | link |
| keigoi | あれか、変換云々もあるけど元の項のequivalenceと変換先のequivalenceの比較なのか | link |
| keigoi | んー。 sound(adequate?)なら、変換先の項でequivalenceが証明できたら変換元の項でも等価。 completeなら、等価な変換元の項を変換先の文脈にぶち込める。 かなぁ | link |
 | esumii | @keigoi 変換前が異なれば（等価でなければ）、変換後も異なる、という説明では駄目ですか？＞soundness | link |
| keigoi | @esumii 恐れ入ります。 いえ、それでわかるんですが、なんとなく full abstraction は 変換の正しさを云々するもの、という印象があって... | link |
| keigoi | @esumii completeness の場合, 変換前の意味(等価性)が変換後にも保存されている，というのはまあわかるんですが、一方 変換後に等しければ変換前でも等しい、という性質の使いどころって何？と思ったのでした。 | link |
| keigoi | @esumii 調べてみてよく考えると、 たとえば表示的意味論では denotationが等しければ 元の項が観測等価になる、みたいな性質のおかげで、わざわざ 元の操作的意味で bisimulation作らなくても等価性が証明できる(例えば) みたいなことができるんですね。 | link |
| esumii | @keigoi そんな難しいこと(?)を考えなくても、単に（対偶をとって）「働きが異なるプログラムの意味が同じになってしまったらおかしい」というだけの話だと思います。 > soundness | link |
| esumii | ちなみに「soundness」より「adequacy」のほうが標準的用語かもしれません。 | link |
| keigoi | @esumii マッピング先(例:コンパイルされたバイナリ)で等価な出力を出すやつがマッピング元(例:ソース)で構文的に全然違うプログラムだったとしても困らないなぁなどと考えていたのでした。 | link |
| keigoi | @esumii Sangiorgiの The π-calulus... では、adequacyとsoundnessが微妙に違う用法で使われていたので少し混乱していました。 | link |
| esumii | @keigoi あれ、すみません、質問を勘違いしてたかも…。Full abstractionとかadequacyとかいうときの「変換前の等価性」は、構文的な同一性ではなくて、プログラムの振る舞いに基づく等価性（文脈等価性や双模倣など）を用いることが通常です。 | link |
| keigoi | @esumii そういうことだったんですね。調べててうすうす気づいていたんですが、確証が得られてうれしいです。 そもそも疑問を正しくことばにできてなかったですね。 ありがとうございます！ | link |
| keigoi | @esumii さらに ぐぐって見つけた http://bit.ly/44lmbQ (PDF注意) では adequacy=soundness+(弱い)completeness となっていて、full abstractionそれより強い性質みたいでした. いろいろあるんですね… | link |
# ちなみにこの発言ログは Twitterログまとめで作りました
