2014/02/07 (Fri)
    [Today's goal]
    mmap を Task から 関数に変更
    微調整
    様々な測定

    [memo]

    ファーストオーダーロジック

    ゲーテル
    不完全性定理 vlid 
    完全性定理 valid であればその論理の証明が存在する

    強制法
    ↓
    選択公理

    構成可能な集合（空集合を要素にもつ集合）
    構成可能な集合以外を含む集合も証明可能 
    -> 強制法 forcing

    カテゴリ
    A->B ->C

    A->C 

    ハイオーダーロジックは数式とか記号とかでの証明
    カテゴリをコンピュータサイエンスに応用できないか？
    「category theory for computing science」

    唯一まともなのは茂木健一郎「モナド」
    モナドはリフレクションだけが会ってレイフィケーションはない

    リフレクションはオブジェクトをメタオブイェクトに
    ex:ユーザランドからカーネルに設定 limt とかなにか
    レイフィケーションがメタオブジェクトからオブイェクトにする
    ex:pidをとってくるとか

    OS: カーネルランドがメタオブイェクト、ユーザランドがオブジェクト

    ヨコテさんが作ったのがアイボとかに使われている OS

    証明可能の後ろに「否定」をつけると矛盾が生じる

    DSはリフレクションとレイフィケーション両方あるようにつくる