annotate 14/February/memo/07th.txt @ 117:2fa31c1124a3 default tip

fix
author Masataka Kohagura <kohagura@cr.ie.u-ryukyu.ac.jp>
date Mon, 29 Jun 2015 15:32:25 +0900
parents d8f499590d82
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
39
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 2014/02/07 (Fri)
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 [Today's goal]
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 mmap を Task から 関数に変更
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 微調整
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 様々な測定
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 [memo]
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 ファーストオーダーロジック
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 ゲーテル
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 不完全性定理 vlid 
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 完全性定理 valid であればその論理の証明が存在する
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 強制法
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 選択公理
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 構成可能な集合(空集合を要素にもつ集合)
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 構成可能な集合以外を含む集合も証明可能 
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 -> 強制法 forcing
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 カテゴリ
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 A->B ->C
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 A->C 
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ハイオーダーロジックは数式とか記号とかでの証明
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 カテゴリをコンピュータサイエンスに応用できないか?
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 「category theory for computing science」
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 唯一まともなのは茂木健一郎「モナド」
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 モナドはリフレクションだけが会ってレイフィケーションはない
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 リフレクションはオブジェクトをメタオブイェクトに
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ex:ユーザランドからカーネルに設定 limt とかなにか
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 レイフィケーションがメタオブジェクトからオブイェクトにする
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ex:pidをとってくるとか
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 OS: カーネルランドがメタオブイェクト、ユーザランドがオブジェクト
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ヨコテさんが作ったのがアイボとかに使われている OS
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 証明可能の後ろに「否定」をつけると矛盾が生じる
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
4a4d6e475571 add 07th.txt
Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 DSはリフレクションとレイフィケーション両方あるようにつくる