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