PS

Cartesian product

Cartesian product, 直積

集合族  (A _ i) _ {i \in I} について、 \bigcup\nolimits _ {i \in I} A _ iの元の族:

  •  (x _ i) _ {i \in I}

  •  {} ^ \forall i \in I, x _ i \in A _ i

を満たすとき

  •  (x _ i \in A _ i) _ {i \in I}

と(個人的に)書く。このような族の集合を、

  •  \prod\limits _ {i \in I} A _ i

と書き、集合族  (A _ i) _ icartesian productと呼ぶ。つまり、

  •  (x _ i \in A _ i) _ {i \in I} \Leftrightarrow ({} ^ \forall i \in I, x _ i \in A _ i) \Leftrightarrow x \in \prod\limits _ {i \in I} A _ i

Dependent product

型理論においては、 \prod の代わりに  \Pi \forall が使われる。 特に、型を添字集合とする型族の直積をdependent productと呼ぶ。

id関数の型

Haskellid関数の型の意味について、 \mathbb{\ast} を型の集合とすると、

  •  \text{id :: }a \rightarrow a
    •  \sim (\text{id} _ a \in a \rightarrow a) _ {a \in \mathbb{\ast}}
    •  \Leftrightarrow \text{id} \in \forall _ {a \in \mathbb{\ast}}a \rightarrow a
    •  \sim \text{id :: forall } a. a \rightarrow a

選択公理

  •  ({} ^ \forall i \in I, A _ i \neq \emptyset) \Rightarrow \prod\limits _ {i \in I}A _ i \neq \emptyset

記法

  •  \prod A \equiv \prod \lbrace A _ i \mid i \in I \rbrace \equiv \prod\limits _ {i \in I}A _ i
  •  (x _ i : F(i, x _ i) ) _ {i \in I} \equiv (x _ i \in \lbrace y \mid F(i, y) \rbrace  ) _ {i \in I}

参考文献