プログラミング言語Idris自体についての詳しい話はここではしない。このブログの昔の記事で軽く紹介したかもしれないが他人の参考になるかは分からない。
この記事を読むにあたっては、
- ペアノ算術
は知ってないと厳しいと思われる。あとHaskell風の言語にも慣れていた方がいいか。
この記事で使うIdrisのバージョンは0.9.16である（執筆時点の最新版）。これと異なるバージョンだとコードの修正が必要かもしれない。
Idrisの有界な自然数で遊んでみる(0)
1件のフィードバック
投稿者「mod_poppo」のアーカイブ
Union Typesは直和型ではない
【2017年12月18日 追記】この記事は古いTypeScript (2.0以前) を念頭に置いている。もちろん、現在のTypeScriptにも当てはまる記事はあるだろうし、TypeScript以外の言語における合併型 (union types) についてもある程度読み替えられるかもしれない。ただしElmとは “Union Types” の用法が完全に相入れないのでElmユーザーの方はお帰りください。
TypeScript 1.4について、 TypeScript 1.4.1 変更点 – Qiita という記事が目に留まった。で、その中の
直和型(Union Types)
という項目に引っかかりを感じた。:
なぜ引っかかりを感じたかというと、TypeScriptに今回導入されたUnion Typesと、巷に言う直和型というのは、異なる概念であるからだ。
注意：以下の話は型理論の専門家でもないフツーの学生が適当に書いた程度の信憑性しかありません。
TypeScript 1.4がいい感じ
TypeScript 1.4がリリースされた。目玉機能としては Union Types とか ECMAScript 6 出力モードの搭載とかになるのだろうが、他にもいろいろ地味だが嬉しい機能追加などがあるようだった。
前にTypeScriptで組み込みオブジェクトを拡張できないというようなことを書いたが、そのとき感じた問題点が直っている。具体的には以下。
- 各種組み込みオブジェクトのコンストラクタの型が
interface ほにゃららConstructorというものに変更されている。よって、各種組み込みオブジェクトのコンストラクタに勝手なプロパティーを追加できる。 - ECMAScript 6 で追加される関数の型定義が追加されている。つまり、自前で組み込みオブジェクトの型定義をいじらなくていい。（ECMAScript 6 出力モードで使えるようになるようだ）
あと地味に便利だと思ったのはコンパイラ tsc に追加された --noEmitOnError というオプションである。今まではソースコードが解釈さえできれば型チェックが通らなくても ECMAScript の出力が生成（！）されていて、Makefile で TypeScript のコードをコンパイルする時に不便だった。だが、このオプションがあれば型チェックが通ったコードしか出力されないので、Makefile との相性が上がる。
Rustから直接C++を叩いてみる
TeX処理系の気に食わない点(0) — エラー時の挙動
明治維新で新政府がTeXを旧来の陋習として弾圧したとき、TeX使いたちはわざとTeXの使い勝手を悪くすることで難を逃れたと伝えられています。 — TeXしぐさ
↑「適当にでっち上げた嘘です」と注記しようと思ったが元ネタも適当にでっち上げた嘘だった
TeXの気に食わない点…はきっと皆さんいろいろあると思うが、ここではTeX処理系の挙動に絞った話をする。ここに書いた挙動に関しては、TeXもpdfTeXもXeTeXも大差はないようである。
一次分数変換と球面の回転の話(0)
次の形をした複素関数 \(f\) を一次分数変換という:\[
f(z)=\frac{az+b}{cz+d},\quad \text{ただし \(ad-bc\ne0\).}
\]分母が0になるとき（\(z=-d/c\) のとき）は \(f(z)\) の値は複素数としては定まらない、のだが、値が複素数であることにこだわらなければここは \(\infty\) としておくのが都合がいい。逆に、\(z=\infty\) のときは、（\(z\to\infty\) の極限を考えれば分かるように）\(f(z)\) の値は \(a/c\) として定義できそうである。何がいいたいかと言うと、一次分数変換は、複素平面の関数というよりは、複素平面に「無限遠点」を加えたもの \(\Complex\cup\{\infty\}\) の関数をみるのが自然である。
複素平面に無限遠点を加えたもの \(\Complex\cup\{\infty\}\) は、球面と同一視できる（こうやって同一視したものをリーマン球面という）。球面上の点 \(P\) に複素平面の点 \(z\) をどう対応させるかというと、球の北極 \((0,0,1)\) から \(P\) に直線を引いて、その直線が複素平面と交わる点 \(z\) を対応させる。逆に、複素平面の点 \(z\) に対しては、\(z\) と北極 \((0,0,1)\) を結ぶ直線を引いて、それが球面と交わる（北極じゃない方の）点 \(P\) を対応させる。北極に対応する点は複素平面上にはないので、北極には無限遠点 \(\infty\) を対応させる。この対応を立体射影(stereographic projection)という。
続きを読む
SO(2) と SO(3) が弧状連結であることの簡便な（？）証明
特殊直交群 \(SO(n)\) が（弧状）連結であることを示すのはこの記事に書いたやり方がおそらく正攻法なのだろうが、次元が低い時はもっと短い議論でできるんじゃないかなあと思った。
命題. \(SO(2)\) の元 \(A\) は次の形に書ける。\[
A=\begin{pmatrix}
\cos\theta&-\sin\theta \\
\sin\theta&\cos\theta
\end{pmatrix}
\]
A=\begin{pmatrix}
\cos\theta&-\sin\theta \\
\sin\theta&\cos\theta
\end{pmatrix}
\]
証明. \(A\) を成分表示して \(SO(2)\) の条件の式に代入してガリガリ計算すればわかる。
定理. \(SO(2)\) は弧状連結である。
証明. さっきの命題を使えば簡単。
SU(n) と SO(n) が弧状連結であることの証明
特殊ユニタリ群 \(SU(n)\) や特殊直交群 \(SO(n)\) が（弧状）連結であることは当たり前のようにバンバン使うけど自分でそらで証明できるか怪しいなあと思ったので、証明をつけてみることにした。
続きを読む
R^3のベクトル積とso(3)のメモ
今回は \(\mathbf{R}^3\) のベクトル積とか回転行列とかに関する覚え書き。割と初等的。大学2年ぐらいのレベルだろうか。オチはない。
定義とか
3次の実正方行列全体の集合を \(M(3,\mathbf{R})\) で表す。3次の特殊直交群 \(SO(3)\) を\[
SO(3)=\{A\in M(3,\mathbf{R})\mid\det A=1,~{}^tAA=I\}
\]で定める。特殊直交群の元はいわゆる回転を表す行列である。
3次の交代行列全体の集合を \(\mathfrak{so}(3)\) で表す。\(\mathfrak{so}\) は小文字のsoをフラクトゥールで書いたものである。\[
\mathfrak{so}(3)=\{X\in M(3,\mathbf{R})\mid X+{}^tX=0\}
\]\(\mathfrak{so}(3)\) は3次元の実線形空間であり、\begin{align*}
E_1&=\begin{pmatrix}0&0&0\\0&0&-1\\0&1&0\end{pmatrix},&
E_2&=\begin{pmatrix}0&0&1\\0&0&0\\-1&0&0\end{pmatrix},&
E_3&=\begin{pmatrix}0&-1&0\\1&0&0\\0&0&0\end{pmatrix}
\end{align*}は一組の基底となっている。\(\mathfrak{so}(3)\) の元 \(X\in\mathfrak{so}(3)\) は実数 \(a,b,c\in\mathbf{R}\) により\[
X=\begin{pmatrix}0&-c&b\\c&0&-a\\-b&a&0\end{pmatrix}=aE_1+bE_2+cE_3
\]と書ける。
ベクトル積
TeXを勉強したい
（LaTeXではない方の）plain TeXを勉強すべしという電波を受信したので、勉強しようと思った。
じゃあ何を読んで勉強しようかという話だが、TeX Wiki内のTeX入門/マクロの作成 – TeX Wikiというページが入門として良さそうだった。
もうちょっとまじめに勉強しようとなると、TeXの本 – TeX Wikiの下の方にある
- TeX by Topic
- 無料でPDFを入手できる。
- The TeXbook
- Knuth博士の著作。
あたりを読むと良さそう。