Conceptual Mathematics, Session29, Exercise1
対角線定理(Diagonal Theorem)
積を持つ圏で考える。
対象が以下の命題1を満たすならば、任意のendomap
は少なくとも１つの不動点を持つ。
すなわち、
を満たす点
が存在する。
命題1
射が任意の射
をパラメタライズできるような対象
を持つ。
すなわち、
と表せるような点
が存在する。
対角線定理の証明
が与えられており、以下の図式が可換であると仮定する。
このとき、
が不動点を持つことを示す。
ここでは対角写像
である。
図式が可換であることから、任意の点に対して
が成り立つ。
また、は
をパラメタライズできるので、
を満たす点が存在する。
に
を代入すると
となり、が不動点
を持つことが示せた。
対角線定理拡張版
Session29, Exercise1 (p.306)は、対角線定理を少し拡張した以下の定理を示すという問題である。
射が任意の射
を"弱く"パラメタライズできる(weakly parameterize)ならば、
任意のendomap
は不動点を持つ。
"弱くパラメタライズする"の意味
射が任意の射
を弱くパラメタライズするとは、任意の射
に対して
点
が存在し、可換図式1の
が可換図式2を満たすことである。
可換図式1
は定値写像であり、任意の
に対して
。
可換図式2
は任意の点。
対角線定理拡張版の証明
可換図式2のとして対角写像
と
とendomap
の合成
を選ぶ。
以下の図式において、
が成り立つ。
は任意の点。
を
と書くと、
が成り立ち、に
を代入すると
となるので、が
の不動点となることが示せた。
メモ
- amscdだと、斜めの矢印、左矢印、破線矢印が書けなかった
- XyJax を使おうとしたけど、はてなブログでの使い方がわからなかった https://github.com/sonoisa/XyJax
[tex: f(t_{\xi}, t_{\xi})]が表示されなくて困った。t\xiをt_{\xi}の代わりに使った。tex苦手なので間違っているかも。
AArch64をターゲットとしたgcc4.9.2ビルド
configureの階層にbuildディレクトリを作らないとエラーになった。
$ mkdir build $ cd build $ ../configure --target=aarch64-linux-gnu --disable-nls --disable-shared --disable-multilib --disable-libgomp --disable-threads --enable-languages=c,c++ --disable-libstdcxx-pch --disable-bootstrap
makeを実行するとエラーになるのでソースを修正する。
contrib/texi2pod.pl L.319 のbrace"{", "}"をエスケープする。
315 /^\@item\s+(.*\S)\s*$/ and $endw eq "multitable" and do {
316 @columns = ();
317 for $column (split (/\s*\@tab\s*/, $1)) {
318 # @strong{...} is used a @headitem work-alike
319 $column =~ s/^\@strong\{(.*)\}$/$1/;
320 push @columns, $column;
321 }
322 $_ = "\n=item ".join (" : ", @columns)."\n";
323 };
gcc/cp/cfns.gperf L.25〜27を追加
23 #ifdef __GNUC__ 24 __inline 25 #ifdef __GNUC_STDC_INLINE__ 26 __attribute__ ((__gnu_inline__)) 27 #endif 28 #endif 29 const char * libc_name_p (const char *, unsigned int);
gcc/cp/cfns.h L.56〜58を追加
54 #ifdef __GNUC__ 55 __inline 56 #ifdef __GNUC_STDC_INLINE__ 57 __attribute__ ((__gnu_inline__)) 58 #endif 59 #endif 60 const char * libc_name_p (const char *, unsigned int);
ビルド、インストールする
$ make $ sudo make install
tmuxメモ1
起動
tmux
window分割(1つのwindow->複数のpane)
水平分割
c-b "
垂直分割
c-b %
pane移動
# 巡回 c-b o # 往復 c-b ;
スクロール
c-b [ # ↑↓でスクロールできる # g <行番号>でも移動できる
rustメモ
rustupを用いたrustコンパイラツールのインストール
以下のURLからインストーラをダウンロードする。
以下のように、binをPATHに追加する。
source $HOME/.cargo/env
- インストールされるツール
- cargo
- rustc
- rustdoc
新規プロジェクトの作成
以下のようにプロジェクト(e.g. hello)を作成する。
$ cargo new --bin hello
ビルドする。
$ cargo run
標準ライブラリのドキュメントを見る
$ rustup doc --std
crate(依存ライブラリ)のドキュメントを見る
以下のコマンドを実行すると、ドキュメントがプロジェクトのtarget配下にダウンロードされ、ブラウザで開かれる。
crateの例: iron
$ cargo doc -p iron --open
rust言語についてのメモ
- 関数 fn get_form(_request: &mut Request) -> IronResult
{ ... } // 仮引数: 型、&は参照?、->の後ろは戻り値の型 - 変数名を_で始めることでこの変数を使わないことをコンパイラに教える
- ローカル変数 let mut var = xxx; // mutはmutableのこと?
- raw string構文 r#\"...\"# ダブルクォートをエスケープなしで使える
- 関数bodyの最後の式が暗黙に関数の戻り値になる。(注意: セミコロンをつけてはならない)
おまけ ASTダンプ
ASTダンプは、nightly rustでないとできないので、以下のように--channel=nightlyを指定してインストール
$ sh rustup.sh --prefix=/home/xxx/rust_nightly --channel=nightly
ASTダンプコマンド
$ rustc -Z ast-json main.rs
入力ファイル
fn main() {
println!("Hello, world!");
}
以下のASTが出力されたが、よくわからない。
{
"module": {
"inner": {
"lo": 0,
"hi": 44
},
"items": [
{
"ident": "",
"attrs": [
{
"id": {
"_field0": 1
},
"style": "Outer",
"path": {
"span": {
"lo": 0,
"hi": 0
},
"segments": [
{
"ident": "prelude_import",
"args": null
}
]
},
"tokens": [],
"is_sugared_doc": false,
"span": {
"lo": 0,
"hi": 0
}
}
],
"id": 2,
"node": {
"variant": "Use",
"fields": [
{
"prefix": {
"span": {
"lo": 0,
"hi": 0
},
"segments": [
{
"ident": "{{root}}",
"args": null
},
{
"ident": "std",
"args": null
},
{
"ident": "prelude",
"args": null
},
{
"ident": "v1",
"args": null
}
]
},
"kind": "Glob",
"span": {
"lo": 0,
"hi": 0
}
}
]
},
"vis": {
"node": "Inherited",
"span": {
"lo": 0,
"hi": 0
}
},
"span": {
"lo": 0,
"hi": 0
},
"tokens": null
},
{
"ident": "std",
"attrs": [
{
"id": {
"_field0": 0
},
"style": "Outer",
"path": {
"span": {
"lo": 0,
"hi": 0
},
"segments": [
{
"ident": "macro_use",
"args": null
}
]
},
"tokens": [],
"is_sugared_doc": false,
"span": {
"lo": 0,
"hi": 0
}
}
],
"id": 3,
"node": {
"variant": "ExternCrate",
"fields": [
null
]
},
"vis": {
"node": "Inherited",
"span": {
"lo": 0,
"hi": 0
}
},
"span": {
"lo": 0,
"hi": 0
},
"tokens": null
},
{
"ident": "main",
"attrs": [],
"id": 4,
"node": {
"variant": "Fn",
"fields": [
{
"inputs": [],
"output": {
"variant": "Default",
"fields": [
{
"lo": 10,
"hi": 10
}
]
},
"variadic": false
},
{
"unsafety": "Normal",
"asyncness": "NotAsync",
"constness": {
"node": "NotConst",
"span": {
"lo": 0,
"hi": 2
}
},
"abi": "Rust"
},
{
"params": [],
"where_clause": {
"id": 5,
"predicates": [],
"span": {
"lo": 0,
"hi": 0
}
},
"span": {
"lo": 0,
"hi": 0
}
},
{
"stmts": [
{
"id": 22,
"node": {
"variant": "Semi",
"fields": [
{
"id": 10,
"node": {
"variant": "Block",
"fields": [
{
"stmts": [
{
"id": 21,
"node": {
"variant": "Semi",
"fields": [
{
"id": 9,
"node": {
"variant": "Call",
"fields": [
{
"id": 8,
"node": {
"variant": "Path",
"fields": [
null,
{
"span": {
"lo": 7767836,
"hi": 7767859
},
"segments": [
{
"ident": "$crate",
"args": null
},
{
"ident": "io",
"args": null
},
{
"ident": "_print",
"args": null
}
]
}
]
},
"span": {
"lo": 7767836,
"hi": 7767859
},
"attrs": {
"_field0": null
}
},
[
{
"id": 20,
"node": {
"variant": "Call",
"fields": [
{
"id": 11,
"node": {
"variant": "Path",
"fields": [
null,
{
"span": {
"lo": 7767862,
"hi": 7767896
},
"segments": [
{
"ident": "$crate",
"args": null
},
{
"ident": "fmt",
"args": null
},
{
"ident": "Arguments",
"args": null
},
{
"ident": "new_v1",
"args": null
}
]
}
]
},
"span": {
"lo": 7767862,
"hi": 7767896
},
"attrs": {
"_field0": null
}
},
[
{
"id": 14,
"node": {
"variant": "AddrOf",
"fields": [
"Immutable",
{
"id": 13,
"node": {
"variant": "Array",
"fields": [
[
{
"id": 12,
"node": {
"variant": "Lit",
"fields": [
{
"node": {
"variant": "Str",
"fields": [
"Hello, world!\n",
"Cooked"
]
},
"span": {
"lo": 25,
"hi": 40
}
}
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
}
]
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
}
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
},
{
"id": 19,
"node": {
"variant": "AddrOf",
"fields": [
"Immutable",
{
"id": 18,
"node": {
"variant": "Match",
"fields": [
{
"id": 15,
"node": {
"variant": "Tup",
"fields": [
[]
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
},
[
{
"attrs": [],
"pats": [
{
"id": 16,
"node": {
"variant": "Tuple",
"fields": [
[],
null
]
},
"span": {
"lo": 25,
"hi": 40
}
}
],
"guard": null,
"body": {
"id": 17,
"node": {
"variant": "Array",
"fields": [
[]
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
}
}
]
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
}
]
},
"span": {
"lo": 25,
"hi": 40
},
"attrs": {
"_field0": null
}
}
]
]
},
"span": {
"lo": 7767862,
"hi": 7767896
},
"attrs": {
"_field0": null
}
}
]
]
},
"span": {
"lo": 7767836,
"hi": 7767898
},
"attrs": {
"_field0": null
}
}
]
},
"span": {
"lo": 7767836,
"hi": 7767900
}
}
],
"id": 7,
"rules": "Default",
"span": {
"lo": 7767834,
"hi": 7767902
},
"recovered": false
},
null
]
},
"span": {
"lo": 7767834,
"hi": 7767902
},
"attrs": {
"_field0": null
}
}
]
},
"span": {
"lo": 7767834,
"hi": 7767902
}
}
],
"id": 6,
"rules": "Default",
"span": {
"lo": 10,
"hi": 44
},
"recovered": false
}
]
},
"vis": {
"node": "Inherited",
"span": {
"lo": 0,
"hi": 0
}
},
"span": {
"lo": 0,
"hi": 44
},
"tokens": [
{
"variant": "Token",
"fields": [
{
"lo": 0,
"hi": 2
},
{
"variant": "Ident",
"fields": [
"fn",
false
]
}
]
},
{
"variant": "Token",
"fields": [
{
"lo": 3,
"hi": 7
},
{
"variant": "Ident",
"fields": [
"main",
false
]
}
]
},
{
"variant": "Delimited",
"fields": [
{
"lo": 7,
"hi": 9
},
{
"delim": "Paren",
"tts": []
}
]
},
{
"variant": "Delimited",
"fields": [
{
"lo": 10,
"hi": 44
},
{
"delim": "Brace",
"tts": [
{
"variant": "Token",
"fields": [
{
"lo": 16,
"hi": 23
},
{
"variant": "Ident",
"fields": [
"println",
false
]
}
]
},
{
"variant": "Token",
"fields": [
{
"lo": 23,
"hi": 24
},
"Not"
]
},
{
"variant": "Delimited",
"fields": [
{
"lo": 24,
"hi": 41
},
{
"delim": "Paren",
"tts": [
{
"variant": "Token",
"fields": [
{
"lo": 25,
"hi": 40
},
{
"variant": "Literal",
"fields": [
{
"variant": "Str_",
"fields": [
"Hello, world!"
]
},
null
]
}
]
}
]
}
]
},
{
"variant": "Token",
"fields": [
{
"lo": 41,
"hi": 42
},
"Semi"
]
}
]
}
]
}
]
}
]
},
"attrs": [],
"span": {
"lo": 0,
"hi": 44
}
}
TensorFlowをインストールしてみた
今さらですが、TensorFlowをインストールしてみました。
pipのインストール
$ sudo pacman -S pip
TensorFlow 1.5のインストール
1.9だとillegal instruction (core dumped)になってしまったので1.5を指定しました。
$ pip install tensorflow=1.5 --user
ちなみに--userはローカルインストールするためのオプションです。
次のようにして、インストールパスが確認できます。
$ pip show [パッケージ名]
動作確認
$ python
Python 3.6.4 (default, Jan 5 2018, 02:35:40)
[GCC 7.2.1 20171224] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import tensorflow as tf
>>> hello = tf.constant('Hello, TensorFlow!')
>>> sess = tf.Session()
2018-04-19 21:12:12.121902: I tensorflow/core/platform/cpu_feature_guard.cc:137] Your CPU supports instructions that this TensorFlow binary was not compiled to use: SSE4.1 SSE4.2
>>> print(sess.run(hello))
b'Hello, TensorFlow!'
