2013-04-12

類

定義圏論

ラッセルのパラドックス

$\{ X | \textrm{$X$ is a set} \}$

この集合は自分自身を元として含んでしまい、元にアクセスしようとするとスタックがとぶに違いないので何とかしたい。

類, Class

上の集合は不正なものにして、新たに集合と同様の機能(関係や関数など)をもった類というのを設ける。オブジェクト指向的には、集合が類を継承している。類を構築する新しい記号を例えば $\{ ... \}_{\text{class}}$ として

$\{ X | \textrm{$X$ is a set} \}_{\text{class}$

これは類であり、集合ではないので問題がなくなる。これが一般の集合族のcodomainになる。

Conglomerate

同様に、

$\{ X | \textrm{$X$ is a class} \}_{\text{class}}$

もまずいので、やはり同様にして、類と同様の機能を持ったConglomerateを設ける。

$\{ X | \textrm{$X$ is a class} \}_{\text{conglomerate}}$

型, Type

型とは、構築の方法に制限のある集合である、とでも考える。

参考文献

2013-04-08

無名関数

定義圏論

無名関数, anonymous function

縦線つき矢印で対応を書く。

Placeholder syntax

簡単な関数の場合、placeholder syntaxが便利だ(この用語はScalaのもの)。 placeholderの記号はいろいろあって

$(- + 1)^2$
$(x + 1)^2$
$(X + 1)^2$

これらは全て、の意味である。一番上が広く使われているようだが、たぶんマイナス記号ではない。圏論では必須になっている。

2013-04-07

関数の性質

記号論理関数圏論

任意の

$f: X \rightarrow Y$

について

単射, injective

$\forall a \in X, \forall b \in X, (f(a) = f(b) \Rightarrow a = b)$

のとき、fは単射である、という。このとき、圏論では、

と書くようだ。

全射, surjective

$\forall y \in Y, \exists x \in X, f(x) = y$

のとき、fは全射である、という。このときの記号も欲しいが知らない。

全単射, bijective

fが単射かつ全射であるとき、fは全単射である、という。このとき、

$f: X \simeq Y$

と書いてはどうだろう。矢印もつけたいがそういう記号はないらしい。

2の補数, Two's complement

を以下のように定義すると

tは全単射になる。

命題

$(f: \textrm{bijective}) \Leftrightarrow (f^{-1}: Y \rightarrow X)$
$(\exists g: A \rightarrow B, g: \textrm{injective}) \Leftrightarrow (\exists h: B \rightarrow A, h: \textrm{surjective})$

参考文献

isbn:4000054244

2013-04-03

ただ一つの存在

記号論理圏論

ただ一つの存在, unique

「Fを満たすxがただ一つ存在する」という命題を、

$\exists !x F(x)$

と書き、

$\exists x(F(x) \wedge \forall y(F(y) \Rightarrow (x = y)))$

と定義する。

たいていこの定義をそのまま使って証明する。 (このブログの目標である)圏論は、こういう命題だらけである。

$\exists !$ は非常に便利な記号だと思うが、教科書ではあまり見ない気がする。

unique up to G

上を一般化したものが圏論に出てくるので先に定義する。

「Fを満たすxがunique up to G」という命題を、

$\exists x(F(x) \wedge \forall y(F(y) \Rightarrow G(x, y)))$

と定義する。日本語では「Gを除いて一意に定まる」という。

「up to G」の部分はよく省略される。