view 14/February/memo/07th.txt @ 51:d8f499590d82

rename 201* to 1*
author Masataka Kohagura <e085726@ie.u-ryukyu.ac.jp>
date Sun, 16 Mar 2014 13:36:04 +0900
parents 2014/February/memo/07th.txt@4a4d6e475571
children
line wrap: on
line source

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はリフレクションとレイフィケーション両方あるようにつくる