texインストールメモ

以下の記事を参考にさせていただきました。ありがとうございます。

texliveをインストールしました。 圏論の可換図式を書くためのライブラリxy-picは、texliveに含まれているため、すぐ使えました。

$ lsb_release -d
Description:    Ubuntu 18.04.1 LTS
$ sudo apt install texlive-lang-japanese
$ sudo apt install texlive-fonts-recommended
$ sudo apt install texlive-fonts-extra
$ sudo apt install xdvik-ja
$ sudo apt install gv
$ cat test.tex
\documentclass[12pt]{ujarticle}
\usepackage{amsmath,amsfonts,amsthm,amssymb,amscd}
\usepackage[all]{xy}
\def\objectstyle{\displaystyle}
\begin{document}
\[
\xymatrix{
  A \ar[r] \ar[rrd] & B & \ar[d] \\
  C \ar[u] & A \ar[l] \ar[lu] & D
}
\]
\end{document}
$ dvipdfmx test.dvi
$ firefox test.pdf

f:id:yabaniyatun:20190115230900p:plain

Conceptual Mathematics, Session29, Exercise1

対角線定理(Diagonal Theorem)

積を持つ圏で考える。

対象 Yが以下の命題1を満たすならば、任意のendomap  \alpha: Y \to Yは少なくとも1つの不動点を持つ。 すなわち、 \alpha \circ y0 = y0を満たす点 y0: 1 \to Yが存在する。

命題1

 f: T \times T \to Yが任意の射 g: T \to Yをパラメタライズできるような対象 Tを持つ。 すなわち、 g(t) = f(t, t0)と表せるような点 t0: 1 \to Tが存在する。

対角線定理の証明

 Y, T, f, \alphaが与えられており、以下の図式が可換であると仮定する。 このとき、 \alpha: Y \to Y不動点を持つことを示す。


\require{AMScd}
\begin{CD}
T \times T @>{f}>> Y\\
@A{\delta}AA @VV{\alpha}V\\
T @>>{g}> Y
\end{CD}

ここで \deltaは対角写像 \delta: t \mapsto (t, t)である。

図式が可換であることから、任意の点 t: 1 \to Tに対して


g(t) =\alpha(f(t, t))

が成り立つ。

また、 f gをパラメタライズできるので、


g(t) = f(t, t0)

を満たす点 t0: 1 \to Tが存在する。

 t t0を代入すると


g(t0) = f(t0, t0) = \alpha(f(t0, t0))

となり、 \alpha: Y \to Y不動点 f(t0, t0)を持つことが示せた。

対角線定理拡張版

Session29, Exercise1 (p.306)は、対角線定理を少し拡張した以下の定理を示すという問題である。

 f: T \times T \to Yが任意の射 T \to Yを"弱く"パラメタライズできる(weakly parameterize)ならば、 任意のendomap  \alpha: Y \to Y不動点を持つ。

"弱くパラメタライズする"の意味

 f: T \times T \to Yが任意の射 g: T \to Yを弱くパラメタライズするとは、任意の射 gに対して 点 t0: 1 \to Tが存在し、可換図式1の \xiが可換図式2を満たすことである。

可換図式1


\require{AMScd}
\begin{CD}
T @= T\\
@V{\xi}VV @VV{1_T}V\\
T \times T @>{p_1}>> T
\end{CD}


\require{AMScd}
\begin{CD}
T @= T\\
@V{\xi}VV @VV{c}V\\
T \times T @>{p_2}>> T
\end{CD}

 cは定値写像であり、任意の tに対して c(t) = t0

可換図式2


\require{AMScd}
\begin{CD}
1 @>{t}>> T @>{f \circ \xi}>> Y\\
@| @| @|\\
1 @>{t}>> T @>{g}>> Y
\end{CD}

 tは任意の点。

対角線定理拡張版の証明

可換図式2の gとして対角写像 \delta fとendomap  \alphaの合成 \alpha  \circ f \circ \deltaを選ぶ。 以下の図式において、 \alpha \circ f \circ \delta \circ t = f \circ \xi \circ tが成り立つ。


\require{AMScd}
\begin{CD}
1 @>{t}>> T @>{\delta}>> T \times T @>{f}>> Y @>{\alpha}>> Y
\end{CD}

 tは任意の点。

 f \circ \xi \circ t f(t, t\xi)と書くと、


\alpha(f(t, t)) = f(t, t\xi)

が成り立ち、 t t\xiを代入すると


\alpha(f(t\xi, t\xi)) = f(t\xi, t\xi)

となるので、 f(t\xi, t\xi) \alpha: Y \to Y不動点となることが示せた。

メモ

  • amscdだと、斜めの矢印、左矢印、破線矢印が書けなかった
  • XyJax を使おうとしたけど、はてなブログでの使い方がわからなかった https://github.com/sonoisa/XyJax
  • [tex: f(t_{\xi}, t_{\xi})]が表示されなくて困った。t\xit_{\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

rustメモ

rustupを用いたrustコンパイラツールのインストール

以下のURLからインストーラをダウンロードする。

https://rustup.rs/

以下のように、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
    }
}