#【教えて君】f::a->b、g::b->a、ia=g.f、ib=f.gとしたとき、iaおよびibが恒等関数になっているかどうかを形式的に示したいときどんな風に示せばいいのでしょうか。
#反例を上げれば恒等関数になっていることを示せますが、反例が見つからないときに、恒等関数になるということを示すにはどのように論じればいいでしょうか。
#反例を上げれば恒等関数になっている → 反例を上げれば恒等関数になっていない
#fやgがどのように与えられてるかによるような… 定義域,値域が離散・有限でf, gが列挙で与えられてたらtrivialですよね。どういう問題を想定してるんでしょ。
#fはdereference関数、gはreference関数、ただし、dereference関数は引数がnullだったらnullでなくなるまでブロックする
#どのようなsemanticsを与えるかによるんですが、どのようにsemanticsを与えれば議論できるかがわかっていないのです > わし
#私もよくわからないですが、何らかの形式的な仕様が与えられてて、その合成を置換してったら恒等写像になった、っていうふうにできたらまあいいのかなって気はします。
#fとgはプリミティブであるとして、どのようにsemanticsを与えれば、それぞれdereferenceとreferenceと言えるだろうかということを考えています。
#ですくなくとも、f.g と g.f は恒等関数になっていなければならないだろうと。
#操作的意味論を定義して、観測等価性を証明するのが普通の方法かと。
#dereferenceがブロックする可能性があるということを表現するにはどのような操作的意味論を構成するのが通常でしょうか？
#観測等価性とは形式的にはどういうものですか？
#ブロックするのはSTMの論文の操作的意味論を見ると良いかも。
#おお、なるほど、早速さがしてみます
##あれっ。この説明なんか読んだことあるなぁ。いつどこで？>わし
haskell-ja > Archives > 2011/12/15