お知らせ『1月31日に一度初期化したいと思います。』　（他のお知らせを読むにはここをクリック）
並び順： 階層 時系列
0
+30		(・_・)しらちゃ[15:18]
!m 延々私がプログラム意味論に関する証明を書くためのゼロ．☆
1
(・_・)しらちゃ[15:20]
☆
Lemma 5.43
g0 : A State to State "partial" function .
p : State -> Boolean function .
とする．このとき
F g = cond(p, g, g0)
は，continuous functionである．
2
(・_・)しらちゃ[15:23]
Continuous性は，monotone性( d1 <= d2 ならば (f d1) <= (f d2) )を持ち，かつ，fのDomainに対する空ではないchain「Y」に対して，f(□Y) = □{f d | d in Y}であるという性質．ただし，□YはYのLeast Upper Bound(最小上界)のこと．☆
3
(・_・)しらちゃ[15:23]
ここでは，Continuousを示すため，まずmonotone性を示し，その後2つめの性質を示す．☆
4
(・_・)しらちゃ[15:25]
☆
F is monotone?
g1 <= g2 と仮定し，(F g1) <= (F g2)を示せばよいため，
g1 <= g2と仮定する．
sとs'を，((F g) s) = s'となるような，Stateとする．
5
(・_・)しらちゃ[15:26]
☆
ここで，(p s)についてケース分けを行う．
まず，(p s) = trueとする．
6
(・_・)しらちゃ[15:28]
☆
(F g1) s = cond(p, g1, g0) s (from Fの定義)
= (g1 s) (from condの定義(アバウトに言えば第一引数の結果がtrueなら第二引数を返す，falseなら第二引数を返す)と(p s) = trueより．
ところでここで，(F g1) s = s'だったので(g1 s) = s'となる．
7
(・_・)しらちゃ[15:30]
☆
ところで，仮定からg1 <= g2なので，g1 s = s' ならば　g2 s = s'(これは<=がそういう定義)
(F g2) s = cond(p, g2, g0) s (from Fの定義)
= (g2 s) (from condの定義)
= s' (上の議論から g2 s = s')
したがって，p s = ttなら，monotone.
8
(・_・)しらちゃ[15:32]
☆
次に，p s = falseの場合を考える．
(F g1) s = cond(p, g1, g0) s (Fの定義より)
= g0 s (condの定義とp s = falseより)
= s' ( (F g1) s = s' より )
したがって，g0 s = s'
(F g2) s = cond(p, g2, g0) s (Fの定義より)
= g0 s (condの定義とp s = falseより)
= s' (上のg0 s = s'より)
したがって，p s = falseならばmonotone.
9
+7		(・_・)しらちゃ[15:33]
☆
ここまでの結果を合わせると，結局 F は monotone .
証明了．
10
+6		(^-^)目次◆IndexIsVCs[15:34]>>9
なるほど。☆
11
(^-^)目次◆IndexIsVCs[15:34]>>10
わからん。☆
12
+4		(・_・)しらちゃ[15:35]>>10
☆
このゼロの中身は説明するつもり完全ナシで，とりあえず書いてみようって内容なので，気にしたら負けます．
しらちゃって，変なコトしてんなーって想って貰えたらおうけい．
13
+1		(・_・)zzzz◆zzzzzz.bJQ[15:39]>>12
自分にはなにがなんだか分からないけど一貫性があるっぽいのってわくわくするぞ！モスバーガーのあれみたいな！☆
16
(^-^)しらちゃ[15:40]>>13
☆
この辺の話し，プログラム意味論っていって，数学的にプログラムの意味を考えてみましょう－．みたいな分野なのですが
興味のある人がいれば，簡単な集合論から順番に話してみたいなーって想ってたりします．
14
+1		(・_・)しらちゃ[15:39]>>12
☆
さて，次に第二の性質，F(□Y) = □{F g| g in Y) where Y is in State -> State "partial" functionsというのを考えるのですが……．
ここまでに，しらちゃは幾つかLemmaを手に入れてます．
省略しますが，それを使いますと
graph(F(□Y)) が U{graph(F g) | g in Y} の部分集合ならcontinuousです．(ただし，Uは，集合の中身の集合を全部”くっつけた”(和を取った)集合．)
15
(・_・)しらちゃ[15:39]>>14
しまた，ゼロに直下で書くつもりだたのにミスった．☆
17
(・_・)しらちゃ[15:42]
☆
（いろいろ省略)
graph(F(□Y)) が U{graph(F g) | g in Y} の部分集合ならcontinuousです(何)
ただし，graph(f)というのは，f関数の引数と戻り値のペアの全体の集合のことです．

さて，こっからググっと考えないと．．．
18
(・_・)しらちゃ[15:53]
☆
sとs'をそれぞれ，(F □Y) s = s'となるようなStateとします．
すると，あるgがYに含まれていて，(F g) s = s'です．

ここでp sについて条件分けします．まずp s = trueから考えます．
すると，(F □Y) s = (□Y) s = s'なので，sとs'のペアは，graph(□Y)に含まれています．

ところで，ちょっと前にgraph(□Y) = U{graph(g) | g in Y}を証明してあります．
したがって，s, s'のペアは，U{graph(g) | g in Y}にも含まれています．
つまり，p s = trueの時，graph(F(□Y))はU{graph(g) | g in Y}の部分集合と解ります．このケースはOKです．
19
(・_・)しらちゃ[15:59]
☆
p s = falseの場合を考えます．
このとき，
(F □Y) s = cond(p, □Y, g0) (Fの定義から)
= g0 s (condの定義とp s = trueから)
= s' ( (F □Y) s = s' と仮定したので．)
なので， g0 s = s'です．
さらに，gを，Yに含まれるStateからStateへのpartial functionとします．
このとき
(F g) s = cond(p, g, g0) (Fの定義から)
= g s (condの定義とp s = trueから)
= s' ( (F g) s = s' から )
なので，あるgに対して，graph(F g)はs,s'のペアを含みます．
ということは，U{ graph(F g) | g in Y }も s, s'のペアを含みます．
即ち，p s = falseの時，graph(F(□Y))はU{graph(g) | g in Y}の部分集合と解ります．
全ての条件で成り立ちました．証明了．
20
+7		(^-^)しらちゃ[16:01]
てことで，Lemma5.43について証明してみた．☆
21
+6		(・_・)しらちゃ[16:14]>>20
しかしこの試みは余り面白く無かったな．説明不足だらけだから解る人は一人もおるまい．☆
22
+5		(・_・)濡烏[16:19]>>21
たとえ数学科の人でも分野が違えばすぐには分からないと思う。☆
23
(・_・)しらちゃ[16:20]>>22
そうなんですよねー．数学科の間でも，多分絶対通じるのは集合論とか論理学くらい．．．☆
24
+3		(・_・)しらちゃ[16:23]>>22
結局，こういうのって丁寧に説明する以外の手は無い．☆
25
+2		(・_・)濡烏[16:26]>>24
丁寧な説明をすることは自分の理解が正しいかの確認になるけど、さすがに省略したいこととかが出てきてちゃんと説明しようと思ったら結構忍耐力がいる気がする。☆
26
(・_・)しらちゃ[16:35]>>25
ゼミの輪読なんかはそういうの省略一切なしでやる訓練をしたりします．というのもまさにその話しの通りで，本の途中で省かれてる部分を全て埋めることで理解が確かになるので．☆
27
(・_・)しらちゃ[16:35]>>25
なんでまあ，やろうとおもえば省略抜きで全部説明するというのも出来るんですが，実際そういうのって面倒なんですよねー．☆
28
+2		(・_・)いんこぐ[18:08]
これ31以降も見れるように魚拓取っていい？☆
29
+1		(^-^)しらちゃ[18:10]>>28
どうぞー．間違えてたら，すいませんー．あとついでに，この証明は， http://www.amazon.co.jp/dp/1846286913 この本のDenotational Semanticsの章の，途中を埋めた物ですので，本格的に読もうと想えば，この本が必要デス．☆
30
(T-T)いんこぐ[18:11]>>29
まだ本気で読むレベルには達してないな、こんなものもあるのかと参考程度に読むよ☆